Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
c
Commits
3a75339e
Commit
3a75339e
authored
Jul 02, 2018
by
Léon Gondelman
Browse files
fixed bug in the definition of denv_wf_len
parent
cef2551f
Changes
1
Hide whitespace changes
Inline
Sidebyside
theories/vcgen/denv.v
View file @
3a75339e
...
...
@@ 40,7 +40,7 @@ Section denv.
Fixpoint
denv_wf_len
(
E
:
known_locs
)
(
m
:
denv
)
:
bool
:
=
match
E
,
m
with

_
,
[]
=>
true

_
::
E'
,
_
::
m'
=>
denv_wf_len
E
m'

_
::
E'
,
_
::
m'
=>
denv_wf_len
E
'
m'

[],
_
=>
false
end
.
...
...
@@ 684,37 +684,77 @@ Section denv_spec.
E
`
prefix_of
`
E'
→
denv_wf_len
E'
m
.
Proof
.
revert
E
.
induction
m
as
[
x
m'
]
;
intros
.
revert
E
E'
.
induction
m
as
[
x
m'
]
;
intros
.

by
destruct
E'
.

destruct
E'
,
E
;
simplify_eq
/=
;
[

by
apply
prefix_nil_not
in
H1


]
;
by
eauto
.

destruct
E'
,
E
;
[

by
apply
prefix_nil_not
in
H1


]
;
try
by
eauto
.
simpl
.
destruct
m'
;
try
done
.
destruct
E'
;
eauto
.
eapply
IHm'
.
done
.
by
eapply
prefix_cons_inv_2
.
Qed
.
Lemma
denv_wf_len_mono_r
E
m1
m2
:
denv_wf_len
E
(
m1
++
m2
)
→
denv_wf_len
E
m2
.
Proof
.
revert
m1
m2
.
induction
E
;
intros
m1
m2
Hwf
.

destruct
m2
;
first
by
naive_solver
.
simpl
in
Hwf
.
destruct
(
m1
++
o
::
m2
)
as
[]
eqn
:
Hyp
.
+
destruct
m1
;
by
inversion
Hyp
.
+
done
.

destruct
m1
;
first
by
naive_solver
.
destruct
m2
;
first
done
.
*
simpl
in
*.
eapply
IHE
with
(
m1
++
[
o0
]).
rewrite

app_assoc
.
naive_solver
.
Qed
.
Lemma
denv_wf_val_mono_r
E
m1
m2
:
denv_wf_val
E
(
m1
++
m2
)
→
denv_wf_val
E
m2
.
Proof
.
revert
m2
.
induction
m1
;
intros
m2
Hwf
.

naive_solver
.

apply
IHm1
.
simpl
in
Hwf
.
destruct
a
as
[
d
]
;
last
done
.
destruct
d
.
naive_solver
.
Qed
.
Lemma
denv_wf_mono
E
E'
m
:
denv_wf
E
m
→
E
`
prefix_of
`
E'
→
denv_wf
E'
m
.
Proof
.
rewrite
!
andb_True
.
induction
m
as
[[
denv
]
ms
]
;
simpl
;
eauto
.

intros
[
_
Hwf
]
Hpre
;
split
;
first
done
.
by
destruct
E'
.

destruct
denv
.
intros
.
destruct_and
!.
split_and
.
rewrite
andb_True
.
split
.
eapply
dval_wf_mono
;
eauto
.
apply
IHms
;
eauto
.
+
split
;
first
done
;
by
destruct
E
.
+
destruct
E
,
E'
;
simplify_eq
/=
;
try
done
;
first
by
apply
prefix_nil_not
in
H1
.
destruct
ms
;
simplify_eq
/=
;
first
done
.
pose
H1
.
apply
prefix_cons_inv_1
in
p
.
apply
(
denv_wf_len_mono
(
c
::
E
)).
done
.
rewrite

p
in
H1
.
by
rewrite

p
.

intros
.
destruct
H0
as
[
Hwg1
He
].
destruct
E
,
E'
;
try
done
.
+
by
apply
prefix_nil_not
in
H1
.
+
by
apply
IHms
.
rewrite
!
andb_True
.
revert
E
E'
.
induction
m
as
[[
denv
]
ms
]
;
eauto
.

intros
E
E'
[
_
Hwf
]
Hpre
;
split
;
first
done
.
by
destruct
E'
.

intros
E
E'
[
Hwf1
Hwf2
]
Hpre
.
split_and
.
+
destruct
E'
.
*
destruct
E
;
simplify_eq
;
first
by
naive_solver
.
by
apply
prefix_nil_not
in
Hpre
.
*
simpl
.
destruct
denv
as
[
lvl
q
dv
].
rewrite
andb_True
.
split
.
**
simpl
in
Hwf1
.
apply
andb_True
in
Hwf1
as
[
Hwf11
Hwf12
].
by
eapply
dval_wf_mono
.
**
eapply
(
IHms
E
(
c
::
E'
))
;
last
done
.
split
.
***
apply
(
denv_wf_val_mono_r
E
[
Some
{
denv_level
:
=
lvl
;
denv_frac
:
=
q
;
denv_dval
:
=
dv
}]).
naive_solver
.
***
apply
(
denv_wf_len_mono_r
E
[
Some
{
denv_level
:
=
lvl
;
denv_frac
:
=
q
;
denv_dval
:
=
dv
}]).
naive_solver
.
+
by
eapply
denv_wf_len_mono
.

intros
E
E'
[
Hwf1
Hwf2
]
Hpre
.
split_and
.
+
destruct
E'
.
*
destruct
E
;
simplify_eq
;
first
by
naive_solver
.
by
apply
prefix_nil_not
in
Hpre
.
*
simpl
.
eapply
(
IHms
E
(
c
::
E'
))
;
last
done
.
split
.
**
by
eapply
(
denv_wf_val_mono_r
E
[
None
]).
**
by
eapply
(
denv_wf_len_mono_r
E
[
None
]).
+
by
eapply
denv_wf_len_mono
.
Qed
.
Lemma
denv_wf_merge_val
(
E
:
known_locs
)
(
m1
m2
:
denv
)
:
denv_wf_val
E
m1
→
denv_wf_val
E
m2
→
denv_wf_val
E
(
denv_merge
m1
m2
).
Proof
.
...
...
@@ 762,7 +802,7 @@ Section denv_spec.
Lemma
denv_wf_len_unlock
E
m
:
denv_wf_len
E
m
→
denv_wf_len
E
(
denv_unlock
m
).
Proof
.
induction
m
;
destruct
E
;
naive_solver
.
revert
m
;
induction
E
;
destruct
m
;
try
naive_solver
.
Qed
.
Lemma
denv_wf_unlock
E
m
:
...
...
@@ 794,10 +834,16 @@ Section denv_spec.
eapply
IHm
;
eauto
.
Qed
.
Lemma
denv_delete_full_len
i
m
m'
q
dv
:
denv_delete_full_aux
i
m
=
Some
(
m'
,
q
,
dv
)
→
length
m'
=
(
length
m

1
)%
nat
.
Proof
.
Admitted
.
Lemma
denv_delete_full_len_aux_wf
E
i
m
m'
q
dv
:
denv_wf_len
E
m
→
denv_delete_full_aux
i
m
=
Some
(
m'
,
q
,
dv
)
→
denv_wf_len
E
m'
.
Proof
.
Admitted
.
Proof
.
Admitted
.
Lemma
denv_delete_full_aux_wf
E
i
m
m'
q
dv
:
denv_wf
E
m
→
denv_delete_full_aux
i
m
=
Some
(
m'
,
q
,
dv
)
→
...
...
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