Commit 3bed085d authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'master' into gen_proofmode

parents 7ae0b644 891cbf51
...@@ -11,5 +11,5 @@ install: [make "install"] ...@@ -11,5 +11,5 @@ install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [ depends: [
"coq" { (>= "8.7.1" & < "8.9~") | (= "dev") } "coq" { (>= "8.7.1" & < "8.9~") | (= "dev") }
"coq-stdpp" { (= "dev.2018-05-23.0.a8f65af5") | (= "dev") } "coq-stdpp" { (= "dev.2018-05-24.0.de797b31") | (= "dev") }
] ]
...@@ -68,7 +68,7 @@ Lemma wp_lift_atomic_head_step {s E Φ} e1 : ...@@ -68,7 +68,7 @@ Lemma wp_lift_atomic_head_step {s E Φ} e1 :
head_reducible e1 σ1 head_reducible e1 σ1
e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={E}= e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={E}=
state_interp σ2 state_interp σ2
default False (to_val e2) Φ [ list] ef efs, WP ef @ s; {{ _, True }}) from_option Φ False (to_val e2) [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}. WP e1 @ s; E {{ Φ }}.
Proof. Proof.
iIntros (?) "H". iApply wp_lift_atomic_step; eauto. iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
...@@ -82,7 +82,7 @@ Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 : ...@@ -82,7 +82,7 @@ Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
( σ1, state_interp σ1 ={E}= ( σ1, state_interp σ1 ={E}=
head_reducible e1 σ1 head_reducible e1 σ1
e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={E}= e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={E}=
efs = [] state_interp σ2 default False (to_val e2) Φ) efs = [] state_interp σ2 from_option Φ False (to_val e2))
WP e1 @ s; E {{ Φ }}. WP e1 @ s; E {{ Φ }}.
Proof. Proof.
iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto. iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
......
...@@ -71,7 +71,7 @@ Lemma wp_lift_atomic_step {s E Φ} e1 : ...@@ -71,7 +71,7 @@ Lemma wp_lift_atomic_step {s E Φ} e1 :
if s is NotStuck then reducible e1 σ1 else True if s is NotStuck then reducible e1 σ1 else True
e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={E}= e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={E}=
state_interp σ2 state_interp σ2
default False (to_val e2) Φ [ list] ef efs, WP ef @ s; {{ _, True }}) from_option Φ False (to_val e2) [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}. WP e1 @ s; E {{ Φ }}.
Proof. Proof.
iIntros (?) "H". iApply (wp_lift_step s E _ e1)=>//; iIntros (σ1) "Hσ1". iIntros (?) "H". iApply (wp_lift_step s E _ e1)=>//; iIntros (σ1) "Hσ1".
......
...@@ -138,7 +138,7 @@ Section lifting. ...@@ -138,7 +138,7 @@ Section lifting.
Lemma ownP_lift_atomic_step {s E Φ} e1 σ1 : Lemma ownP_lift_atomic_step {s E Φ} e1 σ1 :
(if s is NotStuck then reducible e1 σ1 else to_val e1 = None) (if s is NotStuck then reducible e1 σ1 else to_val e1 = None)
( ownP σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs - ownP σ2 - ( ownP σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs - ownP σ2 -
default False (to_val e2) Φ [ list] ef efs, WP ef @ s; {{ _, True }}) from_option Φ False (to_val e2) [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}. WP e1 @ s; E {{ Φ }}.
Proof. Proof.
iIntros (?) "[Hσ H]"; iApply ownP_lift_step. iIntros (?) "[Hσ H]"; iApply ownP_lift_step.
...@@ -240,7 +240,7 @@ Section ectx_lifting. ...@@ -240,7 +240,7 @@ Section ectx_lifting.
head_reducible e1 σ1 head_reducible e1 σ1
ownP σ1 ( e2 σ2 efs, ownP σ1 ( e2 σ2 efs,
head_step e1 σ1 e2 σ2 efs - ownP σ2 - head_step e1 σ1 e2 σ2 efs - ownP σ2 -
default False (to_val e2) Φ [ list] ef efs, WP ef @ s; {{ _, True }}) from_option Φ False (to_val e2) [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}. WP e1 @ s; E {{ Φ }}.
Proof. Proof.
iIntros (?) "[? H]". iApply ownP_lift_atomic_step; eauto. iIntros (?) "[? H]". iApply ownP_lift_atomic_step; eauto.
......
...@@ -43,7 +43,7 @@ Lemma twp_lift_atomic_head_step {s E Φ} e1 : ...@@ -43,7 +43,7 @@ Lemma twp_lift_atomic_head_step {s E Φ} e1 :
head_reducible e1 σ1 head_reducible e1 σ1
e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={E}= e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={E}=
state_interp σ2 state_interp σ2
default False (to_val e2) Φ [ list] ef efs, WP ef @ s; [{ _, True }]) from_option Φ False (to_val e2) [ list] ef efs, WP ef @ s; [{ _, True }])
WP e1 @ s; E [{ Φ }]. WP e1 @ s; E [{ Φ }].
Proof. Proof.
iIntros (?) "H". iApply twp_lift_atomic_step; eauto. iIntros (?) "H". iApply twp_lift_atomic_step; eauto.
...@@ -56,7 +56,7 @@ Lemma twp_lift_atomic_head_step_no_fork {s E Φ} e1 : ...@@ -56,7 +56,7 @@ Lemma twp_lift_atomic_head_step_no_fork {s E Φ} e1 :
( σ1, state_interp σ1 ={E}= ( σ1, state_interp σ1 ={E}=
head_reducible e1 σ1 head_reducible e1 σ1
e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={E}= e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={E}=
efs = [] state_interp σ2 default False (to_val e2) Φ) efs = [] state_interp σ2 from_option Φ False (to_val e2))
WP e1 @ s; E [{ Φ }]. WP e1 @ s; E [{ Φ }].
Proof. Proof.
iIntros (?) "H". iApply twp_lift_atomic_head_step; eauto. iIntros (?) "H". iApply twp_lift_atomic_head_step; eauto.
......
...@@ -45,7 +45,7 @@ Lemma twp_lift_atomic_step {s E Φ} e1 : ...@@ -45,7 +45,7 @@ Lemma twp_lift_atomic_step {s E Φ} e1 :
if s is NotStuck then reducible e1 σ1 else True if s is NotStuck then reducible e1 σ1 else True
e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={E}= e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={E}=
state_interp σ2 state_interp σ2
default False (to_val e2) Φ [ list] ef efs, WP ef @ s; [{ _, True }]) from_option Φ False (to_val e2) [ list] ef efs, WP ef @ s; [{ _, True }])
WP e1 @ s; E [{ Φ }]. WP e1 @ s; E [{ Φ }].
Proof. Proof.
iIntros (?) "H". iApply (twp_lift_step _ E _ e1)=>//; iIntros (σ1) "Hσ1". iIntros (?) "H". iApply (twp_lift_step _ E _ e1)=>//; iIntros (σ1) "Hσ1".
......
...@@ -526,7 +526,7 @@ Hint Mode IntoInv + ! - : typeclass_instances. ...@@ -526,7 +526,7 @@ Hint Mode IntoInv + ! - : typeclass_instances.
instances to recognize the [emp] case and make it look nicer. *) instances to recognize the [emp] case and make it look nicer. *)
Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP PROP) Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP PROP)
(α β : X PROP) (mγ : X option PROP) : PROP := (α β : X PROP) (mγ : X option PROP) : PROP :=
M1 ( x, α x (β x - M2 (default emp (mγ x) id)))%I. M1 ( x, α x (β x - M2 (from_option id emp (mγ x))))%I.
(* Typeclass for assertions around which accessors can be elliminated. (* Typeclass for assertions around which accessors can be elliminated.
Inputs: [Q], [E1], [E2], [α], [β], [γ] Inputs: [Q], [E1], [E2], [α], [β], [γ]
...@@ -582,7 +582,7 @@ Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances. ...@@ -582,7 +582,7 @@ Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
Class ElimInv {PROP : bi} {X : Type} (φ : Prop) Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
(Pinv Pin : PROP) (Pout : X PROP) (mPclose : option (X PROP)) (Pinv Pin : PROP) (Pout : X PROP) (mPclose : option (X PROP))
(Q : PROP) (Q' : X PROP) := (Q : PROP) (Q' : X PROP) :=
elim_inv : φ Pinv Pin ( x, Pout x (default (λ _, emp) mPclose id) x - Q' x) Q. elim_inv : φ Pinv Pin ( x, Pout x (from_option id (λ _, emp) mPclose) x - Q' x) Q.
Arguments ElimInv {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never. Arguments ElimInv {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
Arguments elim_inv {_} {_} _ _%I _%I _%I _%I _%I _%I {_}. Arguments elim_inv {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances. Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances.
......
...@@ -445,7 +445,7 @@ Proof. ...@@ -445,7 +445,7 @@ Proof.
Qed. Qed.
Lemma maybe_wand_sound (mP : option PROP) Q : Lemma maybe_wand_sound (mP : option PROP) Q :
maybe_wand mP Q (default emp mP id - Q). maybe_wand mP Q (from_option id emp mP - Q).
Proof. destruct mP; simpl; first done. rewrite emp_wand //. Qed. Proof. destruct mP; simpl; first done. rewrite emp_wand //. Qed.
Global Instance envs_Forall2_refl (R : relation PROP) : Global Instance envs_Forall2_refl (R : relation PROP) :
......
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