如何处理COQ的部门？

发布于 2025-01-25 04:34:23 字数 320 浏览 5 评论 0原文

如何在目标中处理该部门？因为我的目标显然是正确的...但是我不能使用lia，而且我认为这与该部门有关。

2 ^ k / 2 ≤ 2 ^ k

Bellow是我的COQ屏幕：

原文

How to deal with with the division in a goal?
Because I have a goal which is clearly true... However I cannot use lia and I think that this is related to the division.

2 ^ k / 2 ≤ 2 ^ k

Bellow is my COQ screen:

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

小女人ら 2025-02-01 04:34:23

自然部门没有自动化 - 它们甚至没有形成一个领域。但是，搜索不难找到相应的引理：

Require Import Lia.

Goal forall k:N, 2 ^ k / 2 <= 2 ^ k.
Proof.
  intros k.
  Search (?a/?b <= ?a/?c).
  Search (_/1).
  rewrite <- N.div_1_r.
  apply N.div_le_compat_l.
  lia.
Qed.

如果您的术语确实很复杂，则可以使用floor（a/b）用于整数a/b ，然后使用COQ Interval。嵌入易于自动化，COQ Interval对于证明真实的不平等现象非常有力，但是如果您有多个楼层，则可能会扼杀。您可以将其与Coq-Gappa结合使用，然后摆脱地板。那时它已经很参与，但仍然完全自动化。但是请注意，它可能无法证明不平等，因为它使用了真实的分析。

nia（要求导入psatz），正如ANA所建议的那样，无法解决此问题（老实说，我停止尝试）。

There is no automation for division on naturals - they don't even form a field. But the corresponding lemmas are not hard to find with Search:

Require Import Lia.

Goal forall k:N, 2 ^ k / 2 <= 2 ^ k.
Proof.
  intros k.
  Search (?a/?b <= ?a/?c).
  Search (_/1).
  rewrite <- N.div_1_r.
  apply N.div_le_compat_l.
  lia.
Qed.

If you have really complicated terms, you can embed the goal into reals using floor (a/b) for integer a/b and then use coq-interval. The embedding is easy to automate and coq-interval is quite powerful for proving real inequalities, but it might choke if you have more than a few floors. You can combine it with coq-gappa then to get rid of the floors. It gets quite involved then, but still fully automated. But be aware that it might not be able to prove very tight inequalities, since it uses real analysis.

Nia (Require Import Psatz), as suggested by Ana, can't solve this (and I honestly stopped trying it).

回复收藏 0 原文