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
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Decidable equivalences.
*
* Author: Matthieu Sozeau
* Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
* 91405 Orsay, France *)
(* $Id: EquivDec.v 11282 2008-07-28 11:51:53Z msozeau $ *)
Set Implicit Arguments.
Unset Strict Implicit.
(** Export notations. *)
Require Export Coq.Classes.Equivalence.
(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more
classically. *)
Require Import Coq.Logic.Decidable.
Open Scope equiv_scope.
Class [ equiv : Equivalence A ] => DecidableEquivalence :=
setoid_decidable : forall x y : A, decidable (x === y).
(** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
Class [ equiv : Equivalence A ] => EqDec :=
equiv_dec : forall x y : A, { x === y } + { x =/= y }.
(** We define the [==] overloaded notation for deciding equality. It does not take precedence
of [==] defined in the type scope, hence we can have both at the same time. *)
Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) : equiv_scope.
Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
match x with
| left H => @right _ _ H
| right H => @left _ _ H
end.
Require Import Coq.Program.Program.
Open Local Scope program_scope.
(** Invert the branches. *)
Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x === y } := swap_sumbool (x == y).
(** Overloaded notation for inequality. *)
Infix "<>" := nequiv_dec (no associativity, at level 70) : equiv_scope.
(** Define boolean versions, losing the logical information. *)
Definition equiv_decb [ EqDec A ] (x y : A) : bool :=
if x == y then true else false.
Definition nequiv_decb [ EqDec A ] (x y : A) : bool :=
negb (equiv_decb x y).
Infix "==b" := equiv_decb (no associativity, at level 70).
Infix "<>b" := nequiv_decb (no associativity, at level 70).
(** Decidable leibniz equality instances. *)
Require Import Coq.Arith.Peano_dec.
(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
Program Instance nat_eq_eqdec : ! EqDec nat eq :=
equiv_dec := eq_nat_dec.
Require Import Coq.Bool.Bool.
Program Instance bool_eqdec : ! EqDec bool eq :=
equiv_dec := bool_dec.
Program Instance unit_eqdec : ! EqDec unit eq :=
equiv_dec x y := in_left.
Next Obligation.
Proof.
destruct x ; destruct y.
reflexivity.
Qed.
Program Instance prod_eqdec [ EqDec A eq, EqDec B eq ] :
! EqDec (prod A B) eq :=
equiv_dec x y :=
let '(x1, x2) := x in
let '(y1, y2) := y in
if x1 == y1 then
if x2 == y2 then in_left
else in_right
else in_right.
Solve Obligations using unfold complement, equiv ; program_simpl.
Program Instance sum_eqdec [ EqDec A eq, EqDec B eq ] :
! EqDec (sum A B) eq :=
equiv_dec x y :=
match x, y with
| inl a, inl b => if a == b then in_left else in_right
| inr a, inr b => if a == b then in_left else in_right
| inl _, inr _ | inr _, inl _ => in_right
end.
Solve Obligations using unfold complement, equiv ; program_simpl.
(** Objects of function spaces with countable domains like bool have decidable equality. *)
Require Import Coq.Program.FunctionalExtensionality.
Program Instance bool_function_eqdec [ EqDec A eq ] : ! EqDec (bool -> A) eq :=
equiv_dec f g :=
if f true == g true then
if f false == g false then in_left
else in_right
else in_right.
Solve Obligations using try red ; unfold equiv, complement ; program_simpl.
Next Obligation.
Proof.
extensionality x.
destruct x ; auto.
Qed.
Require Import List.
Program Instance list_eqdec [ eqa : EqDec A eq ] : ! EqDec (list A) eq :=
equiv_dec :=
fix aux (x : list A) y { struct x } :=
match x, y with
| nil, nil => in_left
| cons hd tl, cons hd' tl' =>
if hd == hd' then
if aux tl tl' then in_left else in_right
else in_right
| _, _ => in_right
end.
Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto).
Next Obligation.
Proof. clear aux. red in H0. subst.
destruct y; intuition (discriminate || eauto).
Defined.
|
