You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

#### 57 lines 1.4 KiB Raw Permalink Blame History

 ```(* 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.`