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
stdpp
Commits
2883ab5a
Commit
2883ab5a
authored
Jul 15, 2019
by
Michael Sammler
Browse files
Proofs about binders
parent
aa051883
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
37 additions
and
16 deletions
+37
16
theories/binders.v
theories/binders.v
+37
16
No files found.
theories/binders.v
View file @
2883ab5a
...
@@ 21,29 +21,50 @@ Instance binder_inhabited : Inhabited binder := populate BAnon.
...
@@ 21,29 +21,50 @@ Instance binder_inhabited : Inhabited binder := populate BAnon.
Instance
binder_countable
:
Countable
binder
.
Instance
binder_countable
:
Countable
binder
.
Proof
.
Proof
.
refine
(
inj_countable'
refine
(
inj_countable'
(
λ
mx
,
match
mx
with
BAnon
=>
None

BNamed
x
=>
Some
x
end
)
(
λ
b
,
match
b
with
BAnon
=>
None

BNamed
s
=>
Some
s
end
)
(
λ
mx
,
match
mx
with
None
=>
BAnon

Some
x
=>
BNamed
x
end
)
_
)
;
by
intros
[].
(
λ
b
,
match
b
with
None
=>
BAnon

Some
s
=>
BNamed
s
end
)
_
)
;
by
intros
[].
Qed
.
Qed
.
(** The functions [cons_binder
mx X
] and [app_binder
mxs X
] are typically used
(** The functions [cons_binder
b ss
] and [app_binder
bs ss
] are typically used
to collect the free variables of an expression. Here [
X
] is the current list of
to collect the free variables of an expression. Here [
ss
] is the current list of
free variables, and [
mx
], respectively [
mx
s], are the binders that are being
free variables, and [
b
], respectively [
b
s], are the binders that are being
added. *)
added. *)
Definition
cons_binder
(
mx
:
binder
)
(
X
:
list
string
)
:
list
string
:
=
Definition
cons_binder
(
b
:
binder
)
(
ss
:
list
string
)
:
list
string
:
=
match
mx
with
BAnon
=>
X

BNamed
x
=>
x
::
X
end
.
match
b
with
BAnon
=>
ss

BNamed
s
=>
s
::
ss
end
.
Infix
":b:"
:
=
cons_binder
(
at
level
60
,
right
associativity
).
Infix
":b:"
:
=
cons_binder
(
at
level
60
,
right
associativity
).
Fixpoint
app_binder
(
mx
s
:
list
binder
)
(
X
:
list
string
)
:
list
string
:
=
Fixpoint
app_binder
(
b
s
:
list
binder
)
(
ss
:
list
string
)
:
list
string
:
=
match
mx
s
with
[]
=>
X

b
::
mx
s
=>
b
:
b
:
app_binder
mxs
X
end
.
match
b
s
with
[]
=>
ss

b
::
b
s
=>
b
:
b
:
app_binder
bs
ss
end
.
Infix
"+b+"
:
=
app_binder
(
at
level
60
,
right
associativity
).
Infix
"+b+"
:
=
app_binder
(
at
level
60
,
right
associativity
).
Instance
set_unfold_cons_binder
x
mx
X
P
:
Instance
set_unfold_cons_binder
s
b
ss
P
:
SetUnfoldElemOf
x
X
P
→
SetUnfoldElemOf
x
(
mx
:
b
:
X
)
(
BNamed
x
=
mx
∨
P
).
SetUnfoldElemOf
s
ss
P
→
SetUnfoldElemOf
s
(
b
:
b
:
ss
)
(
BNamed
s
=
b
∨
P
).
Proof
.
Proof
.
constructor
.
rewrite
<(
set_unfold
(
x
∈
X
)
P
).
constructor
.
rewrite
<(
set_unfold
(
s
∈
ss
)
P
).
destruct
mx
;
simpl
;
rewrite
?elem_of_cons
;
naive_solver
.
destruct
b
;
simpl
;
rewrite
?elem_of_cons
;
naive_solver
.
Qed
.
Qed
.
Instance
set_unfold_app_binder
x
mxl
X
P
:
Instance
set_unfold_app_binder
s
bs
ss
P
Q
:
SetUnfoldElemOf
x
X
P
→
SetUnfoldElemOf
x
(
mxl
+
b
+
X
)
(
BNamed
x
∈
mxl
∨
P
).
SetUnfoldElemOf
(
BNamed
s
)
bs
P
→
SetUnfoldElemOf
s
ss
Q
→
SetUnfoldElemOf
s
(
bs
+
b
+
ss
)
(
P
∨
Q
).
Proof
.
Proof
.
constructor
.
rewrite
<(
set_unfold
(
x
∈
X
)
P
).
induction
mxl
;
set_solver
.
intros
HinP
HinQ
.
constructor
.
rewrite
<(
set_unfold
(
s
∈
ss
)
Q
),
<(
set_unfold
(
BNamed
s
∈
bs
)
P
).
clear
HinP
HinQ
.
induction
bs
;
set_solver
.
Qed
.
Lemma
app_binder_named
ss1
ss2
:
(
BNamed
<$>
ss1
)
+
b
+
ss2
=
ss1
++
ss2
.
Proof
.
induction
ss1
;
by
f_equal
/=.
Qed
.
Lemma
app_binder_snoc
bs
s
ss
:
bs
+
b
+
(
s
::
ss
)
=
(
bs
++
[
BNamed
s
])
+
b
+
ss
.
Proof
.
induction
bs
;
by
f_equal
/=.
Qed
.
Instance
cons_binder_Permutation
b
:
Proper
((
≡
ₚ
)
==>
(
≡
ₚ
))
(
cons_binder
b
).
Proof
.
intros
ss1
ss2
Hss
.
destruct
b
;
csimpl
;
by
rewrite
Hss
.
Qed
.
Instance
app_binder_Permutation
:
Proper
((
≡
ₚ
)
==>
(
≡
ₚ
)
==>
(
≡
ₚ
))
app_binder
.
Proof
.
assert
(
∀
bs
,
Proper
((
≡
ₚ
)
==>
(
≡
ₚ
))
(
app_binder
bs
)).
{
induction
bs
as
[[]]
;
intros
ss1
ss2
;
simpl
;
by
intros
>.
}
induction
1
as
[[][]
[]]
;
intros
ss1
ss2
Hss
;
simpl
;
first
[
by
eauto
using
perm_trans

by
rewrite
1
?perm_swap
,
Hss
].
Qed
.
Qed
.
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