Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Glen Mével
cosmo
Commits
f301a20b
Commit
f301a20b
authored
Jul 01, 2021
by
Glen Mével
Browse files
prove admitted lemmas in program_logic/store.v
parent
82cab7c7
Changes
2
Hide whitespace changes
Inline
Sidebyside
Showing
2 changed files
with
94 additions
and
7 deletions
+94
7
theories/base/base.v
theories/base/base.v
+63
0
theories/program_logic/store.v
theories/program_logic/store.v
+31
7
No files found.
theories/base/base.v
View file @
f301a20b
...
...
@@ 620,3 +620,66 @@ Proof. move=>?????. by apply (anti_symm (⊑)). Qed.
Instance
flip_partialorder
{
A
:
latticeT
}
:
@
PartialOrder
A
(
⊑
)
→
@
PartialOrder
A
(
flip
(
⊑
)).
Proof
.
move
=>?
.
constructor
;
apply
_.
Qed
.
(
**
Lemmas
about
big_sepL2
*
)
From
iris
.
bi
Require
Import
big_op
.
From
iris
.
proofmode
Require
Import
tactics
.
Section
big_sepL2
.
Lemma
big_sepL2_split
{
PROP
:
bi
}
{
A
B
:
Type
}
(
xs
:
list
A
)
(
ys
:
list
B
)
(
Φ
Ψ
:
nat
→
_
→
PROP
)
:
length
xs
=
length
ys
→
([
∗
list
]
i
↦
x
∈
xs
,
Φ
i
x
)
∗
([
∗
list
]
i
↦
y
∈
ys
,
Ψ
i
y
)
⊢
([
∗
list
]
i
↦
x
;
y
∈
xs
;
ys
,
Φ
i
x
∗
Ψ
i
y
).
Proof
.
iIntros
(
?
)
"(HΦ & HΨ)"
.
rewrite
big_sepL2_sep
.
iSplitL
"HΦ"
.
{
rewrite
big_sepL2_alt
.
iSplit
;
first
done
.
rewrite

(
big_sepL_fmap
fst
)
fst_zip
;
last
lia
.
done
.
}
{
rewrite
big_sepL2_alt
.
iSplit
;
first
done
.
rewrite

(
big_sepL_fmap
snd
)
snd_zip
;
last
lia
.
done
.
}
Qed
.
Local
Lemma
destruct_list_end
{
A
:
Type
}
(
xs
:
list
A
)
:
xs
=
[]
∨
∃
xs
'
x
,
xs
=
xs
'
++
[
x
].
Proof
.
induction
xs
as
[

x0
xs
'
IH
];
first
auto
.
right
.
destruct
IH
as
[
>
(
xs
''
&
x
&
>
)].

by
exists
[],
x0
.

