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
Matthieu Sozeau
stdpp
Commits
5e3d8b90
Commit
5e3d8b90
authored
Jun 03, 2021
by
Robbert Krebbers
Browse files
More missing `Hint Mode`s.
parent
8542ca97
Changes
8
Hide whitespace changes
Inline
Side-by-side
theories/base.v
View file @
5e3d8b90
...
...
@@ -460,14 +460,18 @@ Proof. auto. Qed.
relation [R] instead of [⊆] to support multiple orders on the same type. *)
Definition
strict
{
A
}
(
R
:
relation
A
)
:
relation
A
:
=
λ
X
Y
,
R
X
Y
∧
¬
R
Y
X
.
Global
Instance
:
Params
(@
strict
)
2
:
=
{}.
Class
PartialOrder
{
A
}
(
R
:
relation
A
)
:
Prop
:
=
{
partial_order_pre
:
>
PreOrder
R
;
partial_order_anti_symm
:
>
AntiSymm
(=)
R
}.
Global
Hint
Mode
PartialOrder
!
+
:
typeclass_instances
.
Class
TotalOrder
{
A
}
(
R
:
relation
A
)
:
Prop
:
=
{
total_order_partial
:
>
PartialOrder
R
;
total_order_trichotomy
:
>
Trichotomy
(
strict
R
)
}.
Global
Hint
Mode
TotalOrder
!
+
:
typeclass_instances
.
(** * Logic *)
Global
Instance
prop_inhabited
:
Inhabited
Prop
:
=
populate
True
.
...
...
@@ -1007,18 +1011,27 @@ class with the monad laws). *)
Class
MRet
(
M
:
Type
→
Type
)
:
=
mret
:
∀
{
A
},
A
→
M
A
.
Global
Arguments
mret
{
_
_
_
}
_
:
assert
.
Global
Instance
:
Params
(@
mret
)
3
:
=
{}.
Global
Hint
Mode
MRet
!
:
typeclass_instances
.
Class
MBind
(
M
:
Type
→
Type
)
:
=
mbind
:
∀
{
A
B
},
(
A
→
M
B
)
→
M
A
→
M
B
.
Global
Arguments
mbind
{
_
_
_
_
}
_
!
_
/
:
assert
.
Global
Instance
:
Params
(@
mbind
)
4
:
=
{}.
Global
Hint
Mode
MBind
!
:
typeclass_instances
.
Class
MJoin
(
M
:
Type
→
Type
)
:
=
mjoin
:
∀
{
A
},
M
(
M
A
)
→
M
A
.
Global
Arguments
mjoin
{
_
_
_
}
!
_
/
:
assert
.
Global
Instance
:
Params
(@
mjoin
)
3
:
=
{}.
Global
Hint
Mode
MJoin
!
:
typeclass_instances
.
Class
FMap
(
M
:
Type
→
Type
)
:
=
fmap
:
∀
{
A
B
},
(
A
→
B
)
→
M
A
→
M
B
.
Global
Arguments
fmap
{
_
_
_
_
}
_
!
_
/
:
assert
.
Global
Instance
:
Params
(@
fmap
)
4
:
=
{}.
Global
Hint
Mode
FMap
!
:
typeclass_instances
.
Class
OMap
(
M
:
Type
→
Type
)
:
=
omap
:
∀
{
A
B
},
(
A
→
option
B
)
→
M
A
→
M
B
.
Global
Arguments
omap
{
_
_
_
_
}
_
!
_
/
:
assert
.
Global
Instance
:
Params
(@
omap
)
4
:
=
{}.
Global
Hint
Mode
OMap
!
:
typeclass_instances
.
Notation
"m ≫= f"
:
=
(
mbind
f
m
)
(
at
level
60
,
right
associativity
)
:
stdpp_scope
.
Notation
"( m ≫=.)"
:
=
(
λ
f
,
mbind
f
m
)
(
only
parsing
)
:
stdpp_scope
.
...
...
@@ -1044,6 +1057,7 @@ Notation "ps .*2" := (fmap (M:=list) snd ps)
Class
MGuard
(
M
:
Type
→
Type
)
:
=
mguard
:
∀
P
{
dec
:
Decision
P
}
{
A
},
(
P
→
M
A
)
→
M
A
.
Global
Arguments
mguard
_
_
_
!
_
_
_
/
:
assert
.
Global
Hint
Mode
MGuard
!
:
typeclass_instances
.
Notation
"'guard' P ; z"
:
=
(
mguard
P
(
λ
_
,
z
))
(
at
level
20
,
z
at
level
200
,
only
parsing
,
right
associativity
)
:
stdpp_scope
.
Notation
"'guard' P 'as' H ; z"
:
=
(
mguard
P
(
λ
H
,
z
))
...
...
@@ -1283,18 +1297,23 @@ Class SemiSet A C `{ElemOf A C,
elem_of_singleton
(
x
y
:
A
)
:
x
∈
@{
C
}
{[
y
]}
↔
x
=
y
;
elem_of_union
(
X
Y
:
C
)
(
x
:
A
)
:
x
∈
X
∪
Y
↔
x
∈
X
∨
x
∈
Y
}.
Global
Hint
Mode
SemiSet
-
!
-
-
-
-
:
typeclass_instances
.
Class
Set_
A
C
`
{
ElemOf
A
C
,
Empty
C
,
Singleton
A
C
,
Union
C
,
Intersection
C
,
Difference
C
}
:
Prop
:
=
{
set_semi_set
:
>
SemiSet
A
C
;
elem_of_intersection
(
X
Y
:
C
)
(
x
:
A
)
:
x
∈
X
∩
Y
↔
x
∈
X
∧
x
∈
Y
;
elem_of_difference
(
X
Y
:
C
)
(
x
:
A
)
:
x
∈
X
∖
Y
↔
x
∈
X
∧
x
∉
Y
}.
Global
Hint
Mode
Set_
-
!
-
-
-
-
-
-
:
typeclass_instances
.
Class
TopSet
A
C
`
{
ElemOf
A
C
,
Empty
C
,
Top
C
,
Singleton
A
C
,
Union
C
,
Intersection
C
,
Difference
C
}
:
Prop
:
=
{
top_set_set
:
>
Set_
A
C
;
elem_of_top'
(
x
:
A
)
:
x
∈
@{
C
}
⊤;
(* We prove [elem_of_top : x ∈@{C} ⊤ ↔ True]
in [sets.v], which is more convenient for rewriting. *)
}.
Global
Hint
Mode
TopSet
-
!
-
-
-
-
-
-
-
:
typeclass_instances
.
(** We axiomative a finite set as a set whose elements can be
enumerated as a list. These elements, given by the [elements] function, may be
...
...
@@ -1386,6 +1405,7 @@ Class Infinite A := {
infinite_is_fresh
(
xs
:
list
A
)
:
fresh
xs
∉
xs
;
infinite_fresh_Permutation
:
>
Proper
(@
Permutation
A
==>
(=))
fresh
;
}.
Global
Hint
Mode
Infinite
!
:
typeclass_instances
.
Global
Arguments
infinite_fresh
:
simpl
never
.
(** * Miscellaneous *)
...
...
theories/coGset.v
View file @
5e3d8b90
...
...
@@ -138,7 +138,7 @@ End infinite.
Definition
coGpick
`
{
Countable
A
,
Infinite
A
}
(
X
:
coGset
A
)
:
A
:
=
fresh
(
match
X
with
FinGSet
_
=>
∅
|
CoFinGset
X
=>
X
end
).
Lemma
coGpick_elem_of
`
{
Countable
A
,
Infinite
A
}
X
:
Lemma
coGpick_elem_of
`
{
Countable
A
,
Infinite
A
}
(
X
:
coGset
A
)
:
¬
set_finite
X
→
coGpick
X
∈
X
.
Proof
.
unfold
coGpick
.
...
...
theories/fin_maps.v
View file @
5e3d8b90
...
...
@@ -316,7 +316,7 @@ Proof.
destruct
(
decide
(
Exists
(
λ
ix
,
m1
!!
ix
.
1
=
None
)
(
map_to_list
m2
)))
as
[[[
i
x
]
[?%
elem_of_map_to_list
?]]%
Exists_exists
|
Hm
%(
not_Exists_Forall
_
)]
;
[
eauto
|].
destruct
Heq
;
apply
(
anti_symm
_
),
map_subseteq_spec
;
[
done
|
intros
i
x
Hi
].
destruct
Heq
;
apply
(
anti_symm
(
⊆
)
),
map_subseteq_spec
;
[
done
|
intros
i
x
Hi
].
assert
(
is_Some
(
m1
!!
i
))
as
[
x'
?].
{
by
apply
not_eq_None_Some
,
(
proj1
(
Forall_forall
_
_
)
Hm
(
i
,
x
)),
elem_of_map_to_list
.
}
...
...
@@ -689,24 +689,25 @@ Lemma lookup_omap_id_Some {A} (m : M (option A)) i x :
omap
id
m
!!
i
=
Some
x
↔
m
!!
i
=
Some
(
Some
x
).
Proof
.
rewrite
lookup_omap_Some
.
naive_solver
.
Qed
.
Lemma
fmap_empty
{
A
B
}
(
f
:
A
→
B
)
:
f
<$>
∅
=
∅
.
Lemma
fmap_empty
{
A
B
}
(
f
:
A
→
B
)
:
f
<$>
∅
=
@{
M
B
}
∅
.
Proof
.
apply
map_empty
;
intros
i
.
by
rewrite
lookup_fmap
,
lookup_empty
.
Qed
.
Lemma
omap_empty
{
A
B
}
(
f
:
A
→
option
B
)
:
omap
f
∅
=
∅
.
Lemma
omap_empty
{
A
B
}
(
f
:
A
→
option
B
)
:
omap
f
∅
=
@{
M
B
}
∅
.
Proof
.
apply
map_empty
;
intros
i
.
by
rewrite
lookup_omap
,
lookup_empty
.
Qed
.
Lemma
fmap_empty_inv
{
A
B
}
(
f
:
A
→
B
)
m
:
f
<$>
m
=
∅
→
m
=
∅
.
Lemma
fmap_empty_inv
{
A
B
}
(
f
:
A
→
B
)
m
:
f
<$>
m
=
@{
M
B
}
∅
→
m
=
∅
.
Proof
.
intros
Hm
.
apply
map_eq
;
intros
i
.
generalize
(
f_equal
(
lookup
i
)
Hm
).
by
rewrite
lookup_fmap
,
!
lookup_empty
,
fmap_None
.
Qed
.
Lemma
fmap_insert
{
A
B
}
(
f
:
A
→
B
)
m
i
x
:
f
<$>
<[
i
:
=
x
]>
m
=
<[
i
:
=
f
x
]>(
f
<$>
m
).
Lemma
fmap_insert
{
A
B
}
(
f
:
A
→
B
)
(
m
:
M
A
)
i
x
:
f
<$>
<[
i
:
=
x
]>
m
=
<[
i
:
=
f
x
]>(
f
<$>
m
).
Proof
.
apply
map_eq
;
intros
i'
;
destruct
(
decide
(
i'
=
i
))
as
[->|].
-
by
rewrite
lookup_fmap
,
!
lookup_insert
.
-
by
rewrite
lookup_fmap
,
!
lookup_insert_ne
,
lookup_fmap
by
done
.
Qed
.
Lemma
omap_insert
{
A
B
}
(
f
:
A
→
option
B
)
m
i
x
:
Lemma
omap_insert
{
A
B
}
(
f
:
A
→
option
B
)
(
m
:
M
A
)
i
x
:
omap
f
(<[
i
:
=
x
]>
m
)
=
(
match
f
x
with
Some
y
=>
<[
i
:
=
y
]>
|
None
=>
delete
i
end
)
(
omap
f
m
).
Proof
.
...
...
@@ -719,20 +720,21 @@ Proof.
+
by
rewrite
lookup_insert_ne
,
lookup_omap
by
done
.
+
by
rewrite
lookup_delete_ne
,
lookup_omap
by
done
.
Qed
.
Lemma
omap_insert_Some
{
A
B
}
(
f
:
A
→
option
B
)
m
i
x
y
:
Lemma
omap_insert_Some
{
A
B
}
(
f
:
A
→
option
B
)
(
m
:
M
A
)
i
x
y
:
f
x
=
Some
y
→
omap
f
(<[
i
:
=
x
]>
m
)
=
<[
i
:
=
y
]>(
omap
f
m
).
Proof
.
intros
Hx
.
by
rewrite
omap_insert
,
Hx
.
Qed
.
Lemma
omap_insert_None
{
A
B
}
(
f
:
A
→
option
B
)
m
i
x
:
Lemma
omap_insert_None
{
A
B
}
(
f
:
A
→
option
B
)
(
m
:
M
A
)
i
x
:
f
x
=
None
→
omap
f
(<[
i
:
=
x
]>
m
)
=
delete
i
(
omap
f
m
).
Proof
.
intros
Hx
.
by
rewrite
omap_insert
,
Hx
.
Qed
.
Lemma
fmap_delete
{
A
B
}
(
f
:
A
→
B
)
m
i
:
f
<$>
delete
i
m
=
delete
i
(
f
<$>
m
).
Lemma
fmap_delete
{
A
B
}
(
f
:
A
→
B
)
(
m
:
M
A
)
i
:
f
<$>
delete
i
m
=
delete
i
(
f
<$>
m
).
Proof
.
apply
map_eq
;
intros
i'
;
destruct
(
decide
(
i'
=
i
))
as
[->|].
-
by
rewrite
lookup_fmap
,
!
lookup_delete
.
-
by
rewrite
lookup_fmap
,
!
lookup_delete_ne
,
lookup_fmap
by
done
.
Qed
.
Lemma
omap_delete
{
A
B
}
(
f
:
A
→
option
B
)
m
i
:
Lemma
omap_delete
{
A
B
}
(
f
:
A
→
option
B
)
(
m
:
M
A
)
i
:
omap
f
(
delete
i
m
)
=
delete
i
(
omap
f
m
).
Proof
.
apply
map_eq
;
intros
i'
;
destruct
(
decide
(
i'
=
i
))
as
[->|].
...
...
@@ -740,22 +742,23 @@ Proof.
-
by
rewrite
lookup_omap
,
!
lookup_delete_ne
,
lookup_omap
by
done
.
Qed
.
Lemma
map_fmap_singleton
{
A
B
}
(
f
:
A
→
B
)
i
x
:
f
<$>
{[
i
:
=
x
]}
=
{[
i
:
=
f
x
]}.
Lemma
map_fmap_singleton
{
A
B
}
(
f
:
A
→
B
)
i
x
:
f
<$>
{[
i
:
=
x
]}
=@{
M
B
}
{[
i
:
=
f
x
]}.
Proof
.
by
unfold
singletonM
,
map_singleton
;
rewrite
fmap_insert
,
fmap_empty
.
Qed
.
Lemma
omap_singleton
{
A
B
}
(
f
:
A
→
option
B
)
i
x
:
omap
f
{[
i
:
=
x
]}
=
match
f
x
with
Some
y
=>
{[
i
:
=
y
]}
|
None
=>
∅
end
.
omap
f
{[
i
:
=
x
]}
=
@{
M
B
}
match
f
x
with
Some
y
=>
{[
i
:
=
y
]}
|
None
=>
∅
end
.
Proof
.
rewrite
<-
insert_empty
,
omap_insert
,
omap_empty
.
destruct
(
f
x
)
as
[
y
|]
;
simpl
.
-
by
rewrite
insert_empty
.
-
by
rewrite
delete_empty
.
Qed
.
Lemma
omap_singleton_Some
{
A
B
}
(
f
:
A
→
option
B
)
i
x
y
:
f
x
=
Some
y
→
omap
f
{[
i
:
=
x
]}
=
{[
i
:
=
y
]}.
f
x
=
Some
y
→
omap
f
{[
i
:
=
x
]}
=
@{
M
B
}
{[
i
:
=
y
]}.
Proof
.
intros
Hx
.
by
rewrite
omap_singleton
,
Hx
.
Qed
.
Lemma
omap_singleton_None
{
A
B
}
(
f
:
A
→
option
B
)
i
x
:
f
x
=
None
→
omap
f
{[
i
:
=
x
]}
=
∅
.
f
x
=
None
→
omap
f
{[
i
:
=
x
]}
=
@{
M
B
}
∅
.
Proof
.
intros
Hx
.
by
rewrite
omap_singleton
,
Hx
.
Qed
.
Lemma
map_fmap_id
{
A
}
(
m
:
M
A
)
:
id
<$>
m
=
m
.
...
...
@@ -1608,14 +1611,14 @@ Section more_merge.
<[
i
:
=
x
]>(
merge
f
m1
m2
)
=
merge
f
m1
(<[
i
:
=
z
]>
m2
).
Proof
.
by
intros
;
apply
partial_alter_merge_r
.
Qed
.
Lemma
fmap_merge
{
D
}
(
g
:
C
→
D
)
m1
m2
:
Lemma
fmap_merge
{
D
}
(
g
:
C
→
D
)
(
m1
:
M
A
)
(
m2
:
M
B
)
:
g
<$>
merge
f
m1
m2
=
merge
(
λ
mx1
mx2
,
g
<$>
f
mx1
mx2
)
m1
m2
.
Proof
.
assert
(
DiagNone
(
λ
mx1
mx2
,
g
<$>
f
mx1
mx2
)).
{
unfold
DiagNone
.
by
rewrite
diag_none
.
}
apply
map_eq
;
intros
i
.
by
rewrite
lookup_fmap
,
!
lookup_merge
by
done
.
Qed
.
Lemma
omap_merge
{
D
}
(
g
:
C
→
option
D
)
m1
m2
:
Lemma
omap_merge
{
D
}
(
g
:
C
→
option
D
)
(
m1
:
M
A
)
(
m2
:
M
B
)
:
omap
g
(
merge
f
m1
m2
)
=
merge
(
λ
mx1
mx2
,
f
mx1
mx2
≫
=
g
)
m1
m2
.
Proof
.
assert
(
DiagNone
(
λ
mx1
mx2
,
f
mx1
mx2
≫
=
g
)).
...
...
@@ -1682,7 +1685,8 @@ Proof.
rewrite
<-
(
map_fmap_id
m1
)
at
1
.
by
rewrite
map_zip_with_fmap
.
Qed
.
Lemma
map_fmap_zip_with
{
A
B
C
D
}
(
f
:
A
→
B
→
C
)
(
g
:
C
→
D
)
m1
m2
:
Lemma
map_fmap_zip_with
{
A
B
C
D
}
(
f
:
A
→
B
→
C
)
(
g
:
C
→
D
)
(
m1
:
M
A
)
(
m2
:
M
B
)
:
g
<$>
map_zip_with
f
m1
m2
=
map_zip_with
(
λ
x
y
,
g
(
f
x
y
))
m1
m2
.
Proof
.
apply
map_eq
;
intro
i
.
rewrite
lookup_fmap
,
!
map_lookup_zip_with
.
...
...
@@ -2533,7 +2537,7 @@ Section map_seq.
Qed
.
Lemma
fmap_map_seq
{
B
}
(
f
:
A
→
B
)
start
xs
:
f
<$>
map_seq
start
xs
=
map_seq
start
(
f
<$>
xs
).
f
<$>
map_seq
start
xs
=
@{
M
B
}
map_seq
start
(
f
<$>
xs
).
Proof
.
revert
start
.
induction
xs
as
[|
x
xs
IH
]
;
intros
start
;
csimpl
.
{
by
rewrite
fmap_empty
.
}
...
...
theories/list.v
View file @
5e3d8b90
...
...
@@ -3558,7 +3558,7 @@ Section fmap.
Proper
((
≡
)
==>
(
≡
))
f
→
Proper
((
≡
)
==>
(
≡
))
(
fmap
f
).
Proof
.
induction
2
;
simpl
;
[
constructor
|
solve_proper
].
Qed
.
Global
Instance
fmap_inj
:
Inj
(=)
(=)
f
→
Inj
(=)
(=)
(
fmap
f
).
Global
Instance
fmap_inj
:
Inj
(=)
(=)
f
→
Inj
(=
@{
list
A
}
)
(=)
(
fmap
f
).
Proof
.
intros
?
l1
.
induction
l1
as
[|
x
l1
IH
]
;
[
by
intros
[|??]|].
intros
[|??]
;
intros
;
f_equal
/=
;
simplify_eq
;
auto
.
...
...
theories/natmap.v
View file @
5e3d8b90
...
...
@@ -190,7 +190,7 @@ Global Instance natmap_to_list {A} : FinMapToList nat A (natmap A) := λ m,
let
(
l
,
_
)
:
=
m
in
natmap_to_list_raw
0
l
.
Definition
natmap_map_raw
{
A
B
}
(
f
:
A
→
B
)
:
natmap_raw
A
→
natmap_raw
B
:
=
fmap
(
fmap
f
).
fmap
(
fmap
(
M
:
=
option
)
f
).
Lemma
natmap_map_wf
{
A
B
}
(
f
:
A
→
B
)
l
:
natmap_wf
l
→
natmap_wf
(
natmap_map_raw
f
l
).
Proof
.
...
...
theories/numbers.v
View file @
5e3d8b90
...
...
@@ -853,7 +853,7 @@ Global Instance Qp_mul_inj_r p : Inj (=) (=) (Qp_mul p).
Proof
.
destruct
p
as
[
p
?].
intros
[
q1
?]
[
q2
?].
rewrite
<-!
Qp_to_Qc_inj_iff
;
simpl
.
intros
Hpq
.
apply
(
anti_symm
_
)
;
apply
(
Qcmult_le_mono_pos_l
_
_
p
)
;
by
rewrite
?Hpq
.
apply
(
anti_symm
Qcle
)
;
apply
(
Qcmult_le_mono_pos_l
_
_
p
)
;
by
rewrite
?Hpq
.
Qed
.
Global
Instance
Qp_mul_inj_l
p
:
Inj
(=)
(=)
(
λ
q
,
q
*
p
).
Proof
.
...
...
theories/option.v
View file @
5e3d8b90
...
...
@@ -205,10 +205,10 @@ 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
.
Proof
.
by
destruct
mx
.
Qed
.
Lemma
option_fmap_compose
{
A
B
}
(
f
:
A
→
B
)
{
C
}
(
g
:
B
→
C
)
mx
:
Lemma
option_fmap_compose
{
A
B
}
(
f
:
A
→
B
)
{
C
}
(
g
:
B
→
C
)
(
mx
:
option
A
)
:
g
∘
f
<$>
mx
=
g
<$>
(
f
<$>
mx
).
Proof
.
by
destruct
mx
.
Qed
.
Lemma
option_fmap_ext
{
A
B
}
(
f
g
:
A
→
B
)
mx
:
Lemma
option_fmap_ext
{
A
B
}
(
f
g
:
A
→
B
)
(
mx
:
option
A
)
:
(
∀
x
,
f
x
=
g
x
)
→
f
<$>
mx
=
g
<$>
mx
.
Proof
.
intros
;
destruct
mx
;
f_equal
/=
;
auto
.
Qed
.
Lemma
option_fmap_equiv_ext
{
A
}
`
{
Equiv
B
}
(
f
g
:
A
→
B
)
(
mx
:
option
A
)
:
...
...
theories/orders.v
View file @
5e3d8b90
...
...
@@ -13,7 +13,7 @@ Section orders.
Lemma
reflexive_eq
`
{!
Reflexive
R
}
X
Y
:
X
=
Y
→
X
⊆
Y
.
Proof
.
by
intros
<-.
Qed
.
Lemma
anti_symm_iff
`
{!
PartialOrder
R
}
X
Y
:
X
=
Y
↔
R
X
Y
∧
R
Y
X
.
Proof
.
split
;
[
by
intros
->|].
by
intros
[??]
;
apply
(
anti_symm
_
).
Qed
.
Proof
.
split
;
[
by
intros
->|].
by
intros
[??]
;
apply
(
anti_symm
R
).
Qed
.
Lemma
strict_spec
X
Y
:
X
⊂
Y
↔
X
⊆
Y
∧
Y
⊈
X
.
Proof
.
done
.
Qed
.
Lemma
strict_include
X
Y
:
X
⊂
Y
→
X
⊆
Y
.
...
...
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