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
|
(* -*- 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 setoid equality theory.
*
* Author: Matthieu Sozeau
* Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
* 91405 Orsay, France *)
(* $Id: SetoidDec.v 11282 2008-07-28 11:51:53Z msozeau $ *)
Set Implicit Arguments.
Unset Strict Implicit.
(** Export notations. *)
Require Export Coq.Classes.SetoidClass.
(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more
classically. *)
Require Import Coq.Logic.Decidable.
Class DecidableSetoid A [ Setoid A ] :=
setoid_decidable : forall x y : A, decidable (x == y).
(** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
Class (( s : Setoid 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).
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).
(** 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.Arith.
(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
Program Instance eq_setoid A : Setoid A :=
equiv := eq ; setoid_equiv := eq_equivalence.
Program Instance nat_eq_eqdec : EqDec (eq_setoid nat) :=
equiv_dec := eq_nat_dec.
Require Import Coq.Bool.Bool.
Program Instance bool_eqdec : EqDec (eq_setoid bool) :=
equiv_dec := bool_dec.
Program Instance unit_eqdec : EqDec (eq_setoid unit) :=
equiv_dec x y := in_left.
Next Obligation.
Proof.
destruct x ; destruct y.
reflexivity.
Qed.
Program Instance prod_eqdec [ ! EqDec (eq_setoid A), ! EqDec (eq_setoid B) ] : EqDec (eq_setoid (prod A B)) :=
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 ; 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 (eq_setoid A) ] : EqDec (eq_setoid (bool -> A)) :=
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.
|
