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

chap8: init

Browse Source
This commit is contained in:
Oystein Kristoffer Tveit
2026-06-25 23:23:51 +09:00
parent dbac63ed42
commit 13b592ea06
1 changed files with 627 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/chap8.v
+627
View File
@@ -0,0 +1,627 @@
Module Chap8.
(* 8.1 *)
Inductive term : Type :=
| ttrue
| tfalse
| iif (t1 t2 t3 : term)
| O
| succ (t : term)
| pred (t : term)
| iszero (t : term).
Scheme Equality for term.
Inductive is_numeric_val : term -> Prop :=
| nv_O : is_numeric_val O
| nv_succ : forall t, is_numeric_val t -> is_numeric_val (succ t).
Inductive is_value : term -> Prop :=
| v_true : is_value ttrue
| v_false : is_value tfalse
| v_num : forall t, is_numeric_val t -> is_value t.
Lemma numeric_value_is_value : forall (t : term),
is_numeric_val t -> is_value t.
Proof.
intros t H.
destruct H as [| t' H'].
- apply v_num. exact nv_O.
- apply v_num. apply nv_succ. exact H'.
Qed.
(* 8.2 *)
Inductive type : Type :=
| TBool
| TNat.
Scheme Equality for type.
Inductive has_type : term -> type -> Prop :=
| T_True : has_type ttrue TBool
| T_False : has_type tfalse TBool
| T_If : forall t1 t2 t3 T,
has_type t1 TBool ->
has_type t2 T ->
has_type t3 T ->
has_type (iif t1 t2 t3) T
| T_Zero : has_type O TNat
| T_Succ : forall t1,
has_type t1 TNat ->
has_type (succ t1) TNat
| T_Pred : forall t1,
has_type t1 TNat ->
has_type (pred t1) TNat
| T_IsZero : forall t1,
has_type t1 TNat ->
has_type (iszero t1) TBool.
Lemma numeric_value_type : forall (t : term),
is_numeric_val t -> has_type t TNat.
Proof.
intros t H.
induction H as [| t' H' IH].
- apply T_Zero.
- apply T_Succ. exact IH.
Qed.
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)
| E_Succ : forall t1 t1',
step t1 t1' ->
step (succ t1) (succ t1')
| E_PredZero :
step (pred O) O
| E_PredSucc : forall t1,
is_numeric_val t1 ->
step (pred (succ t1)) t1
| E_Pred : forall t1 t1',
step t1 t1' ->
step (pred t1) (pred t1')
| E_IsZeroZero :
step (iszero O) ttrue
| E_IsZeroSucc : forall t1,
is_numeric_val t1 ->
step (iszero (succ t1)) tfalse
| E_IsZero : forall t1 t1',
step t1 t1' ->
step (iszero t1) (iszero t1').
Lemma step_value_stuck : forall (t t' : term),
is_value t ->
step t t' ->
t = t'.
Proof.
intros t t' Hval Hstep.
destruct Hval.
- inversion Hstep.
- inversion Hstep.
- inversion Hstep. subst.
+ inversion H.
+
Admitted.
(* 8.2.1 *)
Definition is_well_typed (t : term) : Prop :=
exists (T : type), has_type t T.
(* 8.2.2 *)
Lemma t_ttrue_inv : forall (T : type),
has_type ttrue T -> T = TBool.
Proof.
intros T H. inversion H. reflexivity.
Qed.
Lemma t_tfalse_inv : forall (T : type),
has_type tfalse T -> T = TBool.
Proof.
intros T H. inversion H. reflexivity.
Qed.
Lemma t_iff_inv : forall (t1 t2 t3 : term) (T : type),
has_type (iif t1 t2 t3) T ->
has_type t1 TBool /\ has_type t2 T /\ has_type t3 T.
Proof.
intros t1 t2 t3 T H.
inversion H as [| | | | | | H0 H1 H2].
split.
- exact H0.
- split.
+ exact H1.
+ exact H2.
Qed.
Lemma t_O_inv : forall T,
has_type O T -> T = TNat.
Proof.
intros T H. inversion H. reflexivity.
Qed.
Lemma t_succ_inv : forall (t1 : term) (T : type),
has_type (succ t1) T -> has_type t1 TNat /\ T = TNat.
Proof.
intros t1 T H.
inversion H as [| | | | | | H0 _].
split.
- exact H0.
- reflexivity.
Qed.
Lemma t_pred_inv : forall (t1 : term) (T : type),
has_type (pred t1) T -> has_type t1 TNat /\ T = TNat.
Proof.
intros t1 T H.
inversion H as [| | | | | | H0 _].
split.
- exact H0.
- reflexivity.
Qed.
Lemma t_iszero_inv : forall (t1 : term) (T : type),
has_type (iszero t1) T -> has_type t1 TNat /\ T = TBool.
Proof.
intros t1 T H.
inversion H as [| | | | | | H0 H1].
split.
- exact H1.
- reflexivity.
Qed.
(* 8.2.3 *)
Lemma wt_succ_inv : forall (t1 : term),
is_well_typed (succ t1) -> is_well_typed t1.
Proof.
intros t1 [T H].
apply t_succ_inv in H.
destruct H as [H1 _].
exists TNat.
exact H1.
Qed.
Lemma wt_pred_inv : forall (t1 : term),
is_well_typed (pred t1) -> is_well_typed t1.
Proof.
intros t1 [T H].
apply t_pred_inv in H.
destruct H as [H1 _].
exists TNat.
exact H1.
Qed.
Lemma wt_iszero_inv : forall (t1 : term),
is_well_typed (iszero t1) -> is_well_typed t1.
Proof.
intros t1 [T H].
apply t_iszero_inv in H.
destruct H as [H1 _].
exists TNat.
exact H1.
Qed.
Lemma wt_if_inv : forall (t1 t2 t3 : term),
is_well_typed (iif t1 t2 t3) -> is_well_typed t1 /\ is_well_typed t2 /\ is_well_typed t3.
Proof.
intros t1 t2 t3 [T H].
apply t_iff_inv in H.
destruct H as [H1 [H2 H3]].
split.
- exists TBool. exact H1.
- split.
+ exists T. exact H2.
+ exists T. exact H3.
Qed.
Inductive subterm : term -> term -> Prop :=
| subterm_refl : forall t, subterm t t
| subterm_if1 : forall t1 t2 t3 s,
subterm s t1 ->
subterm s (iif t1 t2 t3)
| subterm_if2 : forall t1 t2 t3 s,
subterm s t2 ->
subterm s (iif t1 t2 t3)
| subterm_if3 : forall t1 t2 t3 s,
subterm s t3 ->
subterm s (iif t1 t2 t3)
| subterm_succ : forall t1 s,
subterm s t1 ->
subterm s (succ t1)
| subterm_pred : forall t1 s,
subterm s t1 ->
subterm s (pred t1)
| subterm_iszero : forall t1 s,
subterm s t1 ->
subterm s (iszero t1).
Lemma subterms_typed : forall (t s : term) (T : type),
has_type t T ->
subterm s t ->
exists (T' : type), has_type s T'.
Proof.
intros t s T Htype Hst.
generalize dependent T.
induction Hst.
- intros T Htype. exists T. exact Htype.
- intros T Htype.
apply t_iff_inv in Htype.
destruct Htype as [H1 [_ _]].
apply IHHst in H1.
exact H1.
- intros T Htype.
apply t_iff_inv in Htype.
destruct Htype as [_ [H2 _]].
apply IHHst in H2.
exact H2.
- intros T Htype.
apply t_iff_inv in Htype.
destruct Htype as [_ [_ H3]].
apply IHHst in H3.
exact H3.
- intros T Htype.
apply t_succ_inv in Htype.
destruct Htype as [H1 _].
apply IHHst in H1.
exact H1.
- intros T Htype.
apply t_pred_inv in Htype.
destruct Htype as [H1 _].
apply IHHst in H1.
exact H1.
- intros T Htype.
apply t_iszero_inv in Htype.
destruct Htype as [H1 _].
apply IHHst in H1.
exact H1.
Qed.
(*
This is essentially the same as the previous lemma,
and it is piggybacking off it,
but it is stated with the is_well_typed predicate instead.
*)
Corollary subterms_welltyped : forall (t s : term),
is_well_typed t -> subterm s t -> is_well_typed s.
Proof.
intros t s Hwt Hst.
revert Hwt.
induction Hst.
- intros Hwt. exact Hwt.
Admitted.
(* 8.2.4 *)
Lemma uniqueness_of_types : forall (t : term) (T1 T2 : type),
has_type t T1 -> has_type t T2 -> T1 = T2.
Proof.
intros t T1 T2 H1 H2.
generalize dependent T2.
induction H1; intros T2 H2.
- apply t_ttrue_inv in H2. rewrite H2. reflexivity.
- apply t_tfalse_inv in H2. rewrite H2. reflexivity.
- apply t_iff_inv in H2.
destruct H2 as [_ [H2_2 _]].
apply IHhas_type2 in H2_2.
rewrite H2_2.
reflexivity.
- apply t_O_inv in H2. rewrite H2. reflexivity.
- apply t_succ_inv in H2.
destruct H2 as [_ H2_2].
rewrite H2_2.
reflexivity.
- apply t_pred_inv in H2.
destruct H2 as [_ H2_2].
rewrite H2_2.
reflexivity.
- apply t_iszero_inv in H2.
destruct H2 as [_ H2_2].
rewrite H2_2.
reflexivity.
Qed.
(* 8.3.1 *)
Lemma canonical_forms_bool : forall (t : term),
is_value t -> has_type t TBool -> t = ttrue \/ t = tfalse.
Proof.
intros t Hval Htype.
destruct Hval.
- left. reflexivity.
- right. reflexivity.
- apply numeric_value_type in H.
apply uniqueness_of_types with (T1 := TNat) in Htype; try assumption.
discriminate Htype.
Qed.
Lemma canonical_forms_nat : forall (t : term),
is_value t -> has_type t TNat -> is_numeric_val t.
Proof.
intros t Hval Htype.
destruct Hval.
- inversion Htype.
- inversion Htype.
- exact H.
Qed.
(* 8.3.2 *)
Lemma progress : forall (t : term) (T : type),
has_type t T -> is_value t \/ exists (t' : term), step t t'.
Proof.
intros t T Htype.
induction Htype.
(* T-True *)
- left. constructor.
(* T-False *)
- left. constructor.
(* T-If *)
- right. destruct IHHtype1 as [Hval1 | [t1' Hstep1]]; try assumption.
+ apply canonical_forms_bool in Hval1; try assumption.
destruct Hval1 as [Htrue | Hfalse].
* exists t2. rewrite Htrue. constructor.
* exists t3. rewrite Hfalse. constructor.
+ exists (iif t1' t2 t3). constructor. exact Hstep1.
(* T-Zero *)
- left. constructor. constructor.
(* T-Succ *)
- destruct IHHtype as [Hval1 | [t1' Hstep1]]; try assumption.
+ apply canonical_forms_nat in Hval1; try assumption.
left.
apply nv_succ in Hval1.
apply numeric_value_is_value in Hval1.
exact Hval1.
+ right.
exists (succ t1').
constructor.
exact Hstep1.
(* T-Pred *)
- destruct IHHtype as [Hval1 | [t1' Hstep1]]; try assumption.
+ apply canonical_forms_nat in Hval1; try assumption.
right.
destruct Hval1 as [| t1'' Hnv].
* exists O. constructor.
* exists t1''. constructor. exact Hnv.
+ right.
exists (pred t1').
constructor.
exact Hstep1.
(* T-IsZero *)
- destruct IHHtype as [Hval1 | [t1' Hstep1]]; try assumption.
+ apply canonical_forms_nat in Hval1; try assumption.
right.
destruct Hval1 as [| t1'' Hnv].
* exists ttrue. constructor.
* exists tfalse. constructor. exact Hnv.
+ right.
exists (iszero t1').
constructor.
exact Hstep1.
Qed.
(* 8.3.3 *)
Lemma preservation : forall (t t' : term) (T : type),
has_type t T -> step t t' -> has_type t' T.
Proof.
intros t t' T Htype Hstep.
generalize dependent t'.
(* Induction on the typing derivation *)
induction Htype; intros t' Hstep.
(* T-True *)
- inversion Hstep.
(* T-False *)
- inversion Hstep.
(* T-If *)
- inversion Hstep; subst.
+ (* E-IfTrue *)
assumption.
+ (* E-IfFalse *)
assumption.
+ (* E-If *)
apply T_If; try assumption. apply IHHtype1. assumption.
(* T-Zero *)
- inversion Hstep.
(* T-Succ *)
- inversion Hstep; subst.
+ (* E-Succ *)
apply T_Succ. apply IHHtype. assumption.
(* T-Pred *)
- inversion Hstep; subst.
+ (* E-PredZero *)
apply T_Zero.
+ (* E-PredSucc *)
apply numeric_value_type. assumption.
+ (* E-Pred *)
apply T_Pred. apply IHHtype. assumption.
(* T-IsZero *)
- inversion Hstep; subst.
+ (* E-IsZeroZero *)
apply T_True.
+ (* E-IsZeroSucc *)
apply T_False.
+ (* E-IsZero *)
apply T_IsZero. apply IHHtype. assumption.
Qed.
(* 8.3.3 *)
Lemma preservation_by_eval_drvs : forall (t t' : term) (T : type),
has_type t T -> step t t' -> has_type t' T.
Proof.
intros t t' T Htype Hstep.
generalize dependent T.
(* Induction on the evaluation derivation *)
induction Hstep; intros T Htype.
(* E-IfTrue *)
- apply t_iff_inv in Htype.
destruct Htype as [H1 [H2 H3]].
assumption.
(* E-IfFalse *)
- apply t_iff_inv in Htype.
destruct Htype as [H1 [H2 H3]].
assumption.
(* E-If *)
- apply t_iff_inv in Htype.
destruct Htype as [H1 [H2 H3]].
apply T_If; try assumption.
apply IHHstep. exact H1.
(* E-Succ *)
- apply t_succ_inv in Htype.
destruct Htype as [H1 H2].
apply IHHstep in H1.
rewrite H2.
apply T_Succ.
exact H1.
(* E-PredZero *)
- apply t_pred_inv in Htype.
destruct Htype as [H1 H2].
rewrite H2.
apply T_Zero.
(* E-PredSucc *)
- apply t_pred_inv in Htype.
destruct Htype as [H1 H2].
rewrite H2.
apply numeric_value_type.
exact H.
(* E-Pred *)
- apply t_pred_inv in Htype.
destruct Htype as [H1 H2].
apply IHHstep in H1.
rewrite H2.
apply T_Pred.
exact H1.
(* E-IsZeroZero *)
- apply t_iszero_inv in Htype.
destruct Htype as [H1 H2].
rewrite H2.
apply T_True.
(* E-IsZeroSucc *)
- apply t_iszero_inv in Htype.
destruct Htype as [H1 H2].
rewrite H2.
apply T_False.
(* E-IsZero *)
- apply t_iszero_inv in Htype.
destruct Htype as [H1 H2].
apply IHHstep in H1.
rewrite H2.
apply T_IsZero.
exact H1.
Qed.
(* 8.3.6 *)
Lemma not_subject_expansion : ~(
forall (t t' : term) (T : type),
step t t' ->
has_type t' T ->
has_type t T
).
Proof.
intros H.
specialize (H (iif ttrue O ttrue) O TNat).
assert (has_type (iif ttrue O ttrue) TNat).
{ apply H.
- constructor.
- constructor.
}
inversion H0 as [| | | | | | H1 H2 H3].
inversion H3.
Qed.
(* 8.3.7 *)
Inductive step_big : term -> term -> Prop :=
| B_Value : forall (t : term),
is_value t ->
step_big t t
| B_IfTrue : forall (t1 t2 t3 v2 : term),
step_big t1 ttrue ->
is_value v2 ->
step_big t2 v2 ->
step_big (iif ttrue t2 t3) v2
| B_IfFalse : forall (t1 t2 t3 v3 : term),
step_big t1 tfalse ->
is_value v3 ->
step_big t3 v3 ->
step_big (iif tfalse t2 t3) v3
| B_Succ : forall (t1 nv1 : term),
is_numeric_val nv1 ->
step_big t1 nv1 ->
step_big (succ t1) (succ nv1)
| B_PredZero : forall (t1 : term),
step_big t1 O ->
step_big (pred O) O
| B_PredSucc : forall (t1 nv1 : term),
is_numeric_val nv1 ->
step_big t1 (succ nv1) ->
step_big (pred t1) nv1
| B_IsZeroZero : forall (t1 : term),
step_big t1 O ->
step_big (iszero t1) ttrue
| B_IsZeroSucc : forall (t1 nv1 : term),
is_numeric_val nv1 ->
step_big t1 (succ nv1) ->
step_big (iszero t1) tfalse.
Lemma big_step_progress : forall (t : term) (T : type),
has_type t T -> is_value t \/ exists (t' : term), step_big t t'.
Proof.
intros t T Htype.
induction Htype.
(* T-True *)
- left. constructor.
(* T-False *)
- left. constructor.
(* T-If *)
- destruct IHHtype1 as [Hval1 | [t1' Hstep1]]; try assumption.
+ right. apply canonical_forms_bool in Hval1; try assumption.
destruct Hval1 as [Htrue | Hfalse].
* exists t2. rewrite Htrue.
Admitted.
Lemma big_step_preservation : forall (t t' : term) (T : type),
has_type t T -> step_big t t' -> has_type t' T.
Proof.
intros t t' T Htype Hstep.
generalize dependent t'.
induction Htype; intros t' Hstep.
(* T-True *)
- inversion Hstep; subst. apply T_True.
(* T-False *)
- inversion Hstep; subst. apply T_False.
(* T-If *)
- inversion Hstep; subst.
+ apply T_If; try assumption.
+ apply IHHtype2. assumption.
+ apply IHHtype3. assumption.
(* T-Zero *)
- inversion Hstep; subst. apply T_Zero.
(* T-Succ *)
- inversion Hstep; subst.
+ apply T_Succ. exact Htype.
+ apply T_Succ. apply IHHtype. assumption.
(* T-Pred *)
- inversion Hstep; subst.
+ apply T_Pred. assumption.
+ assumption.
+ apply IHHtype in H1.
apply t_succ_inv in H1.
apply H1.
(* T-IsZero *)
- inversion Hstep; subst.
+ apply T_IsZero. assumption.
+ apply T_True.
+ apply T_False.
Qed.
(* 8.3.8 *)
(* Inductive term2 : Type :=
| ttrue
| tfalse
| iif (t1 t2 t3 : term2)
| O
| succ (t : term2)
| pred (t : term2)
| iszero (t : term2)
| wrong. *)
End Chap8.