Debugging of the class_setoid tactic and eauto. Prepare for move from

class_setoid to class_tactics...


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10563 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 39 insertions, 15 deletions

diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v
index 9cc78a970..c05a4b1e1 100644
--- a/theories/Classes/Relations.v
+++ b/theories/Classes/Relations.v
@@ -184,6 +184,12 @@ Ltac relation_refl :=
 
     | [ |- ?R ?A ?B ?C ?D ?X ?X ] => apply (reflexive (R:=R A B C D) X)
     | [ H : ?R ?A ?B ?C ?D ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D) H)
+
+    | [ |- ?R ?A ?B ?C ?D ?E ?X ?X ] => apply (reflexive (R:=R A B C D E) X)
+    | [ H : ?R ?A ?B ?C ?D ?E ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D E) H)
+
+    | [ |- ?R ?A ?B ?C ?D ?E ?F ?X ?X ] => apply (reflexive (R:=R A B C D E F) X)
+    | [ H : ?R ?A ?B ?C ?D ?E ?F ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D E F) H)
   end.
 
 Ltac refl := relation_refl.
@@ -200,6 +206,9 @@ Ltac relation_sym :=
 
     | [ H : ?R ?A ?B ?C ?D ?X ?Y |- ?R ?A ?B ?C ?D ?Y ?X ] => apply (symmetric (R:=R A B C D) (x:=X) (y:=Y) H)
 
+    | [ H : ?R ?A ?B ?C ?D ?E ?X ?Y |- ?R ?A ?B ?C ?D ?E ?Y ?X ] => apply (symmetric (R:=R A B C D E) (x:=X) (y:=Y) H)
+
+    | [ H : ?R ?A ?B ?C ?D ?E ?F ?X ?Y |- ?R ?A ?B ?C ?D ?E ?F ?Y ?X ] => apply (symmetric (R:=R A B C D E F) (x:=X) (y:=Y) H)
   end.
 
 Ltac relation_symmetric := 
@@ -213,6 +222,10 @@ Ltac relation_symmetric :=
     | [ |- ?R ?A ?B ?C ?Y ?X ] => apply (symmetric (R:=R A B C) (x:=X) (y:=Y))
 
     | [ |- ?R ?A ?B ?C ?D ?Y ?X ] => apply (symmetric (R:=R A B C D) (x:=X) (y:=Y))
+
+    | [ |- ?R ?A ?B ?C ?D ?E ?Y ?X ] => apply (symmetric (R:=R A B C D E) (x:=X) (y:=Y))
+
+    | [ |- ?R ?A ?B ?C ?D ?E ?F ?Y ?X ] => apply (symmetric (R:=R A B C D E F) (x:=X) (y:=Y))
   end.
 
 Ltac sym := relation_symmetric.
@@ -236,6 +249,9 @@ Ltac relation_trans :=
 
     | [ H : ?R ?A ?B ?C ?D ?E ?X ?Y, H' : ?R ?A ?B ?C ?D ?E ?Y ?Z |- ?R ?A ?B ?C ?D ?E ?X ?Z ] => 
       apply (transitive (R:=R A B C D E) (x:=X) (y:=Y) (z:=Z) H H')
+
+    | [ H : ?R ?A ?B ?C ?D ?E ?F ?X ?Y, H' : ?R ?A ?B ?C ?D ?E ?F ?Y ?Z |- ?R ?A ?B ?C ?D ?E ?F ?X ?Z ] => 
+      apply (transitive (R:=R A B C D E F) (x:=X) (y:=Y) (z:=Z) H H')
   end.
 
 Ltac relation_transitive Y := 
@@ -254,6 +270,12 @@ Ltac relation_transitive Y :=
 
     | [ |- ?R ?A ?B ?C ?D ?X ?Z ] => 
       apply (transitive (R:=R A B C D) (x:=X) (y:=Y) (z:=Z))
+
+    | [ |- ?R ?A ?B ?C ?D ?E ?X ?Z ] => 
+      apply (transitive (R:=R A B C D E) (x:=X) (y:=Y) (z:=Z))
+
+    | [ |- ?R ?A ?B ?C ?D ?E ?F ?X ?Z ] => 
+      apply (transitive (R:=R A B C D E F) (x:=X) (y:=Y) (z:=Z))
   end.
 
 Ltac trans Y := relation_transitive Y.
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 014ff3a01..3040dd04b 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -9,7 +8,7 @@
 
 (* Standard functions and proofs about them.
  * Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+ * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
  *              91405 Orsay, France *)
 
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
@@ -19,28 +18,26 @@ Unset Strict Implicit.
 
 Require Export Coq.Program.FunctionalExtensionality.
 
-Definition compose `A B C` (g : B -> C) (f : A -> B) := fun x : A => g (f x).
+Notation  "'λ' x : T , y" := (fun x:T => y) (at level 1, x,T,y at level 10) : program_scope.
 
-Definition arrow (A B : Type) := A -> B.
+Open Scope program_scope.
 
-Definition impl (A B : Prop) : Prop := A -> B.
+Definition id `A` := λ x : A, x.
 
-Definition id `A` := fun x : A => x.
+Definition compose `A B C` (g : B -> C) (f : A -> B) := λ x : A , g (f x).
 
 Hint Unfold compose.
 
-Notation " g 'o' f " := (compose g f)  (at level 50, left associativity) : program_scope.
-
-Open Scope program_scope.
+Notation " g ∘ f " := (compose g f)  (at level 50, left associativity) : program_scope.
 
-Lemma compose_id_left : forall A B (f : A -> B), id o f = f.
+Lemma compose_id_left : forall A B (f : A -> B), id ∘ f = f.
 Proof.
   intros.
   unfold id, compose.
   symmetry ; apply eta_expansion.
 Qed.
 
-Lemma compose_id_right : forall A B (f : A -> B), f o id = f.
+Lemma compose_id_right : forall A B (f : A -> B), f ∘ id = f.
 Proof.
   intros.
   unfold id, compose.
@@ -48,13 +45,18 @@ Proof.
 Qed.
 
 Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D), 
-  h o (g o f) = h o g o f.
+  h ∘ (g ∘ f) = h ∘ g ∘ f.
 Proof.
+  intros.
   reflexivity.
 Qed.
 
 Hint Rewrite @compose_id_left @compose_id_right @compose_assoc : core.
 
+Definition arrow (A B : Type) := A -> B.
+
+Definition impl (A B : Prop) : Prop := A -> B.
+
 Notation " f '#' x " := (f x) (at level 100, x at level 200, only parsing).
 
 Definition const `A B` (a : A) := fun x : B => a.
@@ -126,13 +128,13 @@ Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..).
 
 (** n-ary exists ! *)
 
-Notation "'exists' x y , p" := (ex (fun x => (ex (fun y => p))))
+Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p))))
   (at level 200, x ident, y ident, right associativity) : type_scope.
 
-Notation "'exists' x y z , p" := (ex (fun x => (ex (fun y => (ex (fun z => p))))))
+Notation " 'exists' x y z , p" := (ex (fun x => (ex (fun y => (ex (fun z => p))))))
   (at level 200, x ident, y ident, z ident, right associativity) : type_scope.
 
-Notation "'exists' x y z w , p" := (ex (fun x => (ex (fun y => (ex (fun z => (ex (fun w => p))))))))
+Notation " 'exists' x y z w , p" := (ex (fun x => (ex (fun y => (ex (fun z => (ex (fun w => p))))))))
   (at level 200, x ident, y ident, z ident, w ident, right associativity) : type_scope.
 
 Tactic Notation "exist" constr(x) := exists x.