Compare commits
No commits in common. '4c5d54810bc939019f400cf51648df54860955f9' and '19bb4b82381e664e368cb5b21ed5a4f7233f4aae' have entirely different histories.
4c5d54810b
...
19bb4b8238
@ -1,321 +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 app_eq e1 e2 e3 e4:
|
|
||||||
(App e1 e2) = (App e3 e4) → e1 = e3 ∧ e2 = e4.
|
|
||||||
Proof.
|
|
||||||
|
|
||||||
intro h.
|
|
||||||
split.
|
|
||||||
injection h as hnm.
|
|
||||||
assumption.
|
|
||||||
injection h as hnm.
|
|
||||||
assumption.
|
|
||||||
Qed. *)
|
|
||||||
|
|
||||||
Lemma step_det e e' e'':
|
|
||||||
step e e' → step e e'' → e' = e''.
|
|
||||||
Proof.
|
|
||||||
intros H_step H_step'.
|
|
||||||
|
|
||||||
(*
|
|
||||||
`induction` here seems to introduce incorrect induction hypothesis for IH_λ, IH_v, IH_a, IH_b. Those try to prove that e' = e'', when I need them to prove other equalities later introduced by `inversion H_step`.
|
|
||||||
|
|
||||||
When swapping `inversion H_step` and `induction e`,
|
|
||||||
the number of things to prove jumps to 30, and I do not know how to quickly prove the incorrect ones.
|
|
||||||
`inversion e` doesn't introduce any induction hypothesis, so it is also out of the question.
|
|
||||||
*)
|
|
||||||
induction e as [
|
|
||||||
name |
|
|
||||||
name body |
|
|
||||||
e_λ IH_λ e_v IH_v |
|
|
||||||
n |
|
|
||||||
a IH_a b IH_b
|
|
||||||
].
|
|
||||||
- inversion H_step.
|
|
||||||
- inversion H_step.
|
|
||||||
- inversion H_step.
|
|
||||||
{
|
|
||||||
rewrite <-H in H_step'.
|
|
||||||
inversion H_step'.
|
|
||||||
- reflexivity.
|
|
||||||
- inversion H7.
|
|
||||||
- val_no_step.
|
|
||||||
}
|
|
||||||
{
|
|
||||||
inversion H_step'.
|
|
||||||
- rewrite <-H4 in H3.
|
|
||||||
inversion H3.
|
|
||||||
- admit.
|
|
||||||
- val_no_step.
|
|
||||||
}
|
|
||||||
{
|
|
||||||
inversion H_step'.
|
|
||||||
- val_no_step.
|
|
||||||
- val_no_step.
|
|
||||||
- admit.
|
|
||||||
}
|
|
||||||
- inversion H_step.
|
|
||||||
- inversion H_step.
|
|
||||||
{
|
|
||||||
rewrite <-H in H_step'.
|
|
||||||
rewrite <-H1 in H_step'.
|
|
||||||
inversion H_step'.
|
|
||||||
- rewrite <-H6.
|
|
||||||
rewrite <-H2.
|
|
||||||
reflexivity.
|
|
||||||
- val_no_step.
|
|
||||||
- val_no_step.
|
|
||||||
}
|
|
||||||
{
|
|
||||||
inversion H_step'.
|
|
||||||
- rewrite <-H4 in H3.
|
|
||||||
val_no_step.
|
|
||||||
- admit.
|
|
||||||
- val_no_step.
|
|
||||||
}
|
|
||||||
{
|
|
||||||
inversion H_step'.
|
|
||||||
- rewrite <-H5 in H2.
|
|
||||||
val_no_step.
|
|
||||||
- val_no_step.
|
|
||||||
- admit.
|
|
||||||
}
|
|
||||||
Admitted.
|
|
||||||
|
|
||||||
|
|
||||||
(** 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)
|
|
||||||
(* TODO: add more constructors *)
|
|
||||||
.
|
|
||||||
|
|
||||||
(* 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.
|
|
||||||
(* TODO: exercise *)
|
|
||||||
Admitted.
|
|
||||||
|
|
||||||
|
|
||||||
Lemma val_no_cbn_step e e':
|
|
||||||
cbn_step e e' → is_val e → False.
|
|
||||||
Proof.
|
|
||||||
(* TODO: exercise *)
|
|
||||||
Admitted.
|
|
||||||
|
|
||||||
|
|
||||||
(* 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.
|
|
||||||
(* TODO: exercise *)
|
|
||||||
Admitted.
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
(** 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.
|
|
||||||
(* TODO: exercise *)
|
|
||||||
Admitted.
|
|
||||||
|
|
||||||
Lemma rtc_transitive R : Transitive (rtc R).
|
|
||||||
Proof.
|
|
||||||
unfold Transitive.
|
|
||||||
(* TODO: exercise *)
|
|
||||||
Admitted.
|
|
||||||
|
|
||||||
|
|
||||||
Lemma rtc_subrel (R: X → X → Prop) (x y : X): R x y → rtc R x y.
|
|
||||||
Proof.
|
|
||||||
(* TODO: exercise *)
|
|
||||||
Admitted.
|
|
||||||
|
|
||||||
|
|
||||||
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.
|
|
||||||
Print rtc.
|
|
||||||
|
|
||||||
(* 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.
|
|
||||||
(* TODO: exercise *)
|
|
||||||
Admitted.
|
|
||||||
|
|
||||||
|
|
||||||
Lemma plus_left e1 e1' n:
|
|
||||||
rtc step e1 e1' → rtc step (Plus e1 (LitInt n)) (Plus e1' (LitInt n)).
|
|
||||||
Proof.
|
|
||||||
(* TODO: exercise *)
|
|
||||||
Admitted.
|
|
||||||
|
|
||||||
|
|
||||||
(* 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.
|
|
||||||
(* TODO: exercise *)
|
|
||||||
Admitted.
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
(* 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 *)
|
|
||||||
|
|
||||||
|
|
||||||
Lemma big_step_steps e v :
|
|
||||||
big_step e v → rtc step e (of_val v).
|
|
||||||
Proof.
|
|
||||||
(* TODO: exercise *)
|
|
||||||
Admitted.
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
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.
|
|
||||||
(* TODO: exercise *)
|
|
||||||
Admitted.
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
(** Exercise 6 (LN Exercise 5): left-to-right evaluation *)
|
|
||||||
Inductive ltr_step : expr → expr → Prop := .
|
|
||||||
|
|
||||||
#[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.
|
|
||||||
(* TODO: exercise *)
|
|
||||||
Admitted.
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Lemma big_step_ltr_steps e v :
|
|
||||||
big_step e v → rtc ltr_step e (of_val v).
|
|
||||||
Proof.
|
|
||||||
(* TODO: exercise *)
|
|
||||||
Admitted.
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Lemma ltr_steps_big_step e (v: val):
|
|
||||||
rtc ltr_step e v → big_step e v.
|
|
||||||
Proof.
|
|
||||||
(* TODO: exercise *)
|
|
||||||
Admitted.
|
|
@ -1,320 +0,0 @@
|
|||||||
From stdpp Require Export binders strings.
|
|
||||||
From stdpp Require Import options.
|
|
||||||
From semantics.lib Require Import maps.
|
|
||||||
|
|
||||||
(** * Simply Typed Lambda Calculus *)
|
|
||||||
|
|
||||||
(** ** Expressions and values. *)
|
|
||||||
(** [Z] is Coq's version of the integers.
|
|
||||||
All the standard operations, like [+], are defined on it.
|
|
||||||
|
|
||||||
The type [binder] is defined as [x ::= BNamed (s: string) | BAnon]
|
|
||||||
where BAnon can be used if we don't want to use the variable in
|
|
||||||
the function.
|
|
||||||
*)
|
|
||||||
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).
|
|
||||||
|
|
||||||
Inductive val :=
|
|
||||||
| LitIntV (n: Z)
|
|
||||||
| LamV (x : binder) (e : expr).
|
|
||||||
|
|
||||||
(* Injections into expr *)
|
|
||||||
Definition of_val (v : val) : expr :=
|
|
||||||
match v with
|
|
||||||
| LitIntV n => LitInt n
|
|
||||||
| LamV x e => Lam x e
|
|
||||||
end.
|
|
||||||
|
|
||||||
(* try to make an expr into a val *)
|
|
||||||
Definition to_val (e : expr) : option val :=
|
|
||||||
match e with
|
|
||||||
| LitInt n => Some (LitIntV n)
|
|
||||||
| Lam x e => Some (LamV x e)
|
|
||||||
| _ => None
|
|
||||||
end.
|
|
||||||
|
|
||||||
Lemma to_of_val v : to_val (of_val v) = Some v.
|
|
||||||
Proof.
|
|
||||||
destruct v; simpl; reflexivity.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma of_to_val e v : to_val e = Some v → of_val v = e.
|
|
||||||
Proof.
|
|
||||||
destruct e; simpl; try congruence.
|
|
||||||
all: injection 1 as <-; simpl; reflexivity.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
(* Inj is a type class for injective functions.
|
|
||||||
It is defined as:
|
|
||||||
[Inj R S f := ∀ x y, S (f x) (f y) → R x y]
|
|
||||||
*)
|
|
||||||
#[export] Instance of_val_inj : Inj (=) (=) of_val.
|
|
||||||
Proof. by intros ?? Hv; apply (inj Some); rewrite <-!to_of_val, Hv. Qed.
|
|
||||||
|
|
||||||
(* A predicate which holds true whenever an
|
|
||||||
expression is a value. *)
|
|
||||||
Definition is_val (e : expr) : Prop :=
|
|
||||||
match e with
|
|
||||||
| LitInt n => True
|
|
||||||
| Lam x e => True
|
|
||||||
| _ => False
|
|
||||||
end.
|
|
||||||
Lemma is_val_spec e : is_val e ↔ ∃ v, to_val e = Some v.
|
|
||||||
Proof.
|
|
||||||
destruct e; simpl.
|
|
||||||
(* naive_solver is an automation tactic like intuition, firstorder, auto, ...
|
|
||||||
It is provided by the stdpp library. *)
|
|
||||||
all: naive_solver.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
(* values are values *)
|
|
||||||
Lemma is_val_of_val v : is_val (of_val v).
|
|
||||||
Proof.
|
|
||||||
destruct v; simpl; done.
|
|
||||||
Restart.
|
|
||||||
apply is_val_spec. rewrite to_of_val. eauto.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Definition is_val_val := is_val_of_val.
|
|
||||||
|
|
||||||
(* A small tactic that simplifies handling values. *)
|
|
||||||
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.
|
|
||||||
|
|
||||||
(* we tell eauto to use the lemma is_val_of_val *)
|
|
||||||
#[global]
|
|
||||||
Hint Immediate is_val_of_val : core.
|
|
||||||
|
|
||||||
|
|
||||||
(** ** Operational Semantics *)
|
|
||||||
|
|
||||||
(** *** Substitution *)
|
|
||||||
Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
|
|
||||||
match e with
|
|
||||||
| LitInt n => LitInt n
|
|
||||||
(* The function [decide] can be used to decide propositions.
|
|
||||||
[decide P] is of type {P} + {¬ P}.
|
|
||||||
It can only be applied to propositions for which, by type class inference,
|
|
||||||
it can be determined that the proposition is decidable. *)
|
|
||||||
| 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)
|
|
||||||
end.
|
|
||||||
|
|
||||||
(* We lift substitution to binders. *)
|
|
||||||
Definition subst' (mx : binder) (es : expr) : expr → expr :=
|
|
||||||
match mx with BNamed x => subst x es | BAnon => id end.
|
|
||||||
|
|
||||||
|
|
||||||
(** *** Small-Step Semantics *)
|
|
||||||
(* We use right-to-left evaluation order,
|
|
||||||
which means in a binary term (e.g., e1 + e2),
|
|
||||||
the left side can only be reduced once the right
|
|
||||||
side is fully evaluated (i.e., is a value). *)
|
|
||||||
Inductive step : expr → expr → Prop :=
|
|
||||||
| StepBeta x e e' :
|
|
||||||
is_val e' →
|
|
||||||
step (App (Lam x e) e') (subst' x e' e)
|
|
||||||
| StepAppL e1 e1' e2 :
|
|
||||||
is_val e2 →
|
|
||||||
step e1 e1' →
|
|
||||||
step (App e1 e2) (App e1' e2)
|
|
||||||
| StepAppR e1 e2 e2' :
|
|
||||||
step e2 e2' →
|
|
||||||
step (App e1 e2) (App e1 e2')
|
|
||||||
| StepPlusRed (n1 n2 n3: Z) :
|
|
||||||
(n1 + n2)%Z = n3 →
|
|
||||||
step (Plus (LitInt n1) (LitInt n2)) (LitInt n3)
|
|
||||||
| StepPlusL e1 e1' e2 :
|
|
||||||
is_val e2 →
|
|
||||||
step e1 e1' →
|
|
||||||
step (Plus e1 e2) (Plus e1' e2)
|
|
||||||
| StepPlusR e1 e2 e2' :
|
|
||||||
step e2 e2' →
|
|
||||||
step (Plus e1 e2) (Plus e1 e2').
|
|
||||||
|
|
||||||
(* We make the tactic eauto aware of the constructors of [step].
|
|
||||||
Then it can automatically solve goals where we want to prove a step. *)
|
|
||||||
#[global] Hint Constructors step : core.
|
|
||||||
|
|
||||||
|
|
||||||
(* A term is reducible, if it can take a step. *)
|
|
||||||
Definition reducible (e : expr) :=
|
|
||||||
∃ e', step e e'.
|
|
||||||
|
|
||||||
|
|
||||||
(** *** Big-Step Semantics *)
|
|
||||||
Inductive big_step : expr → val → Prop :=
|
|
||||||
| bs_lit (n : Z) :
|
|
||||||
big_step (LitInt n) (LitIntV n)
|
|
||||||
| bs_lam (x : binder) (e : expr) :
|
|
||||||
big_step (Lam x e) (LamV x e)
|
|
||||||
| 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
|
|
||||||
.
|
|
||||||
#[export] Hint Constructors big_step : core.
|
|
||||||
|
|
||||||
|
|
||||||
Lemma big_step_vals (v: val): big_step (of_val v) v.
|
|
||||||
Proof.
|
|
||||||
induction v; econstructor.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma big_step_inv_vals (v w: val): big_step (of_val v) w → v = w.
|
|
||||||
Proof.
|
|
||||||
destruct v; inversion 1; eauto.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
|
|
||||||
(** *** Contextual Semantics *)
|
|
||||||
(** Base reduction *)
|
|
||||||
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).
|
|
||||||
|
|
||||||
Inductive ectx :=
|
|
||||||
| HoleCtx
|
|
||||||
| AppLCtx (K: ectx) (v2 : val)
|
|
||||||
| AppRCtx (e1 : expr) (K: ectx)
|
|
||||||
| PlusLCtx (K: ectx) (v2 : val)
|
|
||||||
| PlusRCtx (e1 : expr) (K: ectx).
|
|
||||||
|
|
||||||
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)
|
|
||||||
end.
|
|
||||||
|
|
||||||
(* filling a context with another context *)
|
|
||||||
Fixpoint comp_ectx (Ko Ki: ectx) :=
|
|
||||||
match Ko with
|
|
||||||
| HoleCtx => Ki
|
|
||||||
| AppLCtx K v2 => AppLCtx (comp_ectx K Ki) v2
|
|
||||||
| AppRCtx e1 K => AppRCtx e1 (comp_ectx K Ki)
|
|
||||||
| PlusLCtx K v2 => PlusLCtx (comp_ectx K Ki) v2
|
|
||||||
| PlusRCtx e1 K => PlusRCtx e1 (comp_ectx K Ki)
|
|
||||||
end.
|
|
||||||
|
|
||||||
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.
|
|
||||||
|
|
||||||
Definition contextual_reducible (e : expr) :=
|
|
||||||
∃ e', contextual_step e e'.
|
|
||||||
|
|
||||||
#[export] Hint Constructors base_step : core.
|
|
||||||
#[export] Hint Constructors contextual_step : core.
|
|
||||||
(* Lemmas about the contextual semantics *)
|
|
||||||
Definition empty_ectx := HoleCtx.
|
|
||||||
|
|
||||||
Lemma fill_empty e : fill empty_ectx e = e.
|
|
||||||
Proof. done. 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_comp (K1 K2 : ectx) e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e.
|
|
||||||
Proof. induction K1; simpl; congruence. 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.
|
|
||||||
|
|
||||||
|
|
||||||
(** Open and closed expressions *)
|
|
||||||
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
|
|
||||||
| App e1 e2
|
|
||||||
| Plus e1 e2 => is_closed X e1 && is_closed X e2
|
|
||||||
end.
|
|
||||||
|
|
||||||
Notation closed X e := (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.
|
|
||||||
|
|
||||||
Lemma closed_weaken X Y e : closed X e → X ⊆ Y → closed Y e.
|
|
||||||
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
|
|
||||||
|
|
||||||
Lemma closed_weaken_nil X e : closed [] e → closed X e.
|
|
||||||
Proof. intros. by apply closed_weaken with [], list_subseteq_nil. Qed.
|
|
||||||
|
|
||||||
Lemma closed_subst X Y e x es :
|
|
||||||
closed Y es → closed (x :: X) e → closed (X ++ Y) (subst x es e).
|
|
||||||
Proof.
|
|
||||||
induction e as [y|y e IH|e1 e2|n|e1 e2]in X |-*; simpl; intros Hc1 Hc2; eauto.
|
|
||||||
- eapply bool_decide_unpack, elem_of_cons in Hc2 as [->|Hc2].
|
|
||||||
+ destruct decide; try congruence. eapply closed_weaken; eauto with set_solver.
|
|
||||||
+ destruct decide.
|
|
||||||
* eapply closed_weaken; eauto with set_solver.
|
|
||||||
* simpl. eapply bool_decide_pack. set_solver.
|
|
||||||
- destruct y as [|y]; simpl in *; eauto.
|
|
||||||
destruct decide as [Heq|].
|
|
||||||
+ injection Heq as ->. eapply closed_weaken; eauto. set_solver.
|
|
||||||
+ rewrite app_comm_cons. eapply IH; eauto.
|
|
||||||
eapply closed_weaken; eauto. set_solver.
|
|
||||||
- eapply andb_True. eapply andb_True in Hc2 as [H1 H2].
|
|
||||||
split; eauto.
|
|
||||||
- eapply andb_True. eapply andb_True in Hc2 as [H1 H2].
|
|
||||||
split; eauto.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma closed_subst_nil X e x es :
|
|
||||||
closed [] es → closed (x :: X) e → closed X (subst x es e).
|
|
||||||
Proof.
|
|
||||||
intros Hc1 Hc2. eapply closed_subst in Hc1; eauto.
|
|
||||||
revert Hc1. rewrite right_id; [done|apply _].
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma closed_do_subst' X e x es :
|
|
||||||
closed [] es → closed (x :b: X) e → closed X (subst' x es e).
|
|
||||||
Proof. destruct x; eauto using closed_subst_nil. Qed.
|
|
||||||
|
|
||||||
Lemma subst_closed X e x es : 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_closed_nil e x es : closed [] e → subst x es e = e.
|
|
||||||
Proof. intros. apply subst_closed with []; set_solver. Qed.
|
|
@ -1,49 +0,0 @@
|
|||||||
From semantics.ts.stlc Require Export lang.
|
|
||||||
Set Default Proof Using "Type".
|
|
||||||
|
|
||||||
|
|
||||||
(* We declare two notation scopes, one for values and one for expressions.
|
|
||||||
Afterwards, we add notations to them, which then do not interfere with
|
|
||||||
any existing Coq notations. *)
|
|
||||||
Declare Scope expr_scope.
|
|
||||||
Declare Scope val_scope.
|
|
||||||
Delimit Scope expr_scope with E.
|
|
||||||
Delimit Scope val_scope with V.
|
|
||||||
Bind Scope expr_scope with expr.
|
|
||||||
Bind Scope val_scope with val.
|
|
||||||
|
|
||||||
(* Values can be embedded into expressions with of_val
|
|
||||||
and integers into expressions with LitInt. The following
|
|
||||||
coercions allow us to omit the embeddings. With them
|
|
||||||
(e1 v2 n3) desugars to (e3 (of_val v2) (LitInt n1)). *)
|
|
||||||
Coercion of_val : val >-> expr.
|
|
||||||
Coercion LitInt : Z >-> expr.
|
|
||||||
Coercion LitIntV : Z >-> val.
|
|
||||||
Coercion App : expr >-> Funclass.
|
|
||||||
Coercion Var : string >-> expr.
|
|
||||||
|
|
||||||
Notation "e1 + e2" := (Plus e1%E e2%E) : expr_scope.
|
|
||||||
|
|
||||||
(* The breaking point '/ ' makes sure that the body of the λ: is indented
|
|
||||||
by two spaces in case the whole λ: does not fit on a single line. *)
|
|
||||||
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)
|
|
||||||
(only parsing, 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.
|
|
@ -1,166 +0,0 @@
|
|||||||
(* Throughout the course, we will be using the [stdpp] library to provide
|
|
||||||
some useful and common features.
|
|
||||||
We will introduce you to its features as we need them.
|
|
||||||
*)
|
|
||||||
From stdpp Require Import base tactics numbers strings.
|
|
||||||
From stdpp Require relations.
|
|
||||||
From semantics.lib Require Import maps.
|
|
||||||
|
|
||||||
(** * Exercise sheet 0 *)
|
|
||||||
|
|
||||||
(* We are using Coq's notion of integers, [Z].
|
|
||||||
All the standard operations, like [+] and [*], are defined on it.
|
|
||||||
*)
|
|
||||||
Inductive expr :=
|
|
||||||
| Const (z : Z)
|
|
||||||
| Plus (e1 e2 : expr)
|
|
||||||
| Mul (e1 e2 : expr).
|
|
||||||
|
|
||||||
(** Exercise 1: Arithmetics *)
|
|
||||||
Fixpoint expr_eval (e : expr) : Z :=
|
|
||||||
match e with
|
|
||||||
| Const z => z
|
|
||||||
| Plus e1 e2 => (expr_eval e1) + (expr_eval e2)
|
|
||||||
| Mul e1 e2 => (expr_eval e1) * (expr_eval e2)
|
|
||||||
end.
|
|
||||||
|
|
||||||
(** Now let's define some notation to make it look nice! *)
|
|
||||||
(* We declare a so-called notation scope, so that we can still use the nice notations for addition on natural numbers [nat] and integers [Z]. *)
|
|
||||||
Declare Scope expr.
|
|
||||||
Delimit Scope expr with E.
|
|
||||||
Notation "e1 + e2" := (Plus e1%Z e2%Z) : expr.
|
|
||||||
Notation "e1 * e2" := (Mul e1%Z e2%Z) : expr.
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Lemma expr_eval_test: expr_eval (Plus (Const (-4)) (Const 5)) = 1%Z.
|
|
||||||
Proof.
|
|
||||||
(* should be solved by: simpl. lia. *)
|
|
||||||
simpl. lia.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma plus_eval_comm e1 e2 :
|
|
||||||
expr_eval (Plus e1 e2) = expr_eval (Plus e2 e1).
|
|
||||||
Proof.
|
|
||||||
simpl. lia.
|
|
||||||
Qed.
|
|
||||||
Lemma plus_syntax_not_comm :
|
|
||||||
Plus (Const 0) (Const 1) ≠ Plus (Const 1) (Const 0).
|
|
||||||
Proof.
|
|
||||||
(* [done] is an automation tactic provided by [stdpp] to solve simple goals. *)
|
|
||||||
intros Heq. injection Heq. done.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
(** Exercise 2: Open arithmetical expressions *)
|
|
||||||
|
|
||||||
(* Finally, we introduce variables into our arithmetic expressions.
|
|
||||||
Variables are of Coq's [string] type.
|
|
||||||
*)
|
|
||||||
Inductive expr' :=
|
|
||||||
| Var (x: string)
|
|
||||||
| Const' (z : Z)
|
|
||||||
| Plus' (e1 e2 : expr')
|
|
||||||
| Mul' (e1 e2 : expr').
|
|
||||||
|
|
||||||
(* We call an expression closed under the list X,
|
|
||||||
if it only contains variables in X *)
|
|
||||||
Fixpoint is_closed (X: list string) (e: expr') : bool :=
|
|
||||||
match e with
|
|
||||||
| Var x => bool_decide (x ∈ X)
|
|
||||||
| Const' z => true
|
|
||||||
| Plus' e1 e2 => is_closed X e1 && is_closed X e2
|
|
||||||
| Mul' e1 e2 => is_closed X e1 && is_closed X e2
|
|
||||||
end.
|
|
||||||
|
|
||||||
Definition closed X e := is_closed X e = true.
|
|
||||||
|
|
||||||
|
|
||||||
(* Some examples of closed terms. *)
|
|
||||||
Lemma example_no_vars_closed:
|
|
||||||
closed [] (Plus' (Const' 3) (Const' 5)).
|
|
||||||
Proof.
|
|
||||||
unfold closed. simpl. done.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
|
|
||||||
Lemma example_some_vars_closed:
|
|
||||||
closed ["x"; "y"] (Plus' (Var "x") (Var "y")).
|
|
||||||
Proof.
|
|
||||||
unfold closed. simpl. done.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma example_not_closed:
|
|
||||||
¬ closed ["x"] (Plus' (Var "x") (Var "y")).
|
|
||||||
Proof.
|
|
||||||
unfold closed. simpl. done.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma closed_mono X Y e:
|
|
||||||
X ⊆ Y → closed X e → closed Y e.
|
|
||||||
Proof.
|
|
||||||
unfold closed. intros Hsub; induction e as [ x | z | e1 IHe1 e2 IHe2 | e1 IHe1 e2 IHe2]; simpl.
|
|
||||||
- (* bool_decide is an stdpp function, which can be used to decide simple decidable propositions.
|
|
||||||
Make a search for it to find the right lemmas to complete this subgoal. *)
|
|
||||||
(* Search bool_decide. *)
|
|
||||||
intros ?%bool_decide_eq_true_1. eapply bool_decide_eq_true_2.
|
|
||||||
naive_solver.
|
|
||||||
- done.
|
|
||||||
- (* Locate the notation for && by typing: Locate "&&". Then search for the right lemmas.*)
|
|
||||||
intros [H1 H2]%andb_prop. rewrite IHe1, IHe2; done.
|
|
||||||
- intros [H1 H2]%andb_prop. rewrite IHe1, IHe2; done.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
(* we define a substitution operation on open expressions *)
|
|
||||||
Fixpoint subst (e: expr') (x: string) (e': expr') : expr' :=
|
|
||||||
match e with
|
|
||||||
| Var y => if (bool_decide (x = y)) then e' else Var y
|
|
||||||
| Const' z => Const' z
|
|
||||||
| Plus' e1 e2 => Plus' (subst e1 x e') (subst e2 x e')
|
|
||||||
| Mul' e1 e2 => Mul' (subst e1 x e') (subst e2 x e')
|
|
||||||
end.
|
|
||||||
|
|
||||||
Lemma subst_closed e e' x X:
|
|
||||||
closed X e → ¬ (x ∈ X) → subst e x e' = e.
|
|
||||||
Proof.
|
|
||||||
unfold closed. induction e as [ y | z | e1 IHe1 e2 IHe2 | e1 IHe1 e2 IHe2]; simpl.
|
|
||||||
- intros Hel%bool_decide_eq_true_1 Hnel.
|
|
||||||
destruct bool_decide eqn: Heq.
|
|
||||||
+ eapply bool_decide_eq_true_1 in Heq. subst.
|
|
||||||
congruence.
|
|
||||||
+ done.
|
|
||||||
- done.
|
|
||||||
- intros [Hcl1 Hcl2]%andb_prop Hnel.
|
|
||||||
rewrite IHe1; eauto.
|
|
||||||
rewrite IHe2; eauto.
|
|
||||||
- intros [Hcl1 Hcl2]%andb_prop Hnel.
|
|
||||||
rewrite IHe1; eauto.
|
|
||||||
rewrite IHe2; eauto.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
(* To evaluate an arithmetic expression, we define an evaluation function [expr_eval], which maps them to integers.
|
|
||||||
Since our expressions contain variables, we pass a finite map as the argument, which is used to look up variables.
|
|
||||||
The type of finite maps that we use is called [gmap].
|
|
||||||
*)
|
|
||||||
Fixpoint expr_eval' (m: gmap string Z) (e : expr') : Z :=
|
|
||||||
match e with
|
|
||||||
| Var x => default 0%Z (m !! x) (* this is the lookup operation on gmaps *)
|
|
||||||
| Const' z => z
|
|
||||||
| Plus' e1 e2 => (expr_eval' m e1) + (expr_eval' m e2)
|
|
||||||
| Mul' e1 e2 => (expr_eval' m e1) * (expr_eval' m e2)
|
|
||||||
end.
|
|
||||||
|
|
||||||
(* Prove the following lemma which explains how substitution interacts with evaluation *)
|
|
||||||
Lemma eval_subst_extend (m: gmap string Z) e x e':
|
|
||||||
expr_eval' m (subst e x e') = expr_eval' (<[x := expr_eval' m e']> m) e.
|
|
||||||
Proof.
|
|
||||||
induction e as [ y | z | e1 IHe1 e2 IHe2 | e1 IHe1 e2 IHe2]; simpl.
|
|
||||||
- destruct bool_decide eqn: Heq.
|
|
||||||
+ eapply bool_decide_eq_true_1 in Heq. subst.
|
|
||||||
rewrite lookup_insert. done.
|
|
||||||
+ eapply bool_decide_eq_false_1 in Heq.
|
|
||||||
rewrite lookup_insert_ne; [|done].
|
|
||||||
simpl. done.
|
|
||||||
- done.
|
|
||||||
- rewrite IHe1, IHe2. done.
|
|
||||||
- rewrite IHe1, IHe2. done.
|
|
||||||
Qed.
|
|
Loading…
Reference in new issue