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.