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
Iris
Iris
Commits
0b05b368
Commit
0b05b368
authored
Jan 21, 2016
by
Ralf Jung
Browse files
Merge branch 'v2.0' of gitlab.mpi-sws.org:FP/iris-coq into v2.0
parents
b2ec2711
161e23ca
Changes
13
Hide whitespace changes
Inline
Side-by-side
.gitmodules
deleted
100644 → 0
View file @
b2ec2711
[submodule "autosubst"]
path = autosubst
url = https://github.com/tebbi/autosubst.git
_CoqProject
View file @
0b05b368
-Q . ""
-R autosubst/theories Autosubst
autosubst
@
07c66946
Compare
07c66946
...
07c66946
Subproject commit 07c669460cd84e6e0b2084e870b19f947b699ded
barrier/heap_lang.v
View file @
0b05b368
Require
Import
Autosubst
.
Autosubst
.
Require
Import
prelude
.
option
prelude
.
gmap
iris
.
language
iris
.
parameter
.
Set
Bullet
Behavior
"Strict Subproofs"
.
Require
Import
prelude
.
option
prelude
.
gmap
iris
.
parameter
.
(** Some tactics useful when dealing with equality of sigma-like types: existT T0 t0 = existT T1 t1.
They all assume such an equality is the first thing on the "stack" (goal). *)
...
...
iris/adequacy.v
0 → 100644
View file @
0b05b368
Require
Export
iris
.
hoare
.
Require
Import
iris
.
wsat
.
Local
Hint
Extern
10
(
_
≤
_
)
=>
omega
.
Local
Hint
Extern
100
(@
eq
coPset
_
_
)
=>
eassumption
||
solve_elem_of
.
Local
Hint
Extern
10
(
✓
{
_
}
_
)
=>
repeat
match
goal
with
H
:
wsat
_
_
_
_
|-
_
=>
apply
wsat_valid
in
H
end
;
solve_validN
.
Section
adequacy
.
Context
{
Σ
:
iParam
}.
Implicit
Types
e
:
iexpr
Σ
.
Implicit
Types
Q
:
ival
Σ
→
iProp
Σ
.
Transparent
uPred_holds
.
Notation
wptp
n
:
=
(
Forall3
(
λ
e
Q
r
,
uPred_holds
(
wp
coPset_all
e
Q
)
n
r
)).
Lemma
wptp_le
Qs
es
rs
n
n'
:
✓
{
n'
}
(
big_op
rs
)
→
wptp
n
es
Qs
rs
→
n'
≤
n
→
wptp
n'
es
Qs
rs
.
Proof
.
induction
2
;
constructor
;
eauto
using
uPred_weaken
.
Qed
.
Lemma
nsteps_wptp
Qs
k
n
t
σ
1
t
σ
2
rs1
:
nsteps
step
k
t
σ
1
t
σ
2
→
1
<
n
→
wptp
(
k
+
n
)
(
t
σ
1
.
1
)
Qs
rs1
→
wsat
(
k
+
n
)
coPset_all
(
t
σ
1
.
2
)
(
big_op
rs1
)
→
∃
rs2
Qs'
,
wptp
n
(
t
σ
2
.
1
)
(
Qs
++
Qs'
)
rs2
∧
wsat
n
coPset_all
(
t
σ
2
.
2
)
(
big_op
rs2
).
Proof
.
intros
Hsteps
Hn
;
revert
Qs
rs1
.
induction
Hsteps
as
[|
k
??
t
σ
3
[
e1
σ
1 e2
σ
2
ef
t1
t2
??
Hstep
]
Hsteps
IH
]
;
simplify_equality'
;
intros
Qs
rs
.
{
by
intros
;
exists
rs
,
[]
;
rewrite
right_id_L
.
}
intros
(
Qs1
&?&
rs1
&?&->&->&?&
(
Q
&
Qs2
&
r
&
rs2
&->&->&
Hwp
&?)%
Forall3_cons_inv_l
)%
Forall3_app_inv_l
?.
destruct
(
wp_step_inv
coPset_all
∅
Q
e1
(
k
+
n
)
(
S
(
k
+
n
))
σ
1
r
(
big_op
(
rs1
++
rs2
)))
as
[
_
Hwpstep
]
;
eauto
using
values_stuck
.
{
by
rewrite
right_id_L
-
big_op_cons
Permutation_middle
.
}
destruct
(
Hwpstep
e2
σ
2
ef
)
as
(
r2
&
r2'
&
Hwsat
&?&?)
;
auto
;
clear
Hwpstep
.
revert
Hwsat
;
rewrite
big_op_app
right_id_L
=>
Hwsat
.
destruct
ef
as
[
e'
|].
*
destruct
(
IH
(
Qs1
++
Q
::
Qs2
++
[
λ
_
,
True
%
I
])
(
rs1
++
r2
::
rs2
++
[
r2'
]))
as
(
rs'
&
Qs'
&?&?).
{
apply
Forall3_app
,
Forall3_cons
,
Forall3_app
,
Forall3_cons
,
Forall3_nil
;
eauto
using
wptp_le
.
}
{
by
rewrite
-
Permutation_middle
/=
(
associative
(++))
(
commutative
(++))
/=
associative
big_op_app
.
}
exists
rs'
,
([
λ
_
,
True
%
I
]
++
Qs'
)
;
split
;
auto
.
by
rewrite
(
associative
_
_
_
Qs'
)
-(
associative
_
Qs1
).
*
apply
(
IH
(
Qs1
++
Q
::
Qs2
)
(
rs1
++
r2
⋅
r2'
::
rs2
)).
{
rewrite
/
option_list
right_id_L
.
apply
Forall3_app
,
Forall3_cons
;
eauto
using
wptp_le
.
apply
uPred_weaken
with
r2
(
k
+
n
)
;
eauto
using
@
ra_included_l
.
}
by
rewrite
-
Permutation_middle
/=
big_op_app
.
Qed
.
Lemma
ht_adequacy_steps
P
Q
k
n
e1
t2
σ
1
σ
2
r1
:
{{
P
}}
e1
@
coPset_all
{{
Q
}}
→
nsteps
step
k
([
e1
],
σ
1
)
(
t2
,
σ
2
)
→
1
<
n
→
wsat
(
k
+
n
)
coPset_all
σ
1
r1
→
P
(
k
+
n
)
r1
→
∃
rs2
Qs'
,
wptp
n
t2
((
λ
v
,
pvs
coPset_all
coPset_all
(
Q
v
))
::
Qs'
)
rs2
∧
wsat
n
coPset_all
σ
2
(
big_op
rs2
).
Proof
.
intros
Hht
????
;
apply
(
nsteps_wptp
[
pvs
coPset_all
coPset_all
∘
Q
]
k
n
([
e1
],
σ
1
)
(
t2
,
σ
2
)
[
r1
])
;
rewrite
/
big_op
?right_id
;
auto
.
constructor
;
last
constructor
.
apply
Hht
with
r1
(
k
+
n
)
;
eauto
using
@
ra_included_unit
.
by
destruct
(
k
+
n
).
Qed
.
Theorem
ht_adequacy_result
E
φ
e
v
t2
σ
1
σ
2
:
{{
ownP
σ
1
}}
e
@
E
{{
λ
v'
,
■
φ
v'
}}
→
rtc
step
([
e
],
σ
1
)
(
of_val
v
::
t2
,
σ
2
)
→
φ
v
.
Proof
.
intros
?
[
k
?]%
rtc_nsteps
.
destruct
(
ht_adequacy_steps
(
ownP
σ
1
)
(
λ
v'
,
■
φ
v'
)%
I
k
2
e
(
of_val
v
::
t2
)
σ
1
σ
2
(
Res
∅
(
Excl
σ
1
)
∅
))
as
(
rs2
&
Qs
&
Hwptp
&?)
;
auto
.
{
by
rewrite
-(
ht_mask_weaken
E
coPset_all
).
}
{
rewrite
Nat
.
add_comm
;
apply
wsat_init
.
}
{
by
rewrite
/
uPred_holds
/=.
}
inversion
Hwptp
as
[|??
r
??
rs
Hwp
_
]
;
clear
Hwptp
;
subst
.
apply
wp_value_inv
in
Hwp
;
destruct
(
Hwp
(
big_op
rs
)
2
∅
σ
2
)
as
[
r'
[]]
;
auto
.
by
rewrite
right_id_L
.
Qed
.
Lemma
ht_adequacy_reducible
E
Q
e1
e2
t2
σ
1
σ
2
:
{{
ownP
σ
1
}}
e1
@
E
{{
Q
}}
→
rtc
step
([
e1
],
σ
1
)
(
t2
,
σ
2
)
→
e2
∈
t2
→
to_val
e2
=
None
→
reducible
e2
σ
2
.
Proof
.
intros
?
[
k
?]%
rtc_nsteps
[
i
?]%
elem_of_list_lookup
He
.
destruct
(
ht_adequacy_steps
(
ownP
σ
1
)
Q
k
3 e1
t2
σ
1
σ
2
(
Res
∅
(
Excl
σ
1
)
∅
))
as
(
rs2
&
Qs
&?&?)
;
auto
.
{
by
rewrite
-(
ht_mask_weaken
E
coPset_all
).
}
{
rewrite
Nat
.
add_comm
;
apply
wsat_init
.
}
{
by
rewrite
/
uPred_holds
/=.
}
destruct
(
Forall3_lookup_l
(
λ
e
Q
r
,
wp
coPset_all
e
Q
3
r
)
t2
(
pvs
coPset_all
coPset_all
∘
Q
::
Qs
)
rs2
i
e2
)
as
(
Q'
&
r2
&?&?&
Hwp
)
;
auto
.
destruct
(
wp_step_inv
coPset_all
∅
Q'
e2
2
3
σ
2
r2
(
big_op
(
delete
i
rs2
)))
;
rewrite
?right_id_L
?big_op_delete
;
auto
.
Qed
.
Theorem
ht_adequacy_safe
E
Q
e1
t2
σ
1
σ
2
:
{{
ownP
σ
1
}}
e1
@
E
{{
Q
}}
→
rtc
step
([
e1
],
σ
1
)
(
t2
,
σ
2
)
→
Forall
(
λ
e
,
is_Some
(
to_val
e
))
t2
∨
∃
t3
σ
3
,
step
(
t2
,
σ
2
)
(
t3
,
σ
3
).
Proof
.
intros
.
destruct
(
decide
(
Forall
(
λ
e
,
is_Some
(
to_val
e
))
t2
))
as
[|
Ht2
]
;
[
by
left
|].
apply
(
not_Forall_Exists
_
),
Exists_exists
in
Ht2
;
destruct
Ht2
as
(
e2
&?&
He2
).
destruct
(
ht_adequacy_reducible
E
Q
e1
e2
t2
σ
1
σ
2
)
as
(
e3
&
σ
3
&
ef
&?)
;
rewrite
?eq_None_not_Some
;
auto
.
destruct
(
elem_of_list_split
t2
e2
)
as
(
t2'
&
t2''
&->)
;
auto
.
right
;
exists
(
t2'
++
e3
::
t2''
++
option_list
ef
),
σ
3
;
econstructor
;
eauto
.
Qed
.
End
adequacy
.
iris/hoare_lifting.v
View file @
0b05b368
...
...
@@ -15,7 +15,7 @@ Import uPred.
Lemma
ht_lift_step
E1
E2
(
φ
:
iexpr
Σ
→
istate
Σ
→
option
(
iexpr
Σ
)
→
Prop
)
P
P'
Q1
Q2
R
e1
σ
1
:
E1
⊆
E2
→
to_val
e1
=
None
→
(
∃
e2
σ
2
ef
,
prim_step
e1
σ
1 e2
σ
2
ef
)
→
reducible
e1
σ
1
→
(
∀
e2
σ
2
ef
,
prim_step
e1
σ
1 e2
σ
2
ef
→
φ
e2
σ
2
ef
)
→
(
P
>{
E2
,
E1
}>
(
ownP
σ
1
★
▷
P'
)
∧
∀
e2
σ
2
ef
,
(
■
φ
e2
σ
2
ef
★
ownP
σ
2
★
P'
)
>{
E1
,
E2
}>
(
Q1
e2
σ
2
ef
★
Q2
e2
σ
2
ef
)
∧
...
...
@@ -45,7 +45,7 @@ Qed.
Lemma
ht_lift_atomic
E
(
φ
:
iexpr
Σ
→
istate
Σ
→
option
(
iexpr
Σ
)
→
Prop
)
P
e1
σ
1
:
atomic
e1
→
(
∃
e2
σ
2
ef
,
prim_step
e1
σ
1 e2
σ
2
ef
)
→
reducible
e1
σ
1
→
(
∀
e2
σ
2
ef
,
prim_step
e1
σ
1 e2
σ
2
ef
→
φ
e2
σ
2
ef
)
→
(
∀
e2
σ
2
ef
,
{{
■
φ
e2
σ
2
ef
★
P
}}
ef
?@
coPset_all
{{
λ
_
,
True
}})
⊑
{{
ownP
σ
1
★
▷
P
}}
e1
@
E
{{
λ
v
,
∃
σ
2
ef
,
ownP
σ
2
★
■
φ
(
of_val
v
)
σ
2
ef
}}.
...
...
@@ -71,7 +71,7 @@ Proof.
Qed
.
Lemma
ht_lift_pure_step
E
(
φ
:
iexpr
Σ
→
option
(
iexpr
Σ
)
→
Prop
)
P
P'
Q
e1
:
to_val
e1
=
None
→
(
∀
σ
1
,
∃
e2
σ
2
ef
,
prim_step
e1
σ
1 e2
σ
2
ef
)
→
(
∀
σ
1
,
reducible
e1
σ
1
)
→
(
∀
σ
1 e2
σ
2
ef
,
prim_step
e1
σ
1 e2
σ
2
ef
→
σ
1
=
σ
2
∧
φ
e2
ef
)
→
(
∀
e2
ef
,
{{
■
φ
e2
ef
★
P
}}
e2
@
E
{{
Q
}}
∧
...
...
@@ -97,7 +97,7 @@ Qed.
Lemma
ht_lift_pure_determistic_step
E
(
φ
:
iexpr
Σ
→
option
(
iexpr
Σ
)
→
Prop
)
P
P'
Q
e1
e2
ef
:
to_val
e1
=
None
→
(
∀
σ
1
,
prim_step
e1
σ
1 e2
σ
1
ef
)
→
(
∀
σ
1
,
reducible
e1
σ
1
)
→
(
∀
σ
1 e2
'
σ
2
ef'
,
prim_step
e1
σ
1 e2
'
σ
2
ef'
→
σ
1
=
σ
2
∧
e2
=
e2'
∧
ef
=
ef'
)
→
({{
P
}}
e2
@
E
{{
Q
}}
∧
{{
P'
}}
ef
?@
coPset_all
{{
λ
_
,
True
}})
⊑
{{
▷
(
P
★
P'
)
}}
e1
@
E
{{
Q
}}.
...
...
iris/language.v
View file @
0b05b368
...
...
@@ -19,6 +19,11 @@ Arguments Build_Language {_ _ _} _ _ _ _ {_ _ _ _ _}.
Section
language
.
Context
`
{
Language
E
V
St
}.
Definition
reducible
(
e
:
E
)
(
σ
:
St
)
:
=
∃
e'
σ
'
ef
,
prim_step
e
σ
e'
σ
'
ef
.
Lemma
reducible_not_val
e
σ
:
reducible
e
σ
→
to_val
e
=
None
.
Proof
.
intros
(?&?&?&?)
;
eauto
using
values_stuck
.
Qed
.
Lemma
atomic_of_val
v
:
¬
atomic
(
of_val
v
).
Proof
.
by
intros
Hat
;
apply
atomic_not_value
in
Hat
;
rewrite
to_of_val
in
Hat
.
...
...
@@ -30,13 +35,10 @@ Section language.
Inductive
step
(
ρ
1
ρ
2
:
cfg
)
:
Prop
:
=
|
step_atomic
e1
σ
1 e2
σ
2
ef
t1
t2
:
ρ
1
=
(
t1
++
e1
::
t2
,
σ
1
)
→
ρ
1
=
(
t1
++
e2
::
t2
++
option_list
ef
,
σ
2
)
→
ρ
2
=
(
t1
++
e2
::
t2
++
option_list
ef
,
σ
2
)
→
prim_step
e1
σ
1 e2
σ
2
ef
→
step
ρ
1
ρ
2
.
Definition
steps
:
=
rtc
step
.
Definition
stepn
:
=
nsteps
step
.
Record
is_ctx
(
K
:
E
→
E
)
:
=
IsCtx
{
is_ctx_value
e
:
to_val
e
=
None
→
to_val
(
K
e
)
=
None
;
is_ctx_step_preserved
e1
σ
1 e2
σ
2
ef
:
...
...
iris/lifting.v
View file @
0b05b368
...
...
@@ -16,7 +16,7 @@ Transparent uPred_holds.
Lemma
wp_lift_step
E1
E2
(
φ
:
iexpr
Σ
→
istate
Σ
→
option
(
iexpr
Σ
)
→
Prop
)
Q
e1
σ
1
:
E1
⊆
E2
→
to_val
e1
=
None
→
(
∃
e2
σ
2
ef
,
prim_step
e1
σ
1 e2
σ
2
ef
)
→
reducible
e1
σ
1
→
(
∀
e2
σ
2
ef
,
prim_step
e1
σ
1 e2
σ
2
ef
→
φ
e2
σ
2
ef
)
→
pvs
E2
E1
(
ownP
σ
1
★
▷
∀
e2
σ
2
ef
,
(
■
φ
e2
σ
2
ef
∧
ownP
σ
2
)
-
★
pvs
E1
E2
(
wp
E2
e2
Q
★
default
True
ef
(
flip
(
wp
coPset_all
)
(
λ
_
,
True
))))
...
...
@@ -37,7 +37,7 @@ Proof.
Qed
.
Lemma
wp_lift_pure_step
E
(
φ
:
iexpr
Σ
→
option
(
iexpr
Σ
)
→
Prop
)
Q
e1
:
to_val
e1
=
None
→
(
∀
σ
1
,
∃
e2
σ
2
ef
,
prim_step
e1
σ
1 e2
σ
2
ef
)
→
(
∀
σ
1
,
reducible
e1
σ
1
)
→
(
∀
σ
1 e2
σ
2
ef
,
prim_step
e1
σ
1 e2
σ
2
ef
→
σ
1
=
σ
2
∧
φ
e2
ef
)
→
(
▷
∀
e2
ef
,
■
φ
e2
ef
→
wp
E
e2
Q
★
default
True
ef
(
flip
(
wp
coPset_all
)
(
λ
_
,
True
)))
...
...
iris/parameter.v
View file @
0b05b368
Require
Export
modures
.
cmra
iris
.
language
.
Set
Bullet
Behavior
"Strict Subproofs"
.
Record
iParam
:
=
IParam
{
iexpr
:
Type
;
ival
:
Type
;
...
...
@@ -29,6 +27,8 @@ Proof.
by
intros
?
;
apply
equiv_dist
=>
n
;
apply
icmra_map_ne
=>
?
;
apply
equiv_dist
.
Qed
.
Canonical
Structure
istateC
Σ
:
=
leibnizC
(
istate
Σ
).
Definition
IParamConst
{
iexpr
ival
istate
:
Type
}
(
ilanguage
:
Language
iexpr
ival
istate
)
(
icmra
:
cmraT
)
{
icmra_empty
:
Empty
icmra
}
...
...
@@ -39,5 +39,3 @@ Unshelve.
-
by
intros
.
-
by
intros
.
Defined
.
Canonical
Structure
istateC
Σ
:
=
leibnizC
(
istate
Σ
).
iris/weakestpre.v
View file @
0b05b368
...
...
@@ -9,7 +9,7 @@ Local Hint Extern 10 (✓{_} _) =>
Record
wp_go
{
Σ
}
(
E
:
coPset
)
(
Q
Qfork
:
iexpr
Σ
→
nat
→
res'
Σ
→
Prop
)
(
k
:
nat
)
(
rf
:
res'
Σ
)
(
e1
:
iexpr
Σ
)
(
σ
1
:
istate
Σ
)
:
=
{
wf_safe
:
∃
e2
σ
2
ef
,
prim_step
e1
σ
1 e2
σ
2
ef
;
wf_safe
:
reducible
e1
σ
1
;
wp_step
e2
σ
2
ef
:
prim_step
e1
σ
1 e2
σ
2
ef
→
∃
r2
r2'
,
...
...
@@ -83,6 +83,17 @@ Proof.
by
intros
Q
Q'
?
;
apply
equiv_dist
=>
n
;
apply
wp_ne
=>
v
;
apply
equiv_dist
.
Qed
.
Lemma
wp_value_inv
E
Q
v
n
r
:
wp
E
(
of_val
v
)
Q
n
r
→
Q
v
n
r
.
Proof
.
inversion
1
as
[|
|???
He
]
;
simplify_equality
;
auto
.
by
rewrite
?to_of_val
in
He
.
Qed
.
Lemma
wp_step_inv
E
Ef
Q
e
k
n
σ
r
rf
:
to_val
e
=
None
→
1
<
k
<
n
→
E
∩
Ef
=
∅
→
wp
E
e
Q
n
r
→
wsat
(
S
k
)
(
E
∪
Ef
)
σ
(
r
⋅
rf
)
→
wp_go
(
E
∪
Ef
)
(
λ
e
,
wp
E
e
Q
)
(
λ
e
,
wp
coPset_all
e
(
λ
_
,
True
%
I
))
k
rf
e
σ
.
Proof
.
intros
He
;
destruct
3
;
[
lia
|
by
rewrite
?to_of_val
in
He
|
eauto
].
Qed
.
Lemma
wp_value
E
Q
v
:
Q
v
⊑
wp
E
(
of_val
v
)
Q
.
Proof
.
by
constructor
.
Qed
.
Lemma
wp_mono
E
e
Q1
Q2
:
(
∀
v
,
Q1
v
⊑
Q2
v
)
→
wp
E
e
Q1
⊑
wp
E
e
Q2
.
...
...
@@ -91,9 +102,7 @@ Lemma wp_pvs E e Q : pvs E E (wp E e Q) ⊑ wp E e (λ v, pvs E E (Q v)).
Proof
.
intros
r
[|
n
]
?
;
[
done
|]
;
intros
Hvs
.
destruct
(
to_val
e
)
as
[
v
|]
eqn
:
He
;
[
apply
of_to_val
in
He
;
subst
|].
{
constructor
;
eapply
pvs_mono
,
Hvs
;
auto
;
clear
.
intros
r
n
?
;
inversion
1
as
[|
|???
He
]
;
simplify_equality
;
auto
.
by
rewrite
?to_of_val
in
He
.
}
{
by
constructor
;
eapply
pvs_mono
,
Hvs
;
[
intros
???
;
apply
wp_value_inv
|].
}
constructor
;
[
done
|
intros
rf
k
Ef
σ
1
???].
destruct
(
Hvs
rf
(
S
k
)
Ef
σ
1
)
as
(
r'
&
Hwp
&?)
;
auto
.
inversion
Hwp
as
[|
|????
Hgo
]
;
subst
;
[
by
rewrite
to_of_val
in
He
|].
...
...
iris/wsat.v
View file @
0b05b368
...
...
@@ -63,6 +63,14 @@ Proof.
destruct
n
;
[
intros
;
apply
cmra_valid_0
|
intros
[
rs
?]].
eapply
cmra_valid_op_l
,
wsat_pre_valid
;
eauto
.
Qed
.
Lemma
wsat_init
k
E
σ
:
wsat
(
S
k
)
E
σ
(
Res
∅
(
Excl
σ
)
∅
).
Proof
.
exists
∅
;
constructor
;
auto
.
*
rewrite
big_opM_empty
right_id
.
split_ands'
;
try
(
apply
cmra_valid_validN
,
ra_empty_valid
)
;
constructor
.
*
by
intros
i
;
rewrite
lookup_empty
=>-[??].
*
intros
i
P
?
;
rewrite
/=
(
left_id
_
_
)
lookup_empty
;
inversion_clear
1
.
Qed
.
Lemma
wsat_open
n
E
σ
r
i
P
:
wld
r
!!
i
={
S
n
}=
Some
(
to_agree
(
Later
(
iProp_unfold
P
)))
→
i
∉
E
→
wsat
(
S
n
)
({[
i
]}
∪
E
)
σ
r
→
∃
rP
,
wsat
(
S
n
)
E
σ
(
rP
⋅
r
)
∧
P
n
rP
.
...
...
modures/ra.v
View file @
0b05b368
...
...
@@ -125,6 +125,10 @@ Lemma ra_empty_least x : ∅ ≼ x.
Proof
.
by
exists
x
;
rewrite
(
left_id
_
_
).
Qed
.
(** * Big ops *)
Lemma
big_op_nil
:
big_op
(@
nil
A
)
=
∅
.
Proof
.
done
.
Qed
.
Lemma
big_op_cons
x
xs
:
big_op
(
x
::
xs
)
=
x
⋅
big_op
xs
.
Proof
.
done
.
Qed
.
Global
Instance
big_op_permutation
:
Proper
((
≡
ₚ
)
==>
(
≡
))
big_op
.
Proof
.
induction
1
as
[|
x
xs1
xs2
?
IH
|
x
y
xs
|
xs1
xs2
xs3
]
;
simpl
;
auto
.
...
...
@@ -147,6 +151,9 @@ Proof.
*
by
transitivity
(
big_op
ys
)
;
[|
apply
ra_included_r
].
*
by
transitivity
(
big_op
ys
).
Qed
.
Lemma
big_op_delete
xs
i
x
:
xs
!!
i
=
Some
x
→
x
⋅
big_op
(
delete
i
xs
)
≡
big_op
xs
.
Proof
.
by
intros
;
rewrite
{
2
}(
delete_Permutation
xs
i
x
).
Qed
.
Context
`
{
FinMap
K
M
}.
Lemma
big_opM_empty
:
big_opM
(
∅
:
M
A
)
≡
∅
.
...
...
prelude/list.v
View file @
0b05b368
...
...
@@ -1372,6 +1372,11 @@ Proof.
induction
l
as
[|
x
l
IH
]
;
[
done
|].
by
rewrite
reverse_cons
,
(
commutative
(++)),
IH
.
Qed
.
Lemma
delete_Permutation
l
i
x
:
l
!!
i
=
Some
x
→
l
≡
ₚ
x
::
delete
i
l
.
Proof
.
revert
i
;
induction
l
as
[|
y
l
IH
]
;
intros
[|
i
]
?
;
simplify_equality'
;
auto
.
by
rewrite
Permutation_swap
,
<-(
IH
i
).
Qed
.
(** ** Properties of the [prefix_of] and [suffix_of] predicates *)
Global
Instance
:
PreOrder
(@
prefix_of
A
).
...
...
@@ -2522,59 +2527,85 @@ End Forall2_order.
Section
Forall3
.
Context
{
A
B
C
}
(
P
:
A
→
B
→
C
→
Prop
).
Hint
Extern
0
(
Forall3
_
_
_
_
)
=>
constructor
.
Lemma
Forall3_app
l1
k1
k1
'
l
2
k
2
k2'
:
Lemma
Forall3_app
l1
l2
k1
k
2
k
1'
k2'
:
Forall3
P
l1
k1
k1'
→
Forall3
P
l2
k2
k2'
→
Forall3
P
(
l1
++
l2
)
(
k1
++
k2
)
(
k1'
++
k2'
).
Proof
.
induction
1
;
simpl
;
auto
.
Qed
.
Lemma
Forall3_cons_inv_m
l
y
l2'
k
:
Forall3
P
l
(
y
::
l2'
)
k
→
∃
x
l2
z
k2
,
l
=
x
::
l2
∧
k
=
z
::
k2
∧
P
x
y
z
∧
Forall3
P
l2
l2'
k2
.
Lemma
Forall3_cons_inv_l
x
l
k
k'
:
Forall3
P
(
x
::
l
)
k
k'
→
∃
y
k2
z
k2'
,
k
=
y
::
k2
∧
k'
=
z
::
k2'
∧
P
x
y
z
∧
Forall3
P
l
k2
k2'
.
Proof
.
inversion_clear
1
;
naive_solver
.
Qed
.
Lemma
Forall3_app_inv_l
l1
l2
k
k'
:
Forall3
P
(
l1
++
l2
)
k
k'
→
∃
k1
k2
k1'
k2'
,
k
=
k1
++
k2
∧
k'
=
k1'
++
k2'
∧
Forall3
P
l1
k1
k1'
∧
Forall3
P
l2
k2
k2'
.
Proof
.
revert
k
k'
.
induction
l1
as
[|
x
l1
IH
]
;
simpl
;
inversion_clear
1
.
*
by
repeat
eexists
;
eauto
.
*
by
repeat
eexists
;
eauto
.
*
edestruct
IH
as
(?&?&?&?&?&?&?&?)
;
eauto
;
naive_solver
.
Qed
.
Lemma
Forall3_cons_inv_m
l
y
k
k'
:
Forall3
P
l
(
y
::
k
)
k'
→
∃
x
l2
z
k2'
,
l
=
x
::
l2
∧
k'
=
z
::
k2'
∧
P
x
y
z
∧
Forall3
P
l2
k
k2'
.
Proof
.
inversion_clear
1
;
naive_solver
.
Qed
.
Lemma
Forall3_app_inv_m
l
k1
k2
k'
:
Forall3
P
l
(
k1
++
k2
)
k'
→
∃
l1
l2
k1'
k2'
,
l
=
l1
++
l2
∧
k'
=
k1'
++
k2'
∧
Forall3
P
l1
k1
k1'
∧
Forall3
P
l2
k2
k2'
.
Proof
.
revert
l
k'
.
induction
k1
as
[|
x
k1
IH
]
;
simpl
;
inversion_clear
1
.
*
by
repeat
eexists
;
eauto
.
*
by
repeat
eexists
;
eauto
.
*
edestruct
IH
as
(?&?&?&?&?&?&?&?)
;
eauto
;
naive_solver
.
Qed
.
Lemma
Forall3_cons_inv_r
l
k
z
k'
:
Forall3
P
l
k
(
z
::
k'
)
→
∃
x
l2
y
k2
,
l
=
x
::
l2
∧
k
=
y
::
k2
∧
P
x
y
z
∧
Forall3
P
l2
k2
k'
.
Proof
.
inversion_clear
1
;
naive_solver
.
Qed
.
Lemma
Forall3_app_inv_
m
l
l
1'
l
2'
k
:
Forall3
P
l
(
l
1'
++
l
2'
)
k
→
∃
l1
l2
k1
k2
,
l
=
l1
++
l2
∧
k
=
k1
++
k2
∧
Forall3
P
l1
l1'
k1
∧
Forall3
P
l2
l2'
k2
.
Lemma
Forall3_app_inv_
r
l
k
k
1'
k
2'
:
Forall3
P
l
k
(
k
1'
++
k
2'
)
→
∃
l1
l2
k1
k2
,
l
=
l1
++
l2
∧
k
=
k1
++
k2
∧
Forall3
P
l1
k1
k1
'
∧
Forall3
P
l2
k2
k2
'
.
Proof
.
revert
l
k
.
induction
l
1'
as
[|
x
l
1'
IH
]
;
simpl
;
inversion_clear
1
.
revert
l
k
.
induction
k
1'
as
[|
x
k
1'
IH
]
;
simpl
;
inversion_clear
1
.
*
by
repeat
eexists
;
eauto
.
*
by
repeat
eexists
;
eauto
.
*
edestruct
IH
as
(?&?&?&?&?&?&?&?)
;
eauto
;
naive_solver
.
Qed
.
Lemma
Forall3_impl
(
Q
:
A
→
B
→
C
→
Prop
)
l
l'
k
:
Forall3
P
l
l'
k
→
(
∀
x
y
z
,
P
x
y
z
→
Q
x
y
z
)
→
Forall3
Q
l
l'
k
.
Proof
.
intros
Hl
?
.
induction
Hl
;
auto
.
Defined
.
Lemma
Forall3_length_lm
l
l'
k
:
Forall3
P
l
l'
k
→
length
l
=
length
l'
.
Lemma
Forall3_impl
(
Q
:
A
→
B
→
C
→
Prop
)
l
k
k
'
:
Forall3
P
l
k
k
'
→
(
∀
x
y
z
,
P
x
y
z
→
Q
x
y
z
)
→
Forall3
Q
l
k
k
'
.
Proof
.
intros
Hl
?
;
induction
Hl
;
auto
.
Defined
.
Lemma
Forall3_length_lm
l
k
k
'
:
Forall3
P
l
k
k
'
→
length
l
=
length
k
.
Proof
.
by
induction
1
;
f_equal'
.
Qed
.
Lemma
Forall3_length_lr
l
l'
k
:
Forall3
P
l
l'
k
→
length
l
=
length
k
.
Lemma
Forall3_length_lr
l
k
k
'
:
Forall3
P
l
k
k
'
→
length
l
=
length
k
'
.
Proof
.
by
induction
1
;
f_equal'
.
Qed
.
Lemma
Forall3_lookup_lmr
l
l'
k
i
x
y
z
:
Forall3
P
l
l'
k
→
l
!!
i
=
Some
x
→
l'
!!
i
=
Some
y
→
k
!!
i
=
Some
z
→
P
x
y
z
.
Lemma
Forall3_lookup_lmr
l
k
k
'
i
x
y
z
:
Forall3
P
l
k
k
'
→
l
!!
i
=
Some
x
→
k
!!
i
=
Some
y
→
k
'
!!
i
=
Some
z
→
P
x
y
z
.
Proof
.
intros
H
.
revert
i
.
induction
H
;
intros
[|?]
???
;
simplify_equality'
;
eauto
.
Qed
.
Lemma
Forall3_lookup_l
l
l'
k
i
x
:
Forall3
P
l
l'
k
→
l
!!
i
=
Some
x
→
∃
y
z
,
l'
!!
i
=
Some
y
∧
k
!!
i
=
Some
z
∧
P
x
y
z
.
Lemma
Forall3_lookup_l
l
k
k
'
i
x
:
Forall3
P
l
k
k
'
→
l
!!
i
=
Some
x
→
∃
y
z
,
k
!!
i
=
Some
y
∧
k
'
!!
i
=
Some
z
∧
P
x
y
z
.
Proof
.
intros
H
.
revert
i
.
induction
H
;
intros
[|?]
?
;
simplify_equality'
;
eauto
.
Qed
.
Lemma
Forall3_lookup_m
l
l'
k
i
y
:
Forall3
P
l
l'
k
→
l'
!!
i
=
Some
y
→
∃
x
z
,
l
!!
i
=
Some
x
∧
k
!!
i
=
Some
z
∧
P
x
y
z
.
Lemma
Forall3_lookup_m
l
k
k
'
i
y
:
Forall3
P
l
k
k
'
→
k
!!
i
=
Some
y
→
∃
x
z
,
l
!!
i
=
Some
x
∧
k
'
!!
i
=
Some
z
∧
P
x
y
z
.
Proof
.
intros
H
.
revert
i
.
induction
H
;
intros
[|?]
?
;
simplify_equality'
;
eauto
.
Qed
.
Lemma
Forall3_lookup_r
l
l'
k
i
z
:
Forall3
P
l
l'
k
→
k
!!
i
=
Some
z
→
∃
x
y
,
l
!!
i
=
Some
x
∧
l'
!!
i
=
Some
y
∧
P
x
y
z
.
Lemma
Forall3_lookup_r
l
k
k
'
i
z
:
Forall3
P
l
k
k
'
→
k
'
!!
i
=
Some
z
→
∃
x
y
,
l
!!
i
=
Some
x
∧
k
!!
i
=
Some
y
∧
P
x
y
z
.
Proof
.
intros
H
.
revert
i
.
induction
H
;
intros
[|?]
?
;
simplify_equality'
;
eauto
.
Qed
.
Lemma
Forall3_alter_lm
f
g
l
l'
k
i
:
Forall3
P
l
l'
k
→
(
∀
x
y
z
,
l
!!
i
=
Some
x
→
l'
!!
i
=
Some
y
→
k
!!
i
=
Some
z
→
Lemma
Forall3_alter_lm
f
g
l
k
k
'
i
:
Forall3
P
l
k
k
'
→
(
∀
x
y
z
,
l
!!
i
=
Some
x
→
k
!!
i
=
Some
y
→
k
'
!!
i
=
Some
z
→
P
x
y
z
→
P
(
f
x
)
(
g
y
)
z
)
→
Forall3
P
(
alter
f
i
l
)
(
alter
g
i
l'
)
k
.
Forall3
P
(
alter
f
i
l
)
(
alter
g
i
k
)
k
'
.
Proof
.
intros
Hl
.
revert
i
.
induction
Hl
;
intros
[|]
;
auto
.
Qed
.
End
Forall3
.
...
...
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