Commit c6f0092f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris.

parent 0809b0fd
Pipeline #14299 passed with stage
in 13 minutes and 16 seconds
......@@ -6,5 +6,5 @@ install: [make "install"]
remove: ["rm" "-rf" "'%{lib}%/coq/user-contrib/fri"]
depends: [
"coq" { (>= "8.7.2") | (= "dev") }
"coq-iris" { (= "dev.2018-11-08.2.9eee9408") | (= "dev") }
"coq-iris" { (= "dev.2019-01-15.0.85509592") | (= "dev") }
]
......@@ -31,7 +31,7 @@ Lemma tac_refine_alloc Δ E i k j t K P :
Proof.
rewrite ?envs_entails_eq.
intros Hl1 Hl2 Haff ? HΔ.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite intuitionistically_elim assoc (refine_alloc _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
......@@ -62,7 +62,7 @@ Proof.
rewrite ?envs_entails_eq.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
destruct side.
- rewrite envs_lookup_persistent_sound //=; simpl.
- rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
......@@ -74,7 +74,7 @@ Proof.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite envs_lookup_persistent_sound //=; simpl.
- rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
......@@ -111,7 +111,7 @@ Proof.
rewrite ?envs_entails_eq.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
destruct side.
- rewrite envs_lookup_persistent_sound //=; simpl.
- rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
......@@ -123,7 +123,7 @@ Proof.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite envs_lookup_persistent_sound //=; simpl.
- rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
......@@ -155,7 +155,7 @@ Lemma tac_refine_send k t e Δ Δ' Δ'' E i j K l side v' l1 l2 P :
Proof.
rewrite ?envs_entails_eq.
intros ? Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
......@@ -194,7 +194,7 @@ Lemma tac_refine_select k t Δ Δ' Δ'' E i j K l side choice l1 l2 P :
Proof.
rewrite ?envs_entails_eq.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
......@@ -234,7 +234,7 @@ Proof.
rewrite ?envs_entails_eq.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
destruct side.
- rewrite envs_lookup_persistent_sound //=; simpl.
- rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
......@@ -246,7 +246,7 @@ Proof.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite envs_lookup_persistent_sound //=; simpl.
- rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
......@@ -278,7 +278,7 @@ Proof.
rewrite ?envs_entails_eq.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
destruct side.
- rewrite envs_lookup_persistent_sound //=; simpl.
- rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
......@@ -290,7 +290,7 @@ Proof.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite envs_lookup_persistent_sound //=; simpl.
- rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
......@@ -326,7 +326,7 @@ Proof.
rewrite ?envs_entails_eq.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
destruct side.
- rewrite envs_lookup_persistent_sound //=; simpl.
- rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
......@@ -338,7 +338,7 @@ Proof.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite envs_lookup_persistent_sound //=; simpl.
- rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
......@@ -365,7 +365,7 @@ Lemma tac_refine_pure Δ Δ' E i k t K e e' P :
Proof.
rewrite ?envs_entails_eq.
intros Hl1 Hl2 Haff ? Hstep HΔ1 HΔ2.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc.
rewrite intuitionistically_elim.
......@@ -505,7 +505,7 @@ Lemma tac_refine_fork j Δ E i k t K e P :
Proof.
rewrite ?envs_entails_eq.
intros Hl1 Hl2 Haff ? HΔ.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite intuitionistically_elim assoc (refine_fork _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
......@@ -542,7 +542,7 @@ Lemma tac_refine_delay Δ E Δ' i k t e K P:
Proof.
rewrite ?envs_entails_eq.
intros Hgt Hl1 Hl2 Haff ? Hrep Hd.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite intuitionistically_elim assoc.
rewrite (refine_delay _ d' _ E); eauto.
......
......@@ -25,7 +25,7 @@ Lemma tac_wp_alloc Δ Δ' E i j e v Φ :
Proof.
rewrite envs_entails_eq.
intros ???? HΔ. rewrite -wp_alloc //.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_intuitionistic_sound //=; simpl.
apply sep_mono; first auto using relevant_elim.
rewrite into_laterN_env_sound. apply later_mono, forall_intro=> l.
destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
......@@ -41,7 +41,7 @@ Lemma tac_wp_load Δ Δ' E i k l q v Φ :
envs_entails (Δ) (WP Load (Lit (LitLoc l)) @ E {{ Φ }}).
Proof.
rewrite ?envs_entails_eq.
intros. rewrite -wp_load // envs_lookup_persistent_sound //=; simpl.
intros. rewrite -wp_load // envs_lookup_intuitionistic_sound //=; simpl.
apply sep_mono; first auto using relevant_elim.
rewrite into_laterN_env_sound -upred_bi.later_sep_affine_l envs_lookup_split //; simpl.
rewrite -(affine_affinely (l {q} v)%I).
......@@ -58,7 +58,7 @@ Lemma tac_wp_store Δ Δ' Δ'' E i k l v e v' Φ :
envs_entails (Δ) (WP Store (Lit (LitLoc l)) e @ E {{ Φ }}).
Proof.
rewrite ?envs_entails_eq.
intros. rewrite -wp_store // envs_lookup_persistent_sound //=; simpl.
intros. rewrite -wp_store // envs_lookup_intuitionistic_sound //=; simpl.
apply sep_mono; first auto using relevant_elim.
rewrite into_laterN_env_sound -upred_bi.later_sep_affine_l envs_simple_replace_sound //; simpl.
rewrite right_id.
......@@ -75,7 +75,7 @@ Lemma tac_wp_cas_fail Δ Δ' E i k l q v e1 v1 e2 v2 Φ :
envs_entails (Δ) (WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}).
Proof.
rewrite ?envs_entails_eq.
intros. rewrite -wp_cas_fail // envs_lookup_persistent_sound //=; simpl.
intros. rewrite -wp_cas_fail // envs_lookup_intuitionistic_sound //=; simpl.
apply sep_mono; first auto using relevant_elim.
rewrite into_laterN_env_sound -upred_bi.later_sep_affine_l envs_lookup_split //; simpl.
rewrite -(affine_affinely (l {q} v)%I).
......@@ -93,7 +93,7 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' E i k l v e1 v1 e2 v2 Φ :
Proof.
rewrite ?envs_entails_eq.
intros; subst.
rewrite -wp_cas_suc // envs_lookup_persistent_sound //=; simpl.
rewrite -wp_cas_suc // envs_lookup_intuitionistic_sound //=; simpl.
apply sep_mono; first auto using relevant_elim.
rewrite into_laterN_env_sound -upred_bi.later_sep_affine_l envs_simple_replace_sound //; simpl.
rewrite right_id.
......@@ -111,7 +111,7 @@ Lemma tac_wp_swap Δ Δ' Δ'' E i k l v e v' Φ :
envs_entails (Δ) (WP Swap (Lit (LitLoc l)) e @ E {{ Φ }}).
Proof.
rewrite ?envs_entails_eq.
intros. rewrite -wp_swap // envs_lookup_persistent_sound //=; simpl.
intros. rewrite -wp_swap // envs_lookup_intuitionistic_sound //=; simpl.
apply sep_mono; first auto using relevant_elim.
rewrite into_laterN_env_sound -upred_bi.later_sep_affine_l envs_simple_replace_sound //; simpl.
rewrite right_id.
......@@ -128,7 +128,7 @@ Lemma tac_wp_fai Δ Δ' Δ'' E i k l k' Φ :
envs_entails (Δ) (WP FAI (Lit (LitLoc l)) @ E {{ Φ }}).
Proof.
rewrite ?envs_entails_eq.
intros. rewrite -wp_fai // envs_lookup_persistent_sound //=; simpl.
intros. rewrite -wp_fai // envs_lookup_intuitionistic_sound //=; simpl.
apply sep_mono; first auto using relevant_elim.
rewrite into_laterN_env_sound -upred_bi.later_sep_affine_l envs_simple_replace_sound //; simpl.
rewrite right_id.
......
......@@ -34,7 +34,7 @@ Lemma tac_refine_alloc Δ E i k j t K e v P :
Proof.
rewrite ?envs_entails_eq.
intros ? Hl1 Hl2 Haff ? HΔ.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite intuitionistically_elim.
rewrite assoc (refine_alloc _ d' _ _ E) //.
......@@ -60,7 +60,7 @@ Lemma tac_refine_load Δ Δ' Δ'' E i k j t K l v q P :
Proof.
rewrite ?envs_entails_eq.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
......@@ -89,7 +89,7 @@ Lemma tac_refine_store Δ Δ' Δ'' E i k j t K l v e v' P :
Proof.
rewrite ?envs_entails_eq.
intros ? Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
......@@ -119,7 +119,7 @@ Lemma tac_refine_cas_fail Δ Δ' Δ'' E i k j t K l q v e1 v1 e2 v2 P :
Proof.
rewrite ?envs_entails_eq.
intros ?? Hl1 Hl2 Hl3 ? Haff ? HΔ1 HΔ2.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
......@@ -150,7 +150,7 @@ Lemma tac_refine_cas_suc Δ Δ' Δ'' E i k j t K l v e1 v1 e2 v2 P :
Proof.
rewrite ?envs_entails_eq.
intros ?? Hl1 Hl2 Hl3 ? Haff ? HΔ1 HΔ2. subst.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
......@@ -178,7 +178,7 @@ Lemma tac_refine_swap Δ Δ' Δ'' E i k j t K l v e v' P :
Proof.
rewrite ?envs_entails_eq.
intros ? Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
......@@ -206,7 +206,7 @@ Lemma tac_refine_fai Δ Δ' Δ'' E i k j t K l k' P :
Proof.
rewrite ?envs_entails_eq.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
......@@ -233,7 +233,7 @@ Lemma tac_refine_pure Δ Δ' E i k t K e e' P :
Proof.
rewrite ?envs_entails_eq.
intros Hl1 Hl2 Haff ? Hstep HΔ1 HΔ2.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc.
rewrite intuitionistically_elim.
......@@ -381,7 +381,7 @@ Lemma tac_refine_fork Δ E i k j t K e P :
Proof.
rewrite ?envs_entails_eq.
intros Hl1 Hl2 Haff ? HΔ.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite intuitionistically_elim assoc (refine_fork _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
......@@ -418,7 +418,7 @@ Lemma tac_refine_delay Δ E Δ' i k t e K P:
Proof.
rewrite ?envs_entails_eq.
intros Hgt Hl1 Hl2 Haff ? Hrep Hd.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_intuitionistic_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite intuitionistically_elim assoc.
rewrite (refine_delay _ d' _ E); eauto.
......
......@@ -179,7 +179,7 @@ Lemma tac_sts_fsa {A} (fsa : FSA Λ _ A) fsaV Δ E N j i γ S T Q Φ :
Proof.
rewrite ?envs_entails_eq.
intros ?? Hl1 Hl2 ? HΔ'. rewrite (is_afsa Q) -(sts_afsaS φ fsa) //.
rewrite envs_lookup_persistent_sound //; simpl.
rewrite envs_lookup_intuitionistic_sound //; simpl.
rewrite bi.intuitionistically_elim. apply sep_mono_r.
clear Hl1.
rewrite envs_lookup_sound //; simpl. apply sep_mono_r.
......
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