From ab579f5cf0e8c1afa374ef06fc0bc838aa5a9d9f Mon Sep 17 00:00:00 2001 From: h7x4 Date: Tue, 30 Jun 2026 16:05:31 +0900 Subject: [PATCH] chap3: revenge --- src/chap3_revenge.v | 550 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 550 insertions(+) create mode 100644 src/chap3_revenge.v diff --git a/src/chap3_revenge.v b/src/chap3_revenge.v new file mode 100644 index 0000000..cd5db37 --- /dev/null +++ b/src/chap3_revenge.v @@ -0,0 +1,550 @@ +(* + I learnt a bit more about how relations could be constructed using Inductive types during chapter 8, + and realized that it would be a lot easier to prove certain things using those instead. + + Attempting chapter 3 again using this approach. +*) + +From Stdlib Require Import + Arith.Arith + Arith.Wf_nat + Lists.List + Lists.ListSet. +Import ListNotations. + + +Module Chap3. + Module BoolArithExpr. + Inductive term : Type := + | ttrue + | tfalse + | iif (t1 t2 t3 : term). + + Scheme Equality for term. + + Inductive is_value : term -> Prop := + | v_true : is_value ttrue + | v_false : is_value tfalse. + + (* 3.3.1 *) + Fixpoint consts (t:term) : set term := + match t with + | ttrue => [ttrue] + | tfalse => [tfalse] + | iif t1 t2 t3 => consts t1 ++ consts t2 ++ consts t3 + end. + + (* 3.3.2 *) + Fixpoint size (t:term) : Nat.t := + match t with + | ttrue => 1 + | tfalse => 1 + | iif t1 t2 t3 => 1 + size t1 + size t2 + size t3 + end. + + Fixpoint depth (t:term) : Nat.t := + match t with + | ttrue => 1 + | tfalse => 1 + | iif t1 t2 t3 => 1 + (Nat.max (depth t1) (Nat.max (depth t2) (depth t3))) + end. + + (* 3.3.3 *) + Lemma consts_less_than_size : forall t : term, length (consts t) <= size t. + Proof. + intros t. + (* structural induction on the term *) + induction t as [| | t1 IHt1 t2 IHt2 t3 IHt3]; try reflexivity. + simpl. + rewrite <- Nat.le_succ_diag_r. + repeat rewrite length_app. + rewrite Nat.add_assoc. + repeat apply Nat.add_le_mono. + all: assumption. + Qed. + + (* 3.3.4 *) + (* NOTE: see also https://gijs-pennings.github.io/rocq-wf-recursion/ *) + + Lemma induction_on_depth : + forall (P : term -> Prop), + (forall (s : term), + (forall (r : term), depth r < depth s -> P r) -> + P s) -> + forall t, P t. + Proof. + intros P H. + apply (well_founded_induction_type (well_founded_ltof term depth)). + exact H. + Qed. + + Lemma induction_on_size : + forall (P : term -> Prop), + (forall (s : term), + (forall (r : term), size r < size s -> P r) -> + P s) -> + forall t, P t. + Proof. + intros P H. + apply (well_founded_induction_type (well_founded_ltof term size)). + exact H. + Qed. + + Inductive immediate_subterm : term -> term -> Prop := + | E_If1 : forall t1 t2 t3, immediate_subterm (iif t1 t2 t3) t1 + | E_If2 : forall t1 t2 t3, immediate_subterm (iif t1 t2 t3) t2 + | E_If3 : forall t1 t2 t3, immediate_subterm (iif t1 t2 t3) t3. + + Lemma structural_induction : + forall (P : term -> Prop), + (forall (s : term), + (forall (r : term), immediate_subterm s r -> P r) -> + P s) -> + forall t, P t. + Proof. + intros P H t. + induction t. + - apply H. intros r Hsub. inversion Hsub. + - apply H. intros r Hsub. inversion Hsub. + - apply H. intros r Hsub. inversion Hsub; subst. + + apply IHt1. + + apply IHt2. + + apply IHt3. + Qed. + + (* 3.5.3 *) + Inductive step : term -> term -> Prop := + | E_IfTrue : forall t2 t3, step (iif ttrue t2 t3) t2 + | E_IfFalse : forall t2 t3, step (iif tfalse t2 t3) t3 + | E_If : forall t1 t1' t2 t3, + step t1 t1' -> + step (iif t1 t2 t3) (iif t1' t2 t3). + + (* 3.5.4 *) + Lemma step_determinancy : forall t t1' t2' : term, + step t t1' -> + step t t2' -> + t1' = t2'. + Proof. + intros t t1' t2' Hstep. + generalize dependent t2'. + (* induction on the derivation of (t -> t1') *) + induction Hstep as [ | | t1 t1'' t2 t3 Hstep IH]. + all: intros t2' Hstep2; inversion Hstep2; subst. + 1,3: reflexivity. + 1,2: inversion H3. + 1,2: inversion Hstep. + f_equal. + apply IH. + exact H3. + Qed. + + (* 3.5.6 *) + Definition is_normal_form (t:term) : Prop := + ~ exists t', step t t'. + + (* 3.5.7 *) + Lemma all_values_are_normal_forms : forall t : term, is_value t -> is_normal_form t. + Proof. + intros t H. + destruct t as [| | t1 t2 t3]. + all: unfold is_normal_form; intros [t' Hstep]. + 1,2: inversion Hstep. + inversion Hstep; subst. + all: inversion H. + Qed. + + (* 3.5.8 *) + + Lemma iif_steps: + forall (t1 t2 t3 : term), + exists t', step (iif t1 t2 t3) t'. + Proof. + intros t1. + (* induction on the structure of t1 *) + induction t1. + - intros t2 t3. exists t2. constructor. + - intros t2 t3. exists t3. constructor. + - intros t2 t3. + destruct (IHt1_1 t1_2 t1_3) as [t' Hstep]. + exists (iif t' t2 t3). + constructor. + exact Hstep. + Qed. + + Lemma iif_not_normal: + forall (t1 t2 t3 : term), + ~ is_normal_form (iif t1 t2 t3). + Proof. + intros t1 t2 t3 H. + unfold is_normal_form in H. + apply H. + apply iif_steps. + Qed. + + Lemma not_value_not_normal_form : + forall t, + ~ is_value t -> ~ (is_normal_form t). + Proof. + intros t Hnv Hnf. + (* induction on the structure of t *) + induction t as [| | t1 IH1 t2 IH2 t3 IH3]. + (* + The premise is that t is not a value, so the first two + cases invalidate the premise. + *) + - apply Hnv. exact v_true. + - apply Hnv. exact v_false. + - destruct t1 eqn:Ht1. + (* + If t1 is either true or false, then t is clearly not a normal form, + because it matches the E_IfTrue and E_IfFalse step constructors. + *) + + apply Hnf. + exists t2. + apply E_IfTrue. + + apply Hnf. + exists t3. + apply E_IfFalse. + (* + If t1 is itself an if expression, then t is not a normal form. + *) + + apply (iif_not_normal (iif t4 t5 t6) t2 t3). + exact Hnf. + Qed. + + Lemma all_normal_forms_are_values : forall t : term, + is_normal_form t -> is_value t. + Proof. + intros t. + destruct t. + - constructor. + - constructor. + - intros H. + exfalso. + apply (iif_not_normal t1 t2 t3). + exact H. + Qed. + + (* 3.5.9 *) + Lemma ss_nostep_eq : + forall t t', + step t t' -> + is_normal_form t -> + t = t'. + Proof. + intros t t' Hstep Hnf. + unfold is_normal_form in Hnf. + exfalso. + apply Hnf. + exists t'. + exact Hstep. + Qed. + + (* This definition of multi_step is defined word for word as the + book defines it *) + Inductive multi_step : term -> term -> Prop := + | multi_refl : forall t, multi_step t t + | multi_step_single : forall t t', step t t' -> multi_step t t' + | multi_step_trans : + forall t t' t'', + multi_step t t' -> + multi_step t' t'' -> + multi_step t t''. + + + (* This structure seems to be more convenient for the following proofs *) + Inductive multi_step' : term -> term -> Prop := + | multi_refl' : forall t, multi_step' t t + | multi_step_split' : + forall t t' t'', + step t t' -> + multi_step' t' t'' -> + multi_step' t t''. + + (* Before continuing, I will prove that these two definitions are equivalent. + Proving equivalency requires a bunch of auxiliary lemmas. + *) + Lemma ms_nostep_eq' : + forall t t', + multi_step' t t' -> + is_normal_form t -> + t = t'. + Proof. + intros t t' Hms Hnf. + (* induction on the derivation of (t ->* t') *) + induction Hms. + - reflexivity. + - unfold is_normal_form in Hnf. + exfalso. + apply Hnf. + exists t'. + exact H. + Qed. + + Lemma ss_singlestep_ms_eq' : + forall t t' t'' : term, + step t t' -> + is_normal_form t' -> + multi_step' t' t'' -> + t' = t''. + Proof. + intros t t' t'' Hstep Hnf Hms. + (* Induction on the derivation of (t' ->* t'') *) + induction Hms. + - reflexivity. + - unfold is_normal_form in Hnf. + exfalso. + apply Hnf. + exists t'. + exact H. + Qed. + + Lemma ss_ms_trans : forall t t' t'' : term, + step t t' -> + multi_step t' t'' -> + multi_step t t''. + Proof. + intros t t' t'' Hms Hstep. + apply multi_step_trans with (t' := t'). + - apply multi_step_single. + exact Hms. + - exact Hstep. + Qed. + + Lemma ss_ms_trans' : forall t t' t'' : term, + step t t' -> + multi_step' t' t'' -> + multi_step' t t''. + Proof. + intros t t' t'' Hms Hstep. + apply multi_step_split' with (t' := t'). + - exact Hms. + - exact Hstep. + Qed. + + Lemma ms_ms_trans' : forall t t' t'' : term, + multi_step' t t' -> + multi_step' t' t'' -> + multi_step' t t''. + Proof. + intros t t' t'' Hms Hstep. + induction Hms as [| t t' u Hstep' Hms' IH]. + - exact Hstep. + - apply multi_step_split' with (t' := t'). + + exact Hstep'. + + specialize (IH Hstep). + exact IH. + Qed. + + (* Now we can prove that the two definitions of multi_step are equivalent *) + Lemma multi_step_equiv : forall t t' : term, multi_step t t' <-> multi_step' t t'. + Proof. + intros t t'. + split. + - intros H. + induction H as [| t t' Hstep | t t' t'' Hms1 IHHms1 Hms2 IHHms2]. + + apply multi_refl'. + + apply multi_step_split' with (t' := t'). + * exact Hstep. + * apply multi_refl'. + + apply ms_ms_trans' with (t' := t'). + * exact IHHms1. + * exact IHHms2. + - intros H. + induction H as [| t t' t'' Hstep Hms IHHms]. + + apply multi_refl. + + assert (multi_step t t') as Hms'. + { + apply multi_step_single. + exact Hstep. + } + apply multi_step_trans with (t' := t'). + * exact Hms'. + * exact IHHms. + Qed. + + (* 3.5.11 *) + Lemma uniqueness_of_normal_forms' : + forall t u1: term, + multi_step' t u1 -> + is_normal_form u1 -> + forall u2 : term, + multi_step' t u2 -> + is_normal_form u2 -> + u1 = u2. + Proof. + intros t u1 Hms1 Hnf1. + (* induction on the derivation of (t ->* u1) *) + induction Hms1 as + [ t + | t u1' u1 Hstep Hms1' + ]. + (* t ->* u1 /\ t = u1 is essentially just ms_nostep_eq *) + - intros u2 Hms2 Hnf2. + apply ms_nostep_eq' with (t := t) (t' := u2). + assumption. + assumption. + + + (* t -> u1' ->* u1 *) + - intros u2 Hms2 Hnf2. + induction Hms2 as + [ t + | t u2' u2 Hstep2 Hms2' + ]. + (* + t -> u1' ->* u1 and t ->* u2 where t = u2 is a contradiction, + because it implies that u1' doesn't exist. + *) + + exfalso. + apply Hnf2. + exists u1'. + exact Hstep. + (* + t -> u1' ->* u1 and t ->* u2' ->* u2, + we can unify u1' and u2' using step_determinancy. + *) + + pose proof (step_determinancy t u1' u2' Hstep Hstep2) as Heq. + subst u2'. + apply IHHms1'. + * assumption. + * assumption. + * assumption. + Qed. + + (* Wrapper by mapping multi_step to multi_step' *) + Lemma uniqueness_of_normal_forms : + forall t u1: term, + multi_step t u1 -> + is_normal_form u1 -> + forall u2 : term, + multi_step t u2 -> + is_normal_form u2 -> + u1 = u2. + Proof. + intros t u1 Hms1 Hnf1 u2 Hms2 Hnf2. + rewrite multi_step_equiv in *. + exact (uniqueness_of_normal_forms' t u1 Hms1 Hnf1 u2 Hms2 Hnf2). + Qed. + + (* 3.5.12 *) + Lemma min_size : forall (t : term), + 1 <= size t. + Proof. + intros t. + induction t as [| | t1 IHt1 t2 IHt2 t3 IHt3]; simpl. + - reflexivity. + - reflexivity. + - apply Nat.lt_lt_succ_r. + auto with arith. + Qed. + + Lemma step_decreases_size : forall t t' : term, step t t' -> size t' < size t. + Proof. + intros t t' Hstep. + induction Hstep as [t2 t3 | t2 t3 | t1 t1' t2 t3 Hstep IH]. + - simpl. + repeat apply Nat.lt_lt_succ_r. + apply Nat.lt_add_pos_r. + apply min_size. + - simpl. + repeat apply Nat.lt_lt_succ_r. + apply Nat.lt_add_pos_l. + apply min_size. + - simpl. + rewrite <- Nat.succ_lt_mono. + apply Nat.add_lt_mono_r. + apply Nat.add_lt_mono_r. + exact IH. + Qed. + + Lemma normal_form_dec : forall t : term, + is_normal_form t \/ (exists t', step t t'). + Proof. + intros t. + unfold is_normal_form. + Admitted. + + Lemma termination_of_evaluation' : forall t : term, + exists t' : term, multi_step' t t' /\ is_normal_form t'. + Proof. + induction t using induction_on_size. + destruct (normal_form_dec t) as [Hnf | Hstep]. + - exists t. + split. + + apply multi_refl'. + + exact Hnf. + - destruct Hstep as [t' Hstep]. + pose proof (step_decreases_size t t' Hstep) as Hlt. + specialize (H t' Hlt). + destruct H as [u [Hms Hnf]]. + exists u. + split. + + apply multi_step_split' with (t' := t'). + * exact Hstep. + * exact Hms. + + exact Hnf. + Qed. + + (* Additional Lemmas *) + Lemma ms_nostep_eq : + forall t t', + multi_step t t' -> + is_normal_form t -> + t = t'. + Proof. + intros t t' Hms Hnf. + (* induction on the derivation of (t ->* t') *) + induction Hms. + - reflexivity. + - unfold is_normal_form in Hnf. + exfalso. + apply Hnf. + exists t'. + assumption. + - specialize (IHHms1 Hnf). + rewrite <- IHHms1 in IHHms2. + specialize (IHHms2 Hnf). + exact IHHms2. + Qed. + + Lemma ss_singlestep_ms_eq : + forall t t' t'' : term, + step t t' -> + is_normal_form t' -> + multi_step t' t'' -> + t' = t''. + Proof. + intros t t' t'' Hstep Hnf Hms. + apply ms_nostep_eq with (t := t'). + - exact Hms. + - exact Hnf. + Qed. + + Lemma ms_dec : + forall t u, + multi_step t u -> + t = u \/ + (exists t', step t t' /\ multi_step t' u). + Proof. + intros t u Hms. + (* induction on the derivation of (t ->* u) *) + induction Hms. + - left. reflexivity. + - right. exists t'. split. + + exact H. + + apply multi_refl. + - destruct IHHms1 as [Heq | [t1 [Hstep Hms']]]. + + subst t'. + exact IHHms2. + + right. + exists t1. + split. + * exact Hstep. + * apply multi_step_trans with (t' := t'). + -- exact Hms'. + -- exact Hms2. + Qed. + End BoolArithExpr. +End Chap3. \ No newline at end of file