Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Fairis
Commits
b0b957ca
Commit
b0b957ca
authored
Oct 23, 2018
by
Ralf Jung
Browse files
bump Iris
parent
c25061df
Pipeline
#12718
failed with stage
in 1 minute and 1 second
Changes
3
Pipelines
17
Hide whitespace changes
Inline
Side-by-side
opam
View file @
b0b957ca
...
...
@@ -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-
07-13.0.cbf73155
") | (= "dev") }
"coq-iris" { (= "dev.2018-
10-22.3.4842a060
") | (= "dev") }
]
theories/prelude/set_finite_setoid.v
View file @
b0b957ca
...
...
@@ -58,7 +58,7 @@ Proof.
**
apply
elem_of_app
.
left
.
rewrite
Hsingle
in
Hequiv
*
.
rewrite
leibniz_equiv_iff
.
intros
;
subst
.
eapply
elem_of_map
.
eapply
Hinl
.
eauto
.
eapply
list
.
elem_of_map
.
eapply
Hinl
.
eauto
.
Qed
.
Lemma
app_eq_disjoint_set
:
...
...
@@ -333,7 +333,7 @@ Proof.
specialize
(
Hfin_in
_
f_in
).
edestruct
(
Hin_l
'
(
f
x
))
as
(
X
'
&
Hsnd
&
Hfin
&
Hin_block
);
eauto
.
exists
X
'
.
split
.
*
replace
X
'
with
(
snd
(
f
x
,
X
'
));
last
auto
.
eapply
elem_of_map
.
*
replace
X
'
with
(
snd
(
f
x
,
X
'
));
last
auto
.
eapply
list
.
elem_of_map
.
eauto
.
*
eapply
Hin_block
;
eauto
.
Qed
.
...
...
@@ -362,7 +362,7 @@ Proof.
edestruct
Hfin_in
as
(
x
'
&?&?
).
edestruct
(
Hin_l
'
x
'
)
as
(
X
'
&
Hsnd
&
Hfin
&
Hin_block
);
eauto
.
exists
X
'
.
split
.
*
replace
X
'
with
(
snd
(
x
'
,
X
'
));
last
auto
.
eapply
elem_of_map
.
*
replace
X
'
with
(
snd
(
x
'
,
X
'
));
last
auto
.
eapply
list
.
elem_of_map
.
eauto
.
*
eapply
Hin_block
;
eauto
.
Qed
.
...
...
@@ -392,7 +392,7 @@ Qed.
edestruct
Hfin_in
as
(
x
'
&?&?
).
edestruct
(
Hin_l
'
x
'
)
as
(
X
'
&
Hsnd
&
Hfin
&
Hin_block
);
eauto
.
exists
X
'
.
split
.
*
replace
X
'
with
(
snd
(
x
'
,
X
'
));
last
auto
.
eapply
elem_of_map
.
*
replace
X
'
with
(
snd
(
x
'
,
X
'
));
last
auto
.
eapply
list
.
elem_of_map
.
eauto
.
*
eapply
Hin_block
;
eauto
.
rewrite
Heq
.
econstructor
;
eauto
.
...
...
@@ -413,7 +413,7 @@ Qed.
exists
(
map
(
λ
a
,
(
a
,
y
))
l
).
intros
x
.
inversion
1.
subst
.
destruct
x
;
subst
.
simpl
.
eapply
(
elem_of_map
(
λ
a
:
X
,
(
a
,
y
))
_
x
).
eapply
(
list
.
elem_of_map
(
λ
a
:
X
,
(
a
,
y
))
_
x
).
eauto
.
*
intros
x
.
inversion
1.
subst
.
intros
.
subst
.
split
;
auto
.
...
...
@@ -444,7 +444,7 @@ Qed.
edestruct
(
Hinl
x
)
as
(
x
'
&
Hequiv
&
Hin
);
eauto
.
exists
(
x
'
,
y
).
split
;
auto
.
**
econstructor
;
auto
.
**
eapply
(
elem_of_map
(
λ
a
:
X
,
(
a
,
y
))
_
x
'
).
eauto
.
**
eapply
(
list
.
elem_of_map
(
λ
a
:
X
,
(
a
,
y
))
_
x
'
).
eauto
.
*
intros
x
.
inversion
1.
subst
.
intros
.
subst
.
split
;
auto
.
-
auto
.
...
...
@@ -520,7 +520,7 @@ Qed.
**
left
.
**
rewrite
-
app_comm_cons
in
Heq
.
inversion
Heq
;
subst
.
right
.
eapply
elem_of_map
.
right
.
eapply
list
.
elem_of_map
.
apply
Hin_L
.
exists
lext
.
eauto
.
Qed
.
...
...
@@ -629,7 +629,7 @@ Qed.
inversion
Heq2
;
subst
.
right
.
assert
(
l
''
++
[
a
'
]
=
(
λ
l
'
,
l
'
++
[
a
'
])
l
''
)
as
Heq
;
auto
.
eapply
(
elem_of_map
(
λ
l
'
,
l
'
++
[
a
'
])
_
l
''
).
eapply
(
list
.
elem_of_map
(
λ
l
'
,
l
'
++
[
a
'
])
_
l
''
).
eapply
Hin_L
.
exists
lext
.
eauto
.
Qed
.
...
...
theories/program_logic/adequacy_inf.v
View file @
b0b957ca
Require
ClassicalEpsilon
.
From
fri
.
algebra
Require
Export
irelations
.
From
fri
.
prelude
Require
Import
list
set_finite_setoid
.
From
fri
.
prelude
Require
Import
set_finite_setoid
list
.
From
fri
.
program_logic
Require
Export
hoare
.
From
fri
.
program_logic
Require
Import
wsat
ownership
.
From
fri
.
program_logic
Require
Import
adequacy
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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