oysteikt/tapl-proofs
0
0
Fork 0
Code Issues Pull Requests Activity

chap3: revenge

Browse Source
This commit is contained in:
Oystein Kristoffer Tveit
2026-06-30 16:05:31 +09:00
parent b914620570
commit ab579f5cf0
1 changed files with 550 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/chap3_revenge.v
+550
View File
@@ -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.