aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/SetoidDec.v
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-01-18 00:12:05 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-01-18 00:12:05 +0000
commit72dccfa0f5edb59b1ba2668e91828742ab91bb1d (patch)
tree46339464eee6a725dc9ae10d38bd8ae45e724e44 /theories/Classes/SetoidDec.v
parentedbb81e324234548c2bb70306fb448420e1bbd70 (diff)
Change notation for setoid inequality, coerce objects before comparing them. Debug tactic redefinition code, streamline Instantiation Tactic implementation using that. Have to adapt obligations tactic still.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10449 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/SetoidDec.v')
-rw-r--r--theories/Classes/SetoidDec.v18
1 files changed, 12 insertions, 6 deletions
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index a9f2ae6de..d20b3df55 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -18,31 +18,37 @@
Set Implicit Arguments.
Unset Strict Implicit.
-Require Import Coq.Classes.SetoidClass.
+(** Export notations. *)
+Require Export Coq.Classes.SetoidClass.
(** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
Class [ Setoid A R ] => EqDec :=
- equiv_dec : forall x y : A, { x == y } + { x =!= y }.
+ 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. *)
-Infix "==" := equiv_dec (no associativity, at level 70).
+Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70).
(** Use program to solve some obligations. *)
+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.
(** Invert the branches. *)
-Program Definition nequiv_dec [ EqDec A R ] (x y : A) : { x =!= y } + { x == y } :=
- if x == y then right else left.
+Program Definition nequiv_dec [ EqDec A R ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
(** Overloaded notation for inequality. *)
-Infix "=!=" := nequiv_dec (no associativity, at level 70).
+Infix "=/=" := nequiv_dec (no associativity, at level 70).
(** Define boolean versions, losing the logical information. *)