Commit 82c06c8e authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents f4f496b8 8ca359a5
Pipeline #224 passed with stage
...@@ -206,7 +206,7 @@ Proof. ...@@ -206,7 +206,7 @@ Proof.
apply exist_elim=>γ. rewrite !sep_exist_r. apply exist_elim=>P. apply exist_elim=>γ. rewrite !sep_exist_r. apply exist_elim=>P.
rewrite !sep_exist_r. apply exist_elim=>Q. rewrite !sep_exist_r. rewrite !sep_exist_r. apply exist_elim=>Q. rewrite !sep_exist_r.
apply exist_elim=>i. rewrite -!assoc. apply const_elim_sep_l=>?. apply exist_elim=>i. rewrite -!assoc. apply const_elim_sep_l=>?.
wp_focus (! _)%L. wp_focus (! _)%E.
(* I think some evars here are better than repeating *everything* *) (* I think some evars here are better than repeating *everything* *)
eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl; eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
eauto with I ndisj. eauto with I ndisj.
......
...@@ -19,10 +19,6 @@ Inductive binder := BAnon | BNamed : string → binder. ...@@ -19,10 +19,6 @@ Inductive binder := BAnon | BNamed : string → binder.
Delimit Scope binder_scope with binder. Delimit Scope binder_scope with binder.
Bind Scope binder_scope with binder. Bind Scope binder_scope with binder.
Delimit Scope lang_scope with L.
Bind Scope lang_scope with base_lit.
Delimit Scope val_scope with V.
Bind Scope val_scope with base_lit.
Inductive expr := Inductive expr :=
(* Base lambda calculus *) (* Base lambda calculus *)
...@@ -51,6 +47,9 @@ Inductive expr := ...@@ -51,6 +47,9 @@ Inductive expr :=
| Store (e1 : expr) (e2 : expr) | Store (e1 : expr) (e2 : expr)
| Cas (e0 : expr) (e1 : expr) (e2 : expr). | Cas (e0 : expr) (e1 : expr) (e2 : expr).
Bind Scope expr_scope with expr.
Delimit Scope expr_scope with E.
Inductive val := Inductive val :=
| RecV (f x : binder) (e : expr) (* e should be closed *) | RecV (f x : binder) (e : expr) (* e should be closed *)
| LitV (l : base_lit) | LitV (l : base_lit)
...@@ -59,9 +58,8 @@ Inductive val := ...@@ -59,9 +58,8 @@ Inductive val :=
| InjRV (v : val) | InjRV (v : val)
| LocV (l : loc). | LocV (l : loc).
Bind Scope binder_scope with expr. Bind Scope val_scope with val.
Bind Scope lang_scope with expr base_lit. Delimit Scope val_scope with V.
Bind Scope val_scope with val base_lit.
Global Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2). Global Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
Proof. solve_decision. Defined. Proof. solve_decision. Defined.
...@@ -293,12 +291,12 @@ Qed. ...@@ -293,12 +291,12 @@ Qed.
Lemma fill_not_val K e : to_val e = None to_val (fill K e) = None. Lemma fill_not_val K e : to_val e = None to_val (fill K e) = None.
Proof. rewrite !eq_None_not_Some; eauto using fill_val. Qed. Proof. rewrite !eq_None_not_Some; eauto using fill_val. Qed.
Lemma values_head_stuck e1 σ1 e2 σ2 ef : Lemma val_head_stuck e1 σ1 e2 σ2 ef :
head_step e1 σ1 e2 σ2 ef to_val e1 = None. head_step e1 σ1 e2 σ2 ef to_val e1 = None.
Proof. destruct 1; naive_solver. Qed. Proof. destruct 1; naive_solver. Qed.
Lemma values_stuck e1 σ1 e2 σ2 ef : prim_step e1 σ1 e2 σ2 ef to_val e1 = None. Lemma val_stuck e1 σ1 e2 σ2 ef : prim_step e1 σ1 e2 σ2 ef to_val e1 = None.
Proof. intros [??? -> -> ?]; eauto using fill_not_val, values_head_stuck. Qed. Proof. intros [??? -> -> ?]; eauto using fill_not_val, val_head_stuck. Qed.
Lemma atomic_not_val e : atomic e to_val e = None. Lemma atomic_not_val e : atomic e to_val e = None.
Proof. destruct e; naive_solver. Qed. Proof. destruct e; naive_solver. Qed.
...@@ -326,7 +324,7 @@ Lemma atomic_step e1 σ1 e2 σ2 ef : ...@@ -326,7 +324,7 @@ Lemma atomic_step e1 σ1 e2 σ2 ef :
atomic e1 prim_step e1 σ1 e2 σ2 ef is_Some (to_val e2). atomic e1 prim_step e1 σ1 e2 σ2 ef is_Some (to_val e2).
Proof. Proof.
intros Hatomic [K e1' e2' -> -> Hstep]. intros Hatomic [K e1' e2' -> -> Hstep].
assert (K = []) as -> by eauto 10 using atomic_fill, values_head_stuck. assert (K = []) as -> by eauto 10 using atomic_fill, val_head_stuck.
naive_solver eauto using atomic_head_step. naive_solver eauto using atomic_head_step.
Qed. Qed.
...@@ -357,7 +355,7 @@ Proof. ...@@ -357,7 +355,7 @@ Proof.
{ exfalso; apply (eq_None_not_Some (to_val (fill K e1))); { exfalso; apply (eq_None_not_Some (to_val (fill K e1)));
eauto using fill_not_val, head_ctx_step_val. } eauto using fill_not_val, head_ctx_step_val. }
cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|]. cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|].
eauto using fill_item_no_val_inj, values_head_stuck, fill_not_val. eauto using fill_item_no_val_inj, val_head_stuck, fill_not_val.
Qed. Qed.
Lemma alloc_fresh e v σ : Lemma alloc_fresh e v σ :
...@@ -373,7 +371,7 @@ Program Canonical Structure heap_lang : language := {| ...@@ -373,7 +371,7 @@ Program Canonical Structure heap_lang : language := {|
atomic := heap_lang.atomic; prim_step := heap_lang.prim_step; atomic := heap_lang.atomic; prim_step := heap_lang.prim_step;
|}. |}.
Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val, Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
heap_lang.values_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step. heap_lang.val_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step.
Global Instance heap_lang_ctx K : LanguageCtx heap_lang (heap_lang.fill K). Global Instance heap_lang_ctx K : LanguageCtx heap_lang (heap_lang.fill K).
Proof. Proof.
......
From heap_lang Require Export derived. From heap_lang Require Export derived.
Arguments wp {_ _} _ _%L _. Arguments wp {_ _} _ _%E _.
Notation "|| e @ E {{ Φ } }" := (wp E e%L Φ) Notation "|| e @ E {{ Φ } }" := (wp E e%E Φ)
(at level 20, e, Φ at level 200, (at level 20, e, Φ at level 200,
format "|| e @ E {{ Φ } }") : uPred_scope. format "|| e @ E {{ Φ } }") : uPred_scope.
Notation "|| e {{ Φ } }" := (wp e%L Φ) Notation "|| e {{ Φ } }" := (wp e%E Φ)
(at level 20, e, Φ at level 200, (at level 20, e, Φ at level 200,
format "|| e {{ Φ } }") : uPred_scope. format "|| e {{ Φ } }") : uPred_scope.
...@@ -19,72 +19,71 @@ Coercion of_val : val >-> expr. ...@@ -19,72 +19,71 @@ Coercion of_val : val >-> expr.
Coercion BNamed : string >-> binder. Coercion BNamed : string >-> binder.
Notation "<>" := BAnon : binder_scope. Notation "<>" := BAnon : binder_scope.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
(* No scope, does not conflict and scope is often not inferred properly. *) (* No scope, does not conflict and scope is often not inferred properly. *)
Notation "# l" := (LitV l%Z%V) (at level 8, format "# l"). Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
Notation "% l" := (LocV l) (at level 8, format "% l"). Notation "% l" := (LocV l) (at level 8, format "% l").
Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : lang_scope. (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope.
Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" := Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
(Match e0 x1 e1 x2 e2) (Match e0 x1 e1 x2 e2)
(e0, x1, e1, x2, e2 at level 200) : lang_scope. (e0, x1, e1, x2, e2 at level 200) : expr_scope.
Notation "()" := LitUnit : val_scope. Notation "()" := LitUnit : val_scope.
Notation "! e" := (Load e%L) (at level 9, right associativity) : lang_scope. Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope.
Notation "'ref' e" := (Alloc e%L) Notation "'ref' e" := (Alloc e%E)
(at level 30, right associativity) : lang_scope. (at level 30, right associativity) : expr_scope.
Notation "- e" := (UnOp MinusUnOp e%L) Notation "- e" := (UnOp MinusUnOp e%E)
(at level 35, right associativity) : lang_scope. (at level 35, right associativity) : expr_scope.
Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L) Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E)
(at level 50, left associativity) : lang_scope. (at level 50, left associativity) : expr_scope.
Notation "e1 - e2" := (BinOp MinusOp e1%L e2%L) Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E)
(at level 50, left associativity) : lang_scope. (at level 50, left associativity) : expr_scope.
Notation "e1 ≤ e2" := (BinOp LeOp e1%L e2%L) (at level 70) : lang_scope. Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E) (at level 70) : expr_scope.
Notation "e1 < e2" := (BinOp LtOp e1%L e2%L) (at level 70) : lang_scope. Notation "e1 < e2" := (BinOp LtOp e1%E e2%E) (at level 70) : expr_scope.
Notation "e1 = e2" := (BinOp EqOp e1%L e2%L) (at level 70) : lang_scope. Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) (at level 70) : expr_scope.
Notation "~ e" := (UnOp NegOp e%L) (at level 75, right associativity) : lang_scope. Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.
(* The unicode ← is already part of the notation "_ ← _; _" for bind. *) (* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
Notation "e1 <- e2" := (Store e1%L e2%L) (at level 80) : lang_scope. Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
Notation "'rec:' f x := e" := (Rec f x e%L) Notation "'rec:' f x := e" := (Rec f x e%E)
(at level 102, f at level 1, x at level 1, e at level 200) : lang_scope. (at level 102, f at level 1, x at level 1, e at level 200) : expr_scope.
Notation "'rec:' f x := e" := (RecV f x e%L) Notation "'rec:' f x := e" := (RecV f x e%E)
(at level 102, f at level 1, x at level 1, e at level 200) : val_scope. (at level 102, f at level 1, x at level 1, e at level 200) : val_scope.
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L) Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
(at level 200, e1, e2, e3 at level 200) : lang_scope. (at level 200, e1, e2, e3 at level 200) : expr_scope.
(** Derived notions, in order of declaration. The notations for let and seq (** Derived notions, in order of declaration. The notations for let and seq
are stated explicitly instead of relying on the Notations Let and Seq as are stated explicitly instead of relying on the Notations Let and Seq as
defined above. This is needed because App is now a coercion, and these defined above. This is needed because App is now a coercion, and these
notations are otherwise not pretty printed back accordingly. *) notations are otherwise not pretty printed back accordingly. *)
Notation "λ: x , e" := (Lam x e%L) Notation "λ: x , e" := (Lam x e%E)
(at level 102, x at level 1, e at level 200) : lang_scope. (at level 102, x at level 1, e at level 200) : expr_scope.
Notation "λ: x , e" := (LamV x e%L) Notation "λ: x , e" := (LamV x e%E)
(at level 102, x at level 1, e at level 200) : val_scope. (at level 102, x at level 1, e at level 200) : val_scope.
Notation "'let:' x := e1 'in' e2" := (Lam x e2%L e1%L) Notation "'let:' x := e1 'in' e2" := (Lam x e2%E e1%E)
(at level 102, x at level 1, e1, e2 at level 200) : lang_scope. (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
Notation "e1 ;; e2" := (Lam BAnon e2%L e1%L) Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
(at level 100, e2 at level 200, format "e1 ;; e2") : lang_scope. (at level 100, e2 at level 200, format "e1 ;; e2") : expr_scope.
(* These are not actually values, but we want them to be pretty-printed. *) (* These are not actually values, but we want them to be pretty-printed. *)
Notation "'let:' x := e1 'in' e2" := (LamV x e2%L e1%L) Notation "'let:' x := e1 'in' e2" := (LamV x e2%E e1%E)
(at level 102, x at level 1, e1, e2 at level 200) : val_scope. (at level 102, x at level 1, e1, e2 at level 200) : val_scope.
Notation "e1 ;; e2" := (LamV BAnon e2%L e1%L) Notation "e1 ;; e2" := (LamV BAnon e2%E e1%E)
(at level 100, e2 at level 200, format "e1 ;; e2") : val_scope. (at level 100, e2 at level 200, format "e1 ;; e2") : val_scope.
Notation "'rec:' f x y := e" := (Rec f x (Lam y e%L)) Notation "'rec:' f x y := e" := (Rec f x (Lam y e%E))
(at level 102, f, x, y at level 1, e at level 200) : lang_scope. (at level 102, f, x, y at level 1, e at level 200) : expr_scope.
Notation "'rec:' f x y := e" := (RecV f x (Lam y e%L)) Notation "'rec:' f x y := e" := (RecV f x (Lam y e%E))
(at level 102, f, x, y at level 1, e at level 200) : val_scope. (at level 102, f, x, y at level 1, e at level 200) : val_scope.
Notation "'rec:' f x y z := e" := (Rec f x (Lam y (Lam z e%L))) Notation "'rec:' f x y z := e" := (Rec f x (Lam y (Lam z e%E)))
(at level 102, f, x, y, z at level 1, e at level 200) : lang_scope. (at level 102, f, x, y, z at level 1, e at level 200) : expr_scope.
Notation "'rec:' f x y z := e" := (RecV f x (Lam y (Lam z e%L))) Notation "'rec:' f x y z := e" := (RecV f x (Lam y (Lam z e%E)))
(at level 102, f, x, y, z at level 1, e at level 200) : val_scope. (at level 102, f, x, y, z at level 1, e at level 200) : val_scope.
Notation "λ: x y , e" := (Lam x (Lam y e%L)) Notation "λ: x y , e" := (Lam x (Lam y e%E))
(at level 102, x, y at level 1, e at level 200) : lang_scope. (at level 102, x, y at level 1, e at level 200) : expr_scope.
Notation "λ: x y , e" := (LamV x (Lam y e%L)) Notation "λ: x y , e" := (LamV x (Lam y e%E))
(at level 102, x, y at level 1, e at level 200) : val_scope. (at level 102, x, y at level 1, e at level 200) : val_scope.
Notation "λ: x y z , e" := (Lam x (Lam y (Lam z e%L))) Notation "λ: x y z , e" := (Lam x (Lam y (Lam z e%E)))
(at level 102, x, y, z at level 1, e at level 200) : lang_scope. (at level 102, x, y, z at level 1, e at level 200) : expr_scope.
Notation "λ: x y z , e" := (LamV x (Lam y (Lam z e%L))) Notation "λ: x y z , e" := (LamV x (Lam y (Lam z e%E)))
(at level 102, x, y, z at level 1, e at level 200) : val_scope. (at level 102, x, y, z at level 1, e at level 200) : val_scope.
...@@ -19,7 +19,7 @@ Ltac inv_step := ...@@ -19,7 +19,7 @@ Ltac inv_step :=
simpl in H; first [subst e|discriminate H|injection H as H] simpl in H; first [subst e|discriminate H|injection H as H]
(* ensure that we make progress for each subgoal *) (* ensure that we make progress for each subgoal *)
| H : head_step ?e _ _ _ _, Hv : of_val ?v = fill ?K ?e |- _ => | H : head_step ?e _ _ _ _, Hv : of_val ?v = fill ?K ?e |- _ =>
apply values_head_stuck, (fill_not_val K) in H; apply val_head_stuck, (fill_not_val K) in H;
by rewrite -Hv to_of_val in H (* maybe use a helper lemma here? *) by rewrite -Hv to_of_val in H (* maybe use a helper lemma here? *)
| H : head_step ?e _ _ _ _ |- _ => | H : head_step ?e _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if e is a variable try (is_var e; fail 1); (* inversion yields many goals if e is a variable
......
...@@ -4,7 +4,7 @@ From heap_lang Require Import wp_tactics heap notation. ...@@ -4,7 +4,7 @@ From heap_lang Require Import wp_tactics heap notation.
Import uPred. Import uPred.
Section LangTests. Section LangTests.
Definition add := (#21 + #21)%L. Definition add := (#21 + #21)%E.
Goal σ, prim_step add σ (#42) σ None. Goal σ, prim_step add σ (#42) σ None.
Proof. intros; do_step done. Qed. Proof. intros; do_step done. Qed.
Definition rec_app : expr := ((rec: "f" "x" := "f" "x") #0). Definition rec_app : expr := ((rec: "f" "x" := "f" "x") #0).
...@@ -14,7 +14,7 @@ Section LangTests. ...@@ -14,7 +14,7 @@ Section LangTests.
by eapply (Ectx_step _ _ _ _ _ []), (BetaS _ _ _ _ #0). by eapply (Ectx_step _ _ _ _ _ []), (BetaS _ _ _ _ #0).
Qed. Qed.
Definition lam : expr := λ: "x", "x" + #21. Definition lam : expr := λ: "x", "x" + #21.
Goal σ, prim_step (lam #21)%L σ add σ None. Goal σ, prim_step (lam #21)%E σ add σ None.
Proof. Proof.
intros. rewrite /lam. (* FIXME: do_step does not work here *) intros. rewrite /lam. (* FIXME: do_step does not work here *)
by eapply (Ectx_step _ _ _ _ _ []), (BetaS <> "x" ("x" + #21) _ #21). by eapply (Ectx_step _ _ _ _ _ []), (BetaS <> "x" ("x" + #21) _ #21).
......
...@@ -33,7 +33,7 @@ Proof. ...@@ -33,7 +33,7 @@ Proof.
(Φ&Φs2&r&rs2&->&->&Hwp&?)%Forall3_cons_inv_l)%Forall3_app_inv_l ?. (Φ&Φs2&r&rs2&->&->&Hwp&?)%Forall3_cons_inv_l)%Forall3_app_inv_l ?.
rewrite wp_eq in Hwp. rewrite wp_eq in Hwp.
destruct (wp_step_inv Φ e1 (k + n) (S (k + n)) σ1 r destruct (wp_step_inv Φ e1 (k + n) (S (k + n)) σ1 r
(big_op (rs1 ++ rs2))) as [_ Hwpstep]; eauto using values_stuck. (big_op (rs1 ++ rs2))) as [_ Hwpstep]; eauto using val_stuck.
{ by rewrite right_id_L -big_op_cons Permutation_middle. } { by rewrite right_id_L -big_op_cons Permutation_middle. }
destruct (Hwpstep e2 σ2 ef) as (r2&r2'&Hwsat&?&?); auto; clear Hwpstep. destruct (Hwpstep e2 σ2 ef) as (r2&r2'&Hwsat&?&?); auto; clear Hwpstep.
revert Hwsat; rewrite big_op_app right_id_L=>Hwsat. revert Hwsat; rewrite big_op_app right_id_L=>Hwsat.
......
...@@ -10,7 +10,7 @@ Structure language := Language { ...@@ -10,7 +10,7 @@ Structure language := Language {
prim_step : expr state expr state option expr Prop; prim_step : expr state expr state option expr Prop;
to_of_val v : to_val (of_val v) = Some v; to_of_val v : to_val (of_val v) = Some v;
of_to_val e v : to_val e = Some v of_val v = e; of_to_val e v : to_val e = Some v of_val v = e;
values_stuck e σ e' σ' ef : prim_step e σ e' σ' ef to_val e = None; val_stuck e σ e' σ' ef : prim_step e σ e' σ' ef to_val e = None;
atomic_not_val e : atomic e to_val e = None; atomic_not_val e : atomic e to_val e = None;
atomic_step e1 σ1 e2 σ2 ef : atomic_step e1 σ1 e2 σ2 ef :
atomic e1 atomic e1
...@@ -23,7 +23,7 @@ Arguments atomic {_} _. ...@@ -23,7 +23,7 @@ Arguments atomic {_} _.
Arguments prim_step {_} _ _ _ _ _. Arguments prim_step {_} _ _ _ _ _.
Arguments to_of_val {_} _. Arguments to_of_val {_} _.
Arguments of_to_val {_} _ _ _. Arguments of_to_val {_} _ _ _.
Arguments values_stuck {_} _ _ _ _ _ _. Arguments val_stuck {_} _ _ _ _ _ _.
Arguments atomic_not_val {_} _ _. Arguments atomic_not_val {_} _ _.
Arguments atomic_step {_} _ _ _ _ _ _ _. Arguments atomic_step {_} _ _ _ _ _ _ _.
...@@ -45,7 +45,7 @@ Section language. ...@@ -45,7 +45,7 @@ Section language.
step ρ1 ρ2. step ρ1 ρ2.
Lemma reducible_not_val e σ : reducible e σ to_val e = None. Lemma reducible_not_val e σ : reducible e σ to_val e = None.
Proof. intros (?&?&?&?); eauto using values_stuck. Qed. Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
Lemma atomic_of_val v : ¬atomic (of_val v). Lemma atomic_of_val v : ¬atomic (of_val v).
Proof. by intros Hat%atomic_not_val; rewrite to_of_val in Hat. Qed. Proof. by intros Hat%atomic_not_val; rewrite to_of_val in Hat. Qed.
Global Instance: Inj (=) (=) (@of_val Λ). Global Instance: Inj (=) (=) (@of_val Λ).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment