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
Hugo Herbelin
iris-coq
Commits
206fa666
Commit
206fa666
authored
Dec 03, 2018
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Prove `agree_map f (to_agree x) = to_agree (f x)`.
parent
4e3d1c58
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
3 additions
and
0 deletions
+3
-0
theories/algebra/agree.v
theories/algebra/agree.v
+3
-0
No files found.
theories/algebra/agree.v
View file @
206fa666
...
...
@@ -255,6 +255,9 @@ Proof. apply agree_eq. by rewrite /= list_fmap_id. Qed.
Lemma
agree_map_compose
{
A
B
C
}
(
f
:
A
→
B
)
(
g
:
B
→
C
)
(
x
:
agree
A
)
:
agree_map
(
g
∘
f
)
x
=
agree_map
g
(
agree_map
f
x
).
Proof
.
apply
agree_eq
.
by
rewrite
/=
list_fmap_compose
.
Qed
.
Lemma
agree_map_to_agree
{
A
B
}
(
f
:
A
→
B
)
(
x
:
A
)
:
agree_map
f
(
to_agree
x
)
=
to_agree
(
f
x
).
Proof
.
by
apply
agree_eq
.
Qed
.
Section
agree_map
.
Context
{
A
B
:
ofeT
}
(
f
:
A
→
B
)
`
{
Hf
:
NonExpansive
f
}.
...
...
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