Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Tej Chajed
stdpp
Commits
575f23a9
Commit
575f23a9
authored
Dec 09, 2016
by
Ralf Jung
Browse files
rename _setoid suffix to _equiv; add variant of fmap_Some_setoid that can be usefully destructed
parent
a4fe5037
Changes
3
Hide whitespace changes
Inline
Side-by-side
theories/fin_maps.v
View file @
575f23a9
...
...
@@ -556,7 +556,7 @@ Proof. apply map_eq; intros i; by rewrite lookup_fmap, option_fmap_id. Qed.
Lemma
map_fmap_compose
{
A
B
C
}
(
f
:
A
→
B
)
(
g
:
B
→
C
)
(
m
:
M
A
)
:
g
∘
f
<$>
m
=
g
<$>
f
<$>
m
.
Proof
.
apply
map_eq
;
intros
i
;
by
rewrite
!
lookup_fmap
,
option_fmap_compose
.
Qed
.
Lemma
map_fmap_
setoid
_ext
`
{
Equiv
A
,
Equiv
B
}
(
f1
f2
:
A
→
B
)
m
:
Lemma
map_fmap_
equiv
_ext
`
{
Equiv
A
,
Equiv
B
}
(
f1
f2
:
A
→
B
)
m
:
(
∀
i
x
,
m
!!
i
=
Some
x
→
f1
x
≡
f2
x
)
→
f1
<$>
m
≡
f2
<$>
m
.
Proof
.
intros
Hi
i
;
rewrite
!
lookup_fmap
.
...
...
theories/list.v
View file @
575f23a9
...
...
@@ -2802,7 +2802,7 @@ Section fmap.
Lemma
list_fmap_ext
(
g
:
A
→
B
)
(
l1
l2
:
list
A
)
:
(
∀
x
,
f
x
=
g
x
)
→
l1
=
l2
→
fmap
f
l1
=
fmap
g
l2
.
Proof
.
intros
?
<-.
induction
l1
;
f_equal
/=
;
auto
.
Qed
.
Lemma
list_fmap_
setoid
_ext
`
{
Equiv
B
}
(
g
:
A
→
B
)
l
:
Lemma
list_fmap_
equiv
_ext
`
{
Equiv
B
}
(
g
:
A
→
B
)
l
:
(
∀
x
,
f
x
≡
g
x
)
→
f
<$>
l
≡
g
<$>
l
.
Proof
.
induction
l
;
constructor
;
auto
.
Qed
.
...
...
theories/option.v
View file @
575f23a9
...
...
@@ -180,7 +180,7 @@ Proof. unfold is_Some; destruct mx; naive_solver. Qed.
Lemma
fmap_Some
{
A
B
}
(
f
:
A
→
B
)
mx
y
:
f
<$>
mx
=
Some
y
↔
∃
x
,
mx
=
Some
x
∧
y
=
f
x
.
Proof
.
destruct
mx
;
naive_solver
.
Qed
.
Lemma
fmap_Some_
setoid
{
A
B
}
`
{
Equiv
B
}
`
{!
Equivalence
((
≡
)
:
relation
B
)}
Lemma
fmap_Some_
equiv
{
A
B
}
`
{
Equiv
B
}
`
{!
Equivalence
((
≡
)
:
relation
B
)}
(
f
:
A
→
B
)
mx
y
:
f
<$>
mx
≡
Some
y
↔
∃
x
,
mx
=
Some
x
∧
y
≡
f
x
.
Proof
.
...
...
@@ -190,6 +190,10 @@ Proof.
-
intros
?%
symmetry
%
equiv_None
.
done
.
-
intros
(?
&
?
&
?).
done
.
Qed
.
Lemma
fmap_Some_equiv'
{
A
B
}
`
{
Equiv
B
}
`
{!
Equivalence
((
≡
)
:
relation
B
)}
(
f
:
A
→
B
)
mx
y
:
f
<$>
mx
≡
Some
y
→
∃
x
,
mx
=
Some
x
∧
y
≡
f
x
.
Proof
.
intros
.
apply
fmap_Some_equiv
.
done
.
Qed
.
Lemma
fmap_None
{
A
B
}
(
f
:
A
→
B
)
mx
:
f
<$>
mx
=
None
↔
mx
=
None
.
Proof
.
by
destruct
mx
.
Qed
.
Lemma
option_fmap_id
{
A
}
(
mx
:
option
A
)
:
id
<$>
mx
=
mx
.
...
...
@@ -200,7 +204,7 @@ Proof. by destruct mx. Qed.
Lemma
option_fmap_ext
{
A
B
}
(
f
g
:
A
→
B
)
mx
:
(
∀
x
,
f
x
=
g
x
)
→
f
<$>
mx
=
g
<$>
mx
.
Proof
.
intros
;
destruct
mx
;
f_equal
/=
;
auto
.
Qed
.
Lemma
option_fmap_
setoid
_ext
`
{
Equiv
A
,
Equiv
B
}
(
f
g
:
A
→
B
)
mx
:
Lemma
option_fmap_
equiv
_ext
`
{
Equiv
A
,
Equiv
B
}
(
f
g
:
A
→
B
)
mx
:
(
∀
x
,
f
x
≡
g
x
)
→
f
<$>
mx
≡
g
<$>
mx
.
Proof
.
destruct
mx
;
constructor
;
auto
.
Qed
.
Lemma
option_fmap_bind
{
A
B
C
}
(
f
:
A
→
B
)
(
g
:
B
→
option
C
)
mx
:
...
...
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