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
Tej Chajed
iris
Commits
ac0d54da
Commit
ac0d54da
authored
Nov 04, 2017
by
Ralf Jung
Browse files
rename sub_values -> sub_redexes_are_values
parent
0582920d
Changes
3
Hide whitespace changes
Inline
Side-by-side
theories/heap_lang/tactics.v
View file @
ac0d54da
...
...
@@ -195,7 +195,7 @@ Proof.
destruct
e
=>
//=
;
repeat
(
simplify_eq
/=
;
case_match
=>//)
;
inversion
1
;
simplify_eq
/=
;
rewrite
?to_of_val
;
eauto
.
unfold
subst'
;
repeat
(
simplify_eq
/=
;
case_match
=>//)
;
eauto
.
-
apply
ectxi_language_sub_values
=>
/=
Ki
e'
Hfill
.
-
apply
ectxi_language_sub_
redexes_are_
values
=>
/=
Ki
e'
Hfill
.
destruct
e
=>
//
;
destruct
Ki
;
repeat
(
simplify_eq
/=
;
case_match
=>//)
;
naive_solver
eauto
using
to_val_is_Some
.
Qed
.
...
...
theories/program_logic/ectx_language.v
View file @
ac0d54da
...
...
@@ -62,7 +62,9 @@ Section ectx_language.
Definition
head_irreducible
(
e
:
expr
)
(
σ
:
state
)
:
=
∀
e'
σ
'
efs
,
¬
head_step
e
σ
e'
σ
'
efs
.
Definition
sub_values
(
e
:
expr
)
:
=
(* All non-value redexes are at the root. In other words, all sub-redexes are
values. *)
Definition
sub_redexes_are_values
(
e
:
expr
)
:
=
∀
K
e'
,
e
=
fill
K
e'
→
to_val
e'
=
None
→
K
=
empty_ectx
.
Inductive
prim_step
(
e1
:
expr
)
(
σ
1
:
state
)
...
...
@@ -103,21 +105,21 @@ Section ectx_language.
Qed
.
Lemma
prim_head_reducible
e
σ
:
reducible
e
σ
→
sub_values
e
→
head_reducible
e
σ
.
reducible
e
σ
→
sub_
redexes_are_
values
e
→
head_reducible
e
σ
.
Proof
.
intros
(
e'
&
σ
'
&
efs
&[
K
e1'
e2'
->
->
Hstep
])
?.
assert
(
K
=
empty_ectx
)
as
->
by
eauto
10
using
val_stuck
.
rewrite
fill_empty
/
head_reducible
;
eauto
.
Qed
.
Lemma
prim_head_irreducible
e
σ
:
head_irreducible
e
σ
→
sub_values
e
→
irreducible
e
σ
.
head_irreducible
e
σ
→
sub_
redexes_are_
values
e
→
irreducible
e
σ
.
Proof
.
rewrite
-
not_reducible
-
not_head_reducible
.
eauto
using
prim_head_reducible
.
Qed
.
Lemma
ectx_language_atomic
e
:
(
∀
σ
e'
σ
'
efs
,
head_step
e
σ
e'
σ
'
efs
→
irreducible
e'
σ
'
)
→
sub_values
e
→
sub_
redexes_are_
values
e
→
Atomic
e
.
Proof
.
intros
Hatomic_step
Hatomic_fill
σ
e'
σ
'
efs
[
K
e1'
e2'
->
->
Hstep
].
...
...
theories/program_logic/ectxi_language.v
View file @
ac0d54da
...
...
@@ -90,8 +90,9 @@ Section ectxi_language.
fill_not_val
,
fill_app
,
step_by_val
,
foldl_app
.
Next
Obligation
.
intros
K1
K2
?%
app_eq_nil
;
tauto
.
Qed
.
Lemma
ectxi_language_sub_values
e
:
(
∀
Ki
e'
,
e
=
fill_item
Ki
e'
→
is_Some
(
to_val
e'
))
→
sub_values
e
.
Lemma
ectxi_language_sub_redexes_are_values
e
:
(
∀
Ki
e'
,
e
=
fill_item
Ki
e'
→
is_Some
(
to_val
e'
))
→
sub_redexes_are_values
e
.
Proof
.
intros
Hsub
K
e'
->.
destruct
K
as
[|
Ki
K
_
]
using
@
rev_ind
=>
//=.
intros
[]%
eq_None_not_Some
.
eapply
fill_val
,
Hsub
.
by
rewrite
/=
fill_app
.
...
...
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