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

Question

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

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.

Answer 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.

Answer 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.