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
Simon Spies
stdpp
Commits
7514c591
Unverified
Commit
7514c591
authored
Jan 24, 2019
by
Maxime Dénès
Browse files
Make trivial instances explicit
This is in preparation for coq/coq#9274.
parent
48758ab8
Changes
4
Hide whitespace changes
Inline
Side-by-side
theories/base.v
View file @
7514c591
...
...
@@ -241,12 +241,12 @@ Definition equivL {A} : Equiv A := (=).
(** A [Params f n] instance forces the setoid rewriting mechanism not to
rewrite in the first [n] arguments of the function [f]. We will declare such
instances for all operational type classes in this development. *)
Instance
:
Params
(@
equiv
)
2
.
Instance
:
Params
(@
equiv
)
2
:
=
{}
.
(** The following instance forces [setoid_replace] to use setoid equality
(for types that have an [Equiv] instance) rather than the standard Leibniz
equality. *)
Instance
equiv_default_relation
`
{
Equiv
A
}
:
DefaultRelation
(
≡
)
|
3
.
Instance
equiv_default_relation
`
{
Equiv
A
}
:
DefaultRelation
(
≡
)
|
3
:
=
{}
.
Hint
Extern
0
(
_
≡
_
)
=>
reflexivity
:
core
.
Hint
Extern
0
(
_
≡
_
)
=>
symmetry
;
assumption
:
core
.
...
...
@@ -396,7 +396,7 @@ Proof. auto. Qed.
(** The classes [PreOrder], [PartialOrder], and [TotalOrder] use an arbitrary
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
.
Instance
:
Params
(@
strict
)
2
.
Instance
:
Params
(@
strict
)
2
:
=
{}
.
Class
PartialOrder
{
A
}
(
R
:
relation
A
)
:
Prop
:
=
{
partial_order_pre
:
>
PreOrder
R
;
partial_order_anti_symm
:
>
AntiSymm
(=)
R
...
...
@@ -592,9 +592,9 @@ Notation "(, y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
Notation
"p .1"
:
=
(
fst
p
)
(
at
level
2
,
left
associativity
,
format
"p .1"
).
Notation
"p .2"
:
=
(
snd
p
)
(
at
level
2
,
left
associativity
,
format
"p .2"
).
Instance
:
Params
(@
pair
)
2
.
Instance
:
Params
(@
fst
)
2
.
Instance
:
Params
(@
snd
)
2
.
Instance
:
Params
(@
pair
)
2
:
=
{}
.
Instance
:
Params
(@
fst
)
2
:
=
{}
.
Instance
:
Params
(@
snd
)
2
:
=
{}
.
Notation
curry
:
=
prod_curry
.
Notation
uncurry
:
=
prod_uncurry
.
...
...
@@ -766,7 +766,7 @@ Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
Class
Union
A
:
=
union
:
A
→
A
→
A
.
Hint
Mode
Union
!
:
typeclass_instances
.
Instance
:
Params
(@
union
)
2
.
Instance
:
Params
(@
union
)
2
:
=
{}
.
Infix
"∪"
:
=
union
(
at
level
50
,
left
associativity
)
:
stdpp_scope
.
Notation
"(∪)"
:
=
union
(
only
parsing
)
:
stdpp_scope
.
Notation
"( x ∪)"
:
=
(
union
x
)
(
only
parsing
)
:
stdpp_scope
.
...
...
@@ -784,7 +784,7 @@ Notation "⋃ l" := (union_list l) (at level 20, format "⋃ l") : stdpp_scope.
Class
Intersection
A
:
=
intersection
:
A
→
A
→
A
.
Hint
Mode
Intersection
!
:
typeclass_instances
.
Instance
:
Params
(@
intersection
)
2
.
Instance
:
Params
(@
intersection
)
2
:
=
{}
.
Infix
"∩"
:
=
intersection
(
at
level
40
)
:
stdpp_scope
.
Notation
"(∩)"
:
=
intersection
(
only
parsing
)
:
stdpp_scope
.
Notation
"( x ∩)"
:
=
(
intersection
x
)
(
only
parsing
)
:
stdpp_scope
.
...
...
@@ -792,7 +792,7 @@ Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope.
Class
Difference
A
:
=
difference
:
A
→
A
→
A
.
Hint
Mode
Difference
!
:
typeclass_instances
.
Instance
:
Params
(@
difference
)
2
.
Instance
:
Params
(@
difference
)
2
:
=
{}
.
Infix
"∖"
:
=
difference
(
at
level
40
,
left
associativity
)
:
stdpp_scope
.
Notation
"(∖)"
:
=
difference
(
only
parsing
)
:
stdpp_scope
.
Notation
"( x ∖)"
:
=
(
difference
x
)
(
only
parsing
)
:
stdpp_scope
.
...
...
@@ -806,7 +806,7 @@ Infix "∖*∖**" := (zip_with (prod_zip (∖) (∖*)))
Class
Singleton
A
B
:
=
singleton
:
A
→
B
.
Hint
Mode
Singleton
-
!
:
typeclass_instances
.
Instance
:
Params
(@
singleton
)
3
.
Instance
:
Params
(@
singleton
)
3
:
=
{}
.
Notation
"{[ x ]}"
:
=
(
singleton
x
)
(
at
level
1
)
:
stdpp_scope
.
Notation
"{[ x ; y ; .. ; z ]}"
:
=
(
union
..
(
union
(
singleton
x
)
(
singleton
y
))
..
(
singleton
z
))
...
...
@@ -818,7 +818,7 @@ Notation "{[ x , y , z ]}" := (singleton (x,y,z))
Class
SubsetEq
A
:
=
subseteq
:
relation
A
.
Hint
Mode
SubsetEq
!
:
typeclass_instances
.
Instance
:
Params
(@
subseteq
)
2
.
Instance
:
Params
(@
subseteq
)
2
:
=
{}
.
Infix
"⊆"
:
=
subseteq
(
at
level
70
)
:
stdpp_scope
.
Notation
"(⊆)"
:
=
subseteq
(
only
parsing
)
:
stdpp_scope
.
Notation
"( X ⊆)"
:
=
(
subseteq
X
)
(
only
parsing
)
:
stdpp_scope
.
...
...
@@ -868,7 +868,7 @@ Hint Mode Lexico ! : typeclass_instances.
Class
ElemOf
A
B
:
=
elem_of
:
A
→
B
→
Prop
.
Hint
Mode
ElemOf
-
!
:
typeclass_instances
.
Instance
:
Params
(@
elem_of
)
3
.
Instance
:
Params
(@
elem_of
)
3
:
=
{}
.
Infix
"∈"
:
=
elem_of
(
at
level
70
)
:
stdpp_scope
.
Notation
"(∈)"
:
=
elem_of
(
only
parsing
)
:
stdpp_scope
.
Notation
"( x ∈)"
:
=
(
elem_of
x
)
(
only
parsing
)
:
stdpp_scope
.
...
...
@@ -883,7 +883,7 @@ Notation "(∈@{ B } )" := (@elem_of _ B _) (only parsing) : stdpp_scope.
Class
Disjoint
A
:
=
disjoint
:
A
→
A
→
Prop
.
Hint
Mode
Disjoint
!
:
typeclass_instances
.
Instance
:
Params
(@
disjoint
)
2
.
Instance
:
Params
(@
disjoint
)
2
:
=
{}
.
Infix
"##"
:
=
disjoint
(
at
level
70
)
:
stdpp_scope
.
Notation
"(##)"
:
=
disjoint
(
only
parsing
)
:
stdpp_scope
.
Notation
"( X ##.)"
:
=
(
disjoint
X
)
(
only
parsing
)
:
stdpp_scope
.
...
...
@@ -904,7 +904,7 @@ Hint Extern 0 (_ ##* _) => symmetry; eassumption : core.
Class
DisjointE
E
A
:
=
disjointE
:
E
→
A
→
A
→
Prop
.
Hint
Mode
DisjointE
-
!
:
typeclass_instances
.
Instance
:
Params
(@
disjointE
)
4
.
Instance
:
Params
(@
disjointE
)
4
:
=
{}
.
Notation
"X ##{ Γ } Y"
:
=
(
disjointE
Γ
X
Y
)
(
at
level
70
,
format
"X ##{ Γ } Y"
)
:
stdpp_scope
.
Notation
"(##{ Γ } )"
:
=
(
disjointE
Γ
)
(
only
parsing
,
Γ
at
level
1
)
:
stdpp_scope
.
...
...
@@ -921,7 +921,7 @@ Hint Extern 0 (_ ##{_} _) => symmetry; eassumption : core.
Class
DisjointList
A
:
=
disjoint_list
:
list
A
→
Prop
.
Hint
Mode
DisjointList
!
:
typeclass_instances
.
Instance
:
Params
(@
disjoint_list
)
2
.
Instance
:
Params
(@
disjoint_list
)
2
:
=
{}
.
Notation
"## Xs"
:
=
(
disjoint_list
Xs
)
(
at
level
20
,
format
"## Xs"
)
:
stdpp_scope
.
Notation
"##@{ A } Xs"
:
=
(@
disjoint_list
A
_
Xs
)
(
at
level
20
,
only
parsing
)
:
stdpp_scope
.
...
...
@@ -955,19 +955,19 @@ notations and do not formalize any theory on monads (we do not even define a
class with the monad laws). *)
Class
MRet
(
M
:
Type
→
Type
)
:
=
mret
:
∀
{
A
},
A
→
M
A
.
Arguments
mret
{
_
_
_
}
_
:
assert
.
Instance
:
Params
(@
mret
)
3
.
Instance
:
Params
(@
mret
)
3
:
=
{}
.
Class
MBind
(
M
:
Type
→
Type
)
:
=
mbind
:
∀
{
A
B
},
(
A
→
M
B
)
→
M
A
→
M
B
.
Arguments
mbind
{
_
_
_
_
}
_
!
_
/
:
assert
.
Instance
:
Params
(@
mbind
)
4
.
Instance
:
Params
(@
mbind
)
4
:
=
{}
.
Class
MJoin
(
M
:
Type
→
Type
)
:
=
mjoin
:
∀
{
A
},
M
(
M
A
)
→
M
A
.
Arguments
mjoin
{
_
_
_
}
!
_
/
:
assert
.
Instance
:
Params
(@
mjoin
)
3
.
Instance
:
Params
(@
mjoin
)
3
:
=
{}
.
Class
FMap
(
M
:
Type
→
Type
)
:
=
fmap
:
∀
{
A
B
},
(
A
→
B
)
→
M
A
→
M
B
.
Arguments
fmap
{
_
_
_
_
}
_
!
_
/
:
assert
.
Instance
:
Params
(@
fmap
)
4
.
Instance
:
Params
(@
fmap
)
4
:
=
{}
.
Class
OMap
(
M
:
Type
→
Type
)
:
=
omap
:
∀
{
A
B
},
(
A
→
option
B
)
→
M
A
→
M
B
.
Arguments
omap
{
_
_
_
_
}
_
!
_
/
:
assert
.
Instance
:
Params
(@
omap
)
4
.
Instance
:
Params
(@
omap
)
4
:
=
{}
.
Notation
"m ≫= f"
:
=
(
mbind
f
m
)
(
at
level
60
,
right
associativity
)
:
stdpp_scope
.
Notation
"( m ≫=)"
:
=
(
λ
f
,
mbind
f
m
)
(
only
parsing
)
:
stdpp_scope
.
...
...
@@ -1005,7 +1005,7 @@ on maps. In the file [fin_maps] we will axiomatize finite maps.
The function look up [m !! k] should yield the element at key [k] in [m]. *)
Class
Lookup
(
K
A
M
:
Type
)
:
=
lookup
:
K
→
M
→
option
A
.
Hint
Mode
Lookup
-
-
!
:
typeclass_instances
.
Instance
:
Params
(@
lookup
)
4
.
Instance
:
Params
(@
lookup
)
4
:
=
{}
.
Notation
"m !! i"
:
=
(
lookup
i
m
)
(
at
level
20
)
:
stdpp_scope
.
Notation
"(!!)"
:
=
lookup
(
only
parsing
)
:
stdpp_scope
.
Notation
"( m !!)"
:
=
(
λ
i
,
m
!!
i
)
(
only
parsing
)
:
stdpp_scope
.
...
...
@@ -1015,14 +1015,14 @@ Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
(** The singleton map *)
Class
SingletonM
K
A
M
:
=
singletonM
:
K
→
A
→
M
.
Hint
Mode
SingletonM
-
-
!
:
typeclass_instances
.
Instance
:
Params
(@
singletonM
)
5
.
Instance
:
Params
(@
singletonM
)
5
:
=
{}
.
Notation
"{[ k := a ]}"
:
=
(
singletonM
k
a
)
(
at
level
1
)
:
stdpp_scope
.
(** The function insert [<[k:=a]>m] should update the element at key [k] with
value [a] in [m]. *)
Class
Insert
(
K
A
M
:
Type
)
:
=
insert
:
K
→
A
→
M
→
M
.
Hint
Mode
Insert
-
-
!
:
typeclass_instances
.
Instance
:
Params
(@
insert
)
5
.
Instance
:
Params
(@
insert
)
5
:
=
{}
.
Notation
"<[ k := a ]>"
:
=
(
insert
k
a
)
(
at
level
5
,
right
associativity
,
format
"<[ k := a ]>"
)
:
stdpp_scope
.
Arguments
insert
_
_
_
_
!
_
_
!
_
/
:
simpl
nomatch
,
assert
.
...
...
@@ -1032,14 +1032,14 @@ Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
returned. *)
Class
Delete
(
K
M
:
Type
)
:
=
delete
:
K
→
M
→
M
.
Hint
Mode
Delete
-
!
:
typeclass_instances
.
Instance
:
Params
(@
delete
)
4
.
Instance
:
Params
(@
delete
)
4
:
=
{}
.
Arguments
delete
_
_
_
!
_
!
_
/
:
simpl
nomatch
,
assert
.
(** The function [alter f k m] should update the value at key [k] using the
function [f], which is called with the original value. *)
Class
Alter
(
K
A
M
:
Type
)
:
=
alter
:
(
A
→
A
)
→
K
→
M
→
M
.
Hint
Mode
Alter
-
-
!
:
typeclass_instances
.
Instance
:
Params
(@
alter
)
5
.
Instance
:
Params
(@
alter
)
5
:
=
{}
.
Arguments
alter
{
_
_
_
_
}
_
!
_
!
_
/
:
simpl
nomatch
,
assert
.
(** The function [partial_alter f k m] should update the value at key [k] using the
...
...
@@ -1049,14 +1049,14 @@ yields [None]. *)
Class
PartialAlter
(
K
A
M
:
Type
)
:
=
partial_alter
:
(
option
A
→
option
A
)
→
K
→
M
→
M
.
Hint
Mode
PartialAlter
-
-
!
:
typeclass_instances
.
Instance
:
Params
(@
partial_alter
)
4
.
Instance
:
Params
(@
partial_alter
)
4
:
=
{}
.
Arguments
partial_alter
_
_
_
_
_
!
_
!
_
/
:
simpl
nomatch
,
assert
.
(** The function [dom C m] should yield the domain of [m]. That is a finite
collection of type [C] that contains the keys that are a member of [m]. *)
Class
Dom
(
M
C
:
Type
)
:
=
dom
:
M
→
C
.
Hint
Mode
Dom
!
!
:
typeclass_instances
.
Instance
:
Params
(@
dom
)
3
.
Instance
:
Params
(@
dom
)
3
:
=
{}
.
Arguments
dom
:
clear
implicits
.
Arguments
dom
{
_
}
_
{
_
}
!
_
/
:
simpl
nomatch
,
assert
.
...
...
@@ -1065,7 +1065,7 @@ constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*)
Class
Merge
(
M
:
Type
→
Type
)
:
=
merge
:
∀
{
A
B
C
},
(
option
A
→
option
B
→
option
C
)
→
M
A
→
M
B
→
M
C
.
Hint
Mode
Merge
!
:
typeclass_instances
.
Instance
:
Params
(@
merge
)
4
.
Instance
:
Params
(@
merge
)
4
:
=
{}
.
Arguments
merge
_
_
_
_
_
_
!
_
!
_
/
:
simpl
nomatch
,
assert
.
(** The function [union_with f m1 m2] is supposed to yield the union of [m1]
...
...
@@ -1074,20 +1074,20 @@ both [m1] and [m2]. *)
Class
UnionWith
(
A
M
:
Type
)
:
=
union_with
:
(
A
→
A
→
option
A
)
→
M
→
M
→
M
.
Hint
Mode
UnionWith
-
!
:
typeclass_instances
.
Instance
:
Params
(@
union_with
)
3
.
Instance
:
Params
(@
union_with
)
3
:
=
{}
.
Arguments
union_with
{
_
_
_
}
_
!
_
!
_
/
:
simpl
nomatch
,
assert
.
(** Similarly for intersection and difference. *)
Class
IntersectionWith
(
A
M
:
Type
)
:
=
intersection_with
:
(
A
→
A
→
option
A
)
→
M
→
M
→
M
.
Hint
Mode
IntersectionWith
-
!
:
typeclass_instances
.
Instance
:
Params
(@
intersection_with
)
3
.
Instance
:
Params
(@
intersection_with
)
3
:
=
{}
.
Arguments
intersection_with
{
_
_
_
}
_
!
_
!
_
/
:
simpl
nomatch
,
assert
.
Class
DifferenceWith
(
A
M
:
Type
)
:
=
difference_with
:
(
A
→
A
→
option
A
)
→
M
→
M
→
M
.
Hint
Mode
DifferenceWith
-
!
:
typeclass_instances
.
Instance
:
Params
(@
difference_with
)
3
.
Instance
:
Params
(@
difference_with
)
3
:
=
{}
.
Arguments
difference_with
{
_
_
_
}
_
!
_
!
_
/
:
simpl
nomatch
,
assert
.
Definition
intersection_with_list
`
{
IntersectionWith
A
M
}
...
...
@@ -1096,7 +1096,7 @@ Arguments intersection_with_list _ _ _ _ _ !_ / : assert.
Class
LookupE
(
E
K
A
M
:
Type
)
:
=
lookupE
:
E
→
K
→
M
→
option
A
.
Hint
Mode
LookupE
-
-
-
!
:
typeclass_instances
.
Instance
:
Params
(@
lookupE
)
6
.
Instance
:
Params
(@
lookupE
)
6
:
=
{}
.
Notation
"m !!{ Γ } i"
:
=
(
lookupE
Γ
i
m
)
(
at
level
20
,
format
"m !!{ Γ } i"
)
:
stdpp_scope
.
Notation
"(!!{ Γ } )"
:
=
(
lookupE
Γ
)
(
only
parsing
,
Γ
at
level
1
)
:
stdpp_scope
.
...
...
@@ -1104,7 +1104,7 @@ Arguments lookupE _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
Class
InsertE
(
E
K
A
M
:
Type
)
:
=
insertE
:
E
→
K
→
A
→
M
→
M
.
Hint
Mode
InsertE
-
-
-
!
:
typeclass_instances
.
Instance
:
Params
(@
insertE
)
6
.
Instance
:
Params
(@
insertE
)
6
:
=
{}
.
Notation
"<[ k := a ]{ Γ }>"
:
=
(
insertE
Γ
k
a
)
(
at
level
5
,
right
associativity
,
format
"<[ k := a ]{ Γ }>"
)
:
stdpp_scope
.
Arguments
insertE
_
_
_
_
_
_
!
_
_
!
_
/
:
simpl
nomatch
,
assert
.
...
...
@@ -1131,7 +1131,7 @@ enumerated as a list. These elements, given by the [elements] function, may be
in any order and should not contain duplicates. *)
Class
Elements
A
C
:
=
elements
:
C
→
list
A
.
Hint
Mode
Elements
-
!
:
typeclass_instances
.
Instance
:
Params
(@
elements
)
3
.
Instance
:
Params
(@
elements
)
3
:
=
{}
.
(** We redefine the standard library's [In] and [NoDup] using type classes. *)
Inductive
elem_of_list
{
A
}
:
ElemOf
A
(
list
A
)
:
=
...
...
@@ -1168,7 +1168,7 @@ Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C, Union C,
Class
Size
C
:
=
size
:
C
→
nat
.
Hint
Mode
Size
!
:
typeclass_instances
.
Arguments
size
{
_
_
}
!
_
/
:
simpl
nomatch
,
assert
.
Instance
:
Params
(@
size
)
2
.
Instance
:
Params
(@
size
)
2
:
=
{}
.
(** The class [CollectionMonad M] axiomatizes a type constructor [M] that can be
used to construct a collection [M A] with elements of type [A]. The advantage
...
...
@@ -1195,7 +1195,7 @@ will later prove that [fresh] is [Proper] with respect to the induced setoid
equality on collections. *)
Class
Fresh
A
C
:
=
fresh
:
C
→
A
.
Hint
Mode
Fresh
-
!
:
typeclass_instances
.
Instance
:
Params
(@
fresh
)
3
.
Instance
:
Params
(@
fresh
)
3
:
=
{}
.
Class
FreshSpec
A
C
`
{
ElemOf
A
C
,
Empty
C
,
Singleton
A
C
,
Union
C
,
Fresh
A
C
}
:
Prop
:
=
{
fresh_collection_simple
:
>>
SimpleCollection
A
C
;
...
...
@@ -1214,7 +1214,7 @@ Notation "½*" := (fmap (M:=list) half) : stdpp_scope.
for the \sqsubseteq symbol. *)
Class
SqSubsetEq
A
:
=
sqsubseteq
:
relation
A
.
Hint
Mode
SqSubsetEq
!
:
typeclass_instances
.
Instance
:
Params
(@
sqsubseteq
)
2
.
Instance
:
Params
(@
sqsubseteq
)
2
:
=
{}
.
Infix
"⊑"
:
=
sqsubseteq
(
at
level
70
)
:
stdpp_scope
.
Notation
"(⊑)"
:
=
sqsubseteq
(
only
parsing
)
:
stdpp_scope
.
Notation
"( x ⊑)"
:
=
(
sqsubseteq
x
)
(
only
parsing
)
:
stdpp_scope
.
...
...
@@ -1223,13 +1223,13 @@ Notation "(⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
Infix
"⊑@{ A }"
:
=
(@
sqsubseteq
A
_
)
(
at
level
70
,
only
parsing
)
:
stdpp_scope
.
Notation
"(⊑@{ A } )"
:
=
(@
sqsubseteq
A
_
)
(
only
parsing
)
:
stdpp_scope
.
Instance
sqsubseteq_rewrite
`
{
SqSubsetEq
A
}
:
RewriteRelation
(
⊑
).
Instance
sqsubseteq_rewrite
`
{
SqSubsetEq
A
}
:
RewriteRelation
(
⊑
)
:
=
{}
.
Hint
Extern
0
(
_
⊑
_
)
=>
reflexivity
:
core
.
Class
Meet
A
:
=
meet
:
A
→
A
→
A
.
Hint
Mode
Meet
!
:
typeclass_instances
.
Instance
:
Params
(@
meet
)
2
.
Instance
:
Params
(@
meet
)
2
:
=
{}
.
Infix
"⊓"
:
=
meet
(
at
level
40
)
:
stdpp_scope
.
Notation
"(⊓)"
:
=
meet
(
only
parsing
)
:
stdpp_scope
.
Notation
"( x ⊓)"
:
=
(
meet
x
)
(
only
parsing
)
:
stdpp_scope
.
...
...
@@ -1237,7 +1237,7 @@ Notation "(⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope.
Class
Join
A
:
=
join
:
A
→
A
→
A
.
Hint
Mode
Join
!
:
typeclass_instances
.
Instance
:
Params
(@
join
)
2
.
Instance
:
Params
(@
join
)
2
:
=
{}
.
Infix
"⊔"
:
=
join
(
at
level
50
)
:
stdpp_scope
.
Notation
"(⊔)"
:
=
join
(
only
parsing
)
:
stdpp_scope
.
Notation
"( x ⊔)"
:
=
(
join
x
)
(
only
parsing
)
:
stdpp_scope
.
...
...
theories/collections.v
View file @
7514c591
...
...
@@ -879,7 +879,7 @@ Fixpoint fresh_list `{Fresh A C, Union C, Singleton A C}
|
0
=>
[]
|
S
n
=>
let
x
:
=
fresh
X
in
x
::
fresh_list
n
({[
x
]}
∪
X
)
end
.
Instance
:
Params
(@
fresh_list
)
6
.
Instance
:
Params
(@
fresh_list
)
6
:
=
{}
.
Inductive
Forall_fresh
`
{
ElemOf
A
C
}
(
X
:
C
)
:
list
A
→
Prop
:
=
|
Forall_fresh_nil
:
Forall_fresh
X
[]
...
...
@@ -1077,7 +1077,7 @@ End seq_set.
(** Mimimal elements *)
Definition
minimal
`
{
ElemOf
A
C
}
(
R
:
relation
A
)
(
x
:
A
)
(
X
:
C
)
:
Prop
:
=
∀
y
,
y
∈
X
→
R
y
x
→
R
x
y
.
Instance
:
Params
(@
minimal
)
5
.
Instance
:
Params
(@
minimal
)
5
:
=
{}
.
Typeclasses
Opaque
minimal
.
Section
minimal
.
...
...
theories/list.v
View file @
7514c591
...
...
@@ -10,9 +10,9 @@ Arguments length {_} _ : assert.
Arguments
cons
{
_
}
_
_
:
assert
.
Arguments
app
{
_
}
_
_
:
assert
.
Instance
:
Params
(@
length
)
1
.
Instance
:
Params
(@
cons
)
1
.
Instance
:
Params
(@
app
)
1
.
Instance
:
Params
(@
length
)
1
:
=
{}
.
Instance
:
Params
(@
cons
)
1
:
=
{}
.
Instance
:
Params
(@
app
)
1
:
=
{}
.
Notation
tail
:
=
tl
.
Notation
take
:
=
firstn
.
...
...
@@ -22,9 +22,9 @@ Arguments tail {_} _ : assert.
Arguments
take
{
_
}
!
_
!
_
/
:
assert
.
Arguments
drop
{
_
}
!
_
!
_
/
:
assert
.
Instance
:
Params
(@
tail
)
1
.
Instance
:
Params
(@
take
)
1
.
Instance
:
Params
(@
drop
)
1
.
Instance
:
Params
(@
tail
)
1
:
=
{}
.
Instance
:
Params
(@
take
)
1
:
=
{}
.
Instance
:
Params
(@
drop
)
1
:
=
{}
.
Arguments
Permutation
{
_
}
_
_
:
assert
.
Arguments
Forall_cons
{
_
}
_
_
_
_
_
:
assert
.
...
...
@@ -90,7 +90,7 @@ Fixpoint list_inserts {A} (i : nat) (k l : list A) : list A :=
|
[]
=>
l
|
y
::
k
=>
<[
i
:
=
y
]>(
list_inserts
(
S
i
)
k
l
)
end
.
Instance
:
Params
(@
list_inserts
)
1
.
Instance
:
Params
(@
list_inserts
)
1
:
=
{}
.
(** The operation [delete i l] removes the [i]th element of [l] and moves
all consecutive elements one position ahead. In case [i] is out of bounds,
...
...
@@ -105,7 +105,7 @@ Instance list_delete {A} : Delete nat (list A) :=
(** The function [option_list o] converts an element [Some x] into the
singleton list [[x]], and [None] into the empty list [[]]. *)
Definition
option_list
{
A
}
:
option
A
→
list
A
:
=
option_rect
_
(
λ
x
,
[
x
])
[].
Instance
:
Params
(@
option_list
)
1
.
Instance
:
Params
(@
option_list
)
1
:
=
{}
.
Instance
maybe_list_singleton
{
A
}
:
Maybe
(
λ
x
:
A
,
[
x
])
:
=
λ
l
,
match
l
with
[
x
]
=>
Some
x
|
_
=>
None
end
.
...
...
@@ -126,23 +126,23 @@ Definition list_find {A} P `{∀ x, Decision (P x)} : list A → option (nat * A
|
[]
=>
None
|
x
::
l
=>
if
decide
(
P
x
)
then
Some
(
0
,
x
)
else
prod_map
S
id
<$>
go
l
end
.
Instance
:
Params
(@
list_find
)
3
.
Instance
:
Params
(@
list_find
)
3
:
=
{}
.
(** The function [replicate n x] generates a list with length [n] of elements
with value [x]. *)
Fixpoint
replicate
{
A
}
(
n
:
nat
)
(
x
:
A
)
:
list
A
:
=
match
n
with
0
=>
[]
|
S
n
=>
x
::
replicate
n
x
end
.
Instance
:
Params
(@
replicate
)
2
.
Instance
:
Params
(@
replicate
)
2
:
=
{}
.
(** The function [reverse l] returns the elements of [l] in reverse order. *)
Definition
reverse
{
A
}
(
l
:
list
A
)
:
list
A
:
=
rev_append
l
[].
Instance
:
Params
(@
reverse
)
1
.
Instance
:
Params
(@
reverse
)
1
:
=
{}
.
(** The function [last l] returns the last element of the list [l], or [None]
if the list [l] is empty. *)
Fixpoint
last
{
A
}
(
l
:
list
A
)
:
option
A
:
=
match
l
with
[]
=>
None
|
[
x
]
=>
Some
x
|
_
::
l
=>
last
l
end
.
Instance
:
Params
(@
last
)
1
.
Instance
:
Params
(@
last
)
1
:
=
{}
.
(** The function [resize n y l] takes the first [n] elements of [l] in case
[length l ≤ n], and otherwise appends elements with value [x] to [l] to obtain
...
...
@@ -153,7 +153,7 @@ Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A :=
|
x
::
l
=>
match
n
with
0
=>
[]
|
S
n
=>
x
::
resize
n
y
l
end
end
.
Arguments
resize
{
_
}
!
_
_
!
_
:
assert
.
Instance
:
Params
(@
resize
)
2
.
Instance
:
Params
(@
resize
)
2
:
=
{}
.
(** The function [reshape k l] transforms [l] into a list of lists whose sizes
are specified by [k]. In case [l] is too short, the resulting list will be
...
...
@@ -162,7 +162,7 @@ Fixpoint reshape {A} (szs : list nat) (l : list A) : list (list A) :=
match
szs
with
|
[]
=>
[]
|
sz
::
szs
=>
take
sz
l
::
reshape
szs
(
drop
sz
l
)
end
.
Instance
:
Params
(@
reshape
)
2
.
Instance
:
Params
(@
reshape
)
2
:
=
{}
.
Definition
sublist_lookup
{
A
}
(
i
n
:
nat
)
(
l
:
list
A
)
:
option
(
list
A
)
:
=
guard
(
i
+
n
≤
length
l
)
;
Some
(
take
n
(
drop
i
l
)).
...
...
@@ -3603,23 +3603,23 @@ with a binding [i] for [x]. *)
Section
quote_lookup
.
Context
{
A
:
Type
}.
Class
QuoteLookup
(
E1
E2
:
list
A
)
(
x
:
A
)
(
i
:
nat
)
:
=
{}.
Global
Instance
quote_lookup_here
E
x
:
QuoteLookup
(
x
::
E
)
(
x
::
E
)
x
0
.
Global
Instance
quote_lookup_end
x
:
QuoteLookup
[]
[
x
]
x
0
.
Global
Instance
quote_lookup_here
E
x
:
QuoteLookup
(
x
::
E
)
(
x
::
E
)
x
0
:
=
{}
.
Global
Instance
quote_lookup_end
x
:
QuoteLookup
[]
[
x
]
x
0
:
=
{}
.
Global
Instance
quote_lookup_further
E1
E2
x
i
y
:
QuoteLookup
E1
E2
x
i
→
QuoteLookup
(
y
::
E1
)
(
y
::
E2
)
x
(
S
i
)
|
1000
.
QuoteLookup
E1
E2
x
i
→
QuoteLookup
(
y
::
E1
)
(
y
::
E2
)
x
(
S
i
)
|
1000
:
=
{}
.
End
quote_lookup
.
Section
quote
.
Context
{
A
:
Type
}.
Class
Quote
(
E1
E2
:
env
A
)
(
l
:
list
A
)
(
t
:
rlist
nat
)
:
=
{}.
Global
Instance
quote_nil
:
Quote
E1
E1
[]
rnil
.
Global
Instance
quote_nil
:
Quote
E1
E1
[]
rnil
:
=
{}
.
Global
Instance
quote_node
E1
E2
l
i
:
QuoteLookup
E1
E2
l
i
→
Quote
E1
E2
l
(
rnode
i
)
|
1000
.
QuoteLookup
E1
E2
l
i
→
Quote
E1
E2
l
(
rnode
i
)
|
1000
:
=
{}
.
Global
Instance
quote_cons
E1
E2
E3
x
l
i
t
:
QuoteLookup
E1
E2
[
x
]
i
→
Quote
E2
E3
l
t
→
Quote
E1
E3
(
x
::
l
)
(
rapp
(
rnode
i
)
t
).
Quote
E2
E3
l
t
→
Quote
E1
E3
(
x
::
l
)
(
rapp
(
rnode
i
)
t
)
:
=
{}
.
Global
Instance
quote_app
E1
E2
E3
l1
l2
t1
t2
:
Quote
E1
E2
l1
t1
→
Quote
E2
E3
l2
t2
→
Quote
E1
E3
(
l1
++
l2
)
(
rapp
t1
t2
).
Quote
E1
E2
l1
t1
→
Quote
E2
E3
l2
t2
→
Quote
E1
E3
(
l1
++
l2
)
(
rapp
t1
t2
)
:
=
{}
.
End
quote
.
Section
eval
.
...
...
theories/option.v
View file @
7514c591
...
...
@@ -23,7 +23,7 @@ Proof. congruence. Qed.
(** The [from_option] is the eliminator for option. *)
Definition
from_option
{
A
B
}
(
f
:
A
→
B
)
(
y
:
B
)
(
mx
:
option
A
)
:
B
:
=
match
mx
with
None
=>
y
|
Some
x
=>
f
x
end
.
Instance
:
Params
(@
from_option
)
3
.
Instance
:
Params
(@
from_option
)
3
:
=
{}
.
Arguments
from_option
{
_
_
}
_
_
!
_
/
:
assert
.
(** The eliminator with the identity function. *)
...
...
@@ -40,7 +40,7 @@ Lemma option_eq_1_alt {A} (mx my : option A) x :
Proof
.
congruence
.
Qed
.
Definition
is_Some
{
A
}
(
mx
:
option
A
)
:
=
∃
x
,
mx
=
Some
x
.
Instance
:
Params
(@
is_Some
)
1
.
Instance
:
Params
(@
is_Some
)
1
:
=
{}
.
Lemma
is_Some_alt
{
A
}
(
mx
:
option
A
)
:
is_Some
mx
↔
match
mx
with
Some
_
=>
True
|
None
=>
False
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