From 7a39bd5650cc49c5c77788fb42fe2caaf35dfdac Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 6 May 2008 14:05:20 +0000
Subject: Postpone the search for the recursive argument index from the user
 given name after internalisation, to get the correct behavior with typeclass
 binders. This simplifies the pretty printing and translation of the recursive
 argument name in various places too. Use this opportunity to factorize the
 different internalization and interpretation functions of binders as well.
 This definitely fixes part 2 of bug #1846 and makes it possible to use
 fixpoint definitions with typeclass arguments in program too, with an example
 given in EquivDec. At the same time, one fix and one enhancement in Program:
 - fix a de Bruijn bug in subtac_cases - introduce locations of obligations
 and use them in case the obligation tactic raises a failure when tried on a
 particular obligation, as suggested by Sean Wilson.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10889 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Classes/EquivDec.v | 25 +++++++++++++++++++++++--
 1 file changed, 23 insertions(+), 2 deletions(-)

(limited to 'theories')

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 17f8970fc9..62744b1d1a 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -29,12 +29,12 @@ Require Import Coq.Logic.Decidable.
 
 Open Scope equiv_scope.
 
-Class [ Equivalence A ] => DecidableEquivalence :=
+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 [ Equivalence A ] => EqDec :=
+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
@@ -135,3 +135,24 @@ Program Instance [ EqDec A eq ] => bool_function_eqdec : ! EqDec (bool -> A) eq
     extensionality x.
     destruct x ; auto.
   Qed.
+
+Require Import List.
+
+Program Instance [ eqa : EqDec A eq ] => list_eqdec : ! 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
-- 
cgit v1.2.3