一种方法如何证明关于 coq 中非原始递归函数的事实？答案

【问题标题】：How does one approach proving facts about non-primitive recursive functions in coq?一种方法如何证明关于 coq 中非原始递归函数的事实？
【发布时间】：2019-12-10 12:29:41
【问题描述】：

我试图证明这两个加法函数在扩展上是相同的，但是我什至无法证明第二个的最简单引理。如何证明非原始递归加法函数？

Fixpoint myadd1 (m n : nat) : nat :=
  match m, n with
    | 0, n => n
    | (S m), n => S (myadd1 m n)
                    end.

Fixpoint myadd2 (m n : nat) : nat :=
  match m, n with
    | 0, n => n
    | (S m), n => myadd2 m (S n)
                    end.

Lemma succlem1 : forall (m n : nat),
  (myadd1 m 0) = m.
Proof.
  intros. induction m.
  - simpl. reflexivity.
  - simpl. rewrite IHm.
    reflexivity.
Qed.

Lemma succlem12 : forall (m n : nat),
  (myadd2 m 0) = m.
Proof.
  intros. induction m.
  - reflexivity.
  - simpl.
Abort.

编辑：

这就是我想要证明的，也是我被引到这个引理的原因。

Lemma succlem : forall (m n : nat),
  S (myadd2 m 0) = myadd2 m 1.
Proof.
  intros. induction m.
  - simpl. reflexivity.
  - simpl. rewrite <- IHm.
    simpl.


Theorem succHomo : forall (m n : nat),
  S (myadd2 m n) = myadd2 m (S n).
Proof.
  intros.
  induction n.
  - simpl. reflexivity.
  - simpl.
    inversion IHm.

Theorem equivadds : forall (m n : nat),
    myadd1 m n = myadd2 m n.
Proof.
  intros.
  induction m.
  - simpl. reflexivity.
  - intros.
    simpl.
    rewrite IHm.
    symmetry.

【问题讨论】：

标签： recursion coq

【解决方案1】：

当你有一个累加器时，你最想概括你的归纳假设。所以，在这种情况下，你可以先证明myadd2 等价于myadd1：

Lemma myadd1Sr m n :
  myadd1 m (S n) = S (myadd1 m n).
Proof.
now induction m as [|m IHm]; trivial; simpl; rewrite IHm.
Qed.

Lemma myadd2_equiv_myadd1 : forall m n : nat,
  myadd2 m n = myadd1 m n.
Proof.
intros m.  (* important: don't introduce `n` yet -- this will make your IH less general than needed *)
induction m as [| m IHm]; trivial; intros n; simpl.
now rewrite IHm, myadd1Sr.
Qed.

那么剩下的可以通过简单的重写来完成：

Lemma succlem12 : forall m : nat,
  myadd2 m 0 = m.
Proof.
now intros m; rewrite myadd2_equiv_myadd1, succlem1.
Qed.

【讨论】：

我原本打算在上述等式的证明中使用引理。我已经做到了你所拥有的（使用广义假设），所以请你建议我如何做这个练习？或者，更确切地说，只是给出练习的答案。

【解决方案2】：

如果你证明myadd1 通勤，就很容易证明它们是平等的：

Lemma myadd1_comm: forall a b, myadd1 a b = myadd1 b a.
  now induction a; intros; auto; simpl; rewrite IHa.
Qed.       

Lemma myadd2_equiv_myadd1: forall m n, myadd1 m n = myadd2 m n.
  now induction m; intros; auto; simpl; rewrite <- IHm, !(myadd1_comm m).
Qed.

【讨论】：

myadd1_comm 隐含地依赖于标准的plus_n_Sm 引理（因为myadd1 和Nat.add 是可转换的），所以从技术上讲，您仍然需要再证明一个引理:)
@AntonTrunov 哎呀！ :)