如何证明自然数阶乘的归纳定义与Fixpoint定义等价？

我为自然数阶乘定义了两种形式：Fixpoint实现的fact_fix，以及归纳谓词fact_prop，目标是证明这两种定义等价（即对任意i,j，若fact_prop i j则j = fact_fix i）。目前只完成了归纳证明的第一步，以下是定义、待证引理及未完成的证明，需要完成剩余步骤：

Fixpoint fact_fix (n: nat): nat:=
match n with
| O => 1
| S m => n * fact_fix m
end.

Inductive fact_prop: nat -> nat -> Prop:=
| fact_0:
      fact_prop 0 1
| fact_mul:
      forall i j: nat, fact_prop i j -> fact_prop (S i) ((S i)*j).

Lemma equiv:
forall i j: nat,
fact_prop i j -> j=fact_fix i.
Proof.
induction i.
- intros j H1.
  simpl.
  inversion H1.
  reflexivity.
- intros j H1.
Admitted.

完成证明的步骤： #

在归纳的第二步（i = S m的情况），我们拿到假设H1: fact_prop (S m) j，接下来可以这样操作：

1. 对H1执行inversion：因为S m不可能匹配fact_0构造子，Coq会自动推导出唯一可能的情况——H1由fact_mul构造而来，由此得到两个新假设：
   • H2: fact_prop m k（k为中间变量）
   • H3: j = (S m) * k
2. 调用归纳假设：归纳假设IHm指出forall k, fact_prop m k -> k = fact_fix m，结合H2可得到k = fact_fix m。
3. 结合fact_fix的定义：fact_fix (S m)展开后就是(S m) * fact_fix m，再结合H3和刚得到的等式，就能推导出j = fact_fix (S m)。

完整的证明代码： #

Lemma equiv:
forall i j: nat,
fact_prop i j -> j=fact_fix i.
Proof.
induction i.
- intros j H1.
  simpl.
  inversion H1.
  reflexivity.
- intros j H1.
  inversion H1 as [| m k H2 H3].
  rewrite IHm in H2.
  rewrite H2.
  rewrite H3.
  simpl fact_fix.
  reflexivity.
Qed.

或者更简洁的写法（直接对fact_prop的归纳结构做归纳）：

Lemma equiv:
forall i j: nat,
fact_prop i j -> j=fact_fix i.
Proof.
induction 1.
- reflexivity.
- rewrite IHfact_prop.
  simpl fact_fix.
  reflexivity.
Qed.

这里induction 1表示直接对传入的fact_prop假设做归纳，比自然数归纳更贴合阶乘的递归定义逻辑。

内容的提问来源于stack exchange，提问作者Marcus