pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-27 23:06:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Rename typing relations from hasty to has_ty

Browse source
This commit is contained in:
Adam Chlipala 2023-03-19 11:59:34 -04:00
parent 04be648f88
commit ac0a15e9f2
4 changed files with 549 additions and 549 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

600
EvaluationContexts.v
View file

File diff suppressed because it is too large Load diff

336
EvaluationContexts_template.v
View file

@ -80,25 +80,25 @@ Module Stlc.
| Nat (* Numbers *) | Nat (* Numbers *)
| Fun (dom ran : type) (* Functions *). | Fun (dom ran : type) (* Functions *).
Inductive hasty : fmap var type -> exp -> type -> Prop := Inductive has_ty : fmap var type -> exp -> type -> Prop :=
| HtVar : forall G x t, | HtVar : forall G x t,
G $? x = Some t G $? x = Some t
-> hasty G (Var x) t -> has_ty G (Var x) t
| HtConst : forall G n, | HtConst : forall G n,
hasty G (Const n) Nat has_ty G (Const n) Nat
| HtPlus : forall G e1 e2, | HtPlus : forall G e1 e2,
hasty G e1 Nat has_ty G e1 Nat
-> hasty G e2 Nat -> has_ty G e2 Nat
-> hasty G (Plus e1 e2) Nat -> has_ty G (Plus e1 e2) Nat
| HtAbs : forall G x e1 t1 t2, | HtAbs : forall G x e1 t1 t2,
hasty (G $+ (x, t1)) e1 t2 has_ty (G $+ (x, t1)) e1 t2
-> hasty G (Abs x e1) (Fun t1 t2) -> has_ty G (Abs x e1) (Fun t1 t2)
| HtApp : forall G e1 e2 t1 t2, | HtApp : forall G e1 e2 t1 t2,
hasty G e1 (Fun t1 t2) has_ty G e1 (Fun t1 t2)
-> hasty G e2 t1 -> has_ty G e2 t1
-> hasty G (App e1 e2) t2. -> has_ty G (App e1 e2) t2.
Local Hint Constructors value plug step0 step hasty : core. Local Hint Constructors value plug step0 step has_ty : core.
(** * Now we adapt the automated proof of type soundness. *) (** * Now we adapt the automated proof of type soundness. *)
@ -110,15 +110,15 @@ Module Stlc.
| [ H : step _ _ |- _ ] => invert H | [ H : step _ _ |- _ ] => invert H
| [ H : step0 _ _ |- _ ] => invert1 H | [ H : step0 _ _ |- _ ] => invert1 H
| [ H : hasty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H | [ H : has_ty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H
| [ H : hasty _ _ _ |- _ ] => invert1 H | [ H : has_ty _ _ _ |- _ ] => invert1 H
| [ H : plug _ _ _ |- _ ] => invert1 H | [ H : plug _ _ _ |- _ ] => invert1 H
end; subst. end; subst.
Ltac t := simplify; propositional; repeat (t0; simplify); try equality; eauto 6. Ltac t := simplify; propositional; repeat (t0; simplify); try equality; eauto 6.
Lemma progress : forall e t, Lemma progress : forall e t,
hasty $0 e t has_ty $0 e t
-> value e -> value e
\/ (exists e' : exp, step e e'). \/ (exists e' : exp, step e e').
Proof. Proof.
@ -137,29 +137,29 @@ Module Stlc.
Local Hint Resolve weakening_override : core. Local Hint Resolve weakening_override : core.
Lemma weakening : forall G e t, Lemma weakening : forall G e t,
hasty G e t has_ty G e t
-> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t) -> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t)
-> hasty G' e t. -> has_ty G' e t.
Proof. Proof.
induct 1; t. induct 1; t.
Qed. Qed.
Local Hint Resolve weakening : core. Local Hint Resolve weakening : core.
Lemma hasty_change : forall G e t, Lemma has_ty_change : forall G e t,
hasty G e t has_ty G e t
-> forall G', G' = G -> forall G', G' = G
-> hasty G' e t. -> has_ty G' e t.
Proof. Proof.
t. t.
Qed. Qed.
Local Hint Resolve hasty_change : core. Local Hint Resolve has_ty_change : core.
Lemma substitution : forall G x t' e t e', Lemma substitution : forall G x t' e t e',
hasty (G $+ (x, t')) e t has_ty (G $+ (x, t')) e t
-> hasty $0 e' t' -> has_ty $0 e' t'
-> hasty G (subst e' x e) t. -> has_ty G (subst e' x e) t.
Proof. Proof.
induct 1; t. induct 1; t.
Qed. Qed.
@ -168,8 +168,8 @@ Module Stlc.
Lemma preservation0 : forall e1 e2, Lemma preservation0 : forall e1 e2,
step0 e1 e2 step0 e1 e2
-> forall t, hasty $0 e1 t -> forall t, has_ty $0 e1 t
-> hasty $0 e2 t. -> has_ty $0 e2 t.
Proof. Proof.
invert 1; t. invert 1; t.
Qed. Qed.
@ -180,8 +180,8 @@ Module Stlc.
plug C e1 e1' plug C e1 e1'
-> forall e2 e2' t, plug C e2 e2' -> forall e2 e2' t, plug C e2 e2'
-> step0 e1 e2 -> step0 e1 e2
-> hasty $0 e1' t -> has_ty $0 e1' t
-> hasty $0 e2' t. -> has_ty $0 e2' t.
Proof. Proof.
induct 1; t. induct 1; t.
Qed. Qed.
@ -190,21 +190,21 @@ Module Stlc.
Lemma preservation : forall e1 e2, Lemma preservation : forall e1 e2,
step e1 e2 step e1 e2
-> forall t, hasty $0 e1 t -> forall t, has_ty $0 e1 t
-> hasty $0 e2 t. -> has_ty $0 e2 t.
Proof. Proof.
invert 1; t. invert 1; t.
Qed. Qed.
Local Hint Resolve progress preservation : core. Local Hint Resolve progress preservation : core.
Theorem safety : forall e t, hasty $0 e t Theorem safety : forall e t, has_ty $0 e t
-> invariantFor (trsys_of e) -> invariantFor (trsys_of e)
(fun e' => value e' (fun e' => value e'
\/ exists e'', step e' e''). \/ exists e'', step e' e'').
Proof. Proof.
simplify. simplify.
apply invariant_weaken with (invariant1 := fun e' => hasty $0 e' t); eauto. apply invariant_weaken with (invariant1 := fun e' => has_ty $0 e' t); eauto.
apply invariant_induction; simplify; eauto; equality. apply invariant_induction; simplify; eauto; equality.
Qed. Qed.
@ -390,33 +390,33 @@ Module StlcPairs.
| Fun (dom ran : type) | Fun (dom ran : type)
| Prod (t1 t2 : type) (* "Prod" for "product," as in Cartesian product *). | Prod (t1 t2 : type) (* "Prod" for "product," as in Cartesian product *).
Inductive hasty : fmap var type -> exp -> type -> Prop := Inductive has_ty : fmap var type -> exp -> type -> Prop :=
| HtVar : forall G x t, | HtVar : forall G x t,
G $? x = Some t G $? x = Some t
-> hasty G (Var x) t -> has_ty G (Var x) t
| HtConst : forall G n, | HtConst : forall G n,
hasty G (Const n) Nat has_ty G (Const n) Nat
| HtPlus : forall G e1 e2, | HtPlus : forall G e1 e2,
hasty G e1 Nat has_ty G e1 Nat
-> hasty G e2 Nat -> has_ty G e2 Nat
-> hasty G (Plus e1 e2) Nat -> has_ty G (Plus e1 e2) Nat
| HtAbs : forall G x e1 t1 t2, | HtAbs : forall G x e1 t1 t2,
hasty (G $+ (x, t1)) e1 t2 has_ty (G $+ (x, t1)) e1 t2
-> hasty G (Abs x e1) (Fun t1 t2) -> has_ty G (Abs x e1) (Fun t1 t2)
| HtApp : forall G e1 e2 t1 t2, | HtApp : forall G e1 e2 t1 t2,
hasty G e1 (Fun t1 t2) has_ty G e1 (Fun t1 t2)
-> hasty G e2 t1 -> has_ty G e2 t1
-> hasty G (App e1 e2) t2 -> has_ty G (App e1 e2) t2
| HtPair : forall G e1 e2 t1 t2, | HtPair : forall G e1 e2 t1 t2,
hasty G e1 t1 has_ty G e1 t1
-> hasty G e2 t2 -> has_ty G e2 t2
-> hasty G (Pair e1 e2) (Prod t1 t2) -> has_ty G (Pair e1 e2) (Prod t1 t2)
| HtFst : forall G e1 t1 t2, | HtFst : forall G e1 t1 t2,
hasty G e1 (Prod t1 t2) has_ty G e1 (Prod t1 t2)
-> hasty G (Fst e1) t1 -> has_ty G (Fst e1) t1
| HtSnd : forall G e1 t1 t2, | HtSnd : forall G e1 t1 t2,
hasty G e1 (Prod t1 t2) has_ty G e1 (Prod t1 t2)
-> hasty G (Snd e1) t2. -> has_ty G (Snd e1) t2.
(* Let's copy and paste the type-soundness proof from above and adapt it. *) (* Let's copy and paste the type-soundness proof from above and adapt it. *)
End StlcPairs. End StlcPairs.
@ -567,46 +567,46 @@ Module StlcSums.
(* New case: *) (* New case: *)
| Sum (t1 t2 : type). | Sum (t1 t2 : type).
Inductive hasty : fmap var type -> exp -> type -> Prop := Inductive has_ty : fmap var type -> exp -> type -> Prop :=
| HtVar : forall G x t, | HtVar : forall G x t,
G $? x = Some t G $? x = Some t
-> hasty G (Var x) t -> has_ty G (Var x) t
| HtConst : forall G n, | HtConst : forall G n,
hasty G (Const n) Nat has_ty G (Const n) Nat
| HtPlus : forall G e1 e2, | HtPlus : forall G e1 e2,
hasty G e1 Nat has_ty G e1 Nat
-> hasty G e2 Nat -> has_ty G e2 Nat
-> hasty G (Plus e1 e2) Nat -> has_ty G (Plus e1 e2) Nat
| HtAbs : forall G x e1 t1 t2, | HtAbs : forall G x e1 t1 t2,
hasty (G $+ (x, t1)) e1 t2 has_ty (G $+ (x, t1)) e1 t2
-> hasty G (Abs x e1) (Fun t1 t2) -> has_ty G (Abs x e1) (Fun t1 t2)
| HtApp : forall G e1 e2 t1 t2, | HtApp : forall G e1 e2 t1 t2,
hasty G e1 (Fun t1 t2) has_ty G e1 (Fun t1 t2)
-> hasty G e2 t1 -> has_ty G e2 t1
-> hasty G (App e1 e2) t2 -> has_ty G (App e1 e2) t2
| HtPair : forall G e1 e2 t1 t2, | HtPair : forall G e1 e2 t1 t2,
hasty G e1 t1 has_ty G e1 t1
-> hasty G e2 t2 -> has_ty G e2 t2
-> hasty G (Pair e1 e2) (Prod t1 t2) -> has_ty G (Pair e1 e2) (Prod t1 t2)
| HtFst : forall G e1 t1 t2, | HtFst : forall G e1 t1 t2,
hasty G e1 (Prod t1 t2) has_ty G e1 (Prod t1 t2)
-> hasty G (Fst e1) t1 -> has_ty G (Fst e1) t1
| HtSnd : forall G e1 t1 t2, | HtSnd : forall G e1 t1 t2,
hasty G e1 (Prod t1 t2) has_ty G e1 (Prod t1 t2)
-> hasty G (Snd e1) t2 -> has_ty G (Snd e1) t2
(* New cases: *) (* New cases: *)
| HtInl : forall G e1 t1 t2, | HtInl : forall G e1 t1 t2,
hasty G e1 t1 has_ty G e1 t1
-> hasty G (Inl e1) (Sum t1 t2) -> has_ty G (Inl e1) (Sum t1 t2)
| HtInr : forall G e1 t1 t2, | HtInr : forall G e1 t1 t2,
hasty G e1 t2 has_ty G e1 t2
-> hasty G (Inr e1) (Sum t1 t2) -> has_ty G (Inr e1) (Sum t1 t2)
| HtMatch : forall G e t1 t2 x1 e1 x2 e2 t, | HtMatch : forall G e t1 t2 x1 e1 x2 e2 t,
hasty G e (Sum t1 t2) has_ty G e (Sum t1 t2)
-> hasty (G $+ (x1, t1)) e1 t -> has_ty (G $+ (x1, t1)) e1 t
-> hasty (G $+ (x2, t2)) e2 t -> has_ty (G $+ (x2, t2)) e2 t
-> hasty G (Match e x1 e1 x2 e2) t. -> has_ty G (Match e x1 e1 x2 e2) t.
(* Type-soundness proof here *) (* Type-soundness proof here *)
End StlcSums. End StlcSums.
@ -777,53 +777,53 @@ Module StlcExceptions.
| Prod (t1 t2 : type) | Prod (t1 t2 : type)
| Sum (t1 t2 : type). | Sum (t1 t2 : type).
Inductive hasty : fmap var type -> exp -> type -> Prop := Inductive has_ty : fmap var type -> exp -> type -> Prop :=
| HtVar : forall G x t, | HtVar : forall G x t,
G $? x = Some t G $? x = Some t
-> hasty G (Var x) t -> has_ty G (Var x) t
| HtConst : forall G n, | HtConst : forall G n,
hasty G (Const n) Nat has_ty G (Const n) Nat
| HtPlus : forall G e1 e2, | HtPlus : forall G e1 e2,
hasty G e1 Nat has_ty G e1 Nat
-> hasty G e2 Nat -> has_ty G e2 Nat
-> hasty G (Plus e1 e2) Nat -> has_ty G (Plus e1 e2) Nat
| HtAbs : forall G x e1 t1 t2, | HtAbs : forall G x e1 t1 t2,
hasty (G $+ (x, t1)) e1 t2 has_ty (G $+ (x, t1)) e1 t2
-> hasty G (Abs x e1) (Fun t1 t2) -> has_ty G (Abs x e1) (Fun t1 t2)
| HtApp : forall G e1 e2 t1 t2, | HtApp : forall G e1 e2 t1 t2,
hasty G e1 (Fun t1 t2) has_ty G e1 (Fun t1 t2)
-> hasty G e2 t1 -> has_ty G e2 t1
-> hasty G (App e1 e2) t2 -> has_ty G (App e1 e2) t2
| HtPair : forall G e1 e2 t1 t2, | HtPair : forall G e1 e2 t1 t2,
hasty G e1 t1 has_ty G e1 t1
-> hasty G e2 t2 -> has_ty G e2 t2
-> hasty G (Pair e1 e2) (Prod t1 t2) -> has_ty G (Pair e1 e2) (Prod t1 t2)
| HtFst : forall G e1 t1 t2, | HtFst : forall G e1 t1 t2,
hasty G e1 (Prod t1 t2) has_ty G e1 (Prod t1 t2)
-> hasty G (Fst e1) t1 -> has_ty G (Fst e1) t1
| HtSnd : forall G e1 t1 t2, | HtSnd : forall G e1 t1 t2,
hasty G e1 (Prod t1 t2) has_ty G e1 (Prod t1 t2)
-> hasty G (Snd e1) t2 -> has_ty G (Snd e1) t2
| HtInl : forall G e1 t1 t2, | HtInl : forall G e1 t1 t2,
hasty G e1 t1 has_ty G e1 t1
-> hasty G (Inl e1) (Sum t1 t2) -> has_ty G (Inl e1) (Sum t1 t2)
| HtInr : forall G e1 t1 t2, | HtInr : forall G e1 t1 t2,
hasty G e1 t2 has_ty G e1 t2
-> hasty G (Inr e1) (Sum t1 t2) -> has_ty G (Inr e1) (Sum t1 t2)
| HtMatch : forall G e t1 t2 x1 e1 x2 e2 t, | HtMatch : forall G e t1 t2 x1 e1 x2 e2 t,
hasty G e (Sum t1 t2) has_ty G e (Sum t1 t2)
-> hasty (G $+ (x1, t1)) e1 t -> has_ty (G $+ (x1, t1)) e1 t
-> hasty (G $+ (x2, t2)) e2 t -> has_ty (G $+ (x2, t2)) e2 t
-> hasty G (Match e x1 e1 x2 e2) t -> has_ty G (Match e x1 e1 x2 e2) t
(* New cases: *) (* New cases: *)
| HtThrow : forall G e1 t, | HtThrow : forall G e1 t,
hasty G e1 Nat has_ty G e1 Nat
-> hasty G (Throw e1) t -> has_ty G (Throw e1) t
| HtCatch : forall G e x1 e1 t, | HtCatch : forall G e x1 e1 t,
hasty G e t has_ty G e t
-> hasty (G $+ (x1, Nat)) e1 t -> has_ty (G $+ (x1, Nat)) e1 t
-> hasty G (Catch e x1 e1) t. -> has_ty G (Catch e x1 e1) t.
End StlcExceptions. End StlcExceptions.
(** * Mutable Variables *) (** * Mutable Variables *)
@ -991,53 +991,53 @@ Module StlcMutable.
(* Now there will be two typing contexts, one for mutable variables and one (* Now there will be two typing contexts, one for mutable variables and one
* for immutable. *) * for immutable. *)
Inductive hasty (M : fmap var type) : fmap var type -> exp -> type -> Prop := Inductive has_ty (M : fmap var type) : fmap var type -> exp -> type -> Prop :=
| HtVar : forall G x t, | HtVar : forall G x t,
G $? x = Some t G $? x = Some t
-> hasty M G (Var x) t -> has_ty M G (Var x) t
| HtConst : forall G n, | HtConst : forall G n,
hasty M G (Const n) Nat has_ty M G (Const n) Nat
| HtPlus : forall G e1 e2, | HtPlus : forall G e1 e2,
hasty M G e1 Nat has_ty M G e1 Nat
-> hasty M G e2 Nat -> has_ty M G e2 Nat
-> hasty M G (Plus e1 e2) Nat -> has_ty M G (Plus e1 e2) Nat
| HtAbs : forall G x e1 t1 t2, | HtAbs : forall G x e1 t1 t2,
hasty M (G $+ (x, t1)) e1 t2 has_ty M (G $+ (x, t1)) e1 t2
-> hasty M G (Abs x e1) (Fun t1 t2) -> has_ty M G (Abs x e1) (Fun t1 t2)
| HtApp : forall G e1 e2 t1 t2, | HtApp : forall G e1 e2 t1 t2,
hasty M G e1 (Fun t1 t2) has_ty M G e1 (Fun t1 t2)
-> hasty M G e2 t1 -> has_ty M G e2 t1
-> hasty M G (App e1 e2) t2 -> has_ty M G (App e1 e2) t2
| HtPair : forall G e1 e2 t1 t2, | HtPair : forall G e1 e2 t1 t2,
hasty M G e1 t1 has_ty M G e1 t1
-> hasty M G e2 t2 -> has_ty M G e2 t2
-> hasty M G (Pair e1 e2) (Prod t1 t2) -> has_ty M G (Pair e1 e2) (Prod t1 t2)
| HtFst : forall G e1 t1 t2, | HtFst : forall G e1 t1 t2,
hasty M G e1 (Prod t1 t2) has_ty M G e1 (Prod t1 t2)
-> hasty M G (Fst e1) t1 -> has_ty M G (Fst e1) t1
| HtSnd : forall G e1 t1 t2, | HtSnd : forall G e1 t1 t2,
hasty M G e1 (Prod t1 t2) has_ty M G e1 (Prod t1 t2)
-> hasty M G (Snd e1) t2 -> has_ty M G (Snd e1) t2
| HtInl : forall G e1 t1 t2, | HtInl : forall G e1 t1 t2,
hasty M G e1 t1 has_ty M G e1 t1
-> hasty M G (Inl e1) (Sum t1 t2) -> has_ty M G (Inl e1) (Sum t1 t2)
| HtInr : forall G e1 t1 t2, | HtInr : forall G e1 t1 t2,
hasty M G e1 t2 has_ty M G e1 t2
-> hasty M G (Inr e1) (Sum t1 t2) -> has_ty M G (Inr e1) (Sum t1 t2)
| HtMatch : forall G e t1 t2 x1 e1 x2 e2 t, | HtMatch : forall G e t1 t2 x1 e1 x2 e2 t,
hasty M G e (Sum t1 t2) has_ty M G e (Sum t1 t2)
-> hasty M (G $+ (x1, t1)) e1 t -> has_ty M (G $+ (x1, t1)) e1 t
-> hasty M (G $+ (x2, t2)) e2 t -> has_ty M (G $+ (x2, t2)) e2 t
-> hasty M G (Match e x1 e1 x2 e2) t -> has_ty M G (Match e x1 e1 x2 e2) t
(* New cases: *) (* New cases: *)
| HtGetVar : forall G x t, | HtGetVar : forall G x t,
M $? x = Some t M $? x = Some t
-> hasty M G (GetVar x) t -> has_ty M G (GetVar x) t
| HtSetVar : forall G x e t, | HtSetVar : forall G x e t,
M $? x = Some t M $? x = Some t
-> hasty M G e t -> has_ty M G e t
-> hasty M G (SetVar x e) t. -> has_ty M G (SetVar x e) t.
End StlcMutable. End StlcMutable.
(** * Concurrency *) (** * Concurrency *)
@ -1218,57 +1218,57 @@ Module StlcConcur.
| Prod (t1 t2 : type) | Prod (t1 t2 : type)
| Sum (t1 t2 : type). | Sum (t1 t2 : type).
Inductive hasty (M : fmap var type) : fmap var type -> exp -> type -> Prop := Inductive has_ty (M : fmap var type) : fmap var type -> exp -> type -> Prop :=
| HtVar : forall G x t, | HtVar : forall G x t,
G $? x = Some t G $? x = Some t
-> hasty M G (Var x) t -> has_ty M G (Var x) t
| HtConst : forall G n, | HtConst : forall G n,
hasty M G (Const n) Nat has_ty M G (Const n) Nat
| HtPlus : forall G e1 e2, | HtPlus : forall G e1 e2,
hasty M G e1 Nat has_ty M G e1 Nat
-> hasty M G e2 Nat -> has_ty M G e2 Nat
-> hasty M G (Plus e1 e2) Nat -> has_ty M G (Plus e1 e2) Nat
| HtAbs : forall G x e1 t1 t2, | HtAbs : forall G x e1 t1 t2,
hasty M (G $+ (x, t1)) e1 t2 has_ty M (G $+ (x, t1)) e1 t2
-> hasty M G (Abs x e1) (Fun t1 t2) -> has_ty M G (Abs x e1) (Fun t1 t2)
| HtApp : forall G e1 e2 t1 t2, | HtApp : forall G e1 e2 t1 t2,
hasty M G e1 (Fun t1 t2) has_ty M G e1 (Fun t1 t2)
-> hasty M G e2 t1 -> has_ty M G e2 t1
-> hasty M G (App e1 e2) t2 -> has_ty M G (App e1 e2) t2
| HtPair : forall G e1 e2 t1 t2, | HtPair : forall G e1 e2 t1 t2,
hasty M G e1 t1 has_ty M G e1 t1
-> hasty M G e2 t2 -> has_ty M G e2 t2
-> hasty M G (Pair e1 e2) (Prod t1 t2) -> has_ty M G (Pair e1 e2) (Prod t1 t2)
| HtFst : forall G e1 t1 t2, | HtFst : forall G e1 t1 t2,
hasty M G e1 (Prod t1 t2) has_ty M G e1 (Prod t1 t2)
-> hasty M G (Fst e1) t1 -> has_ty M G (Fst e1) t1
| HtSnd : forall G e1 t1 t2, | HtSnd : forall G e1 t1 t2,
hasty M G e1 (Prod t1 t2) has_ty M G e1 (Prod t1 t2)
-> hasty M G (Snd e1) t2 -> has_ty M G (Snd e1) t2
| HtInl : forall G e1 t1 t2, | HtInl : forall G e1 t1 t2,
hasty M G e1 t1 has_ty M G e1 t1
-> hasty M G (Inl e1) (Sum t1 t2) -> has_ty M G (Inl e1) (Sum t1 t2)
| HtInr : forall G e1 t1 t2, | HtInr : forall G e1 t1 t2,
hasty M G e1 t2 has_ty M G e1 t2
-> hasty M G (Inr e1) (Sum t1 t2) -> has_ty M G (Inr e1) (Sum t1 t2)
| HtMatch : forall G e t1 t2 x1 e1 x2 e2 t, | HtMatch : forall G e t1 t2 x1 e1 x2 e2 t,
hasty M G e (Sum t1 t2) has_ty M G e (Sum t1 t2)
-> hasty M (G $+ (x1, t1)) e1 t -> has_ty M (G $+ (x1, t1)) e1 t
-> hasty M (G $+ (x2, t2)) e2 t -> has_ty M (G $+ (x2, t2)) e2 t
-> hasty M G (Match e x1 e1 x2 e2) t -> has_ty M G (Match e x1 e1 x2 e2) t
| HtGetVar : forall G x t, | HtGetVar : forall G x t,
M $? x = Some t M $? x = Some t
-> hasty M G (GetVar x) t -> has_ty M G (GetVar x) t
| HtSetVar : forall G x e t, | HtSetVar : forall G x e t,
M $? x = Some t M $? x = Some t
-> hasty M G e t -> has_ty M G e t
-> hasty M G (SetVar x e) t -> has_ty M G (SetVar x e) t
(* New cases: *) (* New cases: *)
| HtPar : forall G e1 t1 e2 t2, | HtPar : forall G e1 t1 e2 t2,
hasty M G e1 t1 has_ty M G e1 t1
-> hasty M G e2 t2 -> has_ty M G e2 t2
-> hasty M G (Par e1 e2) (Prod t1 t2). -> has_ty M G (Par e1 e2) (Prod t1 t2).
(* Type-soundness proof *) (* Type-soundness proof *)
End StlcConcur. End StlcConcur.

110
LambdaCalculusAndTypeSoundness.v
View file

@ -477,25 +477,25 @@ Module Stlc.
* (not to be confused with evaluation contexts) to map free variables to * (not to be confused with evaluation contexts) to map free variables to
* their types. Free variables are those that don't refer to enclosing [Abs] * their types. Free variables are those that don't refer to enclosing [Abs]
* binders. *) * binders. *)
Inductive hasty : fmap var type -> exp -> type -> Prop := Inductive has_ty : fmap var type -> exp -> type -> Prop :=
| HtVar : forall G x t, | HtVar : forall G x t,
G $? x = Some t G $? x = Some t
-> hasty G (Var x) t -> has_ty G (Var x) t
| HtConst : forall G n, | HtConst : forall G n,
hasty G (Const n) Nat has_ty G (Const n) Nat
| HtPlus : forall G e1 e2, | HtPlus : forall G e1 e2,
hasty G e1 Nat has_ty G e1 Nat
-> hasty G e2 Nat -> has_ty G e2 Nat
-> hasty G (Plus e1 e2) Nat -> has_ty G (Plus e1 e2) Nat
| HtAbs : forall G x e1 t1 t2, | HtAbs : forall G x e1 t1 t2,
hasty (G $+ (x, t1)) e1 t2 has_ty (G $+ (x, t1)) e1 t2
-> hasty G (Abs x e1) (Fun t1 t2) -> has_ty G (Abs x e1) (Fun t1 t2)
| HtApp : forall G e1 e2 t1 t2, | HtApp : forall G e1 e2 t1 t2,
hasty G e1 (Fun t1 t2) has_ty G e1 (Fun t1 t2)
-> hasty G e2 t1 -> has_ty G e2 t1
-> hasty G (App e1 e2) t2. -> has_ty G (App e1 e2) t2.
Local Hint Constructors value step hasty : core. Local Hint Constructors value step has_ty : core.
(* Some notation to make it more pleasant to write programs *) (* Some notation to make it more pleasant to write programs *)
Infix "-->" := Fun (at level 60, right associativity). Infix "-->" := Fun (at level 60, right associativity).
@ -507,22 +507,22 @@ Module Stlc.
(* Some examples of typed programs *) (* Some examples of typed programs *)
Example one_plus_one : hasty $0 (1 ^+^ 1) Nat. Example one_plus_one : has_ty $0 (1 ^+^ 1) Nat.
Proof. Proof.
repeat (econstructor; simplify). repeat (econstructor; simplify).
Qed. Qed.
Example add : hasty $0 (\"n", \"m", "n" ^+^ "m") (Nat --> Nat --> Nat). Example add : has_ty $0 (\"n", \"m", "n" ^+^ "m") (Nat --> Nat --> Nat).
Proof. Proof.
repeat (econstructor; simplify). repeat (econstructor; simplify).
Qed. Qed.
Example eleven : hasty $0 ((\"n", \"m", "n" ^+^ "m") @ 7 @ 4) Nat. Example eleven : has_ty $0 ((\"n", \"m", "n" ^+^ "m") @ 7 @ 4) Nat.
Proof. Proof.
repeat (econstructor; simplify). repeat (econstructor; simplify).
Qed. Qed.
Example seven_the_long_way : hasty $0 ((\"x", "x") @ (\"x", "x") @ 7) Nat. Example seven_the_long_way : has_ty $0 ((\"x", "x") @ (\"x", "x") @ 7) Nat.
Proof. Proof.
repeat (econstructor; simplify). repeat (econstructor; simplify).
Qed. Qed.
@ -542,7 +542,7 @@ Module Stlc.
(* Now we're ready for the first of the two key properties to establish that (* Now we're ready for the first of the two key properties to establish that
* invariant: well-typed programs are never stuck. *) * invariant: well-typed programs are never stuck. *)
Lemma progress : forall e t, Lemma progress : forall e t,
hasty $0 e t has_ty $0 e t
-> unstuck e. -> unstuck e.
Proof. Proof.
unfold unstuck; induct 1; simplify; try equality. unfold unstuck; induct 1; simplify; try equality.
@ -556,10 +556,10 @@ Module Stlc.
(* Some automation is needed here to maintain compatibility with (* Some automation is needed here to maintain compatibility with
* name generation in different Coq versions. *) * name generation in different Coq versions. *)
match goal with match goal with
| [ H1 : value e1, H2 : hasty $0 e1 _ |- _ ] => invert H1; invert H2 | [ H1 : value e1, H2 : has_ty $0 e1 _ |- _ ] => invert H1; invert H2
end. end.
match goal with match goal with
| [ H1 : value e2, H2 : hasty $0 e2 _ |- _ ] => invert H1; invert H2 | [ H1 : value e2, H2 : has_ty $0 e2 _ |- _ ] => invert H1; invert H2
end. end.
exists (Const (n + n0)). exists (Const (n + n0)).
constructor. constructor.
@ -596,7 +596,7 @@ Module Stlc.
right. right.
match goal with match goal with
| [ H1 : value e1, H2 : hasty $0 e1 _ |- _ ] => invert H1; invert H2 | [ H1 : value e1, H2 : has_ty $0 e1 _ |- _ ] => invert H1; invert H2
end. end.
exists (subst e2 x e0). exists (subst e2 x e0).
constructor. constructor.
@ -643,9 +643,9 @@ Module Stlc.
(* This lemma lets us transplant a typing derivation into a new context that (* This lemma lets us transplant a typing derivation into a new context that
* includes the old one. *) * includes the old one. *)
Lemma weakening : forall G e t, Lemma weakening : forall G e t,
hasty G e t has_ty G e t
-> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t) -> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t)
-> hasty G' e t. -> has_ty G' e t.
Proof. Proof.
induct 1; simplify. induct 1; simplify.
@ -656,28 +656,28 @@ Module Stlc.
constructor. constructor.
constructor. constructor.
apply IHhasty1. apply IHhas_ty1.
assumption. assumption.
apply IHhasty2. apply IHhas_ty2.
assumption. assumption.
constructor. constructor.
apply IHhasty. apply IHhas_ty.
apply weakening_override. apply weakening_override.
assumption. assumption.
econstructor. econstructor.
apply IHhasty1. apply IHhas_ty1.
assumption. assumption.
apply IHhasty2. apply IHhas_ty2.
assumption. assumption.
Qed. Qed.
(* Replacing a variable with a properly typed term preserves typing. *) (* Replacing a variable with a properly typed term preserves typing. *)
Lemma substitution : forall G x t' e t e', Lemma substitution : forall G x t' e t e',
hasty (G $+ (x, t')) e t has_ty (G $+ (x, t')) e t
-> hasty $0 e' t' -> has_ty $0 e' t'
-> hasty G (subst e' x e) t. -> has_ty G (subst e' x e) t.
Proof. Proof.
induct 1; simplify. induct 1; simplify.
@ -697,8 +697,8 @@ Module Stlc.
constructor. constructor.
constructor. constructor.
eapply IHhasty1; equality. eapply IHhas_ty1; equality.
eapply IHhasty2; equality. eapply IHhas_ty2; equality.
cases (x0 ==v x). cases (x0 ==v x).
@ -715,20 +715,20 @@ Module Stlc.
assumption. assumption.
constructor. constructor.
eapply IHhasty. eapply IHhas_ty.
maps_equal. maps_equal.
assumption. assumption.
econstructor. econstructor.
eapply IHhasty1; equality. eapply IHhas_ty1; equality.
eapply IHhasty2; equality. eapply IHhas_ty2; equality.
Qed. Qed.
(* OK, now we're almost done. Full steps really do preserve typing! *) (* OK, now we're almost done. Full steps really do preserve typing! *)
Lemma preservation : forall e1 e2, Lemma preservation : forall e1 e2,
step e1 e2 step e1 e2
-> forall t, hasty $0 e1 t -> forall t, has_ty $0 e1 t
-> hasty $0 e2 t. -> has_ty $0 e2 t.
Proof. Proof.
induct 1; simplify. induct 1; simplify.
@ -770,7 +770,7 @@ Module Stlc.
* presented from scratch as a proof technique, it turns out that the two key * presented from scratch as a proof technique, it turns out that the two key
* properties, progress and preservation, are just instances of the same methods * properties, progress and preservation, are just instances of the same methods
* we've been applying all along with invariants of transition systems! *) * we've been applying all along with invariants of transition systems! *)
Theorem safety : forall e t, hasty $0 e t Theorem safety : forall e t, has_ty $0 e t
-> invariantFor (trsys_of e) unstuck. -> invariantFor (trsys_of e) unstuck.
Proof. Proof.
simplify. simplify.
@ -778,7 +778,7 @@ Module Stlc.
(* Step 1: strengthen the invariant. In particular, the typing relation is (* Step 1: strengthen the invariant. In particular, the typing relation is
* exactly the right stronger invariant! Our progress theorem proves the * exactly the right stronger invariant! Our progress theorem proves the
* required invariant inclusion. *) * required invariant inclusion. *)
apply invariant_weaken with (invariant1 := fun e' => hasty $0 e' t). apply invariant_weaken with (invariant1 := fun e' => has_ty $0 e' t).
(* Step 2: apply invariant induction, whose induction step turns out to match (* Step 2: apply invariant induction, whose induction step turns out to match
* our preservation theorem exactly! *) * our preservation theorem exactly! *)
@ -805,14 +805,14 @@ Module Stlc.
| [ H : Some _ = Some _ |- _ ] => invert H | [ H : Some _ = Some _ |- _ ] => invert H
| [ H : step _ _ |- _ ] => invert1 H | [ H : step _ _ |- _ ] => invert1 H
| [ H : hasty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H | [ H : has_ty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H
| [ H : hasty _ _ _ |- _ ] => invert1 H | [ H : has_ty _ _ _ |- _ ] => invert1 H
end; subst. end; subst.
Ltac t := simplify; propositional; repeat (t0; simplify); try equality; eauto 6. Ltac t := simplify; propositional; repeat (t0; simplify); try equality; eauto 6.
Lemma progress_snazzy : forall e t, Lemma progress_snazzy : forall e t,
hasty $0 e t has_ty $0 e t
-> value e -> value e
\/ (exists e' : exp, step e e'). \/ (exists e' : exp, step e e').
Proof. Proof.
@ -822,9 +822,9 @@ Module Stlc.
Local Hint Resolve weakening_override : core. Local Hint Resolve weakening_override : core.
Lemma weakening_snazzy : forall G e t, Lemma weakening_snazzy : forall G e t,
hasty G e t has_ty G e t
-> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t) -> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t)
-> hasty G' e t. -> has_ty G' e t.
Proof. Proof.
induct 1; t. induct 1; t.
Qed. Qed.
@ -833,20 +833,20 @@ Module Stlc.
(* Replacing a typing context with an equal one has no effect (useful to guide (* Replacing a typing context with an equal one has no effect (useful to guide
* proof search as a hint). *) * proof search as a hint). *)
Lemma hasty_change : forall G e t, Lemma has_ty_change : forall G e t,
hasty G e t has_ty G e t
-> forall G', G' = G -> forall G', G' = G
-> hasty G' e t. -> has_ty G' e t.
Proof. Proof.
t. t.
Qed. Qed.
Local Hint Resolve hasty_change : core. Local Hint Resolve has_ty_change : core.
Lemma substitution_snazzy : forall G x t' e t e', Lemma substitution_snazzy : forall G x t' e t e',
hasty (G $+ (x, t')) e t has_ty (G $+ (x, t')) e t
-> hasty $0 e' t' -> has_ty $0 e' t'
-> hasty G (subst e' x e) t. -> has_ty G (subst e' x e) t.
Proof. Proof.
induct 1; t. induct 1; t.
Qed. Qed.
@ -855,21 +855,21 @@ Module Stlc.
Lemma preservation_snazzy : forall e1 e2, Lemma preservation_snazzy : forall e1 e2,
step e1 e2 step e1 e2
-> forall t, hasty $0 e1 t -> forall t, has_ty $0 e1 t
-> hasty $0 e2 t. -> has_ty $0 e2 t.
Proof. Proof.
induct 1; t. induct 1; t.
Qed. Qed.
Local Hint Resolve progress_snazzy preservation_snazzy : core. Local Hint Resolve progress_snazzy preservation_snazzy : core.
Theorem safety_snazzy : forall e t, hasty $0 e t Theorem safety_snazzy : forall e t, has_ty $0 e t
-> invariantFor (trsys_of e) -> invariantFor (trsys_of e)
(fun e' => value e' (fun e' => value e'
\/ exists e'', step e' e''). \/ exists e'', step e' e'').
Proof. Proof.
simplify. simplify.
apply invariant_weaken with (invariant1 := fun e' => hasty $0 e' t); eauto. apply invariant_weaken with (invariant1 := fun e' => has_ty $0 e' t); eauto.
apply invariant_induction; simplify; eauto; equality. apply invariant_induction; simplify; eauto; equality.
Qed. Qed.
End Stlc. End Stlc.

50
LambdaCalculusAndTypeSoundness_template.v
View file

@ -419,25 +419,25 @@ Module Stlc.
| Nat (* Numbers *) | Nat (* Numbers *)
| Fun (dom ran : type) (* Functions *). | Fun (dom ran : type) (* Functions *).
Inductive hasty : fmap var type -> exp -> type -> Prop := Inductive has_ty : fmap var type -> exp -> type -> Prop :=
| HtVar : forall G x t, | HtVar : forall G x t,
G $? x = Some t G $? x = Some t
-> hasty G (Var x) t -> has_ty G (Var x) t
| HtConst : forall G n, | HtConst : forall G n,
hasty G (Const n) Nat has_ty G (Const n) Nat
| HtPlus : forall G e1 e2, | HtPlus : forall G e1 e2,
hasty G e1 Nat has_ty G e1 Nat
-> hasty G e2 Nat -> has_ty G e2 Nat
-> hasty G (Plus e1 e2) Nat -> has_ty G (Plus e1 e2) Nat
| HtAbs : forall G x e1 t1 t2, | HtAbs : forall G x e1 t1 t2,
hasty (G $+ (x, t1)) e1 t2 has_ty (G $+ (x, t1)) e1 t2
-> hasty G (Abs x e1) (Fun t1 t2) -> has_ty G (Abs x e1) (Fun t1 t2)
| HtApp : forall G e1 e2 t1 t2, | HtApp : forall G e1 e2 t1 t2,
hasty G e1 (Fun t1 t2) has_ty G e1 (Fun t1 t2)
-> hasty G e2 t1 -> has_ty G e2 t1
-> hasty G (App e1 e2) t2. -> has_ty G (App e1 e2) t2.
Local Hint Constructors value step hasty : core. Local Hint Constructors value step has_ty : core.
(* Some notation to make it more pleasant to write programs *) (* Some notation to make it more pleasant to write programs *)
Infix "-->" := Fun (at level 60, right associativity). Infix "-->" := Fun (at level 60, right associativity).
@ -449,22 +449,22 @@ Module Stlc.
(* Some examples of typed programs *) (* Some examples of typed programs *)
Example one_plus_one : hasty $0 (1 ^+^ 1) Nat. Example one_plus_one : has_ty $0 (1 ^+^ 1) Nat.
Proof. Proof.
repeat (econstructor; simplify). repeat (econstructor; simplify).
Qed. Qed.
Example add : hasty $0 (\"n", \"m", "n" ^+^ "m") (Nat --> Nat --> Nat). Example add : has_ty $0 (\"n", \"m", "n" ^+^ "m") (Nat --> Nat --> Nat).
Proof. Proof.
repeat (econstructor; simplify). repeat (econstructor; simplify).
Qed. Qed.
Example eleven : hasty $0 ((\"n", \"m", "n" ^+^ "m") @ 7 @ 4) Nat. Example eleven : has_ty $0 ((\"n", \"m", "n" ^+^ "m") @ 7 @ 4) Nat.
Proof. Proof.
repeat (econstructor; simplify). repeat (econstructor; simplify).
Qed. Qed.
Example seven_the_long_way : hasty $0 ((\"x", "x") @ (\"x", "x") @ 7) Nat. Example seven_the_long_way : has_ty $0 ((\"x", "x") @ (\"x", "x") @ 7) Nat.
Proof. Proof.
repeat (econstructor; simplify). repeat (econstructor; simplify).
Qed. Qed.
@ -476,7 +476,7 @@ Module Stlc.
\/ (exists e' : exp, step e e'). \/ (exists e' : exp, step e e').
Lemma progress : forall e t, Lemma progress : forall e t,
hasty $0 e t has_ty $0 e t
-> value e -> value e
\/ (exists e' : exp, step e e'). \/ (exists e' : exp, step e e').
Proof. Proof.
@ -484,23 +484,23 @@ Module Stlc.
(* Replacing a typing context with an equal one has no effect (useful to guide (* Replacing a typing context with an equal one has no effect (useful to guide
* proof search as a hint). *) * proof search as a hint). *)
Lemma hasty_change : forall G e t, Lemma has_ty_change : forall G e t,
hasty G e t has_ty G e t
-> forall G', G' = G -> forall G', G' = G
-> hasty G' e t. -> has_ty G' e t.
Proof. Proof.
Admitted. Admitted.
Local Hint Resolve hasty_change : core. Local Hint Resolve has_ty_change : core.
Lemma preservation : forall e1 e2, Lemma preservation : forall e1 e2,
step e1 e2 step e1 e2
-> forall t, hasty $0 e1 t -> forall t, has_ty $0 e1 t
-> hasty $0 e2 t. -> has_ty $0 e2 t.
Proof. Proof.
Admitted. Admitted.
Theorem safety : forall e t, hasty $0 e t Theorem safety : forall e t, has_ty $0 e t
-> invariantFor (trsys_of e) unstuck. -> invariantFor (trsys_of e) unstuck.
Proof. Proof.
simplify. simplify.
@ -508,7 +508,7 @@ Module Stlc.
(* Step 1: strengthen the invariant. In particular, the typing relation is (* Step 1: strengthen the invariant. In particular, the typing relation is
* exactly the right stronger invariant! Our progress theorem proves the * exactly the right stronger invariant! Our progress theorem proves the
* required invariant inclusion. *) * required invariant inclusion. *)
apply invariant_weaken with (invariant1 := fun e' => hasty $0 e' t). apply invariant_weaken with (invariant1 := fun e' => has_ty $0 e' t).
(* Step 2: apply invariant induction, whose induction step turns out to match (* Step 2: apply invariant induction, whose induction step turns out to match
* our preservation theorem exactly! *) * our preservation theorem exactly! *)