Compare commits

..

8 Commits

@ -15,8 +15,19 @@ theories/lib/sets.v
# STLC
theories/type_systems/stlc/lang.v
theories/type_systems/stlc/notation.v
theories/type_systems/stlc/untyped.v
theories/type_systems/stlc/types.v
# Extended STLC
theories/type_systems/stlc_extended/lang.v
theories/type_systems/stlc_extended/notation.v
theories/type_systems/stlc_extended/types.v
theories/type_systems/stlc_extended/bigstep.v
theories/type_systems/stlc_extended/ctxstep.v
# By removing the # below, you can add the exercise sheets to make
theories/type_systems/warmup/warmup.v
#theories/type_systems/warmup/warmup_sol.v
#theories/type_systems/stlc/exercises01.v
theories/type_systems/stlc/exercises01.v
#theories/type_systems/stlc/exercises01_sol.v
theories/type_systems/stlc/exercises02.v

@ -68,13 +68,15 @@ Proof.
| e_l e_l' e_r H_val H_l_step IH
| e_l e_r e_r' H_r_step IH
]; subst.
all: intros e' H_step'; inversion H_step'; subst; try val_no_step.
- reflexivity.
- by rewrite (IH e1').
- by rewrite (IH e2').
- reflexivity.
- by rewrite (IH e1').
- by rewrite (IH e2').
all: intros e' H_step'; inversion H_step' as [
|
_tmp e_ind |
_tmp1 _tmp2 e_ind |
|
_tmp e_ind |
_tmp1 _tmp2 e_ind
]; subst; intuition try val_no_step.
all: by rewrite (IH e_ind).
Qed.
(** Exercise 3 (LN Exercise 2): Call-by-name Semantics *)

@ -0,0 +1,429 @@
From stdpp Require Import gmap base relations tactics.
From iris Require Import prelude.
From semantics.ts.stlc Require Import lang notation.
(** Exercise 2 (LN Exercise 1): Deterministic Operational Semantics *)
Lemma val_no_step e e':
step e e' is_val e False.
Proof.
by destruct 1.
Qed.
(* Note how the above lemma is another way to phrase the statement "values
* cannot step" that doesn't need inversion. It can also be used to prove the
* phrasing we had to use inversion for in the lecture: *)
Lemma val_no_step' (v : val) (e : expr) :
step v e -> False.
Proof.
intros H. eapply val_no_step; first eassumption.
apply is_val_val.
Qed.
(* You might find the following tactic useful,
which derives a contradiction when you have a [step e1 e2] assumption and
[e1] is a value.
Example:
H1: step e e'
H2: is_val e
=====================
???
Then [val_no_step.] will solve the goal by applying the [val_no_step] lemma.
(We neither expect you to understand how exactly the tactic does this nor to
be able to write such a tactic yourself. Where useful, we will always
provide you with custom tactics and explain in a comment what they do.) *)
Ltac val_no_step :=
match goal with
| [H: step ?e1 ?e2 |- _] =>
solve [exfalso; eapply (val_no_step _ _ H); done]
end.
Lemma step_det e e' e'':
step e e' step e e'' e' = e''.
Proof.
induction 1 in e'' |-*; inversion 1; subst; eauto.
all: try val_no_step || naive_solver.
Qed.
(** Exercise 3 (LN Exercise 2): Call-by-name Semantics *)
Inductive cbn_step : expr expr Prop :=
| CBNStepBeta x e e' :
cbn_step (App (Lam x e) e') (subst' x e' e)
| CBNStepAppL e1 e1' e2 :
cbn_step e1 e1'
cbn_step (App e1 e2) (App e1' e2)
| CBNStepPlusRed (n1 n2 n3: Z) :
(n1 + n2)%Z = n3
cbn_step (Plus (LitInt n1) (LitInt n2)) (LitInt n3)
| CBNStepPlusL e1 e1' e2 :
is_val e2
cbn_step e1 e1'
cbn_step (Plus e1 e2) (Plus e1' e2)
| CBNStepPlusR e1 e2 e2' :
cbn_step e2 e2'
cbn_step (Plus e1 e2) (Plus e1 e2').
(* We make the eauto tactic aware of the constructors of cbn_step *)
#[global] Hint Constructors cbn_step : core.
Lemma different_results :
(e: expr) (e1 e2: expr), rtc cbn_step e e1 rtc step e e2 is_val e1 is_val e2 e1 e2.
Proof.
exists ((λ: "x" "y", "x") (4 + 1))%E.
do 2 eexists.
repeat split.
- econstructor 2. econstructor. simpl. reflexivity.
- econstructor 2. eauto.
econstructor 2. econstructor; simpl; done.
reflexivity.
- done.
- done.
- intros ?. injection H as Heq. discriminate Heq.
Qed.
Lemma val_no_cbn_step e e':
cbn_step e e' is_val e False.
Proof.
destruct e; try naive_solver; inversion 1.
Qed.
(* Same tactic as [val_no_step] but for cbn_step.*)
Ltac val_no_cbn_step :=
match goal with
| [H: cbn_step ?e1 ?e2 |- _] =>
solve [exfalso; eapply (val_no_cbn_step _ _ H); done]
end.
Lemma cbn_step_det e e' e'':
cbn_step e e' cbn_step e e'' e' = e''.
Proof.
induction 1 in e'' |-*; inversion 1; subst; eauto.
all: try val_no_cbn_step || naive_solver.
Qed.
(** Exercise 4 (LN Exercise 3): Reflexive Transitive Closure *)
Section rtc.
Context {X : Type}.
Inductive rtc (R : X X Prop) : X X Prop :=
| rtc_base x : rtc R x x
| rtc_step x y z : R x y rtc R y z rtc R x z.
Lemma rtc_reflexive R : Reflexive (rtc R).
Proof.
unfold Reflexive.
intros x. constructor.
Qed.
Lemma rtc_transitive R : Transitive (rtc R).
Proof.
unfold Transitive.
intros x y z HR1 HR2. induction HR1 as [ | ??? HR HR1 IH].
- apply HR2.
- econstructor.
+ apply HR.
+ apply IH; done.
Qed.
Lemma rtc_subrel (R: X X Prop) (x y : X): R x y rtc R x y.
Proof.
intros ?. econstructor.
- done.
- eapply rtc_reflexive.
Qed.
Section typeclass.
(* We can use Coq's typeclass mechanism to enable the use of the [transitivity] and [reflexivity] tactics on our goals.
Typeclasses enable easy extensions of existing mechanisms -- in this case, by telling Coq to use the knowledge about our definition of [rtc].
*)
(* [Transitive] is a typeclass. With [Instance] we provide an instance of it. *)
Global Instance rtc_transitive_inst R : Transitive (rtc R).
Proof.
apply rtc_transitive.
Qed.
Global Instance rtc_reflexive_inst R : Reflexive (rtc R).
Proof.
apply rtc_reflexive.
Qed.
End typeclass.
End rtc.
(* Let's put this to the test! *)
Goal rtc step (LitInt 42) (LitInt 42).
Proof.
(* this uses the [rtc_reflexive_inst] instance we registered. *)
reflexivity.
Qed.
Goal rtc step (LitInt 32 + (LitInt 5 + LitInt 5)%E)%E (LitInt 42).
Proof.
(* this uses the [rtc_transitive_inst] instance we registered. *)
etransitivity.
+ eapply rtc_step; eauto. reflexivity.
+ eapply rtc_step; eauto. reflexivity.
Qed.
Section stdpp.
(* In fact, [rtc] is so common that it is already provided by the [stdpp] library! *)
Import stdpp.relations.
(* The typeclass instances are also already registered. *)
Goal rtc step (LitInt 42) (LitInt 42).
Proof. reflexivity. Qed.
End stdpp.
(* Start by proving these lemmas. Understand why they are useful. *)
Lemma plus_right e1 e2 e2':
rtc step e2 e2' rtc step (Plus e1 e2) (Plus e1 e2').
Proof.
induction 1.
- done.
- econstructor.
+ econstructor 6. done.
+ done.
Qed.
Lemma plus_left e1 e1' n:
rtc step e1 e1' rtc step (Plus e1 (LitInt n)) (Plus e1' (LitInt n)).
Proof.
induction 1.
- done.
- econstructor.
+ econstructor. all: done.
+ done.
Qed.
(* The exercise: *)
Lemma plus_to_consts e1 e2 n m:
rtc step e1 (LitInt n) rtc step e2 (LitInt m) rtc step (e1 + e2)%E (LitInt (n + m)%Z).
Proof.
intros H1 H2. etransitivity.
- eapply plus_right. done.
- etransitivity.
+ eapply plus_left. done.
+ eapply rtc_subrel. econstructor. done.
Qed.
(* Now that you have an understanding of how rtc works, we can make eauto aware of it. *)
#[local] Hint Constructors rtc : core.
(* See its power here: *)
Lemma plus_right_eauto e1 e2 e2':
rtc step e2 e2' rtc step (Plus e1 e2) (Plus e1 e2').
Proof.
induction 1; eauto.
Abort.
(** Exercise 5 (LN Exercise 4): Big-step vs small-step semantics *)
(* We first prove a lemma for each of the interesting cases: *)
Lemma rtc_step_app_l e1 e1' e2:
rtc step e1 e1' is_val e2 rtc step (App e1 e2) (App e1' e2).
Proof.
induction 1; eauto.
Qed.
Lemma rtc_step_app_r e1 e2 e2':
rtc step e2 e2' rtc step (App e1 e2) (App e1 e2').
Proof.
induction 1; eauto.
Qed.
Lemma rtc_step_plus_l e1 e1' e2:
rtc step e1 e1' is_val e2 rtc step (Plus e1 e2) (Plus e1' e2).
Proof.
induction 1; eauto.
Qed.
Lemma rtc_step_plus_r e1 e2 e2':
rtc step e2 e2' rtc step (Plus e1 e2) (Plus e1 e2').
Proof.
induction 1; eauto.
Qed.
Lemma big_step_steps e v :
big_step e v rtc step e (of_val v).
Proof.
induction 1 as [ | | e1 e2 v1 v2 H1 IH1 H2 IH2 | e1 e2 x e v2 v H1 IH1 H2 IH2 H3 IH3].
- constructor.
- constructor.
- etransitivity. eapply rtc_step_plus_r; eauto.
etransitivity. eapply rtc_step_plus_l; eauto.
econstructor 2. apply StepPlusRed; done. done.
- etransitivity. eapply rtc_step_app_r; eauto.
etransitivity. eapply rtc_step_app_l; eauto.
econstructor 2. simpl. econstructor. eauto.
done.
Qed.
(* Again, we will first prove some lemmas: *)
Lemma single_step_big_step_cons e (v : val) :
step e v -> big_step e v.
Proof.
intros H.
inversion H as [x e1 e2 He2 Heq1 Heq| | |n1 n2 n3 Heq1 Heq2 Heq| |]; subst.
2-3,5-6: try (destruct v; discriminate).
- apply is_val_spec in He2 as [v' <-%of_to_val].
econstructor.
+ eauto.
+ apply big_step_vals.
+ rewrite Heq. apply big_step_vals.
- destruct v.
+ injection Heq as <-. repeat constructor.
+ exfalso. discriminate Heq.
Qed.
Lemma step_big_step_cons e e' v :
step e e' big_step e' v big_step e v.
Proof.
induction 1 in v |- *.
- eapply is_val_spec in H as [w <-%of_to_val].
intros Hbig. econstructor; eauto using big_step_vals.
- inversion 1; subst; eauto.
- inversion 1; subst; eauto.
- inversion 1; subst. eauto.
- inversion 1; subst; eauto.
- inversion 1; subst; eauto.
Restart.
(* we can also show this by induction on big_step e' v instead. However, this
* turns out to be more ugly. Both base cases are by the lemma we showed before. *)
intros Hsmall Hbig.
induction Hbig in Hsmall, e |-*. (* with Hsmall and e quantified *)
- apply single_step_big_step_cons, Hsmall.
- apply single_step_big_step_cons, Hsmall.
- inversion Hsmall as [x e3 e4 He4 Heq1 Heq| | | | | ]; subst.
+ apply is_val_spec in He4 as [v' <-%of_to_val].
econstructor. 1-2: eauto using big_step_vals.
rewrite Heq. eauto.
+ eauto.
+ eauto.
- inversion Hsmall as [x' e3 e4 He4 Htemp Heq| | | | | ]; subst.
+ apply is_val_spec in He4 as [v' <-%of_to_val].
econstructor. 1-2: eauto using big_step_vals.
rewrite Heq. eauto.
+ eauto.
+ eauto.
Qed.
Lemma steps_big_step_cons e e' w:
rtc step e e' big_step e' w big_step e w.
Proof.
induction 1; eauto using step_big_step_cons.
Qed.
Lemma steps_big_step e (v: val):
rtc step e v big_step e v.
Proof.
(* Note how there is a coercion (automatic conversion) hidden in the
* statement of this lemma: *)
Set Printing Coercions.
(* It is sometimes very useful to temporarily print coercions if rewrites or
* destructs do not behave as expected. *)
Unset Printing Coercions.
intros Hsteps. eapply steps_big_step_cons; eauto using big_step_vals.
Qed.
(** Exercise 6 (LN Exercise 5): left-to-right evaluation *)
Inductive ltr_step : expr expr Prop := | LTRStepBeta x e e' :
is_val e'
ltr_step (App (Lam x e) e') (subst' x e' e)
| LTRStepAppL e1 e1' e2 :
ltr_step e1 e1'
ltr_step (App e1 e2) (App e1' e2)
| LTRStepAppR e1 e2 e2' :
ltr_step e2 e2'
is_val e1
ltr_step (App e1 e2) (App e1 e2')
| LTRStepPlusRed (n1 n2 n3: Z) :
(n1 + n2)%Z = n3
ltr_step (Plus (LitInt n1) (LitInt n2)) (LitInt n3)
| LTRStepPlusL e1 e1' e2 :
ltr_step e1 e1'
ltr_step (Plus e1 e2) (Plus e1' e2)
| LTRStepPlusR e1 e2 e2' :
is_val e1
ltr_step e2 e2'
ltr_step (Plus e1 e2) (Plus e1 e2').
#[global] Hint Constructors ltr_step : core.
Lemma different_steps_ltr_step :
(e: expr) (e1 e2: expr), ltr_step e e1 step e e2 e1 e2.
Proof.
exists ((4 + 1) + (4 + 1))%E.
do 2 eexists.
repeat split.
- econstructor 5. econstructor. done.
- econstructor 6. econstructor. done.
- intros Heq. injection Heq as Heq. discriminate Heq.
Qed.
Lemma rtc_ltr_step_app_l e1 e1' e2:
rtc ltr_step e1 e1' rtc ltr_step (App e1 e2) (App e1' e2).
Proof.
induction 1; eauto.
Qed.
Lemma rtc_ltr_step_app_r e1 e2 e2':
rtc ltr_step e2 e2' is_val e1 rtc ltr_step (App e1 e2) (App e1 e2').
Proof.
induction 1; eauto.
Qed.
Lemma rtc_ltr_step_plus_l e1 e1' e2:
rtc ltr_step e1 e1' rtc ltr_step (Plus e1 e2) (Plus e1' e2).
Proof.
induction 1; eauto.
Qed.
Lemma rtc_ltr_step_plus_r e1 e2 e2':
rtc ltr_step e2 e2' is_val e1 rtc ltr_step (Plus e1 e2) (Plus e1 e2').
Proof.
induction 1; eauto.
Qed.
Lemma big_step_ltr_steps e v :
big_step e v rtc ltr_step e (of_val v).
Proof.
induction 1 as [ | | e1 e2 v1 v2 H1 IH1 H2 IH2 | e1 e2 x e v2 v H1 IH1 H2 IH2 H3 IH3].
- constructor.
- constructor.
- etransitivity. eapply rtc_ltr_step_plus_l; eauto.
etransitivity. eapply rtc_ltr_step_plus_r; eauto.
econstructor 2. econstructor; done. done.
- etransitivity. eapply rtc_ltr_step_app_l; eauto.
etransitivity. eapply rtc_ltr_step_app_r; eauto.
econstructor 2. simpl. econstructor. eauto.
done.
Qed.
Lemma ltr_step_big_step_cons e e' v :
ltr_step e e' big_step e' v big_step e v.
Proof.
induction 1 in v |-*.
- eapply is_val_spec in H as [w H].
eapply of_to_val in H. subst.
intros Hbig. econstructor; eauto using big_step_vals.
- inversion 1; subst; eauto.
- inversion 1; subst; eauto.
- inversion 1; subst. eauto.
- inversion 1; subst; eauto.
- inversion 1; subst; eauto.
Qed.
Lemma ltr_steps_big_step_cons e e' w:
rtc ltr_step e e' big_step e' w big_step e w.
Proof.
induction 1; eauto using ltr_step_big_step_cons.
Qed.
Lemma ltr_steps_big_step e (v: val):
rtc ltr_step e v big_step e v.
Proof.
intros Hsteps. eapply ltr_steps_big_step_cons; eauto using big_step_vals.
Qed.

@ -0,0 +1,575 @@
From stdpp Require Import gmap base relations tactics.
From iris Require Import prelude.
From semantics.ts.stlc Require Import lang notation.
From semantics.ts.stlc Require untyped types.
(** README: Please also download the assigment sheet as a *.pdf from here:
https://cms.sic.saarland/semantics_ws2324/materials/
It contains additional explanation and excercises. **)
(** ** Exercise 1: Prove that the structural and contextual semantics are equivalent. *)
(** You will find it very helpful to separately derive the structural rules of the
structural semantics for the contextual semantics. *)
Ltac ectx_step K :=
eapply (Ectx_step _ _ K); subst; eauto.
Lemma contextual_step_beta x e e':
is_val e' contextual_step ((λ: x, e) e') (subst' x e' e).
Proof.
intro H_val.
ectx_step HoleCtx.
Qed.
Lemma contextual_step_app_r (e1 e2 e2': expr) :
contextual_step e2 e2'
contextual_step (e1 e2) (e1 e2').
Proof.
intro H_step.
inversion H_step.
induction K eqn:H_K.
(* I am a smart foxxo >:3 *)
all: ectx_step (AppRCtx e1 K).
Qed.
Ltac is_val_to_val v H :=
rewrite (is_val_spec _) in H; destruct H as [v H]; apply of_to_val in H; symmetry in H.
Lemma contextual_step_app_l (e1 e1' e2: expr) :
is_val e2
contextual_step e1 e1'
contextual_step (e1 e2) (e1' e2).
Proof.
intros H_val H_step.
is_val_to_val v H_val.
subst.
inversion H_step.
induction K eqn:H_K.
all: ectx_step (AppLCtx K v).
Qed.
Lemma contextual_step_plus_red (n1 n2 n3: Z) :
(n1 + n2)%Z = n3
contextual_step (n1 + n2)%E n3.
Proof.
intro H_plus.
ectx_step HoleCtx.
Qed.
Lemma contextual_step_plus_r e1 e2 e2' :
contextual_step e2 e2'
contextual_step (Plus e1 e2) (Plus e1 e2').
Proof.
intro H_step.
inversion H_step.
ectx_step (PlusRCtx e1 K).
Qed.
Lemma contextual_step_plus_l e1 e1' e2 :
is_val e2
contextual_step e1 e1'
contextual_step (Plus e1 e2) (Plus e1' e2).
Proof.
intro H_val.
is_val_to_val v H_val.
intro H_step.
inversion H_step.
ectx_step (PlusLCtx K v).
Qed.
(** We register these lemmas as hints for [eauto]. *)
#[global]
Hint Resolve contextual_step_beta contextual_step_app_l contextual_step_app_r contextual_step_plus_red contextual_step_plus_l contextual_step_plus_r : core.
Ltac step_ind H := induction H as [
name e_λ e_v
| e_fn e_fn' e_v H_val H_fn_step IH
| e_fn e_arg e_arg' H_arg_step IH
| n1 n2 n_sum H_plus
| e_l e_l' e_r H_val H_l_step IH
| e_l e_r e_r' H_r_step IH
].
Lemma step_contextual_step e1 e2: step e1 e2 contextual_step e1 e2.
Proof.
intro H_step.
step_ind H_step; eauto.
Qed.
(** Now the other direction. *)
(* You may find it helpful to introduce intermediate lemmas. *)
Lemma contextual_step_step e1 e2:
contextual_step e1 e2 step e1 e2.
Proof.
intro H_cstep.
inversion H_cstep as [K e1' e2' H_eq1 H_eq2 H_bstep]; subst.
inversion H_bstep as [
name body arg H_val H_eq1 H_eq2 H_eq3
| e1 e2 n1 n2 n_sum H_n1 H_n2 H_sum H_eq1 H_eq2
]; subst.
(*
Here we do an induction on K, and we let eauto solve it for us.
In practice, each case of the induction on K can be solved quite easily,
as the induction hypothesis has us prove a `contextual_step`, for which we have plenty of useful lemmas.
*)
all: induction K; unfold fill; eauto.
Qed.
(** ** Exercise 2: Scott encodings *)
Section scott.
(* take a look at untyped.v for usefull lemmas and definitions *)
Import semantics.ts.stlc.untyped.
(** Scott encoding of Booleans *)
Definition true_scott : val := (λ: "t" "f", "t").
Definition false_scott : val := (λ: "t" "f", "f").
(* Lemma steps_beta e_λ e_arg *)
Ltac rtc_single step_cons := eapply rtc_l; last reflexivity; eapply step_cons; auto.
Lemma true_red (v1 v2 : val) :
closed [] v1
closed [] v2
rtc step (true_scott v1 v2) v1.
Proof.
intros H_cl1 H_cl2.
unfold true_scott.
etransitivity.
eapply steps_app_l; auto.
rtc_single StepBeta.
simpl.
etransitivity.
rtc_single StepBeta.
simpl.
rewrite subst_closed_nil; auto.
reflexivity.
Qed.
Lemma steps_plus_r (e1 e2 e2': expr) :
rtc step e2 e2' rtc step (e1 + e2)%E (e1 + e2')%E.
Proof.
induction 1; subst.
reflexivity.
etransitivity; last exact IHrtc.
rtc_single StepPlusR.
Qed.
Lemma steps_plus_l (e1 e1' e2: expr) :
is_val e2
rtc step e1 e1'
rtc step (e1 + e2)%E (e1' + e2)%E.
Proof.
induction 2; subst.
reflexivity.
etransitivity; last exact IHrtc.
rtc_single StepPlusL.
Qed.
Lemma lam_is_val name e_body :
is_val (Lam name e_body).
Proof.
unfold is_val.
intuition.
Qed.
Lemma int_is_val n :
is_val (LitInt n).
Proof.
unfold is_val.
intuition.
Qed.
Hint Resolve lam_is_val int_is_val: core.
(* TODO: recursively traverse the goal for subst instances? *)
Ltac auto_subst :=
(rewrite subst_closed_nil; last assumption) ||
(unfold subst'; unfold subst; simpl; fold subst).
(* This is ridiculously powerful, although it only works when you know all the terms *)
Ltac auto_step :=
match goal with
| [ |- rtc step (App ?e_l ?e_v) ?e_target ] =>
etransitivity;
first eapply steps_app_r;
first auto_step;
simpl;
etransitivity;
first eapply steps_app_l;
first auto;
first auto_step;
simpl;
repeat auto_subst;
rtc_single StepBeta;
simpl;
done
| [ |- rtc step (of_val ?v) ?e_target ] => reflexivity
| [ |- rtc step (Lam ?name ?body) ?e_target ] => reflexivity
| [ |- rtc step (LitInt ?n) ?e_target ] => reflexivity
| [ |- rtc step (Plus ?e1 ?e2) ?e_target ] =>
etransitivity;
first eapply steps_plus_r;
first auto_step;
etransitivity;
first eapply steps_plus_l;
first auto;
first auto_step;
rtc_single StepPlusRed;
done
| [ |- rtc step (subst ?var ?thing) ?e_target ] =>
repeat auto_subst;
auto_step
end
.
Ltac multi_step :=
repeat (reflexivity || (
etransitivity;
first auto_step;
first repeat auto_subst
)).
Lemma false_red (v1 v2 : val) :
closed [] v1
closed [] v2
rtc step (false_scott v1 v2) v2.
Proof.
intros H_cl1 H_cl2.
auto_step.
Qed.
(** Scott encoding of Pairs *)
Definition pair_scott : val := (λ: "lhs" "rhs" "f", ("f" "lhs" "rhs")).
Definition fst_scott : val := (λ: "pair", ("pair" (λ: "lhs" "rhs", "lhs"))).
Definition snd_scott : val := (λ: "pair", ("pair" (λ: "lhs" "rhs", "rhs"))).
Lemma fst_red (v1 v2 : val) :
is_closed [] v1
is_closed [] v2
rtc step (fst_scott (pair_scott v1 v2)) v1.
Proof.
intros H_cl1 H_cl2.
multi_step.
Qed.
Lemma snd_red (v1 v2 : val) :
is_closed [] v1
is_closed [] v2
rtc step (snd_scott (pair_scott v1 v2)) v2.
Proof.
intros H_cl1 H_cl2.
multi_step.
Qed.
End scott.
Import semantics.ts.stlc.types.
(** ** Exercise 3: type erasure *)
(** Source terms *)
Inductive src_expr :=
| ELitInt (n: Z)
(* Base lambda calculus *)
| EVar (x : string)
| ELam (x : binder) (A: type) (e : src_expr)
| EApp (e1 e2 : src_expr)
(* Base types and their operations *)
| EPlus (e1 e2 : src_expr).
(** The erasure function *)
Fixpoint erase (E: src_expr) : expr :=
match E with
| ELitInt n => LitInt n
| EVar x => Var x
| ELam x A e => Lam x (erase e)
| EApp e1 e2 => App (erase e1) (erase e2)
| EPlus e1 e2 => Plus (erase e1) (erase e2)
end.
Reserved Notation "Γ '⊢S' e : A" (at level 74, e, A at next level).
Inductive src_typed : typing_context src_expr type Prop :=
| src_typed_var Γ x A :
Γ !! x = Some A
Γ S (EVar x) : A
| src_typed_lam Γ x E A B :
(<[ x := A]> Γ) S E : B
Γ S (ELam (BNamed x) A E) : (A B)
| src_typed_int Γ z :
Γ S (ELitInt z) : Int
| src_typed_app Γ E1 E2 A B :
Γ S E1 : (A B)
Γ S E2 : A
Γ S EApp E1 E2 : B
| src_typed_add Γ E1 E2 :
Γ S E1 : Int
Γ S E2 : Int
Γ S EPlus E1 E2 : Int
where "Γ '⊢S' E : A" := (src_typed Γ E%E A%ty) : FType_scope.
#[export] Hint Constructors src_typed : core.
Lemma type_erasure_correctness Γ E A:
(Γ S E : A)%ty (Γ erase E : A)%ty.
Proof.
intro H_styped.
induction H_styped; unfold erase; eauto.
Qed.
(** ** Exercise 4: Unique Typing *)
Lemma src_typing_unique Γ E A B:
(Γ S E : A)%ty (Γ S E : B)%ty A = B.
Proof.
intro H_typed.
revert B.
induction H_typed as [
Γ x A H_x_ty
| Γ x e_body A1 A2 H_body_ty IH
| Γ n
| Γ e_fn e_arg A1 A2 H_fn_ty H_arg_ty IH
| Γ e1 e2 H_e1_ty H_e2_ty
]; intro B; intro H_typed'.
all: inversion H_typed' as [
Γ' y B' H_y_ty
| Γ' y e_body' B1 B2 H_body_ty'
| Γ' n'
| Γ' e_fn' e_arg' B1 B2 H_fn_ty' H_arg_ty'
| Γ' e3 e4 H_e3_ty H_e4_ty
]; subst; try auto.
- rewrite H_y_ty in H_x_ty; injection H_x_ty.
intuition.
- rewrite (IH B2); eauto.
- remember (H_arg_ty _ H_fn_ty') as H_eq.
injection H_eq.
intuition.
Qed.
Lemma syn_typing_not_unique:
(Γ: typing_context) (e: expr) (A B: type),
(Γ e: A)%ty (Γ e: B)%ty A B.
Proof.
exists .
exists (λ: "x", "x")%E.
exists (Int Int)%ty.
exists ((Int Int) (Int Int))%ty.
repeat split.
3: discriminate.
all: apply typed_lam; eauto.
Qed.
(** ** Exercise 5: Type Inference *)
Fixpoint type_eq A B :=
match A, B with
| Int, Int => true
| Fun A B, Fun A' B' => type_eq A A' && type_eq B B'
| _, _ => false
end.
Lemma type_eq_iff A B: type_eq A B A = B.
Proof.
induction A in B |-*; destruct B; simpl; naive_solver.
Qed.
Notation ctx := (gmap string type).
Fixpoint infer_type (Γ: ctx) E :=
match E with
| EVar x => Γ !! x
| ELam (BNamed x) A E =>
match infer_type (<[x := A]> Γ) E with
| Some B => Some (Fun A B)
| None => None
end
(* TODO: complete the definition for the remaining cases *)
| ELitInt l => Some (Int) (* TODO *)
| EApp E1 E2 => match infer_type Γ E1, infer_type Γ E2 with
| Some (Fun A B), Some A' => (if type_eq A A' then Some B else None)
| _, _ => None
end
| EPlus E1 E2 => match infer_type Γ E1, infer_type Γ E2 with
| Some Int, Some Int => Some Int
| _, _ => None
end
| ELam BAnon A E => None
end.
Ltac destruct_match H H_eq :=
repeat match goal with
| [H: match ?matcher with _ => _ end = Some _ |- _] =>
induction matcher eqn:H_eq; try discriminate H
end.
(** Prove both directions of the correctness theorem. *)
Lemma infer_type_typing Γ E A:
infer_type Γ E = Some A (Γ S E : A)%ty.
Proof.
revert Γ A.
induction E; intros Γ B H_infer; inversion H_infer; subst; eauto.
- destruct_match H0 H_x.
destruct_match H0 H_eq.
injection H0; intro H_eq'.
subst.
eapply src_typed_lam.
exact (IHE _ _ H_eq).
- destruct_match H0 H_E1.
destruct_match H0 H_a.
destruct_match H0 H_E2.
destruct_match H0 H_eq.
clear IHt1 IHt2.
apply Is_true_eq_left in H_eq.
rewrite type_eq_iff in H_eq.
injection H0; intro H_eq'.
subst.
eapply src_typed_app.
exact (IHE1 _ _ H_E1).
exact (IHE2 _ _ H_E2).
- destruct_match H0 H_E1.
destruct_match H0 H_a.
destruct_match H0 H_E2.
rename a0 into b.
destruct_match H0 H_b.
injection H0; intro H_eq.
subst.
eapply src_typed_add.
exact (IHE1 _ _ H_E1).
exact (IHE2 _ _ H_E2).
Qed.
Lemma typing_infer_type Γ E A:
(Γ S E : A)%ty infer_type Γ E = Some A.
Proof.
intro H_typed.
induction H_typed; simpl; try eauto.
- induction (infer_type (<[x := A]> Γ) E) eqn:H1; try discriminate IHH_typed.
rewrite H1.
injection IHH_typed; intro H_eq.
rewrite H_eq.
intuition.
- induction (infer_type Γ E1) eqn:H1; try discriminate IHH_typed1.
injection IHH_typed1; intro H_eq; subst.
induction (infer_type Γ E2) eqn:H2; try discriminate IHH_typed2.
injection IHH_typed2; intro H_eq; subst.
destruct (type_eq A A) eqn:H_AA.
+ reflexivity.
+ (* idk why I struggled so much to manipulate H_AA *)
assert (A = A) as H_AA_true by reflexivity.
rewrite <-type_eq_iff in H_AA_true.
apply Is_true_eq_true in H_AA_true.
rewrite H_AA_true in H_AA.
discriminate H_AA.
- induction (infer_type Γ E1) eqn:H1; try discriminate IHH_typed.
injection IHH_typed1; intro H_eq; subst.
induction (infer_type Γ E2) eqn:H2; try discriminate IHH_typed2.
injection IHH_typed2; intro H_eq; subst.
+ reflexivity.
+ discriminate IHH_typed1.
Qed.
(** ** Exercise 6: untypable, safe term *)
(* The exercise asks you to:
"Give one example if there is such an expression, otherwise prove their non-existence."
So either finish one section or the other.
*)
Section give_example.
Definition omega : expr := (λ: "x", "x" "x").
(* This is simply binding Ω to a variable, without using it. *)
Definition ust : expr := ((λ: "x" "y", "y") (λ: "_", omega omega) 1)%E.
Lemma ust_safe e':
rtc step ust e' is_val e' reducible e'.
Proof.
intro H_steps.
assert (e' = 1 e' = ((λ: "y", "y") 1)%E e' = ust).
{
refine (rtc_ind_r (λ (e: expr), e = 1 e = ((λ: "y", "y") 1)%E e = ust) ust _ _ _ H_steps).
- right; right; reflexivity.
- intros y z H_steps' H_step_yz H_y.
destruct H_y; subst; try val_no_step.
destruct H; subst.
+ inversion H_step_yz; subst; try val_no_step; simpl.
left; reflexivity.
+ inversion H_step_yz; subst; try val_no_step; simpl.
inversion H3; subst; try val_no_step; simpl.
right; left; reflexivity.
}
destruct H as [ H | [ H | H ]].
- left.
rewrite H.
unfold is_val; intuition.
- right.
exists 1.
subst.
apply StepBeta.
unfold is_val; intuition.
- right.
exists ((λ: "y", "y") 1)%E.
subst.
apply StepAppL.
unfold is_val; intuition.
apply StepBeta.
unfold is_val; intuition.
Qed.
Lemma rec_type_contra A B:
(A B)%ty = A -> False.
Proof.
revert B.
induction A.
- intros B H_eq.
discriminate H_eq.
- intros B H_eq.
injection H_eq.
intros H_eqb H_eqA1.
eapply IHA1.
exact H_eqA1.
Qed.
Lemma ust_no_type Γ A:
¬ (Γ ust : A)%ty.
Proof.
intro H_typed.
inversion H_typed; subst; rename H2 into H_typed_let_omega.
inversion H_typed_let_omega; subst; rename H5 into H_typed_lambda_omega.
inversion H_typed_lambda_omega; subst; rename H5 into H_typed_omega_omega.
inversion H_typed_omega_omega; subst; rename H6 into H_typed_omega.
inversion H_typed_omega; subst; rename H6 into H_typed_omega_inner.
inversion H_typed_omega_inner; subst.
rename H5 into H_typed_x.
rename H7 into H_typed_x'.
inversion H_typed_x; subst; clear H_typed_x; rename H1 into H_typed_x.
inversion H_typed_x'; subst; clear H_typed_x'; rename H1 into H_typed_x'.
rewrite lookup_insert in H_typed_x.
rewrite lookup_insert in H_typed_x'.
injection H_typed_x; intro H_eq1.
injection H_typed_x'; intro H_eq2.
rewrite H_eq1 in H_eq2.
exact (rec_type_contra _ _ H_eq2).
Qed.
End give_example.
(* Section prove_non_existence.
Lemma no_ust :
e, ( e', rtc step e e' is_val e' reducible e') A, ( e : A)%ty.
Proof.
Admitted.
End prove_non_existence. *)

@ -318,3 +318,22 @@ Qed.
Lemma subst_closed_nil e x es : closed [] e subst x es e = e.
Proof. intros. apply subst_closed with []; set_solver. Qed.
Lemma val_no_step e e':
step e e' is_val e False.
Proof.
by destruct 1.
Qed.
Lemma val_no_step' (v : val) (e : expr) :
step (of_val v) e -> False.
Proof.
intros H. eapply (val_no_step _ _ H).
apply is_val_val.
Qed.
Ltac val_no_step :=
match goal with
| [H: step ?e1 ?e2 |- _] =>
solve [exfalso; eapply (val_no_step _ _ H); done]
end.

@ -0,0 +1,235 @@
From stdpp Require Import base relations tactics.
From iris Require Import prelude.
From semantics.ts.stlc Require Import lang notation.
From semantics.lib Require Import sets maps.
(** ** Syntactic typing *)
(** In the Coq formalization, we exclusively define runtime typing (Curry-style). *)
(** It will be an exercise to consider Church-style typing. *)
Inductive type : Set :=
| Int
| Fun (A B : type).
Definition typing_context := gmap string type.
Implicit Types
(Γ : typing_context)
(v : val)
(e : expr)
(A : type)
(x: string).
(** We define notation for types in a new scope with delimiter [ty].
See below for an example. *)
Declare Scope FType_scope.
Delimit Scope FType_scope with ty.
Bind Scope FType_scope with type.
Infix "" := Fun : FType_scope.
Notation "(→)" := Fun (only parsing) : FType_scope.
(** Typing rules *)
(** We need to reserve the notation beforehand to already use it when defining the
typing rules. *)
Reserved Notation "Γ ⊢ e : A" (at level 74, e, A at next level).
Inductive syn_typed : typing_context expr type Prop :=
| typed_var Γ x A :
(* lookup the variable in the context *)
Γ !! x = Some A
Γ (Var x) : A
| typed_lam Γ x e A B :
(* add a new type assignment to the context *)
(<[ x := A]> Γ) e : B
Γ (Lam (BNamed x) e) : (A B)
| typed_int Γ z :
Γ (LitInt z) : Int
| typed_app Γ e1 e2 A B :
Γ e1 : (A B)
Γ e2 : A
Γ e1 e2 : B
| typed_add Γ e1 e2 :
Γ e1 : Int
Γ e2 : Int
Γ e1 + e2 : Int
where "Γ ⊢ e : A" := (syn_typed Γ e%E A%ty) : FType_scope.
(** Add constructors to [eauto]'s hint database. *)
#[export] Hint Constructors syn_typed : core.
Local Open Scope FType_scope.
(** a small example *)
Goal (λ: "x", 1 + "x")%E : (Int Int).
Proof. eauto. Qed.
(** We derive some inversion lemmas -- this is cleaner than directly
using the [inversion] tactic everywhere.*)
Lemma var_inversion Γ (x: string) A: Γ x : A Γ !! x = Some A.
Proof. inversion 1; subst; auto. Qed.
Lemma lam_inversion Γ (x: binder) e C:
Γ (λ: x, e) : C
A B y, C = (A B)%ty x = BNamed y <[y:=A]> Γ e : B.
Proof. inversion 1; subst; eauto 10. Qed.
Lemma lit_int_inversion Γ (n: Z) A: Γ n : A A = Int.
Proof. inversion 1; subst; auto. Qed.
Lemma app_inversion Γ e1 e2 B:
Γ e1 e2 : B
A, Γ e1 : (A B) Γ e2 : A.
Proof. inversion 1; subst; eauto. Qed.
Lemma plus_inversion Γ e1 e2 B:
Γ e1 + e2 : B
B = Int Γ e1 : Int Γ e2 : Int.
Proof. inversion 1; subst; eauto. Qed.
Lemma syn_typed_closed Γ e A X :
Γ e : A
( x, x dom Γ x X)
is_closed X e.
Proof.
induction 1 as [ | ?????? IH | | | ] in X |-*; simpl; intros Hx; try done.
{ (* var *) apply bool_decide_pack, Hx. apply elem_of_dom; eauto. }
{ (* lam *) apply IH.
intros y. rewrite elem_of_dom lookup_insert_is_Some.
intros [<- | [? Hy]]; first by apply elem_of_cons; eauto.
apply elem_of_cons. right. eapply Hx. by apply elem_of_dom.
}
(* everything else *)
all: repeat match goal with
| |- Is_true (_ && _) => apply andb_True; split
end.
all: naive_solver.
Qed.
Lemma typed_weakening Γ Δ e A:
Γ e : A
Γ Δ
Δ e : A.
Proof.
induction 1 as [| Γ x e A B Htyp IH | | | ] in Δ; intros Hsub; eauto.
- econstructor. by eapply lookup_weaken.
- econstructor. eapply IH. by eapply insert_mono.
Qed.
(** Preservation of typing under substitution *)
Lemma typed_substitutivity e e' Γ x A B :
e' : A
<[x := A]> Γ e : B
Γ subst x e' e : B.
Proof.
intros He'. revert B Γ; induction e as [y | y | | |]; intros B Γ; simpl.
- intros Hp%var_inversion; destruct decide; subst; eauto.
+ rewrite lookup_insert in Hp. injection Hp as ->.
eapply typed_weakening; first done. apply map_empty_subseteq.
+ rewrite lookup_insert_ne in Hp; last done. auto.
- intros (C & D & z & -> & -> & Hty)%lam_inversion.
econstructor. destruct decide as [|Heq]; simplify_eq.
+ by rewrite insert_insert in Hty.
+ rewrite insert_commute in Hty; last naive_solver. eauto.
- intros (C & Hty1 & Hty2)%app_inversion; eauto.
- intros ->%lit_int_inversion. eauto.
- intros (-> & Hty1 & Hty2)%plus_inversion; eauto.
Qed.
(** Canonical value lemmas *)
Lemma canonical_values_arr Γ e A B:
Γ e : (A B)
is_val e
x e', e = (λ: x, e')%E.
Proof.
inversion 1; simpl; naive_solver.
Qed.
Lemma canonical_values_int Γ e:
Γ e : Int
is_val e
n: Z, e = n.
Proof.
inversion 1; simpl; naive_solver.
Qed.
(** Progress lemma *)
Lemma typed_progress e A:
e : A is_val e contextual_reducible e.
Proof.
remember as Γ. induction 1 as [| | | Γ e1 e2 A B Hty IH1 _ IH2 | Γ e1 e2 Hty1 IH1 Hty2 IH2].
- subst. naive_solver.
- left. done.
- left. done.
- destruct (IH2 HeqΓ) as [H2|H2]; [destruct (IH1 HeqΓ) as [H1|H1]|].
+ eapply canonical_values_arr in Hty as (x & e & ->); last done.
right. eexists.
eapply base_contextual_step, BetaS; eauto.
+ right. eapply is_val_spec in H2 as [v Heq].
replace e2 with (of_val v); last by eapply of_to_val.
destruct H1 as [e1' Hstep].
eexists. eapply (fill_contextual_step (AppLCtx HoleCtx v)). done.
+ right. destruct H2 as [e2' H2].
eexists. eapply (fill_contextual_step (AppRCtx e1 HoleCtx)). done.
- destruct (IH2 HeqΓ) as [H2|H2]; [destruct (IH1 HeqΓ) as [H1|H1]|].
+ right. eapply canonical_values_int in Hty1 as [n1 ->]; last done.
eapply canonical_values_int in Hty2 as [n2 ->]; last done.
eexists. eapply base_contextual_step. eapply PlusS; eauto.
+ right. eapply is_val_spec in H2 as [v Heq].
replace e2 with (of_val v); last by eapply of_to_val.
destruct H1 as [e1' Hstep].
eexists. eapply (fill_contextual_step (PlusLCtx HoleCtx v)). done.
+ right. destruct H2 as [e2' H2].
eexists. eapply (fill_contextual_step (PlusRCtx e1 HoleCtx)). done.
Qed.
(** Contextual typing *)
Definition ectx_typing (K: ectx) (A B: type) :=
e, e : A (fill K e) : B.
Lemma fill_typing_decompose K e A:
fill K e : A
B, e : B ectx_typing K B A.
Proof.
unfold ectx_typing; induction K in e,A |-*; simpl; eauto.
all: inversion 1; subst; edestruct IHK as [B [Hit Hty]]; eauto.
Qed.
Lemma fill_typing_compose K e A B:
e : B
ectx_typing K B A
fill K e : A.
Proof.
intros H1 H2; by eapply H2.
Qed.
(** Base preservation *)
Lemma typed_preservation_base_step e e' A:
e : A
base_step e e'
e' : A.
Proof.
intros Hty Hstep. destruct Hstep as [| e1 e2 n1 n2 n3 Heq1 Heq2 Heval]; subst.
- eapply app_inversion in Hty as (B & Hty1 & Hty2).
eapply lam_inversion in Hty1 as (B' & A' & y & Heq1 & Heq2 & Hty).
simplify_eq. eapply typed_substitutivity; eauto.
- eapply plus_inversion in Hty as (-> & Hty1 & Hty2).
econstructor.
Qed.
(** Preservation *)
Lemma typed_preservation e e' A:
e : A
contextual_step e e'
e' : A.
Proof.
intros Hty Hstep. destruct Hstep as [K e1 e2 -> -> Hstep].
eapply fill_typing_decompose in Hty as [B [H1 H2]].
eapply fill_typing_compose; last done.
by eapply typed_preservation_base_step.
Qed.
Lemma typed_safety e1 e2 A:
e1 : A
rtc contextual_step e1 e2
is_val e2 contextual_reducible e2.
Proof.
induction 2; eauto using typed_progress, typed_preservation.
Qed.

@ -0,0 +1,221 @@
From stdpp Require Import base relations tactics.
From iris Require Import prelude.
From semantics.lib Require Import sets maps.
From semantics.ts.stlc Require Import lang notation.
(** The following two lemmas will be helpful in the sequel.
They just lift multiple reduction steps (via [rtc]) to application.
*)
Lemma steps_app_r (e1 e2 e2' : expr) :
rtc step e2 e2'
rtc step (e1 e2) (e1 e2').
Proof.
induction 1 as [ e | e e' e'' Hstep Hsteps IH].
- reflexivity.
- eapply (rtc_l _ _ (e1 e')).
{ by eapply StepAppR. }
done.
Qed.
Lemma steps_app_l (e1 e1' e2 : expr) :
is_val e2
rtc step e1 e1'
rtc step (e1 e2) (e1' e2).
Proof.
intros Hv.
induction 1 as [ e | e e' e'' Hstep Hsteps IH].
- reflexivity.
- eapply (rtc_l _ _ (e' e2)).
{ by eapply StepAppL. }
done.
Qed.
(** * Untyped λ calculus *)
(** We do not re-define the language to remove primitive addition -- instead, we just
restrict our usage in this file to variables, application, and lambdas.
*)
Definition I_val : val := λ: "x", "x".
Definition F_val : val := λ: "x" "y", "x".
Definition S_val : val := λ: "x" "y", "y".
Definition ω : val := λ: "x", "x" "x".
Definition Ω : expr := ω ω.
(** Ω reduces to itself! *)
Lemma Omega_step : step Ω Ω.
Proof.
apply StepBeta. done.
Qed.
(** ** Scott encodings *)
Definition zero : val := λ: "x" "y", "x".
Definition succ (n : val) : val := λ: "x" "y", "y" n.
(** [Succ] can be seen as a constructor: it takes [n] at the level of the language. *)
Definition Succ : val := λ: "n" "x" "y", "y" "n".
Fixpoint enc_nat (n : nat) : val :=
match n with
| 0 => zero
| S n => succ (enc_nat n)
end.
Lemma enc_nat_closed n :
closed [] (enc_nat n).
Proof.
induction n as [ | n IH].
- done.
- simpl. by apply closed_weaken_nil.
Qed.
Lemma enc_0_red (z s : val) :
is_closed [] z
rtc step (enc_nat 0 z s) z.
Proof.
intros Hcl.
eapply rtc_l.
{ econstructor; first auto. econstructor. auto. }
simpl. eapply rtc_l.
{ econstructor. auto. }
simpl. rewrite subst_closed_nil; done.
Qed.
Lemma enc_S_red n (z s : val) :
rtc step (enc_nat (S n) z s) (s (enc_nat n)).
Proof.
simpl. eapply rtc_l.
{ econstructor; first auto. econstructor. auto. }
simpl. eapply rtc_l.
{ econstructor. auto. }
simpl. rewrite (subst_closed_nil (enc_nat n)); last apply enc_nat_closed.
rewrite subst_closed_nil; last apply enc_nat_closed.
reflexivity.
Qed.
Lemma Succ_red n : step (Succ (enc_nat n)) (enc_nat (S n)).
Proof. econstructor. apply is_val_val. Qed.
Lemma Succ_red_n n : rtc step (Nat.iter n Succ zero) (enc_nat n).
Proof.
induction n as [ | n IH].
- reflexivity.
- simpl.
etrans.
{ simpl. eapply steps_app_r. apply IH. }
eapply rtc_l.
{ apply Succ_red. }
reflexivity.
Qed.
(** ** Recursion *)
Definition Fix' : val := λ: "z" "y", "y" (λ: "x", "z" "z" "y" "x").
Definition Fix (s : val) : val := λ: "x", Fix' Fix' s "x".
Arguments Fix : simpl never.
Local Hint Immediate is_val_val : core.
(** We prove that it satisfies the recursive unfolding *)
Lemma Fix_step (s r : val) :
is_closed [] s
rtc step (Fix s r) (s ((Fix s))%E r).
Proof.
intros Hclosed.
eapply rtc_l.
{ econstructor. auto. }
eapply rtc_l.
{ simpl. econstructor; first by auto.
econstructor. { rewrite subst_closed_nil; auto. }
econstructor. done.
}
simpl. rewrite subst_closed_nil; last done.
eapply rtc_l.
{ econstructor; first by auto.
econstructor. auto.
}
simpl. reflexivity.
Qed.
(** Example usage: addition on Scott-encoded numbers *)
Definition add_step : val := λ: "r", λ: "n" "m", "n" "m" (λ: "p", Succ ("r" "p" "m")).
Definition add := Fix add_step.
(** We are now going to prove it correct:
[add (enc_nat n) (enc_nat m)) * (enc_nat (n + m))]
First, we prove that it satisfies the expected defining equations for Peano addition.
*)
Lemma add_step_0 m : rtc step (add (enc_nat 0) (enc_nat m)) (enc_nat m).
Proof.
(* use the unfolding equation of the fixpoint combinator *)
etrans.
{ eapply steps_app_l; first by auto.
eapply Fix_step. done.
}
(* subst it into the [add_step] function *)
eapply rtc_l.
{ econstructor; auto. econstructor; auto. econstructor. auto. }
simpl.
(* subst in the zero *)
eapply rtc_l.
{ econstructor; auto. econstructor. done. }
simpl.
(* subst in the m *)
eapply rtc_l.
{ econstructor; auto. }
simpl.
(* do a step *)
etrans.
{ apply (enc_0_red (enc_nat m) (λ: "p", Succ (Fix add_step "p" (enc_nat m)))).
apply enc_nat_closed.
}
reflexivity.
Qed.
Lemma add_step_S n m : rtc step (add (enc_nat (S n)) (enc_nat m)) (Succ (add (enc_nat n) (enc_nat m))).
Proof.
(* use the unfolding equation of the fixpoint combinator *)
etrans.
{ eapply steps_app_l; first by auto.
eapply Fix_step. done.
}
(* subst it into the [add_step] function *)
eapply rtc_l.
{ econstructor; auto. econstructor; auto. econstructor. auto. }
simpl.
(* subst in the zero *)
eapply rtc_l.
{ econstructor; auto. econstructor. done. }
simpl.
(* subst in the m *)
eapply rtc_l.
{ econstructor; auto. }
simpl.
(* do a step *)
etrans.
{ rewrite subst_closed_nil; last apply enc_nat_closed.
apply (enc_S_red n (enc_nat m) (λ: "p", Succ (Fix add_step "p" (enc_nat m)))).
}
eapply rtc_l.
{ econstructor. auto. }
simpl.
rewrite subst_closed_nil; last apply enc_nat_closed.
reflexivity.
Qed.
Lemma add_correct n m : rtc step (add (enc_nat n) (enc_nat m)) (enc_nat (n + m)).
Proof.
induction n as [ | n IH].
- apply add_step_0.
- etrans. { apply add_step_S. }
etrans. { apply steps_app_r. apply IH. }
eapply rtc_l. { apply Succ_red. }
reflexivity.
Qed.

@ -0,0 +1,47 @@
From stdpp Require Import gmap base relations.
From iris Require Import prelude.
From semantics.ts.stlc_extended Require Import lang notation.
(** * Big-step semantics *)
Implicit Types
(v : val)
(e : expr).
Inductive big_step : expr val Prop :=
| bs_lit (n : Z) :
big_step (LitInt n) (LitIntV n)
| bs_lam (x : binder) (e : expr) :
big_step (λ: x, e)%E (λ: x, e)%V
| bs_add e1 e2 (z1 z2 : Z) :
big_step e1 (LitIntV z1)
big_step e2 (LitIntV z2)
big_step (Plus e1 e2) (LitIntV (z1 + z2))%Z
| bs_app e1 e2 x e v2 v :
big_step e1 (LamV x e)
big_step e2 v2
big_step (subst' x (of_val v2) e) v
big_step (App e1 e2) v
(* TODO : extend the big-step semantics *)
.
#[export] Hint Constructors big_step : core.
Lemma big_step_of_val e v :
e = of_val v
big_step e v.
Proof.
intros ->.
induction v; simpl; eauto.
(* TODO : this should be fixed once you have added the right semantics *)
Admitted.
Lemma big_step_val v v' :
big_step (of_val v) v' v' = v.
Proof.
enough ( e, big_step e v' e = of_val v v' = v) by naive_solver.
intros e Hb.
induction Hb in v |-*; intros Heq; subst; destruct v; inversion Heq; subst; naive_solver.
Qed.

@ -0,0 +1,180 @@
From semantics.ts.stlc_extended Require Export lang.
(** The stepping relation *)
Inductive base_step : expr expr Prop :=
| BetaS x e1 e2 e' :
is_val e2
e' = subst' x e2 e1
base_step (App (Lam x e1) e2) e'
| PlusS e1 e2 (n1 n2 n3 : Z):
e1 = (LitInt n1)
e2 = (LitInt n2)
(n1 + n2)%Z = n3
base_step (Plus e1 e2) (LitInt n3)
(* TODO: extend the definition *)
.
#[export] Hint Constructors base_step : core.
(** We define evaluation contexts *)
Inductive ectx :=
| HoleCtx
| AppLCtx (K: ectx) (v2 : val)
| AppRCtx (e1 : expr) (K: ectx)
| PlusLCtx (K: ectx) (v2 : val)
| PlusRCtx (e1 : expr) (K: ectx)
(* TODO: extend the definition *)
.
Fixpoint fill (K : ectx) (e : expr) : expr :=
match K with
| HoleCtx => e
| AppLCtx K v2 => App (fill K e) (of_val v2)
| AppRCtx e1 K => App e1 (fill K e)
| PlusLCtx K v2 => Plus (fill K e) (of_val v2)
| PlusRCtx e1 K => Plus e1 (fill K e)
(* TODO: extend the definition *)
end.
Fixpoint comp_ectx (K: ectx) (K' : ectx) : ectx :=
match K with
| HoleCtx => K'
| AppLCtx K v2 => AppLCtx (comp_ectx K K') v2
| AppRCtx e1 K => AppRCtx e1 (comp_ectx K K')
| PlusLCtx K v2 => PlusLCtx (comp_ectx K K') v2
| PlusRCtx e1 K => PlusRCtx e1 (comp_ectx K K')
(* TODO: extend the definition *)
end.
(** Contextual steps *)
Inductive contextual_step (e1 : expr) (e2 : expr) : Prop :=
Ectx_step K e1' e2' :
e1 = fill K e1' e2 = fill K e2'
base_step e1' e2' contextual_step e1 e2.
#[export] Hint Constructors contextual_step : core.
Definition reducible (e : expr) :=
e', contextual_step e e'.
Definition empty_ectx := HoleCtx.
(** Basic properties about the language *)
Lemma fill_empty e : fill empty_ectx e = e.
Proof. done. Qed.
Lemma fill_comp (K1 K2 : ectx) e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e.
Proof. induction K1; simpl; congruence. Qed.
Lemma base_contextual_step e1 e2 :
base_step e1 e2 contextual_step e1 e2.
Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.
Lemma fill_contextual_step K e1 e2 :
contextual_step e1 e2 contextual_step (fill K e1) (fill K e2).
Proof.
destruct 1 as [K' e1' e2' -> ->].
rewrite !fill_comp. by econstructor.
Qed.
(** We derive a few lemmas about contextual steps:
these essentially provide rules for structural lifting
akin to the structural semantics.
*)
Lemma contextual_step_app_l e1 e1' e2:
is_val e2
contextual_step e1 e1'
contextual_step (App e1 e2) (App e1' e2).
Proof.
intros [v <-%of_to_val]%is_val_spec Hcontextual.
by eapply (fill_contextual_step (AppLCtx HoleCtx v)).
Qed.
Lemma contextual_step_app_r e1 e2 e2':
contextual_step e2 e2'
contextual_step (App e1 e2) (App e1 e2').
Proof.
intros Hcontextual.
by eapply (fill_contextual_step (AppRCtx e1 HoleCtx)).
Qed.
Lemma contextual_step_plus_l e1 e1' e2:
is_val e2
contextual_step e1 e1'
contextual_step (Plus e1 e2) (Plus e1' e2).
Proof.
intros [v <-%of_to_val]%is_val_spec Hcontextual.
by eapply (fill_contextual_step (PlusLCtx HoleCtx v)).
Qed.
Lemma contextual_step_plus_r e1 e2 e2':
contextual_step e2 e2'
contextual_step (Plus e1 e2) (Plus e1 e2').
Proof.
intros Hcontextual.
by eapply (fill_contextual_step (PlusRCtx e1 HoleCtx)).
Qed.
Lemma contextual_step_pair_l e1 e1' e2:
is_val e2
contextual_step e1 e1'
contextual_step (Pair e1 e2) (Pair e1' e2).
Proof.
(* TODO: exercise *)
Admitted.
Lemma contextual_step_pair_r e1 e2 e2':
contextual_step e2 e2'
contextual_step (Pair e1 e2) (Pair e1 e2').
Proof.
(* TODO: exercise *)
Admitted.
Lemma contextual_step_fst e e':
contextual_step e e'
contextual_step (Fst e) (Fst e').
Proof.
(* TODO: exercise *)
Admitted.
Lemma contextual_step_snd e e':
contextual_step e e'
contextual_step (Snd e) (Snd e').
Proof.
(* TODO: exercise *)
Admitted.
Lemma contextual_step_injl e e':
contextual_step e e'
contextual_step (InjL e) (InjL e').
Proof.
(* TODO: exercise *)
Admitted.
Lemma contextual_step_injr e e':
contextual_step e e'
contextual_step (InjR e) (InjR e').
Proof.
(* TODO: exercise *)
Admitted.
Lemma contextual_step_case e e' e1 e2:
contextual_step e e'
contextual_step (Case e e1 e2) (Case e' e1 e2).
Proof.
(* TODO: exercise *)
Admitted.
#[global]
Hint Resolve
contextual_step_app_l contextual_step_app_r contextual_step_plus_l contextual_step_plus_r
contextual_step_case contextual_step_fst contextual_step_injl contextual_step_injr
contextual_step_pair_l contextual_step_pair_r contextual_step_snd : core.

@ -0,0 +1,175 @@
From stdpp Require Export binders strings.
From iris.prelude Require Import options.
From semantics.lib Require Export maps.
Declare Scope expr_scope.
Declare Scope val_scope.
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
Inductive expr :=
(* Base lambda calculus *)
| Var (x : string)
| Lam (x : binder) (e : expr)
| App (e1 e2 : expr)
(* Base types and their operations *)
| LitInt (n: Z)
| Plus (e1 e2 : expr)
(* Products *)
| Pair (e1 e2 : expr)
| Fst (e : expr)
| Snd (e : expr)
(* Sums *)
| InjL (e : expr)
| InjR (e : expr)
| Case (e0 : expr) (e1 : expr) (e2 : expr).
Bind Scope expr_scope with expr.
Inductive val :=
| LitIntV (n: Z)
| LamV (x : binder) (e : expr)
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val)
.
Bind Scope val_scope with val.
Fixpoint of_val (v : val) : expr :=
match v with
| LitIntV n => LitInt n
| LamV x e => Lam x e
| PairV v1 v2 => Pair (of_val v1) (of_val v2)
| InjLV v => InjL (of_val v)
| InjRV v => InjR (of_val v)
end.
Fixpoint to_val (e : expr) : option val :=
match e with
| LitInt n => Some $ LitIntV n
| Lam x e => Some (LamV x e)
| Pair e1 e2 =>
to_val e1 = (λ v1, to_val e2 = (λ v2, Some $ PairV v1 v2))
| InjL e => to_val e = (λ v, Some $ InjLV v)
| InjR e => to_val e = (λ v, Some $ InjRV v)
| _ => None
end.
(** Equality and other typeclass stuff *)
Lemma to_of_val v : to_val (of_val v) = Some v.
Proof.
by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
Qed.
Lemma of_to_val e v : to_val e = Some v of_val v = e.
Proof.
revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
Qed.
#[export] Instance of_val_inj : Inj (=) (=) of_val.
Proof. by intros ?? Hv; apply (inj Some); rewrite <-!to_of_val, Hv. Qed.
(** structural computational version *)
Fixpoint is_val (e : expr) : Prop :=
match e with
| LitInt l => True
| Lam x e => True
| Pair e1 e2 => is_val e1 is_val e2
| InjL e => is_val e
| InjR e => is_val e
| _ => False
end.
Lemma is_val_spec e : is_val e v, to_val e = Some v.
Proof.
induction e as [ | ? e IH | e1 IH1 e2 IH2 | | e1 IH1 e2 IH2 | e1 IH1 e2 IH2 | e IH | e IH | e IH | e IH | e1 IH1 e2 IH2 e3 IH3];
simpl; (split; [ | intros (v & Heq)]); simplify_option_eq; try done; eauto.
- rewrite IH1, IH2. intros [(v1 & ->) (v2 & ->)]. eauto.
- rewrite IH1, IH2. eauto.
- rewrite IH. intros (v & ->). eauto.
- apply IH. eauto.
- rewrite IH. intros (v & ->); eauto.
- apply IH. eauto.
Qed.
Ltac simplify_val :=
repeat match goal with
| H: to_val (of_val ?v) = ?o |- _ => rewrite to_of_val in H
| H: is_val ?e |- _ => destruct (proj1 (is_val_spec e) H) as (? & ?); clear H
end.
(* Misc *)
Lemma is_val_of_val v : is_val (of_val v).
Proof. apply is_val_spec. rewrite to_of_val. eauto. Qed.
(** Substitution *)
Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
match e with
| LitInt _ => e
| Var y => if decide (x = y) then es else Var y
| Lam y e =>
Lam y $ if decide (BNamed x = y) then e else subst x es e
| App e1 e2 => App (subst x es e1) (subst x es e2)
| Plus e1 e2 => Plus (subst x es e1) (subst x es e2)
| Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
| Fst e => Fst (subst x es e)
| Snd e => Snd (subst x es e)
| InjL e => InjL (subst x es e)
| InjR e => InjR (subst x es e)
| Case e0 e1 e2 => Case (subst x es e0) (subst x es e1) (subst x es e2)
end.
Definition subst' (mx : binder) (es : expr) : expr expr :=
match mx with BNamed x => subst x es | BAnon => id end.
(** Closed terms **)
Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with
| Var x => bool_decide (x X)
| Lam x e => is_closed (x :b: X) e
| LitInt _ => true
| Fst e | Snd e | InjL e | InjR e => is_closed X e
| App e1 e2 | Plus e1 e2 | Pair e1 e2 => is_closed X e1 && is_closed X e2
| Case e0 e1 e2 =>
is_closed X e0 && is_closed X e1 && is_closed X e2
end.
(** [closed] states closedness as a Coq proposition, through the [Is_true] transformer. *)
Definition closed (X : list string) (e : expr) : Prop := Is_true (is_closed X e).
#[export] Instance closed_proof_irrel X e : ProofIrrel (closed X e).
Proof. unfold closed. apply _. Qed.
#[export] Instance closed_dec X e : Decision (closed X e).
Proof. unfold closed. apply _. Defined.
(** closed expressions *)
Lemma is_closed_weaken X Y e : is_closed X e X Y is_closed Y e.
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
Lemma is_closed_weaken_nil X e : is_closed [] e is_closed X e.
Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
Lemma is_closed_subst X e x es :
is_closed [] es is_closed (x :: X) e is_closed X (subst x es e).
Proof.
intros ?.
induction e in X |-*; simpl; intros ?; destruct_and?; split_and?; simplify_option_eq;
try match goal with
| H : ¬(_ _) |- _ => apply not_and_l in H as [?%dec_stable|?%dec_stable]
end; eauto using is_closed_weaken with set_solver.
Qed.
Lemma is_closed_do_subst' X e x es :
is_closed [] es is_closed (x :b: X) e is_closed X (subst' x es e).
Proof. destruct x; eauto using is_closed_subst. Qed.
(** Substitution lemmas *)
Lemma subst_is_closed X e x es : is_closed X e x X subst x es e = e.
Proof.
induction e in X |-*; simpl; rewrite ?bool_decide_spec, ?andb_True; intros ??;
repeat case_decide; simplify_eq; simpl; f_equal; intuition eauto with set_solver.
Qed.
Lemma subst_is_closed_nil e x es : is_closed [] e subst x es e = e.
Proof. intros. apply subst_is_closed with []; set_solver. Qed.
Lemma subst'_is_closed_nil e x es : is_closed [] e subst' x es e = e.
Proof. intros. destruct x as [ | x]. { done. } by apply subst_is_closed_nil. Qed.

@ -0,0 +1,56 @@
From semantics.ts.stlc_extended Require Export lang.
Set Default Proof Using "Type".
(** Coercions to make programs easier to type. *)
Coercion of_val : val >-> expr.
Coercion App : expr >-> Funclass.
Coercion Var : string >-> expr.
(** Define some derived forms. *)
Notation Let x e1 e2 := (App (Lam x e2) e1) (only parsing).
Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing).
Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).
(* No scope for the values, does not conflict and scope is often not inferred
properly. *)
Notation "# l" := (LitIntV l%Z%V%stdpp) (at level 8, format "# l").
Notation "# l" := (LitInt l%Z%E%stdpp) (at level 8, format "# l") : expr_scope.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope.
Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope.
Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
(Match e0 x1%binder e1 x2%binder e2)
(e0, x1, e1, x2, e2 at level 200,
format "'[hv' 'match:' e0 'with' '/ ' '[' 'InjL' x1 => '/ ' e1 ']' '/' '[' | 'InjR' x2 => '/ ' e2 ']' '/' 'end' ']'") : expr_scope.
Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
(Match e0 x2%binder e2 x1%binder e1)
(e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope.
Notation "e1 + e2" := (Plus e1%E e2%E) : expr_scope.
(*Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.*)
Notation "λ: x , e" := (Lam x%binder e%E)
(at level 200, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : expr_scope.
Notation "λ: x y .. z , e" := (Lam x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
(at level 200, x, y, z at level 1, e at level 200,
format "'[' 'λ:' x y .. z , '/ ' e ']'") : expr_scope.
Notation "λ: x , e" := (LamV x%binder e%E)
(at level 200, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : val_scope.
Notation "λ: x y .. z , e" := (LamV x%binder (Lam y%binder .. (Lam z%binder e%E) .. ))
(at level 200, x, y, z at level 1, e at level 200,
format "'[' 'λ:' x y .. z , '/ ' e ']'") : val_scope.
Notation "'let:' x := e1 'in' e2" := (Lam x%binder e2%E e1%E)
(at level 200, x at level 1, e1, e2 at level 200,
format "'[' 'let:' x := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope.
Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
(at level 100, e2 at level 200,
format "'[' '[hv' '[' e1 ']' ;; ']' '/' e2 ']'") : expr_scope.

@ -0,0 +1,255 @@
From stdpp Require Import base relations.
From iris Require Import prelude.
From semantics.lib Require Import maps.
From semantics.ts.stlc_extended Require Import lang notation ctxstep.
(** ** Syntactic typing *)
Inductive type : Type :=
| Int
| Fun (A B : type)
| Prod (A B : type)
| Sum (A B : type).
Definition typing_context := gmap string type.
Implicit Types
(Γ : typing_context)
(v : val)
(e : expr).
Declare Scope FType_scope.
Delimit Scope FType_scope with ty.
Bind Scope FType_scope with type.
Infix "" := Fun : FType_scope.
Notation "(→)" := Fun (only parsing) : FType_scope.
Infix "×" := Prod (at level 70) : FType_scope.
Notation "(×)" := Prod (only parsing) : FType_scope.
Infix "+" := Sum : FType_scope.
Notation "(+)" := Sum (only parsing) : FType_scope.
Reserved Notation "Γ ⊢ e : A" (at level 74, e, A at next level).
Inductive syn_typed : typing_context expr type Prop :=
| typed_var Γ x A :
Γ !! x = Some A
Γ (Var x) : A
| typed_lam Γ x e A B :
(<[ x := A]> Γ) e : B
Γ (Lam (BNamed x) e) : (A B)
| typed_lam_anon Γ e A B :
Γ e : B
Γ (Lam BAnon e) : (A B)
| typed_int Γ z : Γ (LitInt z) : Int
| typed_app Γ e1 e2 A B :
Γ e1 : (A B)
Γ e2 : A
Γ (e1 e2)%E : B
| typed_add Γ e1 e2 :
Γ e1 : Int
Γ e2 : Int
Γ e1 + e2 : Int
(* TODO: provide the new typing rules *)
where "Γ ⊢ e : A" := (syn_typed Γ e%E A%ty).
#[export] Hint Constructors syn_typed : core.
(** Examples *)
Goal (λ: "x", "x")%E : (Int Int).
Proof. eauto. Qed.
Lemma syn_typed_closed Γ e A X :
Γ e : A
( x, x dom Γ x X)
is_closed X e.
Proof.
(* TODO: you will need to add the new cases, i.e. "|"'s to the intro pattern. The proof then should go through *)
induction 1 as [ | ?????? IH | | | | ] in X |-*; simpl; intros Hx; try done.
{ (* var *) apply bool_decide_pack, Hx. apply elem_of_dom; eauto. }
{ (* lam *) apply IH.
intros y. rewrite elem_of_dom lookup_insert_is_Some.
intros [<- | [? Hy]]; first by apply elem_of_cons; eauto.
apply elem_of_cons. right. eapply Hx. by apply elem_of_dom.
}
{ (* anon lam *) naive_solver. }
(* everything else *)
all: repeat match goal with
| |- Is_true (_ && _) => apply andb_True; split
end.
all: try naive_solver.
Qed.
Lemma typed_weakening Γ Δ e A:
Γ e : A
Γ Δ
Δ e : A.
Proof.
(* TODO: here you will need to add the new cases to the intro pattern as well. The proof then should go through *)
induction 1 as [| Γ x e A B Htyp IH | | | | ] in Δ |-*; intros Hsub; eauto.
- (* var *) econstructor. by eapply lookup_weaken.
- (* lam *) econstructor. eapply IH; eauto. by eapply insert_mono.
Qed.
(** Typing inversion lemmas *)
Lemma var_inversion Γ (x: string) A: Γ x : A Γ !! x = Some A.
Proof. inversion 1; subst; auto. Qed.
Lemma lam_inversion Γ (x: string) e C:
Γ (λ: x, e) : C
A B, C = (A B)%ty <[x:=A]> Γ e : B.
Proof. inversion 1; subst; eauto 10. Qed.
Lemma lam_anon_inversion Γ e C:
Γ (λ: <>, e) : C
A B, C = (A B)%ty Γ e : B.
Proof. inversion 1; subst; eauto 10. Qed.
Lemma app_inversion Γ e1 e2 B:
Γ e1 e2 : B
A, Γ e1 : (A B) Γ e2 : A.
Proof. inversion 1; subst; eauto. Qed.
Lemma plus_inversion Γ e1 e2 B:
Γ e1 + e2 : B
B = Int Γ e1 : Int Γ e2 : Int.
Proof. inversion 1; subst; eauto. Qed.
(* TODO: add inversion lemmas for the new typing rules.
They will be very useful for the proofs below!
*)
Lemma typed_substitutivity e e' Γ (x: string) A B :
e' : A
(<[x := A]> Γ) e : B
Γ lang.subst x e' e : B.
Proof.
intros He'. revert B Γ; induction e as [y | y | | | | | | | | | ]; intros B Γ; simpl.
- intros Hp % var_inversion.
destruct (decide (x = y)).
+ subst. rewrite lookup_insert in Hp. injection Hp as ->.
eapply typed_weakening; [done| ]. apply map_empty_subseteq.
+ rewrite lookup_insert_ne in Hp; last done. auto.
- destruct y as [ | y].
{ intros (A' & C & -> & Hty) % lam_anon_inversion.
econstructor. destruct decide as [Heq|].
+ congruence.
+ eauto.
}
intros (A' & C & -> & Hty) % lam_inversion.
econstructor. destruct decide as [Heq|].
+ injection Heq as [= ->]. by rewrite insert_insert in Hty.
+ rewrite insert_commute in Hty; last naive_solver. eauto.
- intros (C & Hty1 & Hty2) % app_inversion. eauto.
- inversion 1; subst; auto.
- intros (-> & Hty1 & Hty2)%plus_inversion; eauto.
- (* TODO *) admit.
- (* TODO *) admit.
- (* TODO *) admit.
- (* TODO *) admit.
- (* TODO *) admit.
- (* TODO *) admit.
Admitted.
(** Canonical values *)
Lemma canonical_values_arr Γ e A B:
Γ e : (A B)
is_val e
x e', e = (λ: x, e')%E.
Proof.
inversion 1; simpl; naive_solver.
Qed.
Lemma canonical_values_int Γ e:
Γ e : Int
is_val e
n: Z, e = (#n)%E.
Proof.
inversion 1; simpl; naive_solver.
Qed.
(* TODO: add canonical forms lemmas for the new types *)
(** Progress *)
Lemma typed_progress e A:
e : A is_val e reducible e.
Proof.
remember as Γ.
(* TODO: you will need to extend the intro pattern *)
induction 1 as [| | | | Γ e1 e2 A B Hty IH1 _ IH2 | Γ e1 e2 Hty1 IH1 Hty2 IH2].
- subst. naive_solver.
- left. done.
- left. done.
- (* int *)left. done.
- (* app *)
destruct (IH2 HeqΓ) as [H2|H2]; [destruct (IH1 HeqΓ) as [H1|H1]|].
+ eapply canonical_values_arr in Hty as (x & e & ->); last done.
right. eexists.
eapply base_contextual_step, BetaS; eauto.
+ right. destruct H1 as [e1' Hstep].
eexists. eauto.
+ right. destruct H2 as [e2' H2].
eexists. eauto.
- (* plus *)
destruct (IH2 HeqΓ) as [H2|H2]; [destruct (IH1 HeqΓ) as [H1|H1]|].
+ right. eapply canonical_values_int in Hty1 as [n1 ->]; last done.
eapply canonical_values_int in Hty2 as [n2 ->]; last done.
subst. eexists; eapply base_contextual_step. eauto.
+ right. destruct H1 as [e1' Hstep]. eexists. eauto.
+ right. destruct H2 as [e2' H2]. eexists. eauto.
(* FIXME: prove the new cases *)
Admitted.
Definition ectx_typing (K: ectx) (A B: type) :=
e, e : A (fill K e) : B.
Lemma fill_typing_decompose K e A:
fill K e : A
B, e : B ectx_typing K B A.
Proof.
unfold ectx_typing; induction K in e,A |-*; simpl; eauto.
all: inversion 1; subst; edestruct IHK as [? [Hit Hty]]; eauto.
Qed.
Lemma fill_typing_compose K e A B:
e : B
ectx_typing K B A
fill K e : A.
Proof.
intros H1 H2; by eapply H2.
Qed.
Lemma typed_preservation_base_step e e' A:
e : A
base_step e e'
e' : A.
Proof.
intros Hty Hstep.
destruct Hstep as [ ]; subst.
- eapply app_inversion in Hty as (B & H1 & H2).
destruct x as [|x].
{ eapply lam_anon_inversion in H1 as (C & D & [= -> ->] & Hty). done. }
eapply lam_inversion in H1 as (C & D & Heq & Hty).
injection Heq as -> ->.
eapply typed_substitutivity; eauto.
- eapply plus_inversion in Hty as (-> & Hty1 & Hty2). constructor.
(* TODO: extend this for the new cases *)
Admitted.
Lemma typed_preservation e e' A:
e : A
contextual_step e e'
e' : A.
Proof.
intros Hty Hstep. destruct Hstep as [K e1 e2 -> -> Hstep].
eapply fill_typing_decompose in Hty as [B [H1 H2]].
eapply fill_typing_compose; last done.
by eapply typed_preservation_base_step.
Qed.
Lemma type_safety e1 e2 A:
e1 : A
rtc contextual_step e1 e2
is_val e2 reducible e2.
Proof.
induction 2; eauto using typed_progress, typed_preservation.
Qed.
Loading…
Cancel
Save