归纳法和递归法的等价

Question

我对自然数的阶乘有两个定义。一种是归纳定义，另一种是固定点。我想证明这两个定义的等价性，但一直没能做到。我什至没有非正式的证明，但我的猜测是归纳法应该有效。不管怎样，它们就在这里（定义和引理陈述）。猜猜我如何完成证明？预先感谢。

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.

Answer 1

这里有一个提示：再次使用

inversion

，然后也利用归纳假设...