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
Dan Frumin
ReLoC-v1
Commits
b8da1732
Commit
b8da1732
authored
Sep 13, 2017
by
Dan Frumin
Browse files
Get rid of some unnecessary closedness conditions
parent
940861cf
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/logrel/rules.v
View file @
b8da1732
...
...
@@ -202,8 +202,7 @@ Section properties.
-
by
inv_head_step
.
Qed
.
Lemma
bin_log_related_pack_l
Δ
Γ
E
K
e
e
'
v
t
τ
(
Hclosed
'
:
Closed
∅
e
'
)
:
Lemma
bin_log_related_pack_l
Δ
Γ
E
K
e
e
'
v
t
τ
:
to_val
e
=
Some
v
→
▷
(
{
E
,
E
;
Δ
;
Γ
}
⊨
fill
K
(
App
e
'
e
)
≤
log
≤
t
:
τ
)
⊢
{
E
,
E
;
Δ
;
Γ
}
⊨
fill
K
(
Unpack
(
Pack
e
)
e
'
)
≤
log
≤
t
:
τ
.
...
...
@@ -214,9 +213,7 @@ Section properties.
-
by
inv_head_step
.
Qed
.
Lemma
bin_log_related_case_inl_l
Δ
Γ
E
K
e
v
e1
e2
t
τ
(
Hclosed1
:
Closed
∅
e1
)
(
Hclosed2
:
Closed
∅
e2
)
:
Lemma
bin_log_related_case_inl_l
Δ
Γ
E
K
e
v
e1
e2
t
τ
:
to_val
e
=
Some
v
→
▷
(
{
E
,
E
;
Δ
;
Γ
}
⊨
fill
K
(
App
e1
e
)
≤
log
≤
t
:
τ
)
⊢
{
E
,
E
;
Δ
;
Γ
}
⊨
fill
K
(
Case
(
InjL
e
)
e1
e2
)
≤
log
≤
t
:
τ
.
...
...
@@ -227,9 +224,7 @@ Section properties.
-
by
inv_head_step
.
Qed
.
Lemma
bin_log_related_case_inr_l
Δ
Γ
E
K
e
v
e1
e2
t
τ
(
Hclosed1
:
Closed
∅
e1
)
(
Hclosed2
:
Closed
∅
e2
)
:
Lemma
bin_log_related_case_inr_l
Δ
Γ
E
K
e
v
e1
e2
t
τ
:
to_val
e
=
Some
v
→
▷
(
{
E
,
E
;
Δ
;
Γ
}
⊨
fill
K
(
App
e2
e
)
≤
log
≤
t
:
τ
)
⊢
{
E
,
E
;
Δ
;
Γ
}
⊨
fill
K
(
Case
(
InjR
e
)
e1
e2
)
≤
log
≤
t
:
τ
.
...
...
@@ -240,9 +235,7 @@ Section properties.
-
by
inv_head_step
.
Qed
.
Lemma
bin_log_related_if_true_l
Δ
Γ
E
K
e1
e2
t
τ
(
Hclosed1
:
Closed
∅
e1
)
(
Hclosed2
:
Closed
∅
e2
)
:
Lemma
bin_log_related_if_true_l
Δ
Γ
E
K
e1
e2
t
τ
:
▷
(
{
E
,
E
;
Δ
;
Γ
}
⊨
fill
K
e1
≤
log
≤
t
:
τ
)
⊢
{
E
,
E
;
Δ
;
Γ
}
⊨
fill
K
(
If
#
true
e1
e2
)
≤
log
≤
t
:
τ
.
Proof
.
...
...
@@ -252,9 +245,7 @@ Section properties.
-
by
inv_head_step
.
Qed
.
Lemma
bin_log_related_if_true_masked_l
Δ
Γ
E1
E2
K
e1
e2
t
τ
(
Hclosed1
:
Closed
∅
e1
)
(
Hclosed2
:
Closed
∅
e2
)
:
Lemma
bin_log_related_if_true_masked_l
Δ
Γ
E1
E2
K
e1
e2
t
τ
:
(
{
E1
,
E2
;
Δ
;
Γ
}
⊨
fill
K
e1
≤
log
≤
t
:
τ
)
⊢
{
E1
,
E2
;
Δ
;
Γ
}
⊨
fill
K
(
If
#
true
e1
e2
)
≤
log
≤
t
:
τ
.
Proof
.
...
...
@@ -264,9 +255,7 @@ Section properties.
-
by
inv_head_step
.
Qed
.
Lemma
bin_log_related_if_false_l
Δ
Γ
E
K
e1
e2
t
τ
(
Hclosed1
:
Closed
∅
e1
)
(
Hclosed2
:
Closed
∅
e2
)
:
Lemma
bin_log_related_if_false_l
Δ
Γ
E
K
e1
e2
t
τ
:
▷
(
{
E
,
E
;
Δ
;
Γ
}
⊨
fill
K
e2
≤
log
≤
t
:
τ
)
⊢
{
E
,
E
;
Δ
;
Γ
}
⊨
(
fill
K
(
If
#
false
e1
e2
))
≤
log
≤
t
:
τ
.
Proof
.
...
...
@@ -276,9 +265,7 @@ Section properties.
-
by
inv_head_step
.
Qed
.
Lemma
bin_log_related_if_false_masked_l
Δ
Γ
E1
E2
K
e1
e2
t
τ
(
Hclosed1
:
Closed
∅
e1
)
(
Hclosed2
:
Closed
∅
e2
)
:
Lemma
bin_log_related_if_false_masked_l
Δ
Γ
E1
E2
K
e1
e2
t
τ
:
(
{
E1
,
E2
;
Δ
;
Γ
}
⊨
fill
K
e2
≤
log
≤
t
:
τ
)
⊢
{
E1
,
E2
;
Δ
;
Γ
}
⊨
(
fill
K
(
If
#
false
e1
e2
))
≤
log
≤
t
:
τ
.
Proof
.
...
...
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