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
iris-coq
Commits
c6685a3e
Commit
c6685a3e
authored
May 31, 2016
by
Robbert Krebbers
Browse files
Prove that Countable A gives Countable B for an injection B → A.
parent
f7c4ea23
Changes
1
Hide whitespace changes
Inline
Side-by-side
prelude/countable.v
View file @
c6685a3e
...
...
@@ -78,6 +78,16 @@ Proof.
Qed
.
(
**
*
Instances
*
)
(
**
**
Injection
*
)
Section
injective_countable
.
Context
`
{
Countable
A
,
∀
x
y
:
B
,
Decision
(
x
=
y
)
}
.
Context
(
f
:
B
→
A
)
(
g
:
A
→
option
B
)
(
fg
:
∀
x
,
g
(
f
x
)
=
Some
x
).
Program
Instance
injective_countable
:
Countable
B
:=
{|
encode
y
:=
encode
(
f
y
);
decode
p
:=
x
←
decode
p
;
g
x
|}
.
Next
Obligation
.
intros
y
;
simpl
;
rewrite
decode_encode
;
eauto
.
Qed
.
End
injective_countable
.
(
**
**
Option
*
)
Program
Instance
option_countable
`
{
Countable
A
}
:
Countable
(
option
A
)
:=
{|
encode
o
:=
match
o
with
None
=>
1
|
Some
x
=>
Pos
.
succ
(
encode
x
)
end
;
...
...
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