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
Tej Chajed
stdpp
Commits
2f9f3d3f
Commit
2f9f3d3f
authored
Sep 21, 2017
by
Robbert Krebbers
Browse files
Introduce `RelDecision` for decidable relations and define `EqDecision` using it.
This allows for more control over `Hint Mode`.
parent
929d64cc
Changes
15
Hide whitespace changes
Inline
Side-by-side
theories/base.v
View file @
2f9f3d3f
...
...
@@ -150,13 +150,30 @@ Hint Extern 0 (_ ≡ _) => symmetry; assumption.
(** * Type classes *)
(** ** Decidable propositions *)
(** This type class by (Spitters/van der Weegen, 2011) collects decidable
propositions. For example to declare a parameter expressing decidable equality
on a type [A] we write [`{∀ x y : A, Decision (x = y)}] and use it by writing
[decide (x = y)]. *)
propositions. *)
Class
Decision
(
P
:
Prop
)
:
=
decide
:
{
P
}
+
{
¬
P
}.
Hint
Mode
Decision
!
:
typeclass_instances
.
Arguments
decide
_
{
_
}
:
assert
.
Notation
EqDecision
A
:
=
(
∀
x
y
:
A
,
Decision
(
x
=
y
)).
Arguments
decide
_
{
_
}
:
simpl
never
,
assert
.
(** Although [RelDecision R] is just [∀ x y, Decision (R x y)], we make this
an explicit class instead of a notation for two reasons:
- It allows us to control [Hint Mode] more precisely. In particular, if it were
defined as a notation, the above [Hint Mode] for [Decision] would not prevent
diverging instance search when looking for [RelDecision (@eq ?A)], which would
result in it looking for [Decision (@eq ?A x y)], i.e. an instance where the
head position of [Decision] is not en evar.
- We use it to avoid inefficient computation due to eager evaluation of
propositions by [vm_compute]. This inefficiency arises for example if
[(x = y) := (f x = f y)]. Since [decide (x = y)] evaluates to
[decide (f x = f y)], this would then lead to evaluation of [f x] and [f y].
Using the [RelDecision], the [f] is hidden under a lambda, which prevents
unnecessary evaluation. *)
Class
RelDecision
{
A
B
}
(
R
:
A
→
B
→
Prop
)
:
=
decide_rel
x
y
:
>
Decision
(
R
x
y
).
Hint
Mode
RelDecision
!
!
!
:
typeclass_instances
.
Arguments
decide_rel
{
_
_
}
_
{
_
}
_
_
:
simpl
never
,
assert
.
Notation
EqDecision
A
:
=
(
RelDecision
(@
eq
A
)).
(** ** Inhabited types *)
(** This type class collects types that are inhabited. *)
...
...
theories/bset.v
View file @
2f9f3d3f
...
...
@@ -29,7 +29,8 @@ Proof.
-
intros
X
Y
x
;
unfold
elem_of
,
bset_elem_of
;
simpl
.
destruct
(
bset_car
X
x
),
(
bset_car
Y
x
)
;
simpl
;
tauto
.
Qed
.
Instance
bset_elem_of_dec
{
A
}
x
(
X
:
bset
A
)
:
Decision
(
x
∈
X
)
:
=
_
.
Instance
bset_elem_of_dec
{
A
}
:
RelDecision
(@
elem_of
_
(
bset
A
)
_
).
Proof
.
refine
(
λ
x
X
,
cast_if
(
decide
(
bset_car
X
x
)))
;
done
.
Defined
.
Typeclasses
Opaque
bset_elem_of
.
Global
Opaque
bset_empty
bset_singleton
bset_union
...
...
theories/coPset.v
View file @
2f9f3d3f
...
...
@@ -190,17 +190,18 @@ Proof.
intros
p
;
apply
eq_bool_prop_intro
,
(
HXY
p
).
Qed
.
Instance
coPset_elem_of_dec
(
p
:
positive
)
(
X
:
coPset
)
:
Decision
(
p
∈
X
)
:
=
_
.
Instance
coPset_equiv_dec
(
X
Y
:
coPset
)
:
Decision
(
X
≡
Y
).
Proof
.
refine
(
cast_if
(
decide
(
X
=
Y
)))
;
abstract
(
by
fold_leibniz
).
Defined
.
Instance
mapset_disjoint_dec
(
X
Y
:
coPset
)
:
Decision
(
X
⊥
Y
).
Instance
coPset_elem_of_dec
:
RelDecision
(@
elem_of
_
coPset
_
).
Proof
.
solve_decision
.
Defined
.
Instance
coPset_equiv_dec
:
RelDecision
(@
equiv
coPset
_
).
Proof
.
refine
(
λ
X
Y
,
cast_if
(
decide
(
X
=
Y
)))
;
abstract
(
by
fold_leibniz
).
Defined
.
Instance
mapset_disjoint_dec
:
RelDecision
(@
disjoint
coPset
_
).
Proof
.
refine
(
cast_if
(
decide
(
X
∩
Y
=
∅
)))
;
refine
(
λ
X
Y
,
cast_if
(
decide
(
X
∩
Y
=
∅
)))
;
abstract
(
by
rewrite
disjoint_intersection_L
).
Defined
.
Instance
mapset_subseteq_dec
(
X
Y
:
coPset
)
:
Decision
(
X
⊆
Y
).
Instance
mapset_subseteq_dec
:
RelDecision
(@
subseteq
coPset
_
).
Proof
.
refine
(
cast_if
(
decide
(
X
∪
Y
=
Y
)))
;
abstract
(
by
rewrite
subseteq_union_L
).
refine
(
λ
X
Y
,
cast_if
(
decide
(
X
∪
Y
=
Y
)))
;
abstract
(
by
rewrite
subseteq_union_L
).
Defined
.
(** * Top *)
...
...
theories/collections.v
View file @
2f9f3d3f
...
...
@@ -527,7 +527,7 @@ Section simple_collection.
End
leibniz
.
Section
dec
.
Context
`
{
∀
(
X
Y
:
C
),
Decision
(
X
≡
Y
)}.
Context
`
{
!
RelDecision
(@
equiv
C
_
)}.
Lemma
collection_subseteq_inv
X
Y
:
X
⊆
Y
→
X
⊂
Y
∨
X
≡
Y
.
Proof
.
destruct
(
decide
(
X
≡
Y
))
;
[
by
right
|
left
;
set_solver
].
Qed
.
Lemma
collection_not_subset_inv
X
Y
:
X
⊄
Y
→
X
⊈
Y
∨
X
≡
Y
.
...
...
@@ -692,7 +692,7 @@ Section collection.
End
leibniz
.
Section
dec
.
Context
`
{
∀
(
x
:
A
)
(
X
:
C
),
Decision
(
x
∈
X
)}.
Context
`
{
!
RelDecision
(@
elem_of
A
C
_
)}.
Lemma
not_elem_of_intersection
x
X
Y
:
x
∉
X
∩
Y
↔
x
∉
X
∨
x
∉
Y
.
Proof
.
rewrite
elem_of_intersection
.
destruct
(
decide
(
x
∈
X
))
;
tauto
.
Qed
.
Lemma
not_elem_of_difference
x
X
Y
:
x
∉
X
∖
Y
↔
x
∉
X
∨
x
∈
Y
.
...
...
theories/countable.v
View file @
2f9f3d3f
...
...
@@ -10,6 +10,7 @@ Class Countable A `{EqDecision A} := {
decode
:
positive
→
option
A
;
decode_encode
x
:
decode
(
encode
x
)
=
Some
x
}.
Hint
Mode
Countable
!
-
:
typeclass_instances
.
Arguments
encode
:
simpl
never
.
Arguments
decode
:
simpl
never
.
...
...
@@ -36,8 +37,8 @@ Section choice.
Context
`
{
Countable
A
}
(
P
:
A
→
Prop
).
Inductive
choose_step
:
relation
positive
:
=
|
choose_step_None
{
p
}
:
decode
p
=
None
→
choose_step
(
Psucc
p
)
p
|
choose_step_Some
{
p
x
}
:
|
choose_step_None
{
p
}
:
decode
(
A
:
=
A
)
p
=
None
→
choose_step
(
Psucc
p
)
p
|
choose_step_Some
{
p
}
{
x
:
A
}
:
decode
p
=
Some
x
→
¬
P
x
→
choose_step
(
Psucc
p
)
p
.
Lemma
choose_step_acc
:
(
∃
x
,
P
x
)
→
Acc
choose_step
1
%
positive
.
Proof
.
...
...
@@ -320,7 +321,7 @@ Arguments GenNode {_} _ _ : assert.
Instance
gen_tree_dec
`
{
EqDecision
T
}
:
EqDecision
(
gen_tree
T
).
Proof
.
refine
(
fix
go
t1
t2
:
=
fix
go
t1
t2
:
=
let
_
:
EqDecision
_
:
=
@
go
in
match
t1
,
t2
with
|
GenLeaf
x1
,
GenLeaf
x2
=>
cast_if
(
decide
(
x1
=
x2
))
|
GenNode
n1
ts1
,
GenNode
n2
ts2
=>
...
...
theories/decidable.v
View file @
2f9f3d3f
...
...
@@ -6,8 +6,6 @@ type class. *)
From
stdpp
Require
Export
proof_irrel
.
Set
Default
Proof
Using
"Type*"
.
Hint
Extern
200
(
Decision
_
)
=>
progress
(
lazy
beta
)
:
typeclass_instances
.
Lemma
dec_stable
`
{
Decision
P
}
:
¬¬
P
→
P
.
Proof
.
firstorder
.
Qed
.
...
...
@@ -16,17 +14,6 @@ Proof. destruct b. left; constructor. right. intros []. Qed.
Instance
:
Inj
(=)
(
↔
)
Is_true
.
Proof
.
intros
[]
[]
;
simpl
;
intuition
.
Qed
.
(** We introduce [decide_rel] to avoid inefficienct computation due to eager
evaluation of propositions by [vm_compute]. This inefficiency occurs if
[(x = y) := (f x = f y)] as [decide (x = y)] evaluates to [decide (f x = f y)]
which then might lead to evaluation of [f x] and [f y]. Using [decide_rel]
we hide [f] under a lambda abstraction to avoid this unnecessary evaluation. *)
Definition
decide_rel
{
A
B
}
(
R
:
A
→
B
→
Prop
)
{
dec
:
∀
x
y
,
Decision
(
R
x
y
)}
(
x
:
A
)
(
y
:
B
)
:
Decision
(
R
x
y
)
:
=
dec
x
y
.
Lemma
decide_rel_correct
{
A
B
}
(
R
:
A
→
B
→
Prop
)
`
{
∀
x
y
,
Decision
(
R
x
y
)}
(
x
:
A
)
(
y
:
B
)
:
decide_rel
R
x
y
=
decide
(
R
x
y
).
Proof
.
reflexivity
.
Qed
.
Lemma
decide_True
{
A
}
`
{
Decision
P
}
(
x
y
:
A
)
:
P
→
(
if
decide
P
then
x
else
y
)
=
x
.
Proof
.
destruct
(
decide
P
)
;
tauto
.
Qed
.
...
...
@@ -75,9 +62,10 @@ Ltac solve_trivial_decision :=
|
|-
Decision
(
?P
)
=>
apply
_
|
|-
sumbool
?P
(
¬
?P
)
=>
change
(
Decision
P
)
;
apply
_
end
.
Ltac
solve_decision
:
=
intros
;
first
[
solve_trivial_decision
|
unfold
Decision
;
decide
equality
;
solve_trivial_decision
].
Ltac
solve_decision
:
=
unfold
EqDecision
;
intros
;
first
[
solve_trivial_decision
|
unfold
Decision
;
decide
equality
;
solve_trivial_decision
].
(** The following combinators are useful to create Decision proofs in
combination with the [refine] tactic. *)
...
...
theories/fin_collections.v
View file @
2f9f3d3f
...
...
@@ -23,9 +23,9 @@ Implicit Types X Y : C.
Lemma
fin_collection_finite
X
:
set_finite
X
.
Proof
.
by
exists
(
elements
X
)
;
intros
;
rewrite
elem_of_elements
.
Qed
.
Instance
elem_of_dec_slow
(
x
:
A
)
(
X
:
C
)
:
Decision
(
x
∈
X
)
|
100
.
Instance
elem_of_dec_slow
:
RelDecision
(@
elem_of
A
C
_
)
|
100
.
Proof
.
refine
(
cast_if
(
decide_rel
(
∈
)
x
(
elements
X
)))
;
refine
(
λ
x
X
,
cast_if
(
decide_rel
(
∈
)
x
(
elements
X
)))
;
by
rewrite
<-(
elem_of_elements
_
).
Defined
.
...
...
theories/fin_maps.v
View file @
2f9f3d3f
...
...
@@ -1238,10 +1238,9 @@ Proof.
destruct
(
m1
!!
i
),
(
m2
!!
i
)
;
simplify_eq
/=
;
auto
;
by
eapply
bool_decide_unpack
,
Hm
.
Qed
.
Global
Instance
map_relation_dec
`
{
∀
x
y
,
Decision
(
R
x
y
),
∀
x
,
Decision
(
P
x
),
∀
y
,
Decision
(
Q
y
)}
(
m1
:
M
A
)
(
m2
:
M
B
)
:
Decision
(
map_relation
R
P
Q
m1
m2
).
Global
Instance
map_relation_dec
:
RelDecision
(
map_relation
(
M
:
=
M
)
R
P
Q
).
Proof
.
refine
(
cast_if
(
decide
(
map_Forall
(
λ
_
,
Is_true
)
(
merge
f
m1
m2
))))
;
refine
(
λ
m1
m2
,
cast_if
(
decide
(
map_Forall
(
λ
_
,
Is_true
)
(
merge
f
m1
m2
))))
;
abstract
by
rewrite
map_relation_alt
.
Defined
.
(** Due to the finiteness of finite maps, we can extract a witness if the
...
...
theories/finite.v
View file @
2f9f3d3f
...
...
@@ -8,6 +8,7 @@ Class Finite A `{EqDecision A} := {
NoDup_enum
:
NoDup
enum
;
elem_of_enum
x
:
x
∈
enum
}.
Hint
Mode
Finite
!
-
:
typeclass_instances
.
Arguments
enum
:
clear
implicits
.
Arguments
enum
_
{
_
_
}
:
assert
.
Arguments
NoDup_enum
:
clear
implicits
.
...
...
theories/gmultiset.v
View file @
2f9f3d3f
...
...
@@ -7,18 +7,14 @@ Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }.
Arguments
GMultiSet
{
_
_
_
}
_
:
assert
.
Arguments
gmultiset_car
{
_
_
_
}
_
:
assert
.
Lemma
gmultiset_eq_dec
`
{
Countable
A
}
:
EqDecision
(
gmultiset
A
).
Instance
gmultiset_eq_dec
`
{
Countable
A
}
:
EqDecision
(
gmultiset
A
).
Proof
.
solve_decision
.
Defined
.
Hint
Extern
1
(
Decision
(@
eq
(
gmultiset
_
)
_
_
))
=>
eapply
@
gmultiset_eq_dec
:
typeclass_instances
.
Program
Definition
gmultiset_countable
`
{
Countable
A
}
:
Program
Instance
gmultiset_countable
`
{
Countable
A
}
:
Countable
(
gmultiset
A
)
:
=
{|
encode
X
:
=
encode
(
gmultiset_car
X
)
;
decode
p
:
=
GMultiSet
<$>
decode
p
|}.
Next
Obligation
.
intros
A
??
[
X
]
;
simpl
.
by
rewrite
decode_encode
.
Qed
.
Hint
Extern
1
(
Countable
(
gmultiset
_
))
=>
eapply
@
gmultiset_countable
:
typeclass_instances
.
Section
definitions
.
Context
`
{
Countable
A
}.
...
...
@@ -102,8 +98,8 @@ Proof.
by
split
;
auto
with
lia
.
-
intros
X
Y
x
.
rewrite
!
elem_of_multiplicity
,
multiplicity_union
.
omega
.
Qed
.
Global
Instance
gmultiset_elem_of_dec
x
X
:
Decision
(
x
∈
X
).
Proof
.
unfold
elem_of
,
gmultiset_elem_of
.
apply
_
.
Defined
.
Global
Instance
gmultiset_elem_of_dec
:
Rel
Decision
(
@
elem_of
_
(
gmultiset
A
)
_
).
Proof
.
refine
(
λ
x
X
,
cast_if
(
decide
(
0
<
multiplicity
x
X
)))
;
done
.
Defined
.
(* Algebraic laws *)
Global
Instance
gmultiset_comm
:
Comm
(@
eq
(
gmultiset
A
))
(
∪
).
...
...
@@ -144,8 +140,9 @@ Qed.
Lemma
gmultiset_elements_empty_inv
X
:
elements
X
=
[]
→
X
=
∅
.
Proof
.
destruct
X
as
[
X
]
;
unfold
elements
,
gmultiset_elements
;
simpl
.
intros
;
apply
(
f_equal
GMultiSet
).
destruct
(
map_to_list
X
)
as
[|[]]
eqn
:
?
;
naive_solver
eauto
using
map_to_list_empty_inv
.
intros
;
apply
(
f_equal
GMultiSet
).
destruct
(
map_to_list
X
)
as
[|[]]
eqn
:
?.
-
by
apply
map_to_list_empty_inv
.
-
naive_solver
.
Qed
.
Lemma
gmultiset_elements_empty'
X
:
elements
X
=
[]
↔
X
=
∅
.
Proof
.
...
...
@@ -249,9 +246,9 @@ Proof.
apply
forall_proper
;
intros
x
.
unfold
multiplicity
.
destruct
(
gmultiset_car
X
!!
x
),
(
gmultiset_car
Y
!!
x
)
;
naive_solver
omega
.
Qed
.
Global
Instance
gmultiset_subseteq_dec
X
Y
:
Decision
(
X
⊆
Y
).
Global
Instance
gmultiset_subseteq_dec
:
Rel
Decision
(
@
subseteq
(
gmultiset
A
)
_
).
Proof
.
refine
(
cast_if
(
decide
(
map_relation
(
≤
)
refine
(
λ
X
Y
,
cast_if
(
decide
(
map_relation
(
≤
)
(
λ
_
,
False
)
(
λ
_
,
True
)
(
gmultiset_car
X
)
(
gmultiset_car
Y
))))
;
by
rewrite
gmultiset_subseteq_alt
.
Defined
.
...
...
theories/list.v
View file @
2f9f3d3f
...
...
@@ -311,13 +311,13 @@ Instance list_subseteq {A} : SubsetEq (list A) := λ l1 l2, ∀ x, x ∈ l1 →
Section
list_set
.
Context
`
{
dec
:
EqDecision
A
}.
Global
Instance
elem_of_list_dec
(
x
:
A
)
:
∀
l
:
list
A
,
Decision
(
x
∈
l
).
Global
Instance
elem_of_list_dec
:
RelDecision
(@
elem_of
A
(
list
A
)
_
).
Proof
.
refine
(
fix
go
l
:
=
fix
go
x
l
:
=
match
l
return
Decision
(
x
∈
l
)
with
|
[]
=>
right
_
|
y
::
l
=>
cast_if_or
(
decide
(
x
=
y
))
(
go
l
)
|
y
::
l
=>
cast_if_or
(
decide
(
x
=
y
))
(
go
x
l
)
end
)
;
clear
go
dec
;
subst
;
try
(
by
constructor
)
;
abstract
by
inversion
1
.
Defined
.
Fixpoint
remove_dups
(
l
:
list
A
)
:
list
A
:
=
...
...
@@ -1505,9 +1505,9 @@ Proof.
-
intros
?.
by
eexists
[].
-
intros
???[
k1
->]
[
k2
->].
exists
(
k2
++
k1
).
by
rewrite
(
assoc_L
(++)).
Qed
.
Global
Instance
prefix_dec
`
{!
EqDecision
A
}
:
∀
l1
l2
,
Decision
(
l1
`
prefix_of
`
l2
)
:
=
fix
go
l1
l2
:
=
match
l1
,
l2
return
{
l1
`
prefix_of
`
l2
}
+
{
¬
l1
`
prefix_of
`
l2
}
with
Global
Instance
prefix_dec
`
{!
EqDecision
A
}
:
RelDecision
prefix
:
=
fix
go
l1
l2
:
=
match
l1
,
l2
with
|
[],
_
=>
left
(
prefix_nil
_
)
|
_
,
[]
=>
right
(
prefix_nil_not
_
_
)
|
x
::
l1
,
y
::
l2
=>
...
...
@@ -1639,10 +1639,9 @@ Lemma suffix_length l1 l2 : l1 `suffix_of` l2 → length l1 ≤ length l2.
Proof
.
intros
[?
->].
rewrite
app_length
.
lia
.
Qed
.
Lemma
suffix_cons_not
x
l
:
¬
x
::
l
`
suffix_of
`
l
.
Proof
.
intros
[??].
discriminate_list
.
Qed
.
Global
Instance
suffix_dec
`
{!
EqDecision
A
}
l1
l2
:
Decision
(
l1
`
suffix_of
`
l2
).
Global
Instance
suffix_dec
`
{!
EqDecision
A
}
:
RelDecision
(@
suffix
A
).
Proof
.
refine
(
cast_if
(
decide_rel
prefix
(
reverse
l1
)
(
reverse
l2
)))
;
refine
(
λ
l1
l2
,
cast_if
(
decide_rel
prefix
(
reverse
l1
)
(
reverse
l2
)))
;
abstract
(
by
rewrite
suffix_prefix_reverse
).
Defined
.
...
...
@@ -2087,14 +2086,14 @@ Section submseteq_dec.
destruct
(
list_remove
x
l2
)
as
[
k'
|]
eqn
:
?
;
intros
;
simplify_eq
.
rewrite
submseteq_cons_l
.
eauto
using
list_remove_Some
.
Qed
.
Global
Instance
submseteq_dec
l1
l2
:
Decision
(
l1
⊆
+
l2
).
Global
Instance
submseteq_dec
:
Rel
Decision
(
submseteq
:
relation
(
list
A
)
).
Proof
.
refine
(
cast_if
(
decide
(
is_Some
(
list_remove_list
l1
l2
))))
;
refine
(
λ
l1
l2
,
cast_if
(
decide
(
is_Some
(
list_remove_list
l1
l2
))))
;
abstract
(
rewrite
list_remove_list_submseteq
;
tauto
).
Defined
.
Global
Instance
Permutation_dec
l1
l2
:
Decision
(
l1
≡
ₚ
l2
).
Global
Instance
Permutation_dec
:
Rel
Decision
(
Permutation
:
relation
(
list
A
)
).
Proof
.
refine
(
cast_if_and
refine
(
λ
l1
l2
,
cast_if_and
(
decide
(
length
l1
=
length
l2
))
(
decide
(
l1
⊆
+
l2
)))
;
abstract
(
rewrite
Permutation_alt
;
tauto
).
Defined
.
...
...
@@ -2621,7 +2620,7 @@ Section Forall2.
Qed
.
Global
Instance
Forall2_dec
`
{
dec
:
∀
x
y
,
Decision
(
P
x
y
)}
:
∀
l
k
,
Decision
(
Forall2
P
l
k
).
Rel
Decision
(
Forall2
P
).
Proof
.
refine
(
fix
go
l
k
:
Decision
(
Forall2
P
l
k
)
:
=
...
...
theories/mapset.v
View file @
2f9f3d3f
...
...
@@ -76,18 +76,18 @@ Section deciders.
match
X1
,
X2
with
Mapset
m1
,
Mapset
m2
=>
cast_if
(
decide
(
m1
=
m2
))
end
)
;
abstract
congruence
.
Defined
.
Global
Instance
mapset_equiv_dec
(
X1
X2
:
mapset
M
)
:
Decision
(
X1
≡
X2
)
|
1
.
Proof
.
refine
(
cast_if
(
decide
(
X1
=
X2
)))
;
abstract
(
by
fold_leibniz
).
Defined
.
Global
Instance
mapset_elem_of_dec
x
(
X
:
mapset
M
)
:
Decision
(
x
∈
X
)
|
1
.
Proof
.
solve_decisi
on
.
Defined
.
Global
Instance
mapset_disjoint_dec
(
X1
X2
:
mapset
M
)
:
Decision
(
X1
⊥
X2
).
Global
Instance
mapset_equiv_dec
:
RelDecision
(@
equiv
(
mapset
M
)
_
)
|
1
.
Proof
.
refine
(
λ
X1
X2
,
cast_if
(
decide
(
X1
=
X2
)))
;
abstract
(
by
fold_leibniz
).
Defined
.
Global
Instance
mapset_elem_of_dec
:
RelDecision
(@
elem_of
_
(
mapset
M
)
_
)
|
1
.
Proof
.
refine
(
λ
x
X
,
cast_if
(
decide
(
mapset_car
X
!!
x
=
Some
())))
;
d
on
e
.
Defined
.
Global
Instance
mapset_disjoint_dec
:
RelDecision
(@
disjoint
(
mapset
M
)
_
).
Proof
.
refine
(
cast_if
(
decide
(
X1
∩
X2
=
∅
)))
;
refine
(
λ
X1
X2
,
cast_if
(
decide
(
X1
∩
X2
=
∅
)))
;
abstract
(
by
rewrite
disjoint_intersection_L
).
Defined
.
Global
Instance
mapset_subseteq_dec
(
X1
X2
:
mapset
M
)
:
Decision
(
X1
⊆
X2
).
Global
Instance
mapset_subseteq_dec
:
RelDecision
(@
subseteq
(
mapset
M
)
_
).
Proof
.
refine
(
cast_if
(
decide
(
X1
∪
X2
=
X2
)))
;
refine
(
λ
X1
X2
,
cast_if
(
decide
(
X1
∪
X2
=
X2
)))
;
abstract
(
by
rewrite
subseteq_union_L
).
Defined
.
End
deciders
.
...
...
theories/numbers.v
View file @
2f9f3d3f
...
...
@@ -36,8 +36,8 @@ Infix "`max`" := Nat.max (at level 35) : nat_scope.
Infix
"`min`"
:
=
Nat
.
min
(
at
level
35
)
:
nat_scope
.
Instance
nat_eq_dec
:
EqDecision
nat
:
=
eq_nat_dec
.
Instance
nat_le_dec
:
∀
x
y
:
nat
,
Decision
(
x
≤
y
)
:
=
le_dec
.
Instance
nat_lt_dec
:
∀
x
y
:
nat
,
Decision
(
x
<
y
)
:
=
lt_dec
.
Instance
nat_le_dec
:
Rel
Decision
le
:
=
le_dec
.
Instance
nat_lt_dec
:
Rel
Decision
lt
:
=
lt_dec
.
Instance
nat_inhabited
:
Inhabited
nat
:
=
populate
0
%
nat
.
Instance
S_inj
:
Inj
(=)
(=)
S
.
Proof
.
by
injection
1
.
Qed
.
...
...
@@ -77,9 +77,9 @@ Proof. intros. destruct (Nat_mul_split_l n x2 x1 y2 y1); auto with lia. Qed.
Notation
lcm
:
=
Nat
.
lcm
.
Notation
divide
:
=
Nat
.
divide
.
Notation
"( x | y )"
:
=
(
divide
x
y
)
:
nat_scope
.
Instance
Nat_divide_dec
x
y
:
Decision
(
x
|
y
)
.
Instance
Nat_divide_dec
:
Rel
Decision
Nat
.
divide
.
Proof
.
refine
(
cast_if
(
decide
(
lcm
x
y
=
y
)))
;
by
rewrite
Nat
.
divide_lcm_iff
.
refine
(
λ
x
y
,
cast_if
(
decide
(
lcm
x
y
=
y
)))
;
by
rewrite
Nat
.
divide_lcm_iff
.
Defined
.
Instance
:
PartialOrder
divide
.
Proof
.
...
...
@@ -130,6 +130,10 @@ Arguments Pos.of_nat : simpl never.
Arguments
Pmult
:
simpl
never
.
Instance
positive_eq_dec
:
EqDecision
positive
:
=
Pos
.
eq_dec
.
Instance
positive_le_dec
:
RelDecision
Pos
.
le
.
Proof
.
refine
(
λ
x
y
,
decide
((
x
?=
y
)
≠
Gt
)).
Defined
.
Instance
positive_lt_dec
:
RelDecision
Pos
.
lt
.
Proof
.
refine
(
λ
x
y
,
decide
((
x
?=
y
)
=
Lt
)).
Defined
.
Instance
positive_inhabited
:
Inhabited
positive
:
=
populate
1
.
Instance
maybe_xO
:
Maybe
xO
:
=
λ
p
,
match
p
with
p
~
0
=>
Some
p
|
_
=>
None
end
.
...
...
@@ -218,10 +222,10 @@ Instance Npos_inj : Inj (=) (=) Npos.
Proof
.
by
injection
1
.
Qed
.
Instance
N_eq_dec
:
EqDecision
N
:
=
N
.
eq_dec
.
Program
Instance
N_le_dec
(
x
y
:
N
)
:
Decision
(
x
≤
y
)%
N
:
=
Program
Instance
N_le_dec
:
RelDecision
N
.
le
:
=
λ
x
y
,
match
Ncompare
x
y
with
Gt
=>
right
_
|
_
=>
left
_
end
.
Solve
Obligations
with
naive_solver
.
Program
Instance
N_lt_dec
(
x
y
:
N
)
:
Decision
(
x
<
y
)%
N
:
=
Program
Instance
N_lt_dec
:
RelDecision
N
.
lt
:
=
λ
x
y
,
match
Ncompare
x
y
with
Lt
=>
left
_
|
_
=>
right
_
end
.
Solve
Obligations
with
naive_solver
.
Instance
N_inhabited
:
Inhabited
N
:
=
populate
1
%
N
.
...
...
@@ -259,8 +263,8 @@ Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat.
Proof
.
intros
n1
n2
.
apply
Nat2Z
.
inj
.
Qed
.
Instance
Z_eq_dec
:
EqDecision
Z
:
=
Z
.
eq_dec
.
Instance
Z_le_dec
:
∀
x
y
:
Z
,
Decision
(
x
≤
y
)
:
=
Z_le_dec
.
Instance
Z_lt_dec
:
∀
x
y
:
Z
,
Decision
(
x
<
y
)
:
=
Z_lt_dec
.
Instance
Z_le_dec
:
Rel
Decision
Z
.
le
:
=
Z_le_dec
.
Instance
Z_lt_dec
:
Rel
Decision
Z
.
lt
:
=
Z_lt_dec
.
Instance
Z_inhabited
:
Inhabited
Z
:
=
populate
1
.
Instance
Z_le_po
:
PartialOrder
(
≤
).
Proof
.
...
...
@@ -365,11 +369,11 @@ Hint Extern 1 (_ ≤ _) => reflexivity || discriminate.
Arguments
Qred
:
simpl
never
.
Instance
Qc_eq_dec
:
EqDecision
Qc
:
=
Qc_eq_dec
.
Program
Instance
Qc_le_dec
(
x
y
:
Qc
)
:
Decision
(
x
≤
y
)
:
=
Program
Instance
Qc_le_dec
:
RelDecision
Qcle
:
=
λ
x
y
,
if
Qclt_le_dec
y
x
then
right
_
else
left
_
.
Next
Obligation
.
intros
x
y
;
apply
Qclt_not_le
.
Qed
.
Next
Obligation
.
done
.
Qed
.
Program
Instance
Qc_lt_dec
(
x
y
:
Qc
)
:
Decision
(
x
<
y
)
:
=
Program
Instance
Qc_lt_dec
:
RelDecision
Qclt
:
=
λ
x
y
,
if
Qclt_le_dec
x
y
then
left
_
else
right
_
.
Solve
Obligations
with
done
.
Next
Obligation
.
intros
x
y
;
apply
Qcle_not_lt
.
Qed
.
...
...
theories/orders.v
View file @
2f9f3d3f
...
...
@@ -41,15 +41,16 @@ Section orders.
split
;
try
apply
_
.
eauto
using
strict_transitive_r
,
strict_include
.
Qed
.
Global
Instance
preorder_subset_dec_slow
`
{
∀
X
Y
,
Decision
(
X
⊆
Y
)}
(
X
Y
:
A
)
:
Decision
(
X
⊂
Y
)
|
100
:
=
_
.
Global
Instance
preorder_subset_dec_slow
`
{!
RelDecision
R
}
:
RelDecision
(
strict
R
)
|
100
.
Proof
.
solve_decision
.
Defined
.
Lemma
strict_spec_alt
`
{!
AntiSymm
(=)
R
}
X
Y
:
X
⊂
Y
↔
X
⊆
Y
∧
X
≠
Y
.
Proof
.
split
.
-
intros
[?
HYX
].
split
.
done
.
by
intros
<-.
-
intros
[?
HXY
].
split
.
done
.
by
contradict
HXY
;
apply
(
anti_symm
R
).
Qed
.
Lemma
po_eq_dec
`
{!
PartialOrder
R
,
∀
X
Y
,
Decision
(
X
⊆
Y
)
}
:
EqDecision
A
.
Lemma
po_eq_dec
`
{!
PartialOrder
R
,
!
Rel
Decision
R
}
:
EqDecision
A
.
Proof
.
refine
(
λ
X
Y
,
cast_if_and
(
decide
(
X
⊆
Y
))
(
decide
(
Y
⊆
X
)))
;
abstract
(
rewrite
anti_symm_iff
;
tauto
).
...
...
@@ -76,8 +77,8 @@ Section strict_orders.
Lemma
strict_anti_symm
`
{!
StrictOrder
R
}
X
Y
:
X
⊂
Y
→
Y
⊂
X
→
False
.
Proof
.
intros
.
apply
(
irreflexivity
R
X
).
by
trans
Y
.
Qed
.
Global
Instance
trichotomyT_dec
`
{!
TrichotomyT
R
,
!
StrictOrder
R
}
X
Y
:
Decision
(
X
⊂
Y
)
:
=
Global
Instance
trichotomyT_dec
`
{!
TrichotomyT
R
,
!
StrictOrder
R
}
:
Rel
Decision
R
:
=
λ
X
Y
,
match
trichotomyT
R
X
Y
with
|
inleft
(
left
H
)
=>
left
H
|
inleft
(
right
H
)
=>
right
(
irreflexive_eq
_
_
H
)
...
...
theories/sorting.v
View file @
2f9f3d3f
...
...
@@ -15,7 +15,7 @@ Section merge_sort.
|
[],
_
=>
l2
|
_
,
[]
=>
l1
|
x1
::
l1
,
x2
::
l2
=>
if
decide
_rel
R
x1
x2
then
x1
::
list_merge
l1
(
x2
::
l2
)
if
decide
(
R
x1
x2
)
then
x1
::
list_merge
l1
(
x2
::
l2
)
else
x2
::
list_merge_aux
l2
end
.
Global
Arguments
list_merge
!
_
!
_
/
:
assert
.
...
...
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