0

我有一个已经被证明的证明。

Lemma Equal_Trans : forall T : Type, forall y x z: T, 
      Equal x y -> Equal y z -> Equal x z.

其次，我有加法交换性证明的修正。

Lemma Add_com : forall x x': Nat, Equal (Add x x') (Add x' x).
Proof.
intros.
induction x.
simpl.
apply Add_zero.
simpl.
apply (Equal_Trans Nat (S (Add x' x)) ). (* var y *)
apply Equal_Morph.
assumption.
apply Add_S.
Qed.

但是，我不明白 Equal_trans （第 8 行）的用法。如果我理解， Equal_Trans 需要 3 个参数： yxz ？但是为什么在 Add_com lemma 中只有 1 个参数使用 Equal_Trans 呢？

预先感谢您的帮助。

4

2 回答 2

1

该策略apply尝试填补空白以将所提供术语的类型与目标相匹配。在这种情况下，目标（使用策略时）可能类似于a = b（根据您的跟进，实际上是Equal a b）。Equal_Trans（当使用所有参数时）的类型是x = z( Equal x z)，所以为了统一这两种类型，我们应该有x := aand z := b。这只留下y模棱两可，所以我们必须提供它。

为了解决您的后续问题，不，Equal_Trans不只是一个论点。它需要一个类型（Nat在您的情况下）该类型的三个元素（y和x）z和两个相等证明。但是，请记住 Coq 中的函数是柯里化的，这意味着您可以使用更少的参数调用它们，但结果将是剩余参数的函数。

所以实际上，当我们说 时apply (Equal_Trans Nat (S (Add x' x)).，我们是在说“拿这个有类型的东西，forall (x z: Nat), Equal x (S (Add x' x)) -> Equal (S (Add x' x)) z -> Equal x z并尝试填写一些参数以使其与我的目标相匹配”。

Coq 查看该类型并意识到目标已经看起来像Equal x z，因此它能够推断出什么x和z必须是什么。Equal_Trans仍然需要 Coq 自己无法解决的另外两个参数（ 和 的证明Equal x y）Equal y z，所以这就是其余证明正在做的事情。

我们使用传递性是因为我们可以使用归纳假设 ( )y := S (Add x' x)来证明。我们也可以用 的定义来证明。因此，通过 . 路由相等性证明是很自然的。Equal (S (Add x x')) (S (Add x' x))IHxEqual (S (Add x' x)) (Add x' (S x))AddS (Add x' x)

现在，我们不必使用传递性与y := S (Add x' x). 我们可以证明(S (Add x x'))和(Add x' (S x))都等于 的其他元素Nat。但最简单、最直接的途径是通过S (Add x' x)。

于 2019-02-17T08:30:22.560 回答
0

非常感谢您的帮助。

如果我理解， Equal_trans 只接受 1 个参数，即 y 参数？

但是，在发出命令之前apply (Equal_Trans Nat (S (Add x' x)) )，CoqIDE 告诉我：

1 subgoal
x, x' : Nat
IHx : Equal (Add x x') (Add x' x)
______________________________________(1/1)
Equal (S (Add x x')) (Add x' (S x))

我不明白为什么，在这里，我必须采取 y := S (Add x' x) 来申请 Equal_trans ？

于 2019-02-17T10:16:06.963 回答