Commit de9438cb authored by Robbert Krebbers's avatar Robbert Krebbers

Declare inG arguments of own_* implicit but not maximally inserted.

This way type class inference is not invokved when used in tactics
like iPvs while not having to write an @.

(Idea suggested by Ralf.)
parent cdce49a7
Pipeline #2448 passed with stage
......@@ -80,7 +80,7 @@ Proof.
+ iPvsIntro; iSplitL "Hl Hγ".
{ iNext. iExists _; iFrame; eauto. }
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.
End proof.
......
......@@ -103,14 +103,14 @@ Section auth.
iIntros (??) "(#? & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
iInv N as (a') "[Hγ 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 "Ha'" as (af) "Ha'"; iDestruct "Ha'" as %Ha'.
rewrite ->(left_id _ _) in Ha'; setoid_subst.
iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
{ iApply "HΨ"; by iSplit. }
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Ψ".
iNext. iExists (b af). by iFrame.
Qed.
......
......@@ -69,7 +69,7 @@ Lemma box_own_auth_update E γ b1 b2 b3 :
Proof.
rewrite /box_own_prop -!own_op own_valid_l prod_validI; iIntros "[[Hb _] Hγ]".
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.
Qed.
......
......@@ -82,6 +82,12 @@ Proof.
Qed.
End global.
Arguments own_valid {_ _ _} [_] _ _.
Arguments own_valid_l {_ _ _} [_] _ _.
Arguments own_valid_r {_ _ _} [_] _ _.
Arguments own_updateP {_ _ _} [_] _ _ _ _ _.
Arguments own_update {_ _ _} [_] _ _ _ _ _.
Section global_empty.
Context `{i : inG Λ Σ (A:ucmraT)}.
Implicit Types a : A.
......
......@@ -102,14 +102,14 @@ Section sts.
Proof.
iIntros (??) "(#? & Hγf & HΨ)". rewrite /sts_ctx /sts_ownS /sts_inv /sts_own.
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 ( sts_frag S T) as [??] by eauto using cmra_valid_op_r.
iRevert "Hγ"; rewrite sts_op_auth_frag //; iIntros "Hγ".
iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
{ iApply "HΨ"; by iSplit. }
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]".
iPvsIntro; iSplitL "Hφ Hγ"; last by iApply "HΨ".
iNext; iExists s'; by iFrame.
......
......@@ -84,7 +84,7 @@ Proof.
iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
- wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
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)). }
iApply signal_spec; iFrame "Hs"; iSplit; last done.
iExists x; auto.
......
......@@ -51,7 +51,7 @@ Proof.
- iIntros (n) "!". wp_let.
iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
+ 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). }
iPvsIntro; iRight; iExists n; by iSplitL "Hl".
+ wp_cas_fail. rewrite /one_shot_inv; eauto 10.
......@@ -72,10 +72,10 @@ Proof.
{ by wp_match. }
wp_match. wp_focus (! _)%E.
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.
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|].
wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto.
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