Compare commits
No commits in common. '9f2a8302e9d0543c7e828c17c9bcb11759ee19f3' and 'b0a5c90ebb98a7c3c0ebc3674016fe0e83fd3d96' have entirely different histories.
9f2a8302e9
...
b0a5c90ebb
@ -1,429 +0,0 @@
|
||||
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.
|
||||
@ -1,221 +0,0 @@
|
||||
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.
|
||||
@ -1,47 +0,0 @@
|
||||
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.
|
||||
@ -1,180 +0,0 @@
|
||||
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.
|
||||
@ -1,175 +0,0 @@
|
||||
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.
|
||||
@ -1,56 +0,0 @@
|
||||
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.
|
||||
Loading…
Reference in new issue