summaryrefslogtreecommitdiff
path: root/theories/Classes/EquivDec.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /theories/Classes/EquivDec.v
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'theories/Classes/EquivDec.v')
-rw-r--r--theories/Classes/EquivDec.v158
1 files changed, 158 insertions, 0 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
new file mode 100644
index 00000000..debe953a
--- /dev/null
+++ b/theories/Classes/EquivDec.v
@@ -0,0 +1,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 10919 2008-05-11 22:04:26Z 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).
+
+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.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. \ No newline at end of file