commit
f11abd824e
@ -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.
|
Loading…
Reference in new issue