如何在Coq中证明这个简单的方程

Question

我想在Coq中证明:

convert l' + 1 + (convert l' + 1) = convert l' + convert l' + 1 + 1

只有一些括号是多余的,不要让我使用reflexivity命令; 所以我该怎么做？

所有元素都是nat(自然)类型,因为这convert l'是一个返回nat数的函数,我不想使用像Omega这样的强大策略等等.

Answer 1

Omega 是非常有用的,因为它可以让你继续使用更有趣的证据部分,但是当一个人学习时,我个人觉得看到一个"更简单"的证明是有帮助的(欧米茄生成的证明术语往往很长且不可读) ).

首先请注意,您需要使用关联性和交换性plus.使用Coq的搜索工具来查找有用的引理.使用_作为通配符.您可以找到包含看起来像关联性的结构的lemmas,如下所示:

SearchAbout (_ + (_ + _)= (_ + _) + _).

找到五个包含以下内容的引理:

plus_assoc: forall n m p : nat, n + (m + p) = n + m + p

以同样的方式你可以找到交换性引理

SearchAbout (_ + _ = _ + _).

这是:

plus_comm: forall n m : nat, n + m = m + n

您不能直接应用它们,而是可以使用rewrite允许您处理术语子部分的策略.我建议你玩它来了解它是如何工作的.

这是所需引理的证明.

Require Import Arith.

Lemma nat_lemma: forall n, n + 1 + (n + 1) = n + n + 1 + 1.
  intro n.
  repeat rewrite <- plus_assoc.    (* n + (1 + (n + 1)) = n + (n + (1 + 1)) *)
  rewrite (plus_comm 1 (n+1)).     (* uses (1 + (n + 1) = (n + 1) + 1 *)
  repeat rewrite plus_assoc.
  reflexivity.
Qed.

现在用这个引理来证明你的定理.