Commit df918d8b authored by Ralf Jung's avatar Ralf Jung

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

parents aae046b8 de9438cb
Pipeline #2450 passed with stage
...@@ -307,6 +307,13 @@ Arguments uPred_always_if _ !_ _/. ...@@ -307,6 +307,13 @@ Arguments uPred_always_if _ !_ _/.
Notation "□? p P" := (uPred_always_if p P) Notation "□? p P" := (uPred_always_if p P)
(at level 20, p at level 0, P at level 20, format "□? p P"). (at level 20, p at level 0, P at level 20, format "□? p P").
Definition uPred_laterN {M} (n : nat) (P : uPred M) : uPred M :=
Nat.iter n uPred_later P.
Instance: Params (@uPred_laterN) 2.
Notation "▷^ n P" := (uPred_laterN n P)
(at level 20, n at level 9, right associativity,
format "▷^ n P") : uPred_scope.
Class TimelessP {M} (P : uPred M) := timelessP : P (P False). Class TimelessP {M} (P : uPred M) := timelessP : P (P False).
Arguments timelessP {_} _ {_}. Arguments timelessP {_} _ {_}.
...@@ -437,7 +444,7 @@ Proof. ...@@ -437,7 +444,7 @@ Proof.
intros n P Q HPQ; unseal; split=> -[|n'] x ??; simpl; [done|]. intros n P Q HPQ; unseal; split=> -[|n'] x ??; simpl; [done|].
apply (HPQ n'); eauto using cmra_validN_S. apply (HPQ n'); eauto using cmra_validN_S.
Qed. Qed.
Global Instance later_proper : Global Instance later_proper' :
Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _. Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _.
Global Instance always_ne n : Proper (dist n ==> dist n) (@uPred_always M). Global Instance always_ne n : Proper (dist n ==> dist n) (@uPred_always M).
Proof. Proof.
...@@ -460,10 +467,6 @@ Proof. ...@@ -460,10 +467,6 @@ Proof.
Qed. Qed.
Global Instance valid_proper {A : cmraT} : Global Instance valid_proper {A : cmraT} :
Proper (() ==> (⊣⊢)) (@uPred_valid M A) := ne_proper _. Proper (() ==> (⊣⊢)) (@uPred_valid M A) := ne_proper _.
Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
Proof. unfold uPred_iff; solve_proper. Qed.
Global Instance iff_proper :
Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_iff M) := ne_proper_2 _.
(** Introduction and elimination rules *) (** Introduction and elimination rules *)
Lemma pure_intro φ P : φ P φ. Lemma pure_intro φ P : φ P φ.
...@@ -523,6 +526,11 @@ Proof. ...@@ -523,6 +526,11 @@ Proof.
Qed. Qed.
(* Derived logical stuff *) (* Derived logical stuff *)
Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
Proof. unfold uPred_iff; solve_proper. Qed.
Global Instance iff_proper :
Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_iff M) := ne_proper_2 _.
Lemma False_elim P : False P. Lemma False_elim P : False P.
Proof. by apply (pure_elim False). Qed. Proof. by apply (pure_elim False). Qed.
Lemma True_intro P : P True. Lemma True_intro P : P True.
...@@ -943,7 +951,10 @@ Lemma always_entails_l' P Q : (P ⊢ □ Q) → P ⊢ □ Q ★ P. ...@@ -943,7 +951,10 @@ Lemma always_entails_l' P Q : (P ⊢ □ Q) → P ⊢ □ Q ★ P.
Proof. intros; rewrite -always_and_sep_l'; auto. Qed. Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
Lemma always_entails_r' P Q : (P Q) P P Q. Lemma always_entails_r' P Q : (P Q) P P Q.
Proof. intros; rewrite -always_and_sep_r'; auto. Qed. Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
Lemma always_laterN n P : ^n P ⊣⊢ ^n P.
Proof. induction n as [|n IH]; simpl; auto. by rewrite always_later IH. Qed.
(* Conditional always *)
Global Instance always_if_ne n p : Proper (dist n ==> dist n) (@uPred_always_if M p). Global Instance always_if_ne n p : Proper (dist n ==> dist n) (@uPred_always_if M p).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Global Instance always_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always_if M p). Global Instance always_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always_if M p).
...@@ -1004,6 +1015,9 @@ Proof. ...@@ -1004,6 +1015,9 @@ Proof.
Qed. Qed.
(* Later derived *) (* Later derived *)
Lemma later_proper P Q : (P ⊣⊢ Q) P ⊣⊢ Q.
Proof. by intros ->. Qed.
Hint Resolve later_mono later_proper.
Global Instance later_mono' : Proper (() ==> ()) (@uPred_later M). Global Instance later_mono' : Proper (() ==> ()) (@uPred_later M).
Proof. intros P Q; apply later_mono. Qed. Proof. intros P Q; apply later_mono. Qed.
Global Instance later_flip_mono' : Global Instance later_flip_mono' :
...@@ -1012,18 +1026,69 @@ Proof. intros P Q; apply later_mono. Qed. ...@@ -1012,18 +1026,69 @@ Proof. intros P Q; apply later_mono. Qed.
Lemma later_True : True ⊣⊢ True. Lemma later_True : True ⊣⊢ True.
Proof. apply (anti_symm ()); auto using later_intro. Qed. Proof. apply (anti_symm ()); auto using later_intro. Qed.
Lemma later_impl P Q : (P Q) P Q. Lemma later_impl P Q : (P Q) P Q.
Proof. Proof. apply impl_intro_l; rewrite -later_and; eauto using impl_elim. Qed.
apply impl_intro_l; rewrite -later_and.
apply later_mono, impl_elim with P; auto.
Qed.
Lemma later_exist `{Inhabited A} (Φ : A uPred M) : Lemma later_exist `{Inhabited A} (Φ : A uPred M) :
( a, Φ a) ⊣⊢ ( a, Φ a). ( a, Φ a) ⊣⊢ ( a, Φ a).
Proof. apply: anti_symm; eauto using later_exist_2, later_exist_1. Qed. Proof. apply: anti_symm; eauto using later_exist_2, later_exist_1. Qed.
Lemma later_wand P Q : (P - Q) P - Q. Lemma later_wand P Q : (P - Q) P - Q.
Proof. apply wand_intro_r;rewrite -later_sep; apply later_mono,wand_elim_l. Qed. Proof. apply wand_intro_r;rewrite -later_sep; eauto using wand_elim_l. Qed.
Lemma later_iff P Q : (P Q) P Q. Lemma later_iff P Q : (P Q) P Q.
Proof. by rewrite /uPred_iff later_and !later_impl. Qed. Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
(* n-times later *)
Global Instance laterN_ne n m : Proper (dist n ==> dist n) (@uPred_laterN M m).
Proof. induction m; simpl. by intros ???. solve_proper. Qed.
Global Instance laterN_proper m :
Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_laterN M m) := ne_proper _.
Lemma later_laterN n P : ^(S n) P ⊣⊢ ^n P.
Proof. done. Qed.
Lemma laterN_later n P : ^(S n) P ⊣⊢ ^n P.
Proof. induction n; simpl; auto. Qed.
Lemma laterN_plus n1 n2 P : ^(n1 + n2) P ⊣⊢ ^n1 ^n2 P.
Proof. induction n1; simpl; auto. Qed.
Lemma laterN_le n1 n2 P : n1 n2 ^n1 P ^n2 P.
Proof. induction 1; simpl; by rewrite -?later_intro. Qed.
Lemma laterN_mono n P Q : (P Q) ^n P ^n Q.
Proof. induction n; simpl; auto. Qed.
Lemma laterN_intro n P : P ^n P.
Proof. induction n as [|n IH]; simpl; by rewrite -?later_intro. Qed.
Lemma laterN_and n P Q : ^n (P Q) ⊣⊢ ^n P ^n Q.
Proof. induction n as [|n IH]; simpl; rewrite -?later_and; auto. Qed.
Lemma laterN_or n P Q : ^n (P Q) ⊣⊢ ^n P ^n Q.
Proof. induction n as [|n IH]; simpl; rewrite -?later_or; auto. Qed.
Lemma laterN_forall {A} n (Φ : A uPred M) : (^n a, Φ a) ⊣⊢ ( a, ^n Φ a).
Proof. induction n as [|n IH]; simpl; rewrite -?later_forall; auto. Qed.
Lemma laterN_exist_1 {A} n (Φ : A uPred M) : ( a, ^n Φ a) (^n a, Φ a).
Proof. induction n as [|n IH]; simpl; rewrite ?later_exist_1; auto. Qed.
Lemma laterN_exist_2 `{Inhabited A} n (Φ : A uPred M) :
(^n a, Φ a) a, ^n Φ a.
Proof. induction n as [|n IH]; simpl; rewrite -?later_exist_2; auto. Qed.
Lemma laterN_sep n P Q : ^n (P Q) ⊣⊢ ^n P ^n Q.
Proof. induction n as [|n IH]; simpl; rewrite -?later_sep; auto. Qed.
Global Instance laterN_mono' n : Proper (() ==> ()) (@uPred_laterN M n).
Proof. intros P Q; apply laterN_mono. Qed.
Global Instance laterN_flip_mono' n :
Proper (flip () ==> flip ()) (@uPred_laterN M n).
Proof. intros P Q; apply laterN_mono. Qed.
Lemma laterN_True n : ^n True ⊣⊢ True.
Proof. apply (anti_symm ()); auto using laterN_intro. Qed.
Lemma laterN_impl n P Q : ^n (P Q) ^n P ^n Q.
Proof.
apply impl_intro_l; rewrite -laterN_and; eauto using impl_elim, laterN_mono.
Qed.
Lemma laterN_exist n `{Inhabited A} (Φ : A uPred M) :
^n ( a, Φ a) ⊣⊢ ( a, ^n Φ a).
Proof. apply: anti_symm; eauto using laterN_exist_2, laterN_exist_1. Qed.
Lemma laterN_wand n P Q : ^n (P - Q) ^n P - ^n Q.
Proof.
apply wand_intro_r; rewrite -laterN_sep; eauto using wand_elim_l,laterN_mono.
Qed.
Lemma laterN_iff n P Q : ^n (P Q) ^n P ^n Q.
Proof. by rewrite /uPred_iff laterN_and !laterN_impl. Qed.
(* Own *) (* Own *)
Lemma ownM_op (a1 a2 : M) : Lemma ownM_op (a1 a2 : M) :
uPred_ownM (a1 a2) ⊣⊢ uPred_ownM a1 uPred_ownM a2. uPred_ownM (a1 a2) ⊣⊢ uPred_ownM a1 uPred_ownM a2.
...@@ -1193,6 +1258,8 @@ Global Instance valid_persistent {A : cmraT} (a : A) : ...@@ -1193,6 +1258,8 @@ Global Instance valid_persistent {A : cmraT} (a : A) :
Proof. by intros; rewrite /PersistentP always_valid. Qed. Proof. by intros; rewrite /PersistentP always_valid. Qed.
Global Instance later_persistent P : PersistentP P PersistentP ( P). Global Instance later_persistent P : PersistentP P PersistentP ( P).
Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed. Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed.
Global Instance laterN_persistent n P : PersistentP P PersistentP (^n P).
Proof. induction n; apply _. Qed.
Global Instance ownM_persistent : Persistent a PersistentP (@uPred_ownM M a). Global Instance ownM_persistent : Persistent a PersistentP (@uPred_ownM M a).
Proof. intros. by rewrite /PersistentP always_ownM. Qed. Proof. intros. by rewrite /PersistentP always_ownM. Qed.
Global Instance from_option_persistent {A} P (Ψ : A uPred M) (mx : option A) : Global Instance from_option_persistent {A} P (Ψ : A uPred M) (mx : option A) :
......
...@@ -80,7 +80,7 @@ Proof. ...@@ -80,7 +80,7 @@ Proof.
+ iPvsIntro; iSplitL "Hl Hγ". + iPvsIntro; iSplitL "Hl Hγ".
{ iNext. iExists _; iFrame; eauto. } { iNext. iExists _; iFrame; eauto. }
wp_match. by iApply "Hv". wp_match. by iApply "Hv".
+ iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (@own_valid with "Hγ") as %[]. + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
Qed. Qed.
End proof. End proof.
......
...@@ -103,14 +103,14 @@ Section auth. ...@@ -103,14 +103,14 @@ Section auth.
iIntros (??) "(#? & Hγf & HΨ)". rewrite /auth_ctx /auth_own. iIntros (??) "(#? & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
iInv N as (a') "[Hγ Hφ]". iInv N as (a') "[Hγ Hφ]".
iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ". iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
iDestruct (@own_valid with "#Hγ") as "Hvalid". iDestruct (own_valid with "#Hγ") as "Hvalid".
iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]"; simpl; iClear "Hvalid". iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]"; simpl; iClear "Hvalid".
iDestruct "Ha'" as (af) "Ha'"; iDestruct "Ha'" as %Ha'. iDestruct "Ha'" as (af) "Ha'"; iDestruct "Ha'" as %Ha'.
rewrite ->(left_id _ _) in Ha'; setoid_subst. rewrite ->(left_id _ _) in Ha'; setoid_subst.
iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ". iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
{ iApply "HΨ"; by iSplit. } { iApply "HΨ"; by iSplit. }
iIntros (v); iDestruct 1 as (b) "(% & Hφ & HΨ)". iIntros (v); iDestruct 1 as (b) "(% & Hφ & HΨ)".
iPvs (@own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto. iPvs (own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ". iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
iNext. iExists (b af). by iFrame. iNext. iExists (b af). by iFrame.
Qed. Qed.
......
...@@ -69,7 +69,7 @@ Lemma box_own_auth_update E γ b1 b2 b3 : ...@@ -69,7 +69,7 @@ Lemma box_own_auth_update E γ b1 b2 b3 :
Proof. Proof.
rewrite /box_own_prop -!own_op own_valid_l prod_validI; iIntros "[[Hb _] Hγ]". rewrite /box_own_prop -!own_op own_valid_l prod_validI; iIntros "[[Hb _] Hγ]".
iDestruct "Hb" as % [[[] [= ->]%leibniz_equiv] ?]%auth_valid_discrete. iDestruct "Hb" as % [[[] [= ->]%leibniz_equiv] ?]%auth_valid_discrete.
iApply (@own_update with "Hγ"); apply prod_update; simpl; last reflexivity. iApply (own_update with "Hγ"); apply prod_update; simpl; last reflexivity.
by apply auth_update_no_frame, option_local_update, exclusive_local_update. by apply auth_update_no_frame, option_local_update, exclusive_local_update.
Qed. Qed.
......
...@@ -82,6 +82,12 @@ Proof. ...@@ -82,6 +82,12 @@ Proof.
Qed. Qed.
End global. End global.
Arguments own_valid {_ _ _} [_] _ _.
Arguments own_valid_l {_ _ _} [_] _ _.
Arguments own_valid_r {_ _ _} [_] _ _.
Arguments own_updateP {_ _ _} [_] _ _ _ _ _.
Arguments own_update {_ _ _} [_] _ _ _ _ _.
Section global_empty. Section global_empty.
Context `{i : inG Λ Σ (A:ucmraT)}. Context `{i : inG Λ Σ (A:ucmraT)}.
Implicit Types a : A. Implicit Types a : A.
......
...@@ -102,14 +102,14 @@ Section sts. ...@@ -102,14 +102,14 @@ Section sts.
Proof. Proof.
iIntros (??) "(#? & Hγf & HΨ)". rewrite /sts_ctx /sts_ownS /sts_inv /sts_own. iIntros (??) "(#? & Hγf & HΨ)". rewrite /sts_ctx /sts_ownS /sts_inv /sts_own.
iInv N as (s) "[Hγ Hφ]"; iTimeless "Hγ". iInv N as (s) "[Hγ Hφ]"; iTimeless "Hγ".
iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (@own_valid with "#Hγ") as %Hvalid. iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "#Hγ") as %Hvalid.
assert (s S) by eauto using sts_auth_frag_valid_inv. assert (s S) by eauto using sts_auth_frag_valid_inv.
assert ( sts_frag S T) as [??] by eauto using cmra_valid_op_r. assert ( sts_frag S T) as [??] by eauto using cmra_valid_op_r.
iRevert "Hγ"; rewrite sts_op_auth_frag //; iIntros "Hγ". iRevert "Hγ"; rewrite sts_op_auth_frag //; iIntros "Hγ".
iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ". iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
{ iApply "HΨ"; by iSplit. } { iApply "HΨ"; by iSplit. }
iIntros (a); iDestruct 1 as (s' T') "(% & Hφ & HΨ)". iIntros (a); iDestruct 1 as (s' T') "(% & Hφ & HΨ)".
iPvs (@own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth. iPvs (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth.
iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ Hγf]". iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ Hγf]".
iPvsIntro; iSplitL "Hφ Hγ"; last by iApply "HΨ". iPvsIntro; iSplitL "Hφ Hγ"; last by iApply "HΨ".
iNext; iExists s'; by iFrame. iNext; iExists s'; by iFrame.
......
...@@ -84,7 +84,7 @@ Proof. ...@@ -84,7 +84,7 @@ Proof.
iSplitL "HP Hs Hγ"; [|iSplitL "Hr"]. iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
- wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"]. - wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let. iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
iPvs (@own_update with "Hγ") as "Hx". iPvs (own_update with "Hγ") as "Hx".
{ by apply (cmra_update_exclusive (Shot x)). } { by apply (cmra_update_exclusive (Shot x)). }
iApply signal_spec; iFrame "Hs"; iSplit; last done. iApply signal_spec; iFrame "Hs"; iSplit; last done.
iExists x; auto. iExists x; auto.
......
...@@ -51,7 +51,7 @@ Proof. ...@@ -51,7 +51,7 @@ Proof.
- iIntros (n) "!". wp_let. - iIntros (n) "!". wp_let.
iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]". iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
+ wp_cas_suc. iSplitL; [|by iLeft]. + wp_cas_suc. iSplitL; [|by iLeft].
iPvs (@own_update with "Hγ") as "Hγ". iPvs (own_update with "Hγ") as "Hγ".
{ by apply cmra_update_exclusive with (y:=Shot n). } { by apply cmra_update_exclusive with (y:=Shot n). }
iPvsIntro; iRight; iExists n; by iSplitL "Hl". iPvsIntro; iRight; iExists n; by iSplitL "Hl".
+ wp_cas_fail. rewrite /one_shot_inv; eauto 10. + wp_cas_fail. rewrite /one_shot_inv; eauto 10.
...@@ -72,10 +72,10 @@ Proof. ...@@ -72,10 +72,10 @@ Proof.
{ by wp_match. } { by wp_match. }
wp_match. wp_focus (! _)%E. wp_match. wp_focus (! _)%E.
iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as (m') "[Hl Hγ]". iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as (m') "[Hl Hγ]".
{ iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (@own_valid with "Hγ") as %?. } { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as %?. }
wp_load; iPvsIntro. wp_load; iPvsIntro.
iCombine "Hγ" "Hγ'" as "Hγ". iCombine "Hγ" "Hγ'" as "Hγ".
iDestruct (@own_valid with "#Hγ") as %[=->]%dec_agree_op_inv. iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
iSplitL "Hl"; [iRight; by eauto|]. iSplitL "Hl"; [iRight; by eauto|].
wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto. wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto.
Qed. Qed.
......
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