I have two definitions for factorial of a natural number. One is an inductive definition and the other is a fixpoint. I would like to prove the equivalence of these two definitions, but haven't been able to do so. I also don´t even have an informal proof, but my guess is that induction should work. Anyway, here they go (the definitions and the lemma statement). Guesses on how I could complete the proof? Thanks in advance.
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.
Guesses on how I could complete the proof?
Here is a hint: using again inversion, then also leveraging the inductive hypothesis...