如何在 Coq 中转换两个术语之间的关系答案

【问题标题】：How I can convert the relation between two terms in Coq如何在 Coq 中转换两个术语之间的关系
【发布时间】：2021-06-18 01:31:33
【问题描述】：

我在两个术语之间的关系小于 (S i2)

【问题讨论】：

标签： coq

【解决方案1】：

您可以Search 获取相关引理：

Require Import Arith.

Search (_ < _) (_ <= _).

如果您希望保留相同的信息，您有两种选择：

对i1做案例分析：

1.1。如果是0，那么你有一个不可能的陈述，因为没有小于零的自然数。为了寻找这个事实，Search (_ < 0) 提供了Nat.nlt_0_r。

1.2。如果它是继任者，比如S i1'，那么你的声明就变成了S i2 < S i1'。从我们上面的Search，我们找到了Nat.lt_succ_r，所以我们可以将我们的S i2 < S i1'重写为S i2 <= i1'。
直接使用Nat.lt_le_pred，但这会导致S i2 <= Nat.pred i1，而i1的前身可能对你有用也可能没用。

或者，如果你知道S i2 < i1，但你只关心S i2 <= i2，即你想弱化你的假设，你可以使用Nat.lt_le_incl。

【讨论】：

【解决方案2】：

这些术语并不完全等价，但第一个比第二个强，使用传递性和弱化 i2 <= S (S i2) 就足够了：

Require Import PArith PeanoNat.

Lemma example a b : S a < b -> a <= b.
Proof.
assert (a <= S (S a)).
  now apply Le.le_Sn_le, Le.le_Sn_le.
exact (Nat.le_trans _ _ _ H).
Qed.

回想一下a < b 是S a <= b 的符号。您也可以直接以反向链接方式削弱。

Lemma example2 a b : S a < b -> a <= b.
Proof. now intros hlt; apply Nat.lt_le_incl, Nat.lt_le_incl. Qed.

【讨论】：

【解决方案3】：

除了学习 Coq 的早期阶段，我会推荐 lia 策略：

Require Import PArith PeanoNat.
Require Import Lia.

Lemma example a b : S a < b -> a <= b.
Proof.
  intros H.
  lia.
Qed.

【讨论】：

谢谢。通过使用哪个命令，我可以将 S a
您的问题需要更加精确。我不知道一个名为count 的函数，所以你必须定义它。另一个问题有一个错字（a <= S (S a) 中有两个a），你到底想要什么并不明显。我一般相信lia - 如果它不能证明关于线性整数算术的某些事情，那很可能是错误的。