-
Notifications
You must be signed in to change notification settings - Fork 2
/
dec.v
65 lines (57 loc) · 1.36 KB
/
dec.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
Require Import Coq.Logic.FinFun List.
Class is_dec_eq (A : Set) :=
{
dec_eq: forall (a b : A), { a = b } + { a <> b }
}.
Lemma dec_eq_refl {A : Set} `{is_dec_eq A}:
forall (x : A) (B : Type) (P Q : B),
(if (dec_eq x x) then P else Q) = P.
Proof.
intros.
destruct (dec_eq x x).
- reflexivity.
- congruence.
Qed.
Lemma dec_eq_neq {A : Set} `{is_dec_eq A}:
forall (x y : A) (B : Type) (P Q : B),
x <> y ->
(if (dec_eq x y) then P else Q) = Q.
Proof.
intros.
destruct (dec_eq x y).
- congruence.
- reflexivity.
Qed.
Class is_dec_rel {A B : Set} (f : A -> B -> Prop) :=
{
dec_rel: forall a b, { f a b } + { ~ f a b }
}.
Class is_dec_pred {A : Set} (f : A -> Prop) :=
{
dec_pred: forall (a : A), { f a } + { ~ f a }
}.
Instance dec_eq_pair (A B : Set) `{is_dec_eq A} `{is_dec_eq B} : is_dec_eq (A * B).
Proof.
constructor.
intros [a1 b1] [a2 b2].
destruct (dec_eq a1 a2); subst.
- destruct (dec_eq b1 b2); subst.
+ eauto.
+ right.
intro.
inversion H1; subst.
eauto.
- right.
intro.
inversion H1; subst.
eauto.
Defined.
Hint Resolve dec_eq_pair : typeclass_instances.
Instance in_dec {A : Set} `{is_dec_eq A} {xs : list A} : is_dec_pred (fun a => In a xs).
Proof.
constructor.
intros.
eapply Lists.List.in_dec.
firstorder 2.
Defined.
Hint Resolve in_dec : typeclass_instances.