by
exists
(
x0
::
xs
''
),
x
.
Qed
.
Global
Instance
big_sepL2_into_pure
{
PROP
:
bi
}
{
A
B
:
Type
}
(
xs
:
list
A
)
(
ys
:
list
B
)
(
Φ
φ
:
nat
→
A
→
B
→
_
)
:
(
∀
i
x
y
,
xs
!!
i
=
Some
x
→
ys
!!
i
=
Some
y
→
IntoPure
(
Φ
i
x
y
)
(
φ
i
x
y
))
→
IntoPure
(
PROP
:=
PROP
)
([
∗
list
]
i
↦
x
;
y
∈
xs
;
ys
,
Φ
i
x
y
)
(
length
xs
=
length
ys
∧
∀
i
x
y
,
xs
!!
i
=
Some
x
→
ys
!!
i
=
Some
y
→
φ
i
x
y
).
Proof
.
intros
H
.
rewrite
/
IntoPure
.
iIntros
"Hxys"
.
iAssert
⌜
length
xs
=
length
ys
⌝
%
I
as
%
Hlen
.
{
by
iApply
big_sepL2_length
.
}
iSplit
;
first
done
.
iInduction
xs
as
[

x
xs
'
]
"IH"
using
rev_ind
forall
(
ys
H
Hlen
);
first
by
destruct
ys
.
destruct
(
destruct_list_end
ys
)
as
[
>
(
ys
'
&
y
&
>
)].
{
exfalso
.
rewrite
app_length
/=
in
Hlen
.
lia
.
}
assert
(
length
xs
'
=
length
ys
'
)
as
Hlen
'
.
{
rewrite
2
!
app_length
/=
in
Hlen
.
lia
.
}
iDestruct
(
big_sepL2_app_inv
with
"Hxys"
)
as
"[Hxys' Hxy]"
;
first
done
.
eassert
_
as
H
'
;
last
iDestruct
(
"IH"
$
!
ys
'
H
'
Hlen
'
with
"Hxys'"
)
as
%
Hxys
'
.
{
intros
.
apply
H
;
by
apply
lookup_app_l_Some
.
}
iClear
"IH Hxys'"
.
rewrite
/=
(
right_id
emp
%
I
)
Nat
.
add_0_r
.
assert
(
IntoPure
(
Φ
(
length
xs
'
)
x
y
)
(
φ
(
length
xs
'
)
x
y
))
as
H0
.
{
apply
H
;
rewrite
lookup_app_r
?
Hlen
'
?
Nat
.
sub_diag
;
done
.
}
iDestruct
"Hxy"
as
%
Hxy
.
iPureIntro
.
clear
dependent
PROP
Hlen
.
intros
i
x0
y0
EQxs
EQys
.
destruct
(
decide
(
i
<
length
xs
'
)
%
nat
).
{
rewrite
lookup_app_l
in
EQxs
;
last
done
.
rewrite
lookup_app_l
in
EQys
;
last
by
rewrite

Hlen
'
.
auto
.
}
{
assert
(
i
=
length
xs
'
)
as
>
.
{
apply
lookup_lt_Some
in
EQxs
.
rewrite
app_length
/=
in
EQxs
.
lia
.
}
rewrite
lookup_app_r
Hlen
'
?
Nat
.
sub_diag
/=
in
EQxs
;
last
done
.
injection
EQxs
as
<
.
rewrite
lookup_app_r
Hlen
'
?
Nat
.
sub_diag
/=
in
EQys
;
last
done
.
injection
EQys
as
<
.
done
.
}
Qed
.
End
big_sepL2
.
theories/program_logic/store.v
View file @
f301a20b
...
...
@@ 408,8 +408,6 @@ Notation "ℓ *↦at vs" := (mapsto_at_view_block ℓ ((λ v, (v, ∅)) <$> vs)
Section
blockwise_store
.
Context
`
{!
storeG
Σ
}
.
(
*
TODO
:
Prove
admitted
lemmas
!
*
)
Lemma
mapsto_na_block_equiv
ℓ
vs
q
:
mapsto_na_block
ℓ
vs
q
⊣⊢
mapsto_na_block
'
ℓ
vs
q
.
Proof
.
...
...
@@ 479,13 +477,24 @@ Section blockwise_store.
Lemma
hist_na_block_agree
ℓ
hs1
hs2
q1
q2
:
hist_na_block
ℓ
hs1
q1

∗
hist_na_block
ℓ
hs2
q2

∗
⌜
hs1
=
hs2
⌝
.
Proof
.
Admitted
.
rewrite
hist_na_block_eq
/
hist_na_block_def
.
iIntros
"[Hlen1 Hh1] [Hlen2 Hh2]"
.
iDestruct
(
has_length_agree
with
"Hlen1 Hlen2"
)
as
%
Hlen
.
iDestruct
(
big_sepL2_split
with
"[$Hh1 $Hh2]"
)
as
"H12"
;
first
lia
.
iDestruct
(
big_sepL2_mono
with
"H12"
)
as
"H12"
.
{
intros
.
by
apply
bi
.
wand_elim_l
'
,
hist_na_agree
.
}
iDestruct
"H12"
as
%
[
??
].
iPureIntro
.
eapply
list_eq_same_length
;
by
eauto
.
Qed
.
Lemma
store_interp_hist_na_block
σ
ℓ
hs
q
:
store_interp
σ

∗
hist_na_block
ℓ
hs
q

∗
[
∧
list
]
i
↦
h
∈
hs
,
⌜σ
!!
ℓ
.[
i
]
=
Some
(
store_elt_na
h
)
⌝
.
Proof
.
Admitted
.
rewrite
hist_na_block_eq
/
hist_na_block_def
big_andL_forall
.
iIntros
"Hσ [_?]"
(
i
h
Hi
).
iApply
(
store_interp_hist_na
with
"Hσ"
).
by
iApply
(
big_sepL_lookup
(
λ
i
h
,
hist_na
_
_
_
)
_
_
_
Hi
).
Qed
.
Global
Instance
mapsto_na_block_timeless
ℓ
vs
q
:
Timeless
(
ℓ
*
↦
{
q
}
vs
).
Proof
.
apply
_.
Qed
.
...
...
@@ 549,14 +558,29 @@ Section blockwise_store.
Proof
.
split
.
done
.
apply
_.
Qed
.
Lemma
mapsto_at_view_block_agree
ℓ
vVs1
vVs2
q1
q2
:
ℓ
*
↦
at
{
q1
}
()
vVs1

∗
ℓ
*
↦
at
{
q2
}
()
vVs2

∗
⌜
vVs1
=
vVs2
⌝
.
ℓ
*
↦
at
{
q1
}
()
vVs1

∗
ℓ
*
↦
at
{
q2
}
()
vVs2

∗
⌜
fst
<
$
>
vVs1
=
fst
<
$
>
vVs2
⌝
.
Proof
.
Admitted
.
rewrite
mapsto_at_view_block_eq
/
mapsto_at_view_block_def
.
iIntros
"[Hlen1 H1] [Hlen2 H2]"
.
iDestruct
(
has_length_agree
with
"Hlen1 Hlen2"
)
as
%
Hlen
.
iDestruct
(
big_sepL2_split
with
"[$H1 $H2]"
)
as
"H12"
;
first
lia
.
iDestruct
(
big_sepL2_mono
_
(
λ
_
vV1
vV2
,
⌜
fst
vV1
=
fst
vV2
⌝
%
I
)
with
"H12"
)
as
"H12"
.
{
intros
i
[
??
]
[
??
]
??
.
by
apply
bi
.
wand_elim_l
'
,
mapsto_at_view_agree
.
}
iDestruct
"H12"
as
%
[
??
].
iPureIntro
.
eapply
list_eq_same_length
;
try
by
rewrite
fmap_length
.
intros
i
v1
v2
Hi
H1
H2
.
rewrite
>
list_lookup_fmap
,
fmap_Some
in
H1
;
destruct
H1
as
(
vV1
&
H1
&
>
).
rewrite
>
list_lookup_fmap
,
fmap_Some
in
H2
;
destruct
H2
as
(
vV2
&
H2
&
>
).
by
eauto
.
Qed
.
Lemma
store_interp_mapsto_at_view_block
σ
ℓ
vVs
q
:
store_interp
σ

∗
ℓ
*
↦
at
{
q
}
()
vVs

∗
[
∧
list
]
i
↦
vV
∈
vVs
,
let
'
(
v
,
V
)
:=
vV
in
⌜∃
V
ℓ
,
V
⊑
V
ℓ
∧
σ
!!
ℓ
.[
i
]
=
Some
(
store_elt_at
v
V
ℓ
)
⌝
.
Proof
.
Admitted
.
rewrite
mapsto_at_view_block_eq
/
mapsto_at_view_block_def
big_andL_forall
.
iIntros
"Hσ [_?]"
(
i
[
v
V
]
Hi
).
iApply
(
store_interp_mapsto_at_view
with
"Hσ"
).
by
iApply
(
big_sepL_lookup
(
λ
i
vV
,
let
'
(
v
,
V
)
:=
vV
in
mapsto_at_view
_
_
_
_
)
_
_
_
Hi
).
Qed
.
End
blockwise_store
.
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