57 lines
1.4 KiB
Coq
57 lines
1.4 KiB
Coq
(* I renamed this from factorial to factorial_rec. *)
|
|
Fixpoint factorial_rec (n: nat): nat :=
|
|
match n with
|
|
| O => 1
|
|
| S n' => n * factorial_rec n'
|
|
end.
|
|
|
|
Eval compute in (factorial_rec 5).
|
|
|
|
Inductive factorial : nat -> nat -> Prop :=
|
|
| fact_base : factorial O 1
|
|
| fact_step : forall n m, factorial n m -> factorial (S n) ((S n) * m).
|
|
|
|
Example factorial_5 : factorial 5 120.
|
|
Proof.
|
|
apply (fact_step 4 24).
|
|
apply (fact_step 3 6).
|
|
apply (fact_step 2 2).
|
|
apply (fact_step 1 1).
|
|
apply (fact_step O 1). (* The step ChatGPT missed. *)
|
|
apply fact_base.
|
|
Qed.
|
|
|
|
Lemma factorial_equiv : forall n, factorial n (factorial_rec n).
|
|
Proof.
|
|
induction n.
|
|
- apply fact_base.
|
|
- simpl.
|
|
apply (fact_step n (factorial_rec n)).
|
|
apply IHn.
|
|
Qed.
|
|
|
|
(* This generated lemma was incorrect. I rewrote the claim manually and generated a new proof. *)
|
|
(* Lemma factorial_rec_equiv : forall n, factorial_rec n = factorial n. *)
|
|
(* Proof. *)
|
|
(* intros n. *)
|
|
(* unfold factorial_rec. *)
|
|
(* induction n. *)
|
|
(* - reflexivity. *)
|
|
(* - simpl. *)
|
|
(* rewrite IHn. *)
|
|
(* apply (fact_step n (factorial n)). *)
|
|
(* apply factorial_equiv. *)
|
|
(* Qed. *)
|
|
|
|
Lemma factorial_rec_equiv : forall n m, factorial_rec n = m -> factorial n m.
|
|
Proof.
|
|
intros n m H.
|
|
rewrite <- H.
|
|
clear H.
|
|
induction n.
|
|
- apply fact_base.
|
|
- simpl.
|
|
apply (fact_step n (factorial_rec n)).
|
|
apply IHn.
|
|
(* reflexivity. *) (* This proved (ha) unnecessary. *)
|
|
Qed. |