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
Iris
Iris
Commits
5027bad5
Commit
5027bad5
authored
Dec 11, 2015
by
Robbert Krebbers
Browse files
More countable stuff.
Also, use a different encoding of lists.
parent
83cfef45
Changes
1
Hide whitespace changes
Inline
Side-by-side
prelude/countable.v
View file @
5027bad5
...
...
@@ -9,6 +9,8 @@ Class Countable A `{∀ x y : A, Decision (x = y)} := {
decode
:
positive
→
option
A
;
decode_encode
x
:
decode
(
encode
x
)
=
Some
x
}.
Arguments
encode
:
simpl
never
.
Arguments
decode
:
simpl
never
.
Definition
encode_nat
`
{
Countable
A
}
(
x
:
A
)
:
nat
:
=
pred
(
Pos
.
to_nat
(
encode
x
)).
...
...
@@ -19,6 +21,8 @@ Proof.
intros
x
y
Hxy
;
apply
(
injective
Some
).
by
rewrite
<-(
decode_encode
x
),
Hxy
,
decode_encode
.
Qed
.
Instance
encode_nat_injective
`
{
Countable
A
}
:
Injective
(=)
(=)
encode_nat
.
Proof
.
unfold
encode_nat
;
intros
x
y
Hxy
;
apply
(
injective
encode
)
;
lia
.
Qed
.
Lemma
decode_encode_nat
`
{
Countable
A
}
x
:
decode_nat
(
encode_nat
x
)
=
Some
x
.
Proof
.
pose
proof
(
Pos2Nat
.
is_pos
(
encode
x
)).
...
...
@@ -26,6 +30,7 @@ Proof.
by
rewrite
Pos2Nat
.
id
,
decode_encode
.
Qed
.
(** * Choice principles *)
Section
choice
.
Context
`
{
Countable
A
}
(
P
:
A
→
Prop
)
`
{
∀
x
,
Decision
(
P
x
)}.
...
...
@@ -33,7 +38,6 @@ Section choice.
|
choose_step_None
{
p
}
:
decode
p
=
None
→
choose_step
(
Psucc
p
)
p
|
choose_step_Some
{
p
x
}
:
decode
p
=
Some
x
→
¬
P
x
→
choose_step
(
Psucc
p
)
p
.
Lemma
choose_step_acc
:
(
∃
x
,
P
x
)
→
Acc
choose_step
1
%
positive
.
Proof
.
intros
[
x
Hx
].
cut
(
∀
i
p
,
...
...
@@ -46,13 +50,11 @@ Section choice.
constructor
.
intros
j
.
inversion
1
as
[?
Hd
|?
y
Hd
]
;
subst
;
auto
with
lia
.
Qed
.
Fixpoint
choose_go
{
i
}
(
acc
:
Acc
choose_step
i
)
:
A
:
=
match
Some_dec
(
decode
i
)
with
|
inleft
(
x
↾
Hx
)
=>
match
decide
(
P
x
)
with
|
left
_
=>
x
|
right
H
=>
choose_go
(
Acc_inv
acc
(
choose_step_Some
Hx
H
))
|
left
_
=>
x
|
right
H
=>
choose_go
(
Acc_inv
acc
(
choose_step_Some
Hx
H
))
end
|
inright
H
=>
choose_go
(
Acc_inv
acc
(
choose_step_None
H
))
end
.
...
...
@@ -76,18 +78,18 @@ Proof.
intros
y
.
by
rewrite
(
choose_correct
(
λ
x
,
f
x
=
y
)
(
surjective
f
y
)).
Qed
.
(** ** Instances *)
(** * Instances *)
(** ** Option *)
Program
Instance
option_countable
`
{
Countable
A
}
:
Countable
(
option
A
)
:
=
{|
encode
o
:
=
match
o
with
None
=>
1
|
Some
x
=>
Pos
.
succ
(
encode
x
)
end
;
decode
p
:
=
if
decide
(
p
=
1
)
then
Some
None
else
Some
<$>
decode
(
Pos
.
pred
p
)
encode
o
:
=
match
o
with
None
=>
1
|
Some
x
=>
Pos
.
succ
(
encode
x
)
end
;
decode
p
:
=
if
decide
(
p
=
1
)
then
Some
None
else
Some
<$>
decode
(
Pos
.
pred
p
)
|}.
Next
Obligation
.
intros
???
[
x
|]
;
simpl
;
repeat
case_decide
;
auto
with
lia
.
by
rewrite
Pos
.
pred_succ
,
decode_encode
.
Qed
.
(** ** Sums *)
Program
Instance
sum_countable
`
{
Countable
A
}
`
{
Countable
B
}
:
Countable
(
A
+
B
)%
type
:
=
{|
encode
xy
:
=
...
...
@@ -99,6 +101,7 @@ Program Instance sum_countable `{Countable A} `{Countable B} :
|}.
Next
Obligation
.
by
intros
??????
[
x
|
y
]
;
simpl
;
rewrite
decode_encode
.
Qed
.
(** ** Products *)
Fixpoint
prod_encode_fst
(
p
:
positive
)
:
positive
:
=
match
p
with
|
1
=>
1
...
...
@@ -162,75 +165,82 @@ Proof.
Qed
.
Program
Instance
prod_countable
`
{
Countable
A
}
`
{
Countable
B
}
:
Countable
(
A
*
B
)%
type
:
=
{|
encode
xy
:
=
let
(
x
,
y
)
:
=
xy
in
prod_encode
(
encode
x
)
(
encode
y
)
;
encode
xy
:
=
prod_encode
(
encode
(
xy
.
1
)
)
(
encode
(
xy
.
2
)
)
;
decode
p
:
=
x
←
prod_decode_fst
p
≫
=
decode
;
y
←
prod_decode_snd
p
≫
=
decode
;
Some
(
x
,
y
)
|}.
Next
Obligation
.
intros
??????
[
x
y
]
;
simpl
.
rewrite
prod_decode_encode_fst
,
prod_decode_encode_snd
.
csimpl
.
by
rewrite
!
decode_encode
.
rewrite
prod_decode_encode_fst
,
prod_decode_encode_snd
;
simpl
.
by
rewrite
!
decode_encode
.
Qed
.
Fixpoint
list_encode_
(
l
:
list
positive
)
:
positive
:
=
match
l
with
[]
=>
1
|
x
::
l
=>
prod_encode
x
(
list_encode_
l
)
end
.
Definition
list_encode
(
l
:
list
positive
)
:
positive
:
=
prod_encode
(
Pos
.
of_nat
(
S
(
length
l
)))
(
list_encode_
l
).
Fixpoint
list_decode_
(
n
:
nat
)
(
p
:
positive
)
:
option
(
list
positive
)
:
=
match
n
with
|
O
=>
guard
(
p
=
1
)
;
Some
[]
|
S
n
=>
x
←
prod_decode_fst
p
;
pl
←
prod_decode_snd
p
;
l
←
list_decode_
n
pl
;
Some
(
x
::
l
)
(** ** Lists *)
(* Lists are encoded as 1 separated sequences of 0s corresponding to the unary
representation of the elements. *)
Fixpoint
list_encode
`
{
Countable
A
}
(
acc
:
positive
)
(
l
:
list
A
)
:
positive
:
=
match
l
with
|
[]
=>
acc
|
x
::
l
=>
list_encode
(
Nat
.
iter
(
encode_nat
x
)
(~
0
)
(
acc
~
1
))
l
end
.
Definition
list_decode
(
p
:
positive
)
:
option
(
list
positive
)
:
=
pn
←
prod_decode_fst
p
;
pl
←
prod_decode_snd
p
;
list_decode_
(
pred
(
Pos
.
to_nat
pn
))
pl
.
Lemma
list_decode_encode
l
:
list_decode
(
list_encode
l
)
=
Some
l
.
Fixpoint
list_decode
`
{
Countable
A
}
(
acc
:
list
A
)
(
n
:
nat
)
(
p
:
positive
)
:
option
(
list
A
)
:
=
match
p
with
|
1
=>
Some
acc
|
p
~
0
=>
list_decode
acc
(
S
n
)
p
|
p
~
1
=>
x
←
decode_nat
n
;
list_decode
(
x
::
acc
)
O
p
end
.
Lemma
x0_iter_x1
n
acc
:
Nat
.
iter
n
(~
0
)
acc
~
1
=
acc
++
Nat
.
iter
n
(~
0
)
3
.
Proof
.
by
induction
n
;
f_equal'
.
Qed
.
Lemma
list_encode_app'
`
{
Countable
A
}
(
l1
l2
:
list
A
)
acc
:
list_encode
acc
(
l1
++
l2
)
=
list_encode
acc
l1
++
list_encode
1
l2
.
Proof
.
cut
(
list_decode_
(
length
l
)
(
list_encode_
l
)
=
Some
l
).
{
intros
help
.
unfold
list_decode
,
list_encode
.
rewrite
prod_decode_encode_fst
,
prod_decode_encode_snd
;
csimpl
.
by
rewrite
Nat2Pos
.
id
by
done
;
simpl
.
}
induction
l
;
simpl
;
auto
.
by
rewrite
prod_decode_encode_fst
,
prod_decode_encode_snd
;
simplify_option_equality
.
revert
acc
;
induction
l1
;
simpl
;
auto
.
induction
l2
as
[|
x
l
IH
]
;
intros
acc
;
simpl
;
[
by
rewrite
?(
left_id_L
_
_
)|].
by
rewrite
!(
IH
(
Nat
.
iter
_
_
_
)),
(
associative_L
_
),
x0_iter_x1
.
Qed
.
Program
Instance
list_countable
`
{
Countable
A
}
:
Countable
(
list
A
)
:
=
{|
encode
l
:
=
list_encode
(
encode
<$>
l
)
;
decode
p
:
=
list_decode
p
≫
=
mapM
decode
|}.
Program
Instance
list_countable
`
{
Countable
A
}
:
Countable
(
list
A
)
:
=
{|
encode
:
=
list_encode
1
;
decode
:
=
list_decode
[]
0
|}.
Next
Obligation
.
intros
???
l
;
simpl
;
rewrite
list_decode_encode
;
simpl
.
apply
mapM_fmap_Some
;
auto
using
decode_encode
.
intros
A
??
;
simpl
.
assert
(
∀
m
acc
n
p
,
list_decode
acc
n
(
Nat
.
iter
m
(~
0
)
p
)
=
list_decode
acc
(
n
+
m
)
p
)
as
decode_iter
.
{
induction
m
as
[|
m
IH
]
;
intros
acc
n
p
;
simpl
;
[
by
rewrite
Nat
.
add_0_r
|].
by
rewrite
IH
,
Nat
.
add_succ_r
.
}
cut
(
∀
l
acc
,
list_decode
acc
0
(
list_encode
1
l
)
=
Some
(
l
++
acc
))%
list
.
{
by
intros
help
l
;
rewrite
help
,
(
right_id_L
_
_
).
}
induction
l
as
[|
x
l
IH
]
using
@
rev_ind
;
intros
acc
;
[
done
|].
rewrite
list_encode_app'
;
simpl
;
rewrite
<-
x0_iter_x1
,
decode_iter
;
simpl
.
by
rewrite
decode_encode_nat
;
simpl
;
rewrite
IH
,
<-(
associative_L
_
).
Qed
.
Program
Instance
pos_countable
:
Countable
positive
:
=
{|
encode
:
=
id
;
decode
:
=
Some
;
decode_encode
x
:
=
eq_refl
|}.
Lemma
list_encode_app
`
{
Countable
A
}
(
l1
l2
:
list
A
)
:
encode
(
l1
++
l2
)%
list
=
encode
l1
++
encode
l2
.
Proof
.
apply
list_encode_app'
.
Qed
.
Lemma
list_encode_cons
`
{
Countable
A
}
x
(
l
:
list
A
)
:
encode
(
x
::
l
)
=
Nat
.
iter
(
encode_nat
x
)
(~
0
)
3
++
encode
l
.
Proof
.
apply
(
list_encode_app'
[
_
]).
Qed
.
Lemma
list_encode_suffix
`
{
Countable
A
}
(
l
k
:
list
A
)
:
l
`
suffix_of
`
k
→
∃
q
,
encode
k
=
q
++
encode
l
.
Proof
.
intros
[
l'
->]
;
exists
(
encode
l'
)
;
apply
list_encode_app
.
Qed
.
(** ** Numbers *)
Instance
pos_countable
:
Countable
positive
:
=
{|
encode
:
=
id
;
decode
:
=
Some
;
decode_encode
x
:
=
eq_refl
|}.
Program
Instance
N_countable
:
Countable
N
:
=
{|
encode
x
:
=
match
x
with
N0
=>
1
|
Npos
p
=>
Pos
.
succ
p
end
;
decode
p
:
=
if
decide
(
p
=
1
)
then
Some
0
%
N
else
Some
(
Npos
(
Pos
.
pred
p
))
|}.
Next
Obligation
.
intros
[|
p
]
;
simpl
;
repeat
case_decide
;
auto
with
lia
.
by
rewrite
Pos
.
pred_succ
.
by
intros
[|
p
]
;
simpl
;
[|
rewrite
decide_False
,
Pos
.
pred_succ
by
(
by
destruct
p
)].
Qed
.
Program
Instance
Z_countable
:
Countable
Z
:
=
{|
encode
x
:
=
match
x
with
Z0
=>
1
|
Zpos
p
=>
p
~
0
|
Zneg
p
=>
p
~
1
end
;
decode
p
:
=
Some
match
p
with
1
=>
Z0
|
p
~
0
=>
Zpos
p
|
p
~
1
=>
Zneg
p
end
encode
x
:
=
match
x
with
Z0
=>
1
|
Zpos
p
=>
p
~
0
|
Zneg
p
=>
p
~
1
end
;
decode
p
:
=
Some
match
p
with
1
=>
Z0
|
p
~
0
=>
Zpos
p
|
p
~
1
=>
Zneg
p
end
|}.
Next
Obligation
.
by
intros
[|
p
|
p
].
Qed
.
Program
Instance
nat_countable
:
Countable
nat
:
=
{|
encode
x
:
=
encode
(
N
.
of_nat
x
)
;
decode
p
:
=
N
.
to_nat
<$>
decode
p
|}.
Program
Instance
nat_countable
:
Countable
nat
:
=
{|
encode
x
:
=
encode
(
N
.
of_nat
x
)
;
decode
p
:
=
N
.
to_nat
<$>
decode
p
|}.
Next
Obligation
.
intros
x
;
lazy
beta
;
rewrite
decode_encode
;
csimpl
.
by
rewrite
Nat2N
.
id
.
by
intros
x
;
lazy
beta
;
rewrite
decode_encode
;
csimpl
;
rewrite
Nat2N
.
id
.
Qed
.
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