1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* Decidable setoid equality theory.
11
* Author: Matthieu Sozeau
12
* Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
13
* 91405 Orsay, France *)
15
(* $Id: SetoidDec.v 11800 2009-01-18 18:34:15Z msozeau $ *)
17
Set Implicit Arguments.
18
Unset Strict Implicit.
20
(** Export notations. *)
22
Require Export Coq.Classes.SetoidClass.
24
(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more
27
Require Import Coq.Logic.Decidable.
29
Class DecidableSetoid `(S : Setoid A) :=
30
setoid_decidable : forall x y : A, decidable (x == y).
32
(** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
34
Class EqDec `(S : Setoid A) :=
35
equiv_dec : forall x y : A, { x == y } + { x =/= y }.
37
(** We define the [==] overloaded notation for deciding equality. It does not take precedence
38
of [==] defined in the type scope, hence we can have both at the same time. *)
40
Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70).
42
Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
44
| left H => @right _ _ H
45
| right H => @left _ _ H
48
Require Import Coq.Program.Program.
50
Open Local Scope program_scope.
52
(** Invert the branches. *)
54
Program Definition nequiv_dec `{EqDec A} (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
56
(** Overloaded notation for inequality. *)
58
Infix "=/=" := nequiv_dec (no associativity, at level 70).
60
(** Define boolean versions, losing the logical information. *)
62
Definition equiv_decb `{EqDec A} (x y : A) : bool :=
63
if x == y then true else false.
65
Definition nequiv_decb `{EqDec A} (x y : A) : bool :=
66
negb (equiv_decb x y).
68
Infix "==b" := equiv_decb (no associativity, at level 70).
69
Infix "<>b" := nequiv_decb (no associativity, at level 70).
71
(** Decidable leibniz equality instances. *)
73
Require Import Coq.Arith.Arith.
75
(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
77
Program Instance eq_setoid A : Setoid A | 10 :=
78
{ equiv := eq ; setoid_equiv := eq_equivalence }.
80
Program Instance nat_eq_eqdec : EqDec (eq_setoid nat) :=
83
Require Import Coq.Bool.Bool.
85
Program Instance bool_eqdec : EqDec (eq_setoid bool) :=
88
Program Instance unit_eqdec : EqDec (eq_setoid unit) :=
93
destruct x ; destruct y.
97
Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : EqDec (eq_setoid (prod A B)) :=
100
let '(y1, y2) := y in
102
if x2 == y2 then in_left
106
Solve Obligations using unfold complement ; program_simpl.
108
(** Objects of function spaces with countable domains like bool have decidable equality. *)
110
Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) : EqDec (eq_setoid (bool -> A)) :=
112
if f true == g true then
113
if f false == g false then in_left
117
Solve Obligations using try red ; unfold equiv, complement ; program_simpl.