Add 'Factorial.v'

Factorial.v

@@ -0,0 +1,57 @@
+(* 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.