Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Dan Frumin
ReLoC-v1
Commits
efe1b574
Commit
efe1b574
authored
Jul 06, 2016
by
Robbert Krebbers
Browse files
Fix for solve_ndisj no longer being able to fail due to Iris 65296d1a.
parent
8400d728
Changes
1
Hide whitespace changes
Inline
Side-by-side
F_mu_ref_par/fundamental_binary.v
View file @
efe1b574
...
...
@@ -321,8 +321,8 @@ Section fundamental.
iTimeless
"Hw2"
.
iPvs
(
step_load
_
_
j
K
l
'
1
w
'
with
"[Hv Hw2]"
)
as
"[Hv Hw2]"
;
[
unfold
logN
,
specN
;
solve_ndisj
|
by
iFrame
|
].
iApply
(
wp_load
_
_
1
);
[
|
iFrame
"Hh"
];
trivial
;
try
unfold
logN
,
heapN
;
solve_ndisj
.
iApply
(
wp_load
_
_
1
);
[
|
iFrame
"Hh"
];
trivial
.
unfold
logN
,
heapN
;
solve_ndisj
.
iIntros
"{$Hw1} > Hw1"
.
iPvsIntro
.
iSplitL
"Hw1 Hw2"
.
-
iNext
;
iExists
(
w
,
w
'
);
by
iFrame
.
-
iExists
w
'
;
by
iFrame
.
...
...
@@ -371,21 +371,21 @@ Section fundamental.
destruct
(
decide
(
v
=
w
))
as
[
|
Hneq
];
subst
.
-
iPvs
(
step_cas_suc
_
_
j
K
l
'
(#
w
'
)
w
'
v
'
(#
u
'
)
u
'
with
"[Hu Hv2]"
)
as
"[Hw Hv2]"
;
simpl
;
eauto
;
first
unfold
logN
,
specN
;
solve_ndisj
.
first
(
unfold
logN
,
specN
;
solve_ndisj
)
.
{
iIntros
"{$Hs $Hu $Hv2} >"
.
rewrite
?
interp_EqType_agree
;
trivial
.
by
iSimplifyEq
.
}
iApply
wp_cas_suc
;
eauto
using
to_of_val
;
first
unfold
logN
,
heapN
;
solve_ndisj
.
first
(
unfold
logN
,
heapN
;
solve_ndisj
)
.
iIntros
"{$Hh $Hv1} > Hv1"
.
iPvsIntro
.
iSplitL
"Hv1 Hv2"
.
+
iNext
;
iExists
(
_
,
_
);
by
iFrame
.
+
iExists
(
♭
v
true
);
iFrame
;
eauto
.
-
iPvs
(
step_cas_fail
_
_
j
K
l
'
1
v
'
(#
w
'
)
w
'
(#
u
'
)
u
'
with
"[Hu Hv2]"
)
as
"[Hw Hv2]"
;
simpl
;
eauto
;
first
unfold
logN
,
specN
;
solve_ndisj
.
first
(
unfold
logN
,
specN
;
solve_ndisj
)
.
{
iIntros
"{$Hs $Hu $Hv2} >"
.
rewrite
?
interp_EqType_agree
;
trivial
.
by
iSimplifyEq
.
}
iApply
wp_cas_fail
;
eauto
using
to_of_val
;
first
unfold
logN
,
heapN
;
solve_ndisj
.
first
(
unfold
logN
,
heapN
;
solve_ndisj
)
.
iIntros
"{$Hh $Hv1} > Hv1"
.
iPvsIntro
.
iSplitL
"Hv1 Hv2"
.
+
iNext
;
iExists
(
_
,
_
);
by
iFrame
.
+
iExists
(
♭
v
false
);
eauto
.
...
...
Write
Preview
Supports
Markdown
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