Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Simon Spies
Iris
Commits
347cd0f5
Commit
347cd0f5
authored
Nov 23, 2017
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Use solely canonical structures for language hierarchy.
parent
d7f8ff30
Changes
8
Hide whitespace changes
Inline
Side-by-side
Showing
8 changed files
with
240 additions
and
179 deletions
+240
-179
theories/heap_lang/lang.v
theories/heap_lang/lang.v
+10
-12
theories/heap_lang/lifting.v
theories/heap_lang/lifting.v
+0
-10
theories/heap_lang/proofmode.v
theories/heap_lang/proofmode.v
+2
-3
theories/program_logic/ectx_language.v
theories/program_logic/ectx_language.v
+103
-61
theories/program_logic/ectx_lifting.v
theories/program_logic/ectx_lifting.v
+4
-13
theories/program_logic/ectxi_language.v
theories/program_logic/ectxi_language.v
+94
-70
theories/program_logic/language.v
theories/program_logic/language.v
+24
-6
theories/program_logic/ownp.v
theories/program_logic/ownp.v
+3
-4
No files found.
theories/heap_lang/lang.v
View file @
347cd0f5
...
...
@@ -374,7 +374,7 @@ Lemma fill_item_val Ki e :
is_Some
(
to_val
(
fill_item
Ki
e
))
→
is_Some
(
to_val
e
).
Proof
.
intros
[
v
?].
destruct
Ki
;
simplify_option_eq
;
eauto
.
Qed
.
Lemma
val_stuck
e1
σ
1 e2
σ
2
efs
:
head_step
e1
σ
1 e2
σ
2
efs
→
to_val
e1
=
None
.
Lemma
val_
head_
stuck
e1
σ
1 e2
σ
2
efs
:
head_step
e1
σ
1 e2
σ
2
efs
→
to_val
e1
=
None
.
Proof
.
destruct
1
;
naive_solver
.
Qed
.
Lemma
head_ctx_step_val
Ki
e
σ
1 e2
σ
2
efs
:
...
...
@@ -467,20 +467,18 @@ Lemma subst_rec_ne' f y e x es :
(
x
≠
f
∨
f
=
BAnon
)
→
(
x
≠
y
∨
y
=
BAnon
)
→
subst'
x
es
(
Rec
f
y
e
)
=
Rec
f
y
(
subst'
x
es
e
).
Proof
.
intros
.
destruct
x
;
simplify_option_eq
;
naive_solver
.
Qed
.
Lemma
heap_lang_mixin
:
EctxiLanguageMixin
of_val
to_val
fill_item
head_step
.
Proof
.
split
;
apply
_
||
eauto
using
to_of_val
,
of_to_val
,
val_head_stuck
,
fill_item_val
,
fill_item_no_val_inj
,
head_ctx_step_val
.
Qed
.
End
heap_lang
.
(** Language *)
Program
Instance
heap_ectxi_lang
:
EctxiLanguage
(
heap_lang
.
expr
)
heap_lang
.
val
heap_lang
.
ectx_item
heap_lang
.
state
:
=
{|
of_val
:
=
heap_lang
.
of_val
;
to_val
:
=
heap_lang
.
to_val
;
fill_item
:
=
heap_lang
.
fill_item
;
head_step
:
=
heap_lang
.
head_step
|}.
Solve
Obligations
with
eauto
using
heap_lang
.
to_of_val
,
heap_lang
.
of_to_val
,
heap_lang
.
val_stuck
,
heap_lang
.
fill_item_val
,
heap_lang
.
fill_item_no_val_inj
,
heap_lang
.
head_ctx_step_val
.
Canonical
Structure
heap_lang
:
=
ectx_lang
(
heap_lang
.
expr
).
Canonical
Structure
heap_ectxi_lang
:
=
EctxiLanguage
heap_lang
.
heap_lang_mixin
.
Canonical
Structure
heap_ectx_lang
:
=
EctxLanguageOfEctxi
heap_ectxi_lang
.
Canonical
Structure
heap_lang
:
=
LanguageOfEctx
heap_ectx_lang
.
(* Prefer heap_lang names over ectx_language names. *)
Export
heap_lang
.
...
...
theories/heap_lang/lifting.v
View file @
347cd0f5
...
...
@@ -61,16 +61,6 @@ Implicit Types Φ : val → iProp Σ.
Implicit
Types
efs
:
list
expr
.
Implicit
Types
σ
:
state
.
(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
Lemma
wp_bind
{
E
e
}
K
Φ
:
WP
e
@
E
{{
v
,
WP
fill
K
(
of_val
v
)
@
E
{{
Φ
}}
}}
⊢
WP
fill
K
e
@
E
{{
Φ
}}.
Proof
.
exact
:
wp_ectx_bind
.
Qed
.
Lemma
wp_bindi
{
E
e
}
Ki
Φ
:
WP
e
@
E
{{
v
,
WP
fill_item
Ki
(
of_val
v
)
@
E
{{
Φ
}}
}}
⊢
WP
fill_item
Ki
e
@
E
{{
Φ
}}.
Proof
.
exact
:
weakestpre
.
wp_bind
.
Qed
.
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma
wp_fork
E
e
Φ
:
▷
Φ
(
LitV
LitUnit
)
∗
▷
WP
e
{{
_
,
True
}}
⊢
WP
Fork
e
@
E
{{
Φ
}}.
...
...
theories/heap_lang/proofmode.v
View file @
347cd0f5
...
...
@@ -13,8 +13,7 @@ Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
envs_entails
Δ
(
WP
fill
K
e1
@
E
{{
Φ
}}).
Proof
.
rewrite
/
envs_entails
=>
???
H
Δ
'
.
rewrite
into_laterN_env_sound
/=.
rewrite
-
lifting
.
wp_bind
H
Δ
'
-
wp_pure_step_later
//.
by
rewrite
-
ectx_lifting
.
wp_ectx_bind_inv
.
rewrite
-
wp_bind
H
Δ
'
-
wp_pure_step_later
//.
by
rewrite
-
wp_bind_inv
.
Qed
.
Lemma
tac_wp_value
`
{
heapG
Σ
}
Δ
E
Φ
e
v
:
...
...
@@ -55,7 +54,7 @@ Tactic Notation "wp_match" := wp_case; wp_let.
Lemma
tac_wp_bind
`
{
heapG
Σ
}
K
Δ
E
Φ
e
:
envs_entails
Δ
(
WP
e
@
E
{{
v
,
WP
fill
K
(
of_val
v
)
@
E
{{
Φ
}}
}})%
I
→
envs_entails
Δ
(
WP
fill
K
e
@
E
{{
Φ
}}).
Proof
.
rewrite
/
envs_entails
=>
->.
by
apply
wp_bind
.
Qed
.
Proof
.
rewrite
/
envs_entails
=>
->.
by
apply
:
wp_bind
.
Qed
.
Ltac
wp_bind_core
K
:
=
lazymatch
eval
hnf
in
K
with
...
...
theories/program_logic/ectx_language.v
View file @
347cd0f5
...
...
@@ -4,9 +4,46 @@ From iris.algebra Require Export base.
From
iris
.
program_logic
Require
Import
language
.
Set
Default
Proof
Using
"Type"
.
(* We need to make thos arguments indices that we want canonical structure
inference to use a keys. *)
Class
EctxLanguage
(
expr
val
ectx
state
:
Type
)
:
=
{
Section
ectx_language_mixin
.
Context
{
expr
val
ectx
state
:
Type
}.
Context
(
of_val
:
val
→
expr
).
Context
(
to_val
:
expr
→
option
val
).
Context
(
empty_ectx
:
ectx
).
Context
(
comp_ectx
:
ectx
→
ectx
→
ectx
).
Context
(
fill
:
ectx
→
expr
→
expr
).
Context
(
head_step
:
expr
→
state
→
expr
→
state
→
list
expr
→
Prop
).
Record
EctxLanguageMixin
:
=
{
mixin_to_of_val
v
:
to_val
(
of_val
v
)
=
Some
v
;
mixin_of_to_val
e
v
:
to_val
e
=
Some
v
→
of_val
v
=
e
;
mixin_val_head_stuck
e1
σ
1 e2
σ
2
efs
:
head_step
e1
σ
1 e2
σ
2
efs
→
to_val
e1
=
None
;
mixin_fill_empty
e
:
fill
empty_ectx
e
=
e
;
mixin_fill_comp
K1
K2
e
:
fill
K1
(
fill
K2
e
)
=
fill
(
comp_ectx
K1
K2
)
e
;
mixin_fill_inj
K
:
Inj
(=)
(=)
(
fill
K
)
;
mixin_fill_val
K
e
:
is_Some
(
to_val
(
fill
K
e
))
→
is_Some
(
to_val
e
)
;
(* There are a whole lot of sensible axioms (like associativity, and left and
right identity, we could demand for [comp_ectx] and [empty_ectx]. However,
positivity suffices. *)
mixin_ectx_positive
K1
K2
:
comp_ectx
K1
K2
=
empty_ectx
→
K1
=
empty_ectx
∧
K2
=
empty_ectx
;
mixin_step_by_val
K
K'
e1
e1'
σ
1 e2
σ
2
efs
:
fill
K
e1
=
fill
K'
e1'
→
to_val
e1
=
None
→
head_step
e1'
σ
1 e2
σ
2
efs
→
∃
K''
,
K'
=
comp_ectx
K
K''
;
}.
End
ectx_language_mixin
.
Structure
ectxLanguage
:
=
EctxLanguage
{
expr
:
Type
;
val
:
Type
;
ectx
:
Type
;
state
:
Type
;
of_val
:
val
→
expr
;
to_val
:
expr
→
option
val
;
empty_ectx
:
ectx
;
...
...
@@ -14,61 +51,58 @@ Class EctxLanguage (expr val ectx state : Type) := {
fill
:
ectx
→
expr
→
expr
;
head_step
:
expr
→
state
→
expr
→
state
→
list
expr
→
Prop
;
to_of_val
v
:
to_val
(
of_val
v
)
=
Some
v
;
of_to_val
e
v
:
to_val
e
=
Some
v
→
of_val
v
=
e
;
val_stuck
e1
σ
1 e2
σ
2
efs
:
head_step
e1
σ
1 e2
σ
2
efs
→
to_val
e1
=
None
;
fill_empty
e
:
fill
empty_ectx
e
=
e
;
fill_comp
K1
K2
e
:
fill
K1
(
fill
K2
e
)
=
fill
(
comp_ectx
K1
K2
)
e
;
fill_inj
K
:
>
Inj
(=)
(=)
(
fill
K
)
;
fill_not_val
K
e
:
to_val
e
=
None
→
to_val
(
fill
K
e
)
=
None
;
(* There are a whole lot of sensible axioms (like associativity, and left and
right identity, we could demand for [comp_ectx] and [empty_ectx]. However,
positivity suffices. *)
ectx_positive
K1
K2
:
comp_ectx
K1
K2
=
empty_ectx
→
K1
=
empty_ectx
∧
K2
=
empty_ectx
;
step_by_val
K
K'
e1
e1'
σ
1 e2
σ
2
efs
:
fill
K
e1
=
fill
K'
e1'
→
to_val
e1
=
None
→
head_step
e1'
σ
1 e2
σ
2
efs
→
exists
K''
,
K'
=
comp_ectx
K
K''
;
ectx_language_mixin
:
EctxLanguageMixin
of_val
to_val
empty_ectx
comp_ectx
fill
head_step
}.
Arguments
of_val
{
_
_
_
_
_
}
_
%
V
.
Arguments
to_val
{
_
_
_
_
_
}
_
%
E
.
Arguments
empty_ectx
{
_
_
_
_
_
}.
Arguments
comp_ectx
{
_
_
_
_
_
}
_
_
.
Arguments
fill
{
_
_
_
_
_
}
_
_
%
E
.
Arguments
head_step
{
_
_
_
_
_
}
_
%
E
_
_
%
E
_
_
.
Arguments
to_of_val
{
_
_
_
_
_
}
_
.
Arguments
of_to_val
{
_
_
_
_
_
}
_
_
_
.
Arguments
val_stuck
{
_
_
_
_
_
}
_
_
_
_
_
_
.
Arguments
fill_empty
{
_
_
_
_
_
}
_
.
Arguments
fill_comp
{
_
_
_
_
_
}
_
_
_
.
Arguments
fill_not_val
{
_
_
_
_
_
}
_
_
_
.
Arguments
ectx_positive
{
_
_
_
_
_
}
_
_
_
.
Arguments
step_by_val
{
_
_
_
_
_
}
_
_
_
_
_
_
_
_
_
_
_
.
Arguments
EctxLanguage
{
_
_
_
_
_
_
_
_
_
_
}
_
.
Arguments
of_val
{
_
}
_
%
V
.
Arguments
to_val
{
_
}
_
%
E
.
Arguments
empty_ectx
{
_
}.
Arguments
comp_ectx
{
_
}
_
_
.
Arguments
fill
{
_
}
_
_
%
E
.
Arguments
head_step
{
_
}
_
%
E
_
_
%
E
_
_
.
(* From an ectx_language, we can construct a language. *)
Section
ectx_language
.
Context
{
expr
val
ectx
state
}
{
Λ
:
EctxLanguage
expr
val
ectx
state
}.
Implicit
Types
(
e
:
expr
)
(
K
:
ectx
).
Context
{
Λ
:
ectxLanguage
}.
Implicit
Types
v
:
val
Λ
.
Implicit
Types
e
:
expr
Λ
.
Implicit
Types
K
:
ectx
Λ
.
(* Only project stuff out of the mixin that is not also in language *)
Lemma
val_head_stuck
e1
σ
1 e2
σ
2
efs
:
head_step
e1
σ
1 e2
σ
2
efs
→
to_val
e1
=
None
.
Proof
.
apply
ectx_language_mixin
.
Qed
.
Lemma
fill_empty
e
:
fill
empty_ectx
e
=
e
.
Proof
.
apply
ectx_language_mixin
.
Qed
.
Lemma
fill_comp
K1
K2
e
:
fill
K1
(
fill
K2
e
)
=
fill
(
comp_ectx
K1
K2
)
e
.
Proof
.
apply
ectx_language_mixin
.
Qed
.
Global
Instance
fill_inj
K
:
Inj
(=)
(=)
(
fill
K
).
Proof
.
apply
ectx_language_mixin
.
Qed
.
Lemma
fill_val
K
e
:
is_Some
(
to_val
(
fill
K
e
))
→
is_Some
(
to_val
e
).
Proof
.
apply
ectx_language_mixin
.
Qed
.
Lemma
ectx_positive
K1
K2
:
comp_ectx
K1
K2
=
empty_ectx
→
K1
=
empty_ectx
∧
K2
=
empty_ectx
.
Proof
.
apply
ectx_language_mixin
.
Qed
.
Lemma
step_by_val
K
K'
e1
e1'
σ
1 e2
σ
2
efs
:
fill
K
e1
=
fill
K'
e1'
→
to_val
e1
=
None
→
head_step
e1'
σ
1 e2
σ
2
efs
→
∃
K''
,
K'
=
comp_ectx
K
K''
.
Proof
.
apply
ectx_language_mixin
.
Qed
.
Definition
head_reducible
(
e
:
expr
)
(
σ
:
state
)
:
=
Definition
head_reducible
(
e
:
expr
Λ
)
(
σ
:
state
Λ
)
:
=
∃
e'
σ
'
efs
,
head_step
e
σ
e'
σ
'
efs
.
Definition
head_irreducible
(
e
:
expr
)
(
σ
:
state
)
:
=
Definition
head_irreducible
(
e
:
expr
Λ
)
(
σ
:
state
Λ
)
:
=
∀
e'
σ
'
efs
,
¬
head_step
e
σ
e'
σ
'
efs
.
(* All non-value redexes are at the root. In other words, all sub-redexes are
values. *)
Definition
sub_redexes_are_values
(
e
:
expr
)
:
=
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
)
(
e2
:
expr
)
(
σ
2
:
state
)
(
efs
:
list
expr
)
:
Prop
:
=
Inductive
prim_step
(
e1
:
expr
Λ
)
(
σ
1
:
state
Λ
)
(
e2
:
expr
Λ
)
(
σ
2
:
state
Λ
)
(
efs
:
list
(
expr
Λ
)
)
:
Prop
:
=
Ectx_step
K
e1'
e2'
:
e1
=
fill
K
e1'
→
e2
=
fill
K
e2'
→
head_step
e1'
σ
1 e2
'
σ
2
efs
→
prim_step
e1
σ
1 e2
σ
2
efs
.
...
...
@@ -77,19 +111,21 @@ Section ectx_language.
head_step
e1
σ
1 e2
σ
2
efs
→
prim_step
(
fill
K
e1
)
σ
1
(
fill
K
e2
)
σ
2
efs
.
Proof
.
econstructor
;
eauto
.
Qed
.
Lemma
val_prim_stuck
e1
σ
1 e2
σ
2
efs
:
prim_step
e1
σ
1 e2
σ
2
efs
→
to_val
e1
=
None
.
Proof
.
intros
[???
->
->
?]
;
eauto
using
fill_not_val
,
val_stuck
.
Qed
.
Definition
ectx_lang_mixin
:
LanguageMixin
of_val
to_val
prim_step
.
Proof
.
split
.
-
apply
ectx_language_mixin
.
-
apply
ectx_language_mixin
.
-
intros
?????
[???
->
->
?%
val_head_stuck
].
apply
eq_None_not_Some
.
by
intros
?%
fill_val
%
eq_None_not_Some
.
Qed
.
Canonical
Structure
ectx_lang
:
language
:
=
{|
language
.
expr
:
=
expr
;
language
.
val
:
=
val
;
language
.
state
:
=
state
;
language
.
of_val
:
=
of_val
;
language
.
to_val
:
=
to_val
;
language
.
prim_step
:
=
prim_step
;
language
.
to_of_val
:
=
to_of_val
;
language
.
of_to_val
:
=
of_to_val
;
language
.
val_stuck
:
=
val_prim_stuck
;
|}.
Canonical
Structure
ectx_lang
:
language
:
=
Language
ectx_lang_mixin
.
(* Some lemmas about this language *)
Lemma
fill_not_val
K
e
:
to_val
e
=
None
→
to_val
(
fill
K
e
)
=
None
.
Proof
.
rewrite
!
eq_None_not_Some
.
eauto
using
fill_val
.
Qed
.
Lemma
head_prim_step
e1
σ
1 e2
σ
2
efs
:
head_step
e1
σ
1 e2
σ
2
efs
→
prim_step
e1
σ
1 e2
σ
2
efs
.
Proof
.
apply
Ectx_step
with
empty_ectx
;
by
rewrite
?fill_empty
.
Qed
.
...
...
@@ -108,7 +144,7 @@ Section ectx_language.
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
.
assert
(
K
=
empty_ectx
)
as
->
by
eauto
10
using
val_
head_
stuck
.
rewrite
fill_empty
/
head_reducible
;
eauto
.
Qed
.
Lemma
prim_head_irreducible
e
σ
:
...
...
@@ -123,7 +159,7 @@ Section ectx_language.
Atomic
e
.
Proof
.
intros
Hatomic_step
Hatomic_fill
σ
e'
σ
'
efs
[
K
e1'
e2'
->
->
Hstep
].
assert
(
K
=
empty_ectx
)
as
->
by
eauto
10
using
val_stuck
.
assert
(
K
=
empty_ectx
)
as
->
by
eauto
10
using
val_
head_
stuck
.
rewrite
fill_empty
.
eapply
Hatomic_step
.
by
rewrite
fill_empty
.
Qed
.
...
...
@@ -135,14 +171,14 @@ Section ectx_language.
intros
(
e2''
&
σ
2
''
&
efs''
&?)
[
K
e1'
e2'
->
->
Hstep
].
destruct
(
step_by_val
K
empty_ectx
e1'
(
fill
K
e1'
)
σ
1 e2
''
σ
2
''
efs''
)
as
[
K'
[->
_
]%
symmetry
%
ectx_positive
]
;
eauto
using
fill_empty
,
fill_not_val
,
val_stuck
.
eauto
using
fill_empty
,
fill_not_val
,
val_
head_
stuck
.
by
rewrite
!
fill_empty
.
Qed
.
(* Every evaluation context is a context. *)
Global
Instance
ectx_lang_ctx
K
:
LanguageCtx
ectx_lang
(
fill
K
).
Global
Instance
ectx_lang_ctx
K
:
LanguageCtx
_
(
fill
K
).
Proof
.
split
.
split
;
simpl
.
-
eauto
using
fill_not_val
.
-
intros
?????
[
K'
e1'
e2'
Heq1
Heq2
Hstep
].
by
exists
(
comp_ectx
K
K'
)
e1'
e2'
;
rewrite
?Heq1
?Heq2
?fill_comp
.
...
...
@@ -166,4 +202,10 @@ Section ectx_language.
Qed
.
End
ectx_language
.
Arguments
ectx_lang
_
{
_
_
_
_
}.
Arguments
ectx_lang
:
clear
implicits
.
Coercion
ectx_lang
:
ectxLanguage
>->
language
.
Definition
LanguageOfEctx
(
Λ
:
ectxLanguage
)
:
language
:
=
let
'
@
EctxLanguage
E
V
C
St
of_val
to_val
empty
comp
fill
head
mix
:
=
Λ
in
@
Language
E
V
St
of_val
to_val
_
(@
ectx_lang_mixin
(@
EctxLanguage
E
V
C
St
of_val
to_val
empty
comp
fill
head
mix
)).
theories/program_logic/ectx_lifting.v
View file @
347cd0f5
...
...
@@ -4,22 +4,13 @@ From iris.proofmode Require Import tactics.
Set
Default
Proof
Using
"Type"
.
Section
wp
.
Context
{
expr
val
ectx
state
}
{
Λ
:
EctxLanguage
expr
val
ectx
state
}.
Context
`
{
irisG
(
ectx_lang
expr
)
Σ
}
{
Hinh
:
Inhabited
state
}.
Context
{
Λ
:
ectxLanguage
}
`
{
irisG
Λ
Σ
}
{
Hinh
:
Inhabited
(
state
Λ
)}.
Implicit
Types
P
:
iProp
Σ
.
Implicit
Types
Φ
:
val
→
iProp
Σ
.
Implicit
Types
v
:
val
.
Implicit
Types
e
:
expr
.
Implicit
Types
Φ
:
val
Λ
→
iProp
Σ
.
Implicit
Types
v
:
val
Λ
.
Implicit
Types
e
:
expr
Λ
.
Hint
Resolve
head_prim_reducible
head_reducible_prim_step
.
Lemma
wp_ectx_bind
{
E
Φ
}
K
e
:
WP
e
@
E
{{
v
,
WP
fill
K
(
of_val
v
)
@
E
{{
Φ
}}
}}
⊢
WP
fill
K
e
@
E
{{
Φ
}}.
Proof
.
apply
:
weakestpre
.
wp_bind
.
Qed
.
Lemma
wp_ectx_bind_inv
{
E
Φ
}
K
e
:
WP
fill
K
e
@
E
{{
Φ
}}
⊢
WP
e
@
E
{{
v
,
WP
fill
K
(
of_val
v
)
@
E
{{
Φ
}}
}}.
Proof
.
apply
:
weakestpre
.
wp_bind_inv
.
Qed
.
Lemma
wp_lift_head_step
{
E
Φ
}
e1
:
to_val
e1
=
None
→
(
∀
σ
1
,
state_interp
σ
1
={
E
,
∅
}=
∗
...
...
theories/program_logic/ectxi_language.v
View file @
347cd0f5
...
...
@@ -4,92 +4,108 @@ From iris.algebra Require Export base.
From
iris
.
program_logic
Require
Import
language
ectx_language
.
Set
Default
Proof
Using
"Type"
.
(* We need to make thos arguments indices that we want canonical structure
inference to use a keys. *)
Class
EctxiLanguage
(
expr
val
ectx_item
state
:
Type
)
:
=
{
Section
ectxi_language_mixin
.
Context
{
expr
val
ectx_item
state
:
Type
}.
Context
(
of_val
:
val
→
expr
).
Context
(
to_val
:
expr
→
option
val
).
Context
(
fill_item
:
ectx_item
→
expr
→
expr
).
Context
(
head_step
:
expr
→
state
→
expr
→
state
→
list
expr
→
Prop
).
Record
EctxiLanguageMixin
:
=
{
mixin_to_of_val
v
:
to_val
(
of_val
v
)
=
Some
v
;
mixin_of_to_val
e
v
:
to_val
e
=
Some
v
→
of_val
v
=
e
;
mixin_val_stuck
e1
σ
1 e2
σ
2
efs
:
head_step
e1
σ
1 e2
σ
2
efs
→
to_val
e1
=
None
;
mixin_fill_item_inj
Ki
:
Inj
(=)
(=)
(
fill_item
Ki
)
;
mixin_fill_item_val
Ki
e
:
is_Some
(
to_val
(
fill_item
Ki
e
))
→
is_Some
(
to_val
e
)
;
mixin_fill_item_no_val_inj
Ki1
Ki2
e1
e2
:
to_val
e1
=
None
→
to_val
e2
=
None
→
fill_item
Ki1
e1
=
fill_item
Ki2
e2
→
Ki1
=
Ki2
;
mixin_head_ctx_step_val
Ki
e
σ
1 e2
σ
2
efs
:
head_step
(
fill_item
Ki
e
)
σ
1 e2
σ
2
efs
→
is_Some
(
to_val
e
)
;
}.
End
ectxi_language_mixin
.
Structure
ectxiLanguage
:
=
EctxiLanguage
{
expr
:
Type
;
val
:
Type
;
ectx_item
:
Type
;
state
:
Type
;
of_val
:
val
→
expr
;
to_val
:
expr
→
option
val
;
fill_item
:
ectx_item
→
expr
→
expr
;
head_step
:
expr
→
state
→
expr
→
state
→
list
expr
→
Prop
;
to_of_val
v
:
to_val
(
of_val
v
)
=
Some
v
;
of_to_val
e
v
:
to_val
e
=
Some
v
→
of_val
v
=
e
;
val_stuck
e1
σ
1 e2
σ
2
efs
:
head_step
e1
σ
1 e2
σ
2
efs
→
to_val
e1
=
None
;
fill_item_inj
Ki
:
>
Inj
(=)
(=)
(
fill_item
Ki
)
;
fill_item_val
Ki
e
:
is_Some
(
to_val
(
fill_item
Ki
e
))
→
is_Some
(
to_val
e
)
;
fill_item_no_val_inj
Ki1
Ki2
e1
e2
:
to_val
e1
=
None
→
to_val
e2
=
None
→
fill_item
Ki1
e1
=
fill_item
Ki2
e2
→
Ki1
=
Ki2
;
head_ctx_step_val
Ki
e
σ
1 e2
σ
2
efs
:
head_step
(
fill_item
Ki
e
)
σ
1 e2
σ
2
efs
→
is_Some
(
to_val
e
)
;
ectxi_language_mixin
:
EctxiLanguageMixin
of_val
to_val
fill_item
head_step
}.
Arguments
of_val
{
_
_
_
_
_
}
_
%
V
.
Arguments
to_val
{
_
_
_
_
_
}
_
%
E
.
Arguments
fill_item
{
_
_
_
_
_
}
_
_
%
E
.
Arguments
head_step
{
_
_
_
_
_
}
_
%
E
_
_
%
E
_
_
.
Arguments
to_of_val
{
_
_
_
_
_
}
_
.
Arguments
of_to_val
{
_
_
_
_
_
}
_
_
_
.
Arguments
val_stuck
{
_
_
_
_
_
}
_
_
_
_
_
_
.
Arguments
fill_item_val
{
_
_
_
_
_
}
_
_
_
.
Arguments
fill_item_no_val_inj
{
_
_
_
_
_
}
_
_
_
_
_
_
_
.
Arguments
head_ctx_step_val
{
_
_
_
_
_
}
_
_
_
_
_
_
_
.
Arguments
step_by_val
{
_
_
_
_
_
}
_
_
_
_
_
_
_
_
_
_
_
.
Arguments
EctxiLanguage
{
_
_
_
_
_
_
_
_
}
_
.
Arguments
of_val
{
_
}
_
%
V
.
Arguments
to_val
{
_
}
_
%
E
.
Arguments
fill_item
{
_
}
_
_
%
E
.
Arguments
head_step
{
_
}
_
%
E
_
_
%
E
_
_
.
Section
ectxi_language
.
Context
{
expr
val
ectx_item
state
}
{
Λ
:
EctxiLanguage
expr
val
ectx_item
state
}.
Implicit
Types
(
e
:
expr
)
(
Ki
:
ectx_item
).
Notation
ectx
:
=
(
list
ectx_item
).
Context
{
Λ
:
ectxiLanguage
}.
Implicit
Types
(
e
:
expr
Λ
)
(
Ki
:
ectx_item
Λ
).
Notation
ectx
:
=
(
list
(
ectx_item
Λ
)).
(* Only project stuff out of the mixin that is not also in ectxLanguage *)
Global
Instance
fill_item_inj
Ki
:
Inj
(=)
(=)
(
fill_item
Ki
).
Proof
.
apply
ectxi_language_mixin
.
Qed
.
Lemma
fill_item_val
Ki
e
:
is_Some
(
to_val
(
fill_item
Ki
e
))
→
is_Some
(
to_val
e
).
Proof
.
apply
ectxi_language_mixin
.
Qed
.
Lemma
fill_item_no_val_inj
Ki1
Ki2
e1
e2
:
to_val
e1
=
None
→
to_val
e2
=
None
→
fill_item
Ki1
e1
=
fill_item
Ki2
e2
→
Ki1
=
Ki2
.
Proof
.
apply
ectxi_language_mixin
.
Qed
.
Lemma
head_ctx_step_val
Ki
e
σ
1 e2
σ
2
efs
:
head_step
(
fill_item
Ki
e
)
σ
1 e2
σ
2
efs
→
is_Some
(
to_val
e
).
Proof
.
apply
ectxi_language_mixin
.
Qed
.
Definition
fill
(
K
:
ectx
)
(
e
:
expr
)
:
expr
:
=
foldl
(
flip
fill_item
)
e
K
.
Definition
fill
(
K
:
ectx
)
(
e
:
expr
Λ
)
:
expr
Λ
:
=
foldl
(
flip
fill_item
)
e
K
.
Lemma
fill_app
(
K1
K2
:
ectx
)
e
:
fill
(
K1
++
K2
)
e
=
fill
K2
(
fill
K1
e
).
Proof
.
apply
foldl_app
.
Qed
.
Instance
fill_inj
K
:
Inj
(=)
(=)
(
fill
K
).
Proof
.
induction
K
as
[|
Ki
K
IH
]
;
rewrite
/
Inj
;
naive_solver
.
Qed
.
Lemma
fill_val
K
e
:
is_Some
(
to_val
(
fill
K
e
))
→
is_Some
(
to_val
e
).
Definition
ectxi_lang_ectx_mixin
:
EctxLanguageMixin
of_val
to_val
[]
(
flip
(++))
fill
head_step
.
Proof
.
revert
e
.
induction
K
as
[|
Ki
K
IH
]=>
e
//=.
by
intros
?%
IH
%
fill_item_val
.
assert
(
fill_val
:
∀
K
e
,
is_Some
(
to_val
(
fill
K
e
))
→
is_Some
(
to_val
e
)).
{
intros
K
.
induction
K
as
[|
Ki
K
IH
]=>
e
//=.
by
intros
?%
IH
%
fill_item_val
.
}
assert
(
fill_not_val
:
∀
K
e
,
to_val
e
=
None
→
to_val
(
fill
K
e
)
=
None
).
{
intros
K
e
.
rewrite
!
eq_None_not_Some
.
eauto
.
}
split
.
-
apply
ectxi_language_mixin
.
-
apply
ectxi_language_mixin
.
-
apply
ectxi_language_mixin
.
-
done
.
-
intros
K1
K2
e
.
by
rewrite
/
fill
/=
foldl_app
.
-
intros
K
;
induction
K
as
[|
Ki
K
IH
]
;
rewrite
/
Inj
;
naive_solver
.
-
done
.
-
by
intros
[]
[].
-
intros
K
K'
e1
e1'
σ
1 e2
σ
2
efs
Hfill
Hred
Hstep
;
revert
K'
Hfill
.
induction
K
as
[|
Ki
K
IH
]
using
rev_ind
=>
/=
K'
Hfill
;
eauto
using
app_nil_r
.
destruct
K'
as
[|
Ki'
K'
_
]
using
@
rev_ind
;
simplify_eq
/=.
{
rewrite
fill_app
in
Hstep
.
apply
head_ctx_step_val
in
Hstep
.
apply
fill_val
in
Hstep
.
by
apply
not_eq_None_Some
in
Hstep
.
}
rewrite
!
fill_app
/=
in
Hfill
.
assert
(
Ki
=
Ki'
)
as
->.
{
eapply
fill_item_no_val_inj
,
Hfill
;
eauto
using
val_head_stuck
.
apply
fill_not_val
.
revert
Hstep
.
apply
ectxi_language_mixin
.
}
simplify_eq
.
destruct
(
IH
K'
)
as
[
K''
->]
;
auto
.
exists
K''
.
by
rewrite
assoc
.
Qed
.
Canonical
Structure
ectxi_lang_ectx
:
=
EctxLanguage
ectxi_lang_ectx_mixin
.
Canonical
Structure
ectxi_lang
:
=
LanguageOfEctx
ectxi_lang_ectx
.
Lemma
fill_not_val
K
e
:
to_val
e
=
None
→
to_val
(
fill
K
e
)
=
None
.
Proof
.
rewrite
!
eq_None_not_Some
.
eauto
using
fill_val
.
Qed
.
(* When something does a step, and another decomposition of the same expression
has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
other words, [e] also contains the reducible expression *)
Lemma
step_by_val
K
K'
e1
e1'
σ
1 e2
σ
2
efs
:
fill
K
e1
=
fill
K'
e1'
→
to_val
e1
=
None
→
head_step
e1'
σ
1 e2
σ
2
efs
→
exists
K''
,
K'
=
K''
++
K
.
(* K `prefix_of` K' *)
Proof
.
intros
Hfill
Hred
Hstep
;
revert
K'
Hfill
.
induction
K
as
[|
Ki
K
IH
]
using
rev_ind
=>
/=
K'
Hfill
;
eauto
using
app_nil_r
.
destruct
K'
as
[|
Ki'
K'
_
]
using
@
rev_ind
;
simplify_eq
/=.
{
rewrite
fill_app
in
Hstep
.
exfalso
;
apply
(
eq_None_not_Some
(
to_val
(
fill
K
e1
)))
;
eauto
using
fill_not_val
,
head_ctx_step_val
.
}
rewrite
!
fill_app
/=
in
Hfill
.
assert
(
Ki
=
Ki'
)
as
->
by
eauto
using
fill_item_no_val_inj
,
val_stuck
,
fill_not_val
.
simplify_eq
.
destruct
(
IH
K'
)
as
[
K''
->]
;
auto
.
exists
K''
.
by
rewrite
assoc
.
Qed
.
Global
Program
Instance
ectxi_lang_ectx
:
EctxLanguage
expr
val
ectx
state
:
=
{|
ectx_language
.
of_val
:
=
of_val
;
ectx_language
.
to_val
:
=
to_val
;
empty_ectx
:
=
[]
;
comp_ectx
:
=
flip
(++)
;
ectx_language
.
fill
:
=
fill
;
ectx_language
.
head_step
:
=
head_step
|}.
Solve
Obligations
with
simpl
;
eauto
using
to_of_val
,
of_to_val
,
val_stuck
,
fill_not_val
,
fill_app
,
step_by_val
,
foldl_app
.
Next
Obligation
.
intros
K1
K2
?%
app_eq_nil
;
tauto
.
Qed
.
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
.
...
...
@@ -98,9 +114,17 @@ Section ectxi_language.
intros
[]%
eq_None_not_Some
.
eapply
fill_val
,
Hsub
.
by
rewrite
/=
fill_app
.
Qed
.
Global
Instance
ectxi_lang_ctx_item
Ki
:
LanguageCtx
(
ectx_lang
expr
)
(
fill_item
Ki
).
Proof
.
change
(
LanguageCtx
_
(
fill
[
Ki
])).
apply
_
.
Qed
.
Global
Instance
ectxi_lang_ctx_item
Ki
:
LanguageCtx
_
(
fill_item
Ki
).
Proof
.
change
(
LanguageCtx
ectxi_lang
(
fill
[
Ki
])).
apply
_
.
Qed
.
End
ectxi_language
.
Arguments
fill
{
_
_
_
_
_
}
_
_
%
E
.
Arguments
fill
{
_
}
_
_
%
E
.
Arguments
ectxi_lang_ectx
:
clear
implicits
.
Arguments
ectxi_lang
:
clear
implicits
.
Coercion
ectxi_lang_ectx
:
ectxiLanguage
>->
ectxLanguage
.
Coercion
ectxi_lang
:
ectxiLanguage
>->
language
.
Definition
EctxLanguageOfEctxi
(
Λ
:
ectxiLanguage
)
:
ectxLanguage
:
=
let
'
@
EctxiLanguage
E
V
C
St
of_val
to_val
fill
head
mix
:
=
Λ
in
@
EctxLanguage
E
V
(
list
C
)
St
of_val
to_val
_
_
_
_