Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
E
examples
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
Merge Requests
2
Merge Requests
2
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Iris
examples
Commits
ffb27f4a
Commit
ffb27f4a
authored
May 24, 2019
by
Hai Dang
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Bump Iris with changes in `auth`
parent
3e8fcd4c
Changes
19
Hide whitespace changes
Inline
Side-by-side
Showing
19 changed files
with
72 additions
and
69 deletions
+72
-69
opam
opam
+1
-1
theories/hocap/contrib_bag.v
theories/hocap/contrib_bag.v
+1
-1
theories/lecture_notes/ccounter.v
theories/lecture_notes/ccounter.v
+1
-1
theories/lecture_notes/coq_intro_example_2.v
theories/lecture_notes/coq_intro_example_2.v
+5
-5
theories/logatom/elimination_stack/hocap_spec.v
theories/logatom/elimination_stack/hocap_spec.v
+3
-3
theories/logatom/elimination_stack/stack.v
theories/logatom/elimination_stack/stack.v
+6
-6
theories/logatom/flat_combiner/misc.v
theories/logatom/flat_combiner/misc.v
+1
-1
theories/logatom/snapshot/atomic_snapshot.v
theories/logatom/snapshot/atomic_snapshot.v
+4
-4
theories/logatom/treiber2.v
theories/logatom/treiber2.v
+3
-2
theories/logrel/F_mu_ref/rules_binary.v
theories/logrel/F_mu_ref/rules_binary.v
+7
-7
theories/logrel/F_mu_ref/soundness.v
theories/logrel/F_mu_ref/soundness.v
+1
-1
theories/logrel/F_mu_ref/soundness_binary.v
theories/logrel/F_mu_ref/soundness_binary.v
+4
-4
theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
+1
-1
theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
+2
-2
theories/logrel/F_mu_ref_conc/rules_binary.v
theories/logrel/F_mu_ref_conc/rules_binary.v
+13
-12
theories/logrel/F_mu_ref_conc/soundness_binary.v
theories/logrel/F_mu_ref_conc/soundness_binary.v
+3
-3
theories/logrel/F_mu_ref_conc/soundness_unary.v
theories/logrel/F_mu_ref_conc/soundness_unary.v
+1
-1
theories/logrel_heaplang/lib/symbol_adt.v
theories/logrel_heaplang/lib/symbol_adt.v
+6
-3
theories/spanning_tree/mon.v
theories/spanning_tree/mon.v
+9
-11
No files found.
opam
View file @
ffb27f4a
...
...
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2019-0
4-17.0.60d28bbb
") | (= "dev") }
"coq-iris" { (= "dev.2019-0
5-24.0.c9984c7f
") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
theories/hocap/contrib_bag.v
View file @
ffb27f4a
...
...
@@ -50,7 +50,7 @@ Section proof.
iIntros
(
Φ
)
"_ HΦ"
.
iApply
wp_fupd
.
iApply
(
newBag_spec
b
NB
)
;
eauto
.
iNext
.
iIntros
(
v
γ
b
)
"[#Hbag Hcntn]"
.
iMod
(
own_alloc
(
●
!
∅
⋅
◯
!
∅
))
as
(
γ
)
"[Hown Hpart]"
;
first
done
.
iMod
(
own_alloc
(
●
!
∅
⋅
◯
!
∅
))
as
(
γ
)
"[Hown Hpart]"
;
first
by
apply
auth_both_valid
.
iMod
(
inv_alloc
NI
_
(
∃
X
,
bag_contents
b
γ
b
X
∗
own
γ
(
●
!
X
))%
I
with
"[Hcntn Hown]"
)
as
"#Hinv"
.
{
iNext
.
iExists
_
.
iFrame
.
}
iApply
"HΦ"
.
iModIntro
.
iExists
_
,
_
.
iFrame
"Hinv Hbag Hpart"
.
...
...
theories/lecture_notes/ccounter.v
View file @
ffb27f4a
...
...
@@ -58,7 +58,7 @@ Section ccounter.
iIntros
(
Φ
)
"_ HΦ"
.
rewrite
-
wp_fupd
.
wp_apply
newcounter_spec
;
auto
.
iIntros
(
ℓ
)
"H"
;
iDestruct
"H"
as
(
γ₂
)
"[#HCnt Hown]"
.
iMod
(
own_alloc
(
●
!
m
%
nat
⋅
◯
!
m
%
nat
))
as
(
γ₁
)
"[Hγ Hγ']"
;
first
done
.
iMod
(
own_alloc
(
●
!
m
%
nat
⋅
◯
!
m
%
nat
))
as
(
γ₁
)
"[Hγ Hγ']"
;
first
by
apply
auth_both_valid
.
iMod
(
inv_alloc
(
N
.@
"counter"
)
_
(
ccounter_inv
γ₁
γ₂
)
with
"[Hγ Hown]"
).
{
iNext
.
iExists
_
.
by
iFrame
.
}
iModIntro
.
iApply
"HΦ"
.
rewrite
/
is_ccounter
;
eauto
.
...
...
theories/lecture_notes/coq_intro_example_2.v
View file @
ffb27f4a
...
...
@@ -29,7 +29,7 @@ Section monotone_counter.
algebra we shall be using. The Iris library contains all the ingredients
needed to compose this particular resource algebra from simpler components,
however to illustrate how to define our own we will define it from scratch.
In the subsequent section we show how to obtain an equivalent resource
algebra from the building blocks provided by the Iris Coq library.
*)
...
...
@@ -423,7 +423,7 @@ Section monotone_counter'.
Proof
.
(* Use a simplified definition of validity for when the underlying CMRA is discrete, i.e., an RA.
The general definition also involves the use of step-indices, which is not needed in our case. *)
rewrite
auth_
valid_discrete_2
.
rewrite
auth_
both_valid
.
split
.
-
intros
[?
_
]
;
by
apply
mnat_included
.
-
intros
?%
mnat_included
;
done
.
...
...
@@ -460,7 +460,7 @@ Section monotone_counter'.
iIntros
(
Φ
)
"_ HCont"
.
rewrite
/
newCounter
-
wp_fupd
.
wp_lam
.
iMod
(
own_alloc
(
●
(
0
%
nat
:
mnatUR
)
⋅
◯
0
%
nat
))
as
(
γ
)
"[HAuth HFrac]"
.
iMod
(
own_alloc
(
●
(
0
%
nat
:
mnatUR
)
⋅
◯
(
0
%
nat
:
mnatUR
)
))
as
(
γ
)
"[HAuth HFrac]"
.
-
apply
mcounterRA_valid_auth_frag'
;
auto
.
-
wp_alloc
ℓ
as
"Hpt"
.
iMod
(
inv_alloc
N
_
(
counter_inv'
ℓ
γ
)
with
"[Hpt HAuth]"
)
as
"HInv"
.
...
...
@@ -505,7 +505,7 @@ Section monotone_counter'.
iInv
N
as
(
k
)
">[Hpt HOwnAuth]"
"HClose"
.
destruct
(
decide
(
k
=
m
))
;
subst
.
+
wp_cas_suc
.
iMod
(
own_update
γ
((
●
m
⋅
◯
n
))
(
●
(
S
m
:
mnatUR
)
⋅
(
◯
S
n
))
with
"[HOwnFrag HOwnAuth]"
)
as
"[HOwnAuth HOwnFrag]"
.
iMod
(
own_update
γ
((
●
m
⋅
◯
n
))
(
●
(
S
m
:
mnatUR
)
⋅
(
◯
(
S
n
:
mnatUR
)
))
with
"[HOwnFrag HOwnAuth]"
)
as
"[HOwnAuth HOwnFrag]"
.
{
apply
mcounterRA_update'
.
}
{
rewrite
own_op
;
iFrame
.
}
iMod
(
"HClose"
with
"[Hpt HOwnAuth]"
)
as
"_"
.
...
...
@@ -606,7 +606,7 @@ Section ccounter.
{{{
γ
ℓ
,
RET
#
ℓ
;
is_ccounter
γ
ℓ
1
0
%
nat
}}}.
Proof
.
iIntros
(
Φ
)
"_ HΦ"
.
rewrite
-
wp_fupd
/
newCounter
/=.
wp_lam
.
wp_alloc
ℓ
as
"Hpt"
.
iMod
(
own_alloc
(
●
!
O
%
nat
⋅
◯
!
0
%
nat
))
as
(
γ
)
"[Hγ Hγ']"
;
first
done
.
iMod
(
own_alloc
(
●
!
O
%
nat
⋅
◯
!
0
%
nat
))
as
(
γ
)
"[Hγ Hγ']"
;
first
by
apply
auth_both_valid
.
iMod
(
inv_alloc
N
_
(
ccounter_inv
γ
ℓ
)
with
"[Hpt Hγ]"
).
{
iNext
.
iExists
0
%
nat
.
by
iFrame
.
}
iModIntro
.
iApply
"HΦ"
.
rewrite
/
is_ccounter
;
eauto
.
...
...
theories/logatom/elimination_stack/hocap_spec.v
View file @
ffb27f4a
...
...
@@ -165,7 +165,7 @@ Section logatom_hocap.
iIntros
(
Φ
)
"_ HΦ"
.
iApply
wp_fupd
.
iApply
logatom
.
new_stack_spec
;
first
done
.
iIntros
"!>"
(
γ
s
s
)
"[Hstack Hcont]"
.
iMod
(
own_alloc
(
●
Excl'
[]
⋅
◯
Excl'
[]))
as
(
γ
w
)
"[Hs● Hs◯]"
.
{
apply
auth_
valid_discrete_2
.
split
;
done
.
}
{
apply
auth_
both_valid
.
split
;
done
.
}
iApply
(
"HΦ"
$!
(
γ
s
,
γ
w
)).
rewrite
/
hocap_is_stack
.
iFrame
.
iApply
inv_alloc
.
eauto
with
iFrame
.
Qed
.
...
...
@@ -212,11 +212,11 @@ Section logatom_hocap.
iIntros
(???)
"Hf1 Hf2"
.
iDestruct
(
own_valid_2
with
"Hf1 Hf2"
)
as
%[].
Qed
.
Next
Obligation
.
iIntros
(???)
"Ha1 Ha2"
.
iDestruct
(
own_valid_2
with
"Ha1 Ha2"
)
as
%[].
iIntros
(???)
"Ha1 Ha2"
.
by
iDestruct
(
own_valid_2
with
"Ha1 Ha2"
)
as
%[].
Qed
.
Next
Obligation
.
iIntros
(???)
"Hf Ha"
.
iDestruct
(
own_valid_2
with
"Ha Hf"
)
as
%[->%
Excl_included
%
leibniz_equiv
_
]%
auth_
valid_discrete_2
.
done
.
%[->%
Excl_included
%
leibniz_equiv
_
]%
auth_
both_valid
.
done
.
Qed
.
Next
Obligation
.
iIntros
(???)
"Hf Ha"
.
iMod
(
own_update_2
with
"Ha Hf"
)
as
"[? ?]"
.
...
...
theories/logatom/elimination_stack/stack.v
View file @
ffb27f4a
...
...
@@ -175,7 +175,7 @@ Section stack.
wp_apply
alloc_spec
;
first
done
.
iIntros
(
head
)
"Hhead"
.
wp_let
.
wp_apply
alloc_spec
;
first
done
.
iIntros
(
offer
)
"Hoffer"
.
wp_let
.
iMod
(
own_alloc
(
●
Excl'
[]
⋅
◯
Excl'
[]))
as
(
γ
s
)
"[Hs● Hs◯]"
.
{
apply
auth_
valid_discrete_2
.
split
;
done
.
}
{
apply
auth_
both_valid
.
split
;
done
.
}
iMod
(
inv_alloc
stackN
_
(
stack_inv
γ
s
head
offer
)
with
"[-HΦ Hs◯]"
).
{
iNext
.
iExists
None
,
None
,
_
.
iFrame
.
done
.
}
wp_pures
.
iApply
"HΦ"
.
iFrame
"Hs◯"
.
iModIntro
.
iExists
_
,
_
.
auto
.
...
...
@@ -209,7 +209,7 @@ Section stack.
-
(* The CAS succeeded. Update everything accordingly. *)
iMod
"AU"
as
(
l'
)
"[Hl' [_ Hclose]]"
.
iDestruct
(
own_valid_2
with
"Hs● Hl'"
)
as
%[->%
Excl_included
%
leibniz_equiv
_
]%
auth_
valid_discrete_2
.
%[->%
Excl_included
%
leibniz_equiv
_
]%
auth_
both_valid
.
iMod
(
own_update_2
with
"Hs● Hl'"
)
as
"[Hs● Hl']"
.
{
eapply
auth_update
,
option_local_update
,
(
exclusive_local_update
_
(
Excl
_
)).
done
.
}
iMod
(
"Hclose"
with
"Hl'"
)
as
"HΦ"
.
iModIntro
.
...
...
@@ -283,7 +283,7 @@ Section stack.
iDestruct
"Hlist"
as
">%"
.
subst
stack_rep
.
iMod
"AU"
as
(
l'
)
"[Hl' [_ Hclose]]"
.
iDestruct
(
own_valid_2
with
"Hs● Hl'"
)
as
%[->%
Excl_included
%
leibniz_equiv
_
]%
auth_
valid_discrete_2
.
%[->%
Excl_included
%
leibniz_equiv
_
]%
auth_
both_valid
.
iMod
(
"Hclose"
with
"Hl'"
)
as
"HΦ"
.
iSplitR
"HΦ"
;
first
by
eauto
10
with
iFrame
.
iIntros
"!>"
.
wp_pures
.
by
iApply
"HΦ"
.
...
...
@@ -305,7 +305,7 @@ Section stack.
and we are done. *)
iMod
"AU"
as
(
l'
)
"[Hl' [_ Hclose]]"
.
iDestruct
(
own_valid_2
with
"Hs● Hl'"
)
as
%[->%
Excl_included
%
leibniz_equiv
_
]%
auth_
valid_discrete_2
.
%[->%
Excl_included
%
leibniz_equiv
_
]%
auth_
both_valid
.
destruct
l
as
[|
v'
l
]
;
simpl
.
{
(* Contradiction. *)
iDestruct
"Hlist"
as
">%"
.
done
.
}
iDestruct
"Hlist"
as
(
tail'
q'
rep'
)
"[>Heq [>Htail' Hlist]]"
.
...
...
@@ -345,13 +345,13 @@ Section stack.
iInv
stackN
as
(
stack_rep
offer_rep
l
)
"(>Hs● & >H↦ & Hlist & Hoff)"
.
iMod
"AUoff"
as
(
l'
)
"[Hl' [_ Hclose]]"
.
iDestruct
(
own_valid_2
with
"Hs● Hl'"
)
as
%[->%
Excl_included
%
leibniz_equiv
_
]%
auth_
valid_discrete_2
.
%[->%
Excl_included
%
leibniz_equiv
_
]%
auth_
both_valid
.
iMod
(
own_update_2
with
"Hs● Hl'"
)
as
"[Hs● Hl']"
.
{
eapply
auth_update
,
option_local_update
,
(
exclusive_local_update
_
(
Excl
_
)).
done
.
}
iMod
(
"Hclose"
with
"Hl'"
)
as
"HQoff"
.
iMod
"AU"
as
(
l'
)
"[Hl' [_ Hclose]]"
.
iDestruct
(
own_valid_2
with
"Hs● Hl'"
)
as
%[->%
Excl_included
%
leibniz_equiv
_
]%
auth_
valid_discrete_2
.
%[->%
Excl_included
%
leibniz_equiv
_
]%
auth_
both_valid
.
iMod
(
own_update_2
with
"Hs● Hl'"
)
as
"[Hs● Hl']"
.
{
eapply
auth_update
,
option_local_update
,
(
exclusive_local_update
_
(
Excl
_
)).
done
.
}
iMod
(
"Hclose"
with
"Hl'"
)
as
"HΦ"
.
...
...
theories/logatom/flat_combiner/misc.v
View file @
ffb27f4a
...
...
@@ -2,7 +2,7 @@
From
iris
.
program_logic
Require
Export
weakestpre
.
From
iris
.
heap_lang
Require
Export
lang
proofmode
notation
.
From
iris
.
algebra
Require
Import
auth
frac
gmap
agree
.
From
iris
.
algebra
Require
Import
excl
auth
frac
gmap
agree
.
From
iris
.
bi
Require
Import
fractional
.
From
iris
.
base_logic
Require
Import
auth
.
...
...
theories/logatom/snapshot/atomic_snapshot.v
View file @
ffb27f4a
...
...
@@ -160,11 +160,11 @@ Section atomic_snapshot.
wp_alloc
ly
as
"Hly"
.
set
(
Excl'
(
v1
,
v2
))
as
p
.
iMod
(
own_alloc
(
●
p
⋅
◯
p
))
as
(
γ
1
)
"[Hp⚫ Hp◯]"
.
{
rewrite
/
p
.
apply
auth_
valid_discrete_2
.
split
;
done
.
rewrite
/
p
.
apply
auth_
both_valid
.
split
;
done
.
}
set
(
new_timestamp
0
v1
)
as
t
.
iMod
(
own_alloc
(
●
gmap_to_UR
t
⋅
◯
gmap_to_UR
t
))
as
(
γ
2
)
"[Ht⚫ Ht◯]"
.
{
rewrite
/
t
/
new_timestamp
.
apply
auth_
valid_discrete_2
.
rewrite
/
t
/
new_timestamp
.
apply
auth_
both_valid
.
split
;
first
done
.
rewrite
/
gmap_to_UR
map_fmap_singleton
.
apply
singleton_valid
.
done
.
}
wp_pures
.
iApply
(
"Hp"
$!
(
γ
1
,
γ
2
)).
...
...
@@ -192,7 +192,7 @@ Section atomic_snapshot.
Proof
.
iIntros
"Hγ● Hγ◯"
.
iDestruct
(
own_valid_2
with
"Hγ● Hγ◯"
)
as
%[
H
%
Excl_included
%
leibniz_equiv
_
]%
auth_
valid_discrete_2
.
%[
H
%
Excl_included
%
leibniz_equiv
_
]%
auth_
both_valid
.
done
.
Qed
.
...
...
@@ -223,7 +223,7 @@ Section atomic_snapshot.
Proof
.
iIntros
"[Hγ⚫ Hγ◯]"
.
iDestruct
(
own_valid_2
with
"Hγ⚫ Hγ◯"
)
as
%[
H
Hv
]%
auth_
valid_discrete_2
.
iPureIntro
.
intros
t
x
HT2
.
%[
H
Hv
]%
auth_
both_valid
.
iPureIntro
.
intros
t
x
HT2
.
pose
proof
(
iffLR
(
lookup_included
(
gmap_to_UR
T2
)
(
gmap_to_UR
T1
))
H
t
)
as
Ht
.
rewrite
!
lookup_fmap
HT2
/=
in
Ht
.
destruct
(
is_Some_included
_
_
Ht
)
as
[?
[
t2
[
Ht2
->]]%
fmap_Some_1
]
;
first
by
eauto
.
...
...
theories/logatom/treiber2.v
View file @
ffb27f4a
...
...
@@ -156,7 +156,7 @@ Lemma auth_agree γ xs ys :
own
γ
(
●
(
Excl'
xs
))
-
∗
own
γ
(
◯
(
Excl'
ys
))
-
∗
⌜
xs
=
ys
⌝
.
Proof
.
iIntros
"Hγ● Hγ◯"
.
by
iDestruct
(
own_valid_2
with
"Hγ● Hγ◯"
)
as
%[<-%
Excl_included
%
leibniz_equiv
_
]%
auth_
valid_discrete_2
.
as
%[<-%
Excl_included
%
leibniz_equiv
_
]%
auth_
both_valid
.
Qed
.
(** The view of the authority can be updated together with the local view. *)
...
...
@@ -223,7 +223,8 @@ Proof.
our camera named [γ], containing the empty list. This step (and the next)
requires the fancy update modality that was introduced earlier. *)
iMod
(
own_alloc
(
●
(
Some
(
Excl
[]))
⋅
◯
(
Some
(
Excl
[]))))
as
(
γ
)
"[Hγ● Hγ◯]"
;
(* Validity is trivial. *)
first
done
.
as
(
γ
)
"[Hγ● Hγ◯]"
;
(* Validity is trivial. *)
first
by
apply
auth_both_valid
.
(* We can then allocate the invariant (with mask [N]). Note that we can use
[eauto 10 with iFrame] to prove [▷ stack_inv ℓ γ]. *)
iMod
(
inv_alloc
N
_
(
stack_inv
ℓ
γ
)
with
"[Hl Hγ●]"
)
...
...
theories/logrel/F_mu_ref/rules_binary.v
View file @
ffb27f4a
From
iris
.
program_logic
Require
Import
lifting
.
From
iris
.
algebra
Require
Import
auth
frac
agree
gmap
list
.
From
iris
.
algebra
Require
Import
excl
auth
frac
agree
gmap
list
.
From
iris_examples
.
logrel
.
F_mu_ref
Require
Export
rules
.
From
iris
.
proofmode
Require
Import
tactics
.
Import
uPred
.
...
...
@@ -65,7 +65,7 @@ Section cfg.
iInv
specN
as
">Hspec"
"Hclose"
.
iDestruct
"Hspec"
as
(
e''
σ
)
"[Hown %]"
.
iDestruct
(@
own_valid_2
with
"Hown Hj"
)
as
%[[?%
Excl_included
%
leibniz_equiv
_
]%
prod_included
Hvalid
]%
auth_
valid_discrete_2
;
subst
.
as
%[[?%
Excl_included
%
leibniz_equiv
_
]%
prod_included
Hvalid
]%
auth_
both_valid
;
subst
.
iMod
(
own_update_2
with
"Hown Hj"
)
as
"[Hown Hj]"
.
{
by
eapply
auth_update
,
prod_local_update_1
,
option_local_update
,
(
exclusive_local_update
_
(
Excl
(
fill
K
e'
))).
}
...
...
@@ -93,7 +93,7 @@ Section cfg.
iInv
specN
as
">Hinv'"
"Hclose"
.
iDestruct
"Hinv'"
as
(
e2
σ
)
"[Hown %]"
.
destruct
(
exist_fresh
(
dom
(
gset
positive
)
σ
))
as
[
l
Hl
%
not_elem_of_dom
].
iDestruct
(
own_valid_2
_
with
"Hown Hj"
)
as
%[[?%
Excl_included
%
leibniz_equiv
_
]%
prod_included
?]%
auth_
valid_discrete_2
.
as
%[[?%
Excl_included
%
leibniz_equiv
_
]%
prod_included
?]%
auth_
both_valid
.
subst
.
iMod
(
own_update_2
with
"Hown Hj"
)
as
"[Hown Hj]"
.
{
by
eapply
auth_update
,
prod_local_update_1
,
option_local_update
,
...
...
@@ -117,10 +117,10 @@ Section cfg.
rewrite
/
spec_ctx
/
tpool_mapsto
/
heapS_mapsto
.
iInv
specN
as
">Hinv'"
"Hclose"
.
iDestruct
"Hinv'"
as
(
e2
σ
)
"[Hown %]"
.
iDestruct
(
own_valid_2
_
with
"Hown Hj"
)
as
%[[?%
Excl_included
%
leibniz_equiv
_
]%
prod_included
?]%
auth_
valid_discrete_2
.
as
%[[?%
Excl_included
%
leibniz_equiv
_
]%
prod_included
?]%
auth_
both_valid
.
subst
.
iDestruct
(
own_valid_2
with
"Hown Hl"
)
as
%[[
_
?%
gen_heap_singleton_included
]%
prod_included
_
]%
auth_
valid_discrete_2
.
as
%[[
_
?%
gen_heap_singleton_included
]%
prod_included
_
]%
auth_
both_valid
.
iMod
(
own_update_2
with
"Hown Hj"
)
as
"[Hown Hj]"
.
{
by
eapply
auth_update
,
prod_local_update_1
,
option_local_update
,
(
exclusive_local_update
_
(
Excl
(
fill
K
(
of_val
v
)))).
}
...
...
@@ -139,10 +139,10 @@ Section cfg.
rewrite
/
spec_ctx
/
tpool_mapsto
/
heapS_mapsto
.
iInv
specN
as
">Hinv'"
"Hclose"
.
iDestruct
"Hinv'"
as
(
e2
σ
)
"[Hown %]"
.
iDestruct
(
own_valid_2
_
with
"Hown Hj"
)
as
%[[?%
Excl_included
%
leibniz_equiv
_
]%
prod_included
?]%
auth_
valid_discrete_2
.
as
%[[?%
Excl_included
%
leibniz_equiv
_
]%
prod_included
?]%
auth_
both_valid
.
subst
.
iDestruct
(
own_valid_2
_
with
"Hown Hl"
)
as
%[[
_
Hl
%
gen_heap_singleton_included
]%
prod_included
_
]%
auth_
valid_discrete_2
.
as
%[[
_
Hl
%
gen_heap_singleton_included
]%
prod_included
_
]%
auth_
both_valid
.
iMod
(
own_update_2
with
"Hown Hj"
)
as
"[Hown Hj]"
.
{
by
eapply
auth_update
,
prod_local_update_1
,
option_local_update
,
(
exclusive_local_update
_
(
Excl
(
fill
K
Unit
))).
}
...
...
theories/logrel/F_mu_ref/soundness.v
View file @
ffb27f4a
...
...
@@ -17,7 +17,7 @@ Proof.
eapply
(
wp_adequacy
Σ
_
)
;
eauto
.
iIntros
(
Hinv
?).
iMod
(
own_alloc
(
●
to_gen_heap
σ
))
as
(
γ
)
"Hh"
.
{
apply
(
auth_auth_valid
_
(
to_gen_heap_valid
_
_
σ
))
.
}
{
by
apply
auth_auth_valid
,
to_gen_heap_valid
.
}
iModIntro
.
iExists
(
λ
σ
_
,
own
γ
(
●
to_gen_heap
σ
))
;
iFrame
.
set
(
Heap
Σ
:
=
(
HeapG
Σ
Hinv
(
GenHeapG
_
_
Σ
_
_
_
γ
))).
iApply
(
wp_wand
with
"[]"
).
...
...
theories/logrel/F_mu_ref/soundness_binary.v
View file @
ffb27f4a
From
iris_examples
.
logrel
.
F_mu_ref
Require
Export
context_refinement
.
From
iris
.
algebra
Require
Import
auth
frac
agree
.
From
iris
.
algebra
Require
Import
excl
auth
frac
agree
.
From
iris
.
proofmode
Require
Import
tactics
.
From
iris
.
program_logic
Require
Import
adequacy
.
From
iris_examples
.
logrel
.
F_mu_ref
Require
Import
soundness
.
...
...
@@ -16,10 +16,10 @@ Proof.
eapply
(
wp_adequacy
Σ
)
;
first
by
apply
_
.
iIntros
(
Hinv
?).
iMod
(
own_alloc
(
●
to_gen_heap
∅
))
as
(
γ
)
"Hh"
.
{
apply
(
auth_auth_valid
_
(
to_gen_heap_valid
_
_
∅
))
.
}
{
by
apply
auth_auth_valid
,
to_gen_heap_valid
.
}
iMod
(
own_alloc
(
●
(
Excl'
e'
,
∅
)
⋅
◯
((
Excl'
e'
,
∅
)
:
cfgUR
)))
as
(
γ
c
)
"[Hcfg1 Hcfg2]"
.
{
apply
auth_
valid_discrete_2
.
split
=>//.
}
{
apply
auth_
both_valid
.
split
=>//.
}
set
(
Hcfg
:
=
CFGSG
_
_
γ
c
).
iMod
(
inv_alloc
specN
_
(
spec_ctx
([
e'
],
∅
))
with
"[Hcfg1]"
)
as
"#Hcfg"
.
{
iNext
.
iExists
e'
,
∅
.
iSplit
;
eauto
.
...
...
@@ -38,7 +38,7 @@ Proof.
iDestruct
"Hinv"
as
(
e''
σ
)
"[Hown %]"
.
rewrite
/
tpool_mapsto
/=.
iDestruct
(
own_valid_2
with
"Hown Hj"
)
as
%
Hvalid
.
move
:
Hvalid
=>
/
auth_
valid_discrete_2
move
:
Hvalid
=>
/
auth_
both_valid
[/
prod_included
[
Hv2
_
]
_
].
apply
Excl_included
,
leibniz_equiv
in
Hv2
.
subst
.
iMod
(
"Hclose"
with
"[-]"
)
as
"_"
.
+
iExists
(#
v2
),
σ
.
auto
.
...
...
theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
View file @
ffb27f4a
...
...
@@ -47,7 +47,7 @@ Section Stack_refinement.
simpl
.
iApply
wp_pure_step_later
;
trivial
.
iNext
.
simpl
.
iAsimpl
.
(* establishing the invariant *)
iMod
(
own_alloc
(
●
(
∅
:
stackUR
)))
as
(
γ
)
"Hemp"
;
first
done
.
iMod
(
own_alloc
(
●
(
∅
:
stackUR
)))
as
(
γ
)
"Hemp"
;
first
by
apply
auth_auth_valid
.
set
(
istkG
:
=
StackG
_
_
γ
).
change
γ
with
(@
stack_name
_
istkG
).
change
H1
with
(@
stack_inG
_
istkG
).
...
...
theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
View file @
ffb27f4a
...
...
@@ -25,7 +25,7 @@ Section Rules.
Lemma
stack_mapstos_agree
l
v
w
:
l
↦ˢᵗᵏ
v
∗
l
↦ˢᵗᵏ
w
⊢
⌜
v
=
w
⌝
.
Proof
.
rewrite
-
own_op
-
auth_frag_op
op_singleton
own_valid
.
by
iIntros
(->%
auth_
own
_valid
%
singleton_valid
%
agree_op_invL'
).
by
iIntros
(->%
auth_
frag
_valid
%
singleton_valid
%
agree_op_invL'
).
Qed
.
Program
Definition
StackLink_pre
(
Q
:
D
)
:
D
-
n
>
D
:
=
λ
ne
P
v
,
...
...
@@ -94,7 +94,7 @@ Section Rules.
Proof
.
iIntros
"[Howns Hls] Hl"
.
iDestruct
(
own_valid_2
with
"Howns Hl"
)
as
%[[
az
[
Haz
Hq
]]%
singleton_included
_
]%
auth_
valid_discrete_2
.
as
%[[
az
[
Haz
Hq
]]%
singleton_included
_
]%
auth_
both_valid
.
rewrite
lookup_fmap
in
Haz
.
assert
(
∃
z
,
h
!!
l
=
Some
z
)
as
Hz
.
{
revert
Haz
;
case
:
(
h
!!
l
)
=>
[
z
|]
Hz
;
first
(
by
eauto
)
;
inversion
Hz
.
}
...
...
theories/logrel/F_mu_ref_conc/rules_binary.v
View file @
ffb27f4a
From
iris
.
program_logic
Require
Export
language
ectx_language
ectxi_language
.
From
iris
.
program_logic
Require
Import
lifting
.
From
iris
.
algebra
Require
Import
auth
frac
agree
gmap
list
.
From
iris
.
algebra
Require
Import
excl
auth
frac
agree
gmap
list
.
From
iris_examples
.
logrel
.
F_mu_ref_conc
Require
Export
rules
.
From
iris
.
proofmode
Require
Import
tactics
.
Import
uPred
.
...
...
@@ -174,7 +174,7 @@ Section cfg.
iInv
specN
as
(
tp
σ
)
">[Hown Hrtc]"
"Hclose"
.
iDestruct
"Hrtc"
as
%
Hrtc
.
iDestruct
(
own_valid_2
with
"Hown Hj"
)
as
%[[
Htpj
%
tpool_singleton_included'
_
]%
prod_included
?]%
auth_
valid_discrete_2
.
as
%[[
Htpj
%
tpool_singleton_included'
_
]%
prod_included
?]%
auth_
both_valid
.
iMod
(
own_update_2
with
"Hown Hj"
)
as
"[Hown Hj]"
.
{
by
eapply
auth_update
,
prod_local_update_1
,
singleton_local_update
,
(
exclusive_local_update
_
(
Excl
(
fill
K
e'
))).
}
...
...
@@ -221,7 +221,7 @@ Section cfg.
iInv
specN
as
(
tp
σ
)
">[Hown %]"
"Hclose"
.
destruct
(
exist_fresh
(
dom
(
gset
positive
)
σ
))
as
[
l
Hl
%
not_elem_of_dom
].
iDestruct
(
own_valid_2
with
"Hown Hj"
)
as
%[[?%
tpool_singleton_included'
_
]%
prod_included
?]%
auth_
valid_discrete_2
.
as
%[[?%
tpool_singleton_included'
_
]%
prod_included
?]%
auth_
both_valid
.
iMod
(
own_update_2
with
"Hown Hj"
)
as
"[Hown Hj]"
.
{
by
eapply
auth_update
,
prod_local_update_1
,
singleton_local_update
,
(
exclusive_local_update
_
(
Excl
(
fill
K
(
Loc
l
)))).
}
...
...
@@ -244,9 +244,10 @@ Section cfg.
rewrite
/
spec_ctx
/
tpool_mapsto
/
heapS_mapsto
.
iInv
specN
as
(
tp
σ
)
">[Hown %]"
"Hclose"
.
iDestruct
(
own_valid_2
with
"Hown Hj"
)
as
%[[?%
tpool_singleton_included'
_
]%
prod_included
?]%
auth_
valid_discrete_2
.
as
%[[?%
tpool_singleton_included'
_
]%
prod_included
?]%
auth_
both_valid
.
iDestruct
(
own_valid_2
with
"Hown Hl"
)
as
%[[?
?%
gen_heap_singleton_included
]%
prod_included
?]%
auth_valid_discrete_2
.
iMod
(
own_update_2
with
"Hown Hj"
)
as
"[Hown Hj]"
.
as
%[[?
?%
gen_heap_singleton_included
]%
prod_included
?]%
auth_both_valid
.
iMod
(
own_update_2
with
"Hown Hj"
)
as
"[Hown Hj]"
.
{
by
eapply
auth_update
,
prod_local_update_1
,
singleton_local_update
,
(
exclusive_local_update
_
(
Excl
(
fill
K
(
of_val
v
)))).
}
iFrame
"Hj Hl"
.
iApply
"Hclose"
.
iNext
.
...
...
@@ -264,9 +265,9 @@ Section cfg.
rewrite
/
spec_ctx
/
tpool_mapsto
/
heapS_mapsto
.
iInv
specN
as
(
tp
σ
)
">[Hown %]"
"Hclose"
.
iDestruct
(
own_valid_2
with
"Hown Hj"
)
as
%[[?%
tpool_singleton_included'
_
]%
prod_included
_
]%
auth_
valid_discrete_2
.
as
%[[?%
tpool_singleton_included'
_
]%
prod_included
_
]%
auth_
both_valid
.
iDestruct
(
own_valid_2
with
"Hown Hl"
)
as
%[[
_
Hl
%
gen_heap_singleton_included
]%
prod_included
_
]%
auth_
valid_discrete_2
.
as
%[[
_
Hl
%
gen_heap_singleton_included
]%
prod_included
_
]%
auth_
both_valid
.
iMod
(
own_update_2
with
"Hown Hj"
)
as
"[Hown Hj]"
.
{
by
eapply
auth_update
,
prod_local_update_1
,
singleton_local_update
,
(
exclusive_local_update
_
(
Excl
(
fill
K
Unit
))).
}
...
...
@@ -289,9 +290,9 @@ Section cfg.
rewrite
/
spec_ctx
/
tpool_mapsto
/
heapS_mapsto
.
iInv
specN
as
(
tp
σ
)
">[Hown %]"
"Hclose"
.
iDestruct
(
own_valid_2
with
"Hown Hj"
)
as
%[[?%
tpool_singleton_included'
_
]%
prod_included
?]%
auth_
valid_discrete_2
.
as
%[[?%
tpool_singleton_included'
_
]%
prod_included
?]%
auth_
both_valid
.
iDestruct
(
own_valid_2
with
"Hown Hl"
)
as
%[[
_
?%
gen_heap_singleton_included
]%
prod_included
_
]%
auth_
valid_discrete_2
.
as
%[[
_
?%
gen_heap_singleton_included
]%
prod_included
_
]%
auth_
both_valid
.
iMod
(
own_update_2
with
"Hown Hj"
)
as
"[Hown Hj]"
.
{
by
eapply
auth_update
,
prod_local_update_1
,
singleton_local_update
,
(
exclusive_local_update
_
(
Excl
(
fill
K
(#
♭
false
)))).
}
...
...
@@ -310,9 +311,9 @@ Section cfg.
rewrite
/
spec_ctx
/
tpool_mapsto
/
heapS_mapsto
.
iInv
specN
as
(
tp
σ
)
">[Hown %]"
"Hclose"
.
iDestruct
(
own_valid_2
with
"Hown Hj"
)
as
%[[?%
tpool_singleton_included'
_
]%
prod_included
_
]%
auth_
valid_discrete_2
.
as
%[[?%
tpool_singleton_included'
_
]%
prod_included
_
]%
auth_
both_valid
.
iDestruct
(
own_valid_2
with
"Hown Hl"
)
as
%[[
_
Hl
%
gen_heap_singleton_included
]%
prod_included
_
]%
auth_
valid_discrete_2
.
as
%[[
_
Hl
%
gen_heap_singleton_included
]%
prod_included
_
]%
auth_
both_valid
.
iMod
(
own_update_2
with
"Hown Hj"
)
as
"[Hown Hj]"
.
{
by
eapply
auth_update
,
prod_local_update_1
,
singleton_local_update
,
(
exclusive_local_update
_
(
Excl
(
fill
K
(#
♭
true
)))).
}
...
...
@@ -405,7 +406,7 @@ Section cfg.
iIntros
(?)
"[#Hspec Hj]"
.
rewrite
/
spec_ctx
/
tpool_mapsto
.
iInv
specN
as
(
tp
σ
)
">[Hown %]"
"Hclose"
.
iDestruct
(
own_valid_2
with
"Hown Hj"
)
as
%[[?%
tpool_singleton_included'
_
]%
prod_included
?]%
auth_
valid_discrete_2
.
as
%[[?%
tpool_singleton_included'
_
]%
prod_included
?]%
auth_
both_valid
.
assert
(
j
<
length
tp
)
by
eauto
using
lookup_lt_Some
.
iMod
(
own_update_2
with
"Hown Hj"
)
as
"[Hown Hj]"
.
{
by
eapply
auth_update
,
prod_local_update_1
,
...
...
theories/logrel/F_mu_ref_conc/soundness_binary.v
View file @
ffb27f4a
...
...
@@ -15,10 +15,10 @@ Proof.
{
destruct
1
;
naive_solver
.
}
eapply
(
wp_adequacy
Σ
_
)
;
iIntros
(
Hinv
?).
iMod
(
own_alloc
(
●
to_gen_heap
∅
))
as
(
γ
)
"Hh"
.
{
apply
(
auth_auth_valid
_
(
to_gen_heap_valid
_
_
∅
))
.
}
{
by
apply
auth_auth_valid
,
to_gen_heap_valid
.
}
iMod
(
own_alloc
(
●
(
to_tpool
[
e'
],
∅
)
⋅
◯
((
to_tpool
[
e'
]
:
tpoolUR
,
∅
)
:
cfgUR
)))
as
(
γ
c
)
"[Hcfg1 Hcfg2]"
.
{
apply
auth_
valid_discrete_2
.
split
=>//.
split
=>//.
apply
to_tpool_valid
.
}
{
apply
auth_
both_valid
.
split
=>//.
split
=>//.
apply
to_tpool_valid
.
}
set
(
Hcfg
:
=
CFGSG
_
_
γ
c
).
iMod
(
inv_alloc
specN
_
(
spec_inv
([
e'
],
∅
))
with
"[Hcfg1]"
)
as
"#Hcfg"
.
{
iNext
.
iExists
[
e'
],
∅
.
rewrite
/
to_gen_heap
fin_maps
.
map_fmap_empty
.
auto
.
}
...
...
@@ -36,7 +36,7 @@ Proof.
iInv
specN
as
(
tp
σ
)
">[Hown Hsteps]"
"Hclose"
;
iDestruct
"Hsteps"
as
%
Hsteps'
.
rewrite
/
tpool_mapsto
/=.
iDestruct
(
own_valid_2
with
"Hown Hj"
)
as
%
Hvalid
.
move
:
Hvalid
=>
/
auth_
valid_discrete_2
move
:
Hvalid
=>
/
auth_
both_valid
[/
prod_included
[/
tpool_singleton_included
Hv2
_
]
_
].
destruct
tp
as
[|?
tp'
]
;
simplify_eq
/=.
iMod
(
"Hclose"
with
"[-]"
)
as
"_"
;
[
iExists
(
_
::
tp'
),
σ
;
auto
|].
...
...
theories/logrel/F_mu_ref_conc/soundness_unary.v
View file @
ffb27f4a
...
...
@@ -16,7 +16,7 @@ Proof.
intros
Hlog
??.
cut
(
adequate
NotStuck
e
σ
(
λ
_
_
,
True
))
;
first
(
intros
[
_
?]
;
eauto
).
eapply
(
wp_adequacy
Σ
_
).
iIntros
(
Hinv
?).
iMod
(
own_alloc
(
●
to_gen_heap
σ
))
as
(
γ
)
"Hh"
.
{
apply
(
auth_auth_valid
_
(
to_gen_heap_valid
_
_
σ
))
.
}
{
by
apply
auth_auth_valid
,
to_gen_heap_valid
.
}
iModIntro
.
iExists
(
λ
σ
_
,
own
γ
(
●
to_gen_heap
σ
))
;
iFrame
.
set
(
Heap
Σ
:
=
(
HeapIG
Σ
Hinv
(
GenHeapG
_
_
Σ
_
_
_
γ
))).
iApply
(
wp_wand
with
"[]"
).
...
...
theories/logrel_heaplang/lib/symbol_adt.v
View file @
ffb27f4a
...
...
@@ -31,13 +31,16 @@ Section symbol_ghosts.
Proof
.
apply
_
.
Qed
.
Lemma
counter_exclusive
γ
n1
n2
:
counter
γ
n1
-
∗
counter
γ
n2
-
∗
False
.
Proof
.
apply
bi
.
wand_intro_r
.
by
rewrite
-
own_op
own_valid
auth_validI
.
Qed
.
Proof
.
apply
bi
.
wand_intro_r
.
rewrite
-
own_op
own_valid
/=.
by
iDestruct
1
as
%[].
Qed
.
Global
Instance
symbol_persistent
γ
n
:
Persistent
(
symbol
γ
n
).
Proof
.
apply
_
.
Qed
.
Lemma
counter_alloc
n
:
(|==>
∃
γ
,
counter
γ
n
)%
I
.
Proof
.
iMod
(
own_alloc
(
●
(
n
:
mnat
)
⋅
◯
(
n
:
mnat
)))
as
(
γ
)
"[Hγ Hγf]"
;
first
done
.
iMod
(
own_alloc
(
●
(
n
:
mnat
)
⋅
◯
(
n
:
mnat
)))
as
(
γ
)
"[Hγ Hγf]"
;
first
by
apply
auth_both_valid
.
iExists
γ
.
by
iFrame
.
Qed
.
...
...
@@ -50,7 +53,7 @@ Section symbol_ghosts.
Lemma
symbol_obs
γ
s
n
:
counter
γ
n
-
∗
symbol
γ
s
-
∗
⌜
(
s
<
n
)%
nat
⌝
.
Proof
.
iIntros
"Hc Hs"
.
iDestruct
(
own_valid_2
with
"Hc Hs"
)
as
%[?%
mnat_included
_
]%
auth_
valid_discrete_2
.
iDestruct
(
own_valid_2
with
"Hc Hs"
)
as
%[?%
mnat_included
_
]%
auth_
both_valid
.
iPureIntro
.
omega
.
Qed
.
End
symbol_ghosts
.
...
...
theories/spanning_tree/mon.v
View file @
ffb27f4a
...
...
@@ -48,7 +48,7 @@ Section marking_definitions.
own
graph_marking_name
(
●
(
m
⋅
({[
l
]}
:
gset
loc
)))
∗
is_marked
l
.
Proof
.
iIntros
"H"
.
rewrite
-
own_op
(
comm
_
m
).
iMod
(
@
own_update
with
"H"
)
as
"Y"
;
eauto
.
iMod
(
own_update
with
"H"
)
as
"Y"
;
eauto
.
apply
auth_update_alloc
.
setoid_replace
({[
l
]}
:
gset
loc
)
with
(({[
l
]}
:
gset
loc
)
⋅
∅
)
at
2
by
(
by
rewrite
right_id
).
...
...
@@ -189,10 +189,10 @@ Section graph_ctx_alloc.
∗
own_graph
1
%
Qp
∅
.
Proof
.
iIntros
"H1"
.
iMod
(
own_alloc
(
●
(
∅
:
markingUR
)))
as
(
mn
)
"H2"
;
first
done
.
iMod
(
own_alloc
(
●
(
∅
:
markingUR
)))
as
(
mn
)
"H2"
;
first
by
apply
auth_auth_valid
.
iMod
(
own_alloc
(
●
(
Some
(
1
%
Qp
,
∅
:
Gmon
)
:
graphUR
)
⋅
◯
(
Some
(
1
%
Qp
,
∅
:
Gmon
)
:
graphUR
)))
as
(
gn
)
"H3"
.
{
done
.
}
{
by
apply
auth_both_valid
.
}
iDestruct
"H3"
as
"[H31 H32]"
.
set
(
Ig
:
=
GraphG
_
_
mn
_
gn
).
iExists
Ig
.
...
...
@@ -279,7 +279,8 @@ Section graph.
Lemma
auth_own_graph_valid
q
G
:
own
graph_name
(
●
Some
(
q
,
G
))
⊢
✓
G
.
Proof
.
iIntros
"H"
.
unfold
own_graph
.
by
iDestruct
(
own_valid
with
"H"
)
as
%[
_
[
_
?]].
iDestruct
(
own_valid
with
"H"
)
as
%
VAL
.
move
:
VAL
=>
/
auth_auth_valid
[
_
?]
//.
Qed
.
Lemma
whole_frac
(
G
G'
:
Gmon
)
:
...
...
@@ -287,10 +288,8 @@ Section graph.
Proof
.
iIntros
"[H1 H2]"
.
rewrite
/
own_graph
.
iCombine
"H1"
"H2"
as
"H"
.
iDestruct
(
own_valid
with
"H"
)
as
%[
H1
H2
]
;
cbn
in
*
.
iDestruct
(
own_valid
with
"H"
)
as
%[
H1
H2
]
%
auth_both_valid
.
iPureIntro
.
specialize
(
H1
O
).
apply
cmra_discrete_included_iff
in
H1
.
apply
option_included
in
H1
;
destruct
H1
as
[
H1
|
H1
]
;
[
inversion
H1
|].
destruct
H1
as
(
u1
&
u2
&
Hu1
&
Hu2
&
H3
)
;
inversion
Hu1
;
inversion
Hu2
;
subst
.
...
...
@@ -345,10 +344,8 @@ Section graph.
⊢
⌜
G
=
{[
x
:
=
Excl
w
]}
⋅
(
delete
x
G
)
⌝
.
Proof
.
rewrite
/
own_graph
-
?own_op
.
iIntros
"H"
.
iDestruct
(
@
own_valid
with
"H"
)
as
%[
H1
H2
]
;
simpl
in
*
.
iDestruct
(
own_valid
with
"H"
)
as
%[
H1
H2
]%
auth_both_valid
.
iPureIntro
.
specialize
(
H1
O
).
apply
cmra_discrete_included_iff
in
H1
.
apply
option_included
in
H1
;
destruct
H1
as
[
H1
|
H1
]
;
[
inversion
H1
|].
destruct
H1
as
(
u1
&
u2
&
Hu1
&
Hu2
&
H1
)
;
inversion
Hu1
;
inversion
Hu2
;
subst
.
...
...
@@ -399,7 +396,8 @@ Section graph.
Proof
.
iIntros
"H"
.
unfold
is_marked
.
rewrite
-
own_op
.
iDestruct
(
own_valid
with
"H"
)
as
%
Hvl
.
iPureIntro
.
destruct
Hvl
as
[
Hvl
_
].
destruct
(
Hvl
O
)
as
[
z
Hvl'
].
move
:
Hvl
=>
/
auth_both_valid
[[
z
Hvl'
]
_
].
iPureIntro
.
rewrite
Hvl'
/=
!
gset_op_union
!
elem_of_union
elem_of_singleton
;
tauto
.
Qed
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment