Enhanced discrimination nets implementation, which can now work with

goals containing existentials and use transparency information on
constants (optionally). Only used by the typeclasses eauto engine for
now, but could be used for other hint bases easily (just switch a boolean).
Had to add a new "creation" hint to be able to set said boolean upon
creation of the typeclass_instances hint db.
Improve the proof-search algorithm for Morphism, up to 10 seconds
gained in e.g. Field_theory, Ring_polynom. Added a morphism
declaration for [compose].
One needs to declare more constants as being unfoldable using
the [Typeclasses unfold] command so that discrimination is done correctly, but
that amounts to only 6 declarations in the standard library.


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

12 files changed, 83 insertions, 83 deletions

diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 42961baea2..d77704c12a 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -134,8 +134,8 @@ End Respecting.
 
 (** The default equivalence on function spaces, with higher-priority than [eq]. *)
 
-Program Instance pointwise_equivalence [ Equivalence A eqA ] :
-  Equivalence (B -> A) (pointwise_relation eqA) | 9.
+Program Instance pointwise_equivalence [ Equivalence B eqB ] :
+  Equivalence (A -> B) (pointwise_relation eqB) | 9.
 
   Next Obligation.
   Proof.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 05167bdc58..7240217990 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -39,10 +39,6 @@ Class Morphism A (R : relation A) (m : A) : Prop :=
 
 Implicit Arguments Morphism [A].
 
-(** We allow to unfold the [relation] definition while doing morphism search. *)
-
-Typeclasses unfold relation.
-
 (** Respectful morphisms. *)
 
 (** The fully dependent version, not used yet. *)
@@ -79,6 +75,15 @@ Arguments Scope respectful [type_scope type_scope signature_scope signature_scop
 
 Open Local Scope signature_scope.
 
+(** Pointwise lifting is just respect with leibnize equality on the left. *)
+
+Definition pointwise_relation {A B : Type} (R : relation B) : relation (A -> B) := 
+  fun f g => forall x : A, R (f x) (g x).
+
+Lemma pointwise_pointwise A B (R : relation B) : 
+  relation_equivalence (pointwise_relation R) (@eq A ==> R).
+Proof. intros. split. simpl_relation. firstorder. Qed.
+
 (** We can build a PER on the Coq function space if we have PERs on the domain and
    codomain. *)
 
@@ -99,17 +104,18 @@ Proof. firstorder. Qed.
 
 (** The subrelation property goes through products as usual. *)
 
-Instance morphisms_subrelation [ sub : subrelation A R₁ R₂ ] :
-  ! subrelation (B -> A) (R ==> R₁) (R ==> R₂).
-Proof. firstorder. Qed.
+Instance morphisms_subrelation_respectful [ subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂ ] :
+  subrelation (R₁ ==> S₁) (R₂ ==> S₂).
+Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed.
 
-Instance morphisms_subrelation_left [ sub : subrelation A R₂ R₁ ] :
-  ! subrelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3.
-Proof. firstorder. Qed.
+(** And of course it is reflexive. *)
+
+Instance morphisms_subrelation_refl : ! subrelation A R R | 10.
+Proof. simpl_relation. Qed.
 
 (** [Morphism] is itself a covariant morphism for [subrelation]. *)
 
-Lemma subrelation_morphism [ sub : subrelation A R₁ R₂, mor : Morphism A R₁ m ] : Morphism R₂ m.
+Lemma subrelation_morphism [ mor : Morphism A R₁ m, sub : subrelation A R₁ R₂ ] : Morphism R₂ m.
 Proof.
   intros. apply sub. apply mor.
 Qed.
@@ -121,8 +127,9 @@ Proof. reduce. subst. firstorder. Qed.
 (** We use an external tactic to manage the application of subrelation, which is otherwise
    always applicable. We allow its use only once per branch. *)
 
-Inductive subrelation_done : Prop :=
-  did_subrelation : subrelation_done.
+Inductive subrelation_done : Prop := did_subrelation : subrelation_done.
+
+Inductive normalization_done : Prop := did_normalization.
 
 Ltac subrelation_tac := 
   match goal with
@@ -131,7 +138,7 @@ Ltac subrelation_tac :=
       set(H:=did_subrelation) ; eapply @subrelation_morphism
   end.
 
-Hint Extern 4 (@Morphism _ _ _) => subrelation_tac : typeclass_instances.
+Hint Extern 5 (@Morphism _ _ _) => subrelation_tac : typeclass_instances.
 
 (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
 
@@ -181,20 +188,10 @@ Program Instance trans_contra_co_morphism
     transitivity x0...
   Qed.
 
-(* (** Dually... *) *)
-
-(* Program Instance [ Transitive A R ] => *)
-(*   trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R. *)
-  
-(*   Next Obligation. *)
-(*   Proof with auto. *)
-(*     apply* trans_contra_co_morphism ; eauto. eauto. *)
-(*   Qed. *)
-
 (** Morphism declarations for partial applications. *)
 
 Program Instance trans_contra_inv_impl_morphism
-  [ Transitive A R ] : Morphism (R --> inverse impl) (R x).
+  [ Transitive A R ] : Morphism (R --> inverse impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -202,7 +199,7 @@ Program Instance trans_contra_inv_impl_morphism
   Qed.
 
 Program Instance trans_co_impl_morphism
-  [ Transitive A R ] : Morphism (R ==> impl) (R x).
+  [ Transitive A R ] : Morphism (R ==> impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -210,23 +207,23 @@ Program Instance trans_co_impl_morphism
   Qed.
 
 Program Instance trans_sym_co_inv_impl_morphism
-  [ Transitive A R, Symmetric A R ] : Morphism (R ==> inverse impl) (R x).
+  [ PER A R ] : Morphism (R ==> inverse impl) (R x) | 2.
 
   Next Obligation.
   Proof with auto.
-    transitivity y...
+    transitivity y... symmetry...
   Qed.
 
 Program Instance trans_sym_contra_impl_morphism
-  [ Transitive A R, Symmetric _ R ] : Morphism (R --> impl) (R x).
+  [ PER A R ] : Morphism (R --> impl) (R x) | 2.
 
   Next Obligation.
   Proof with auto.
-    transitivity x0...
+    transitivity x0... symmetry...
   Qed.
 
 Program Instance equivalence_partial_app_morphism
-  [ Equivalence A R ] : Morphism (R ==> iff) (R x).
+  [ Equivalence A R ] : Morphism (R ==> iff) (R x) | 1.
 
   Next Obligation.
   Proof with auto.
@@ -240,36 +237,16 @@ Program Instance equivalence_partial_app_morphism
    to get an [R y z] goal. *)
 
 Program Instance trans_co_eq_inv_impl_morphism
-  [ Transitive A R ] : Morphism (R ==> (@eq A) ==> inverse impl) R.
+  [ Transitive A R ] : Morphism (R ==> (@eq A) ==> inverse impl) R | 2.
 
   Next Obligation.
   Proof with auto.
     transitivity y...
   Qed.
 
-(* Program Instance [ Transitive A R ] =>  *)
-(*   trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R. *)
-
-(*   Next Obligation. *)
-(*   Proof with auto. *)
-(*     transitivity x... *)
-(*   Qed. *)
-
 (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
 
-Program Instance trans_sym_morphism
-  [ Transitive A R, Symmetric _ R ] : Morphism (R ==> R ==> iff) R.
-
-  Next Obligation.
-  Proof with auto.
-    split ; intros.
-    transitivity x0... transitivity x...
-  
-    transitivity y... transitivity y0... 
-  Qed.
-
-Program Instance equiv_morphism [ Equivalence A R ] :
-  Morphism (R ==> R ==> iff) R.
+Program Instance PER_morphism [ PER A R ] : Morphism (R ==> R ==> iff) R | 1.
 
   Next Obligation.
   Proof with auto.
@@ -293,6 +270,15 @@ Program Instance iff_impl_id :
 Program Instance inverse_iff_impl_id :
   Morphism (iff --> impl) id.
   
+Program Instance compose_morphism A B C R₀ R₁ R₂ :
+  Morphism ((R₁ ==> R₂) ==> (R₀ ==> R₁) ==> (R₀ ==> R₂)) (@compose A B C).
+
+  Next Obligation.
+  Proof.
+    simpl_relation.
+    unfold compose. apply H. apply H0. apply H1.
+  Qed.
+
 (** Coq functions are morphisms for leibniz equality, 
    applied only if really needed. *)
 
@@ -342,10 +328,6 @@ Instance morphism_morphism_proxy
   [ Morphism A R x ] : MorphismProxy A R x | 2.
 Proof. firstorder. Qed.
 
-(* Instance (A : Type) [ Reflexive B R ] => *)
-(*   eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *)
-(* Proof. simpl_relation. Qed. *)
-
 (** [R] is Reflexive, hence we can build the needed proof. *)
 
 Lemma Reflexive_partial_app_morphism [ Morphism (A -> B) (R ==> R') m, MorphismProxy A R x ] :
@@ -373,12 +355,11 @@ Ltac partial_application_tactic :=
     end
   in
   match goal with
+    | [ _ : subrelation_done |- _ ] => fail 1
+    | [ _ : normalization_done |- _ ] => fail 1      
     | [ |- @Morphism _ _ ?m ] => on_morphism m
   end.
 
-(* Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive A R ] (x : A) => *)
-(*   reflexive_partial_app_morphism : Morphism R' (m x). *)
-
 Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances.
 
 Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
@@ -406,8 +387,8 @@ Proof. firstorder. Qed.
 
 Instance inverse_respectful_rec_norm [ Normalizes B R' (inverse R'') ] :
   Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')).
-Proof. red ; intros.  
-  pose normalizes as r.
+Proof. red ; intros. 
+  assert(r:=normalizes).
   setoid_rewrite r.
   setoid_rewrite inverse_respectful.
   reflexivity.
@@ -415,8 +396,14 @@ Qed.
 
 (** Once we have normalized, we will apply this instance to simplify the problem. *)
 
-Program Instance morphism_inverse_morphism
-  [ Morphism A R m ] : Morphism (inverse R) m | 2.
+Definition morphism_inverse_morphism [ mor : Morphism A R m ] : Morphism (inverse R) m := mor.
+
+Ltac morphism_inverse :=
+  match goal with
+    [ |- @Morphism _ (flip _) _ ] => eapply @morphism_inverse_morphism
+  end.
+
+Hint Extern 2 (@Morphism _ _ _) => morphism_inverse : typeclass_instances.
 
 (** Bootstrap !!! *)
 
@@ -441,10 +428,9 @@ Proof.
   assumption.
 Qed.
 
-Inductive normalization_done : Prop := did_normalization.
-
 Ltac morphism_normalization := 
   match goal with
+    | [ _ : subrelation_done |- _ ] => fail 1
     | [ _ : normalization_done |- _ ] => fail 1
     | [ |- @Morphism _ _ _ ] => let H := fresh "H" in
       set(H:=did_normalization) ; eapply @morphism_releq_morphism
@@ -465,4 +451,4 @@ Ltac morphism_reflexive :=
     | [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism
   end.
 
-Hint Extern 4 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances.
+Hint Extern 7 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances.
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index 7dc1f95ef5..ec62e12ecd 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -29,7 +29,7 @@ Program Instance not_iff_morphism :
 
 (** Logical conjunction. *)
 
-Program Instance and_impl_iff_morphism :
+Program Instance and_impl_morphism :
   Morphism (impl ==> impl ==> impl) and.
 
 (* Program Instance and_impl_iff_morphism :  *)
@@ -49,7 +49,7 @@ Program Instance and_iff_morphism :
 
 (** Logical disjunction. *)
 
-Program Instance or_impl_iff_morphism : 
+Program Instance or_impl_morphism : 
   Morphism (impl ==> impl ==> impl) or.
 
 (* Program Instance or_impl_iff_morphism :  *)
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index 5018fa01ec..1b3896678a 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -48,3 +48,11 @@ Proof. intro. apply (predicate_equivalence_pointwise (cons A (cons A nil))). Qed
 Instance subrelation_pointwise :
   Morphism (subrelation ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) impl)) id.
 Proof. intro. apply (predicate_implication_pointwise (cons A (cons A nil))). Qed.
+
+
+Lemma inverse_pointwise_relation A (R : relation A) : 
+  relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)).
+Proof. intros. split; firstorder. Qed.
+
+
+
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 31398aa3b9..c4e98c24ab 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -21,13 +21,14 @@ Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 Require Export Coq.Relations.Relation_Definitions.
 
+(** We allow to unfold the [relation] definition while doing morphism search. *)
+
+Typeclasses unfold relation.
+
 Notation inverse R := (flip (R:relation _) : relation _).
 
 Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False.
 
-Definition pointwise_relation {A B : Type} (R : relation B) : relation (A -> B) := 
-  fun f g => forall x : A, R (f x) (g x).
-
 (** These are convertible. *)
 
 Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R).
@@ -394,7 +395,3 @@ Program Instance subrelation_partial_order :
   Proof.
     unfold relation_equivalence in *. firstorder.
   Qed.
-
-Lemma inverse_pointwise_relation A (R : relation A) : 
-  relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)).
-Proof. reflexivity. Qed.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 227a932071..adeb38d490 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -41,13 +41,13 @@ Typeclasses unfold equiv.
 (** Shortcuts to make proof search easier. *)
 
 Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv.
-Proof. eauto with typeclass_instances. Qed.
+Proof. typeclasses eauto. Qed.
 
 Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv.
-Proof. eauto with typeclass_instances. Qed.
+Proof. typeclasses eauto. Qed.
 
 Definition setoid_trans [ sa : Setoid A ] : Transitive equiv.
-Proof. eauto with typeclass_instances. Qed.
+Proof. typeclasses eauto. Qed.
 
 Existing Instance setoid_refl.
 Existing Instance setoid_sym.
@@ -123,7 +123,7 @@ Ltac setoidify := repeat setoidify_tac.
 (** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *)
 
 Program Definition setoid_morphism [ sa : Setoid A ] : Morphism (equiv ++> equiv ++> iff) equiv :=
-  trans_sym_morphism.
+  PER_morphism.
 
 (** Add this very useful instance in the database. *)
 
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index e033343d1d..20f4623f9f 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -660,6 +660,8 @@ Add Relation key E.eq
  transitivity proved by E.eq_trans 
  as KeySetoid.
 
+Typeclasses unfold key.
+
 Implicit Arguments Equal [[elt]].
 
 Add Parametric Relation (elt : Type) : (t elt) Equal  
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 6afb8fcb7b..4d24f54f45 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -309,6 +309,8 @@ Add Relation elt E.eq
  transitivity proved by E.eq_trans 
  as EltSetoid.
 
+Typeclasses unfold elt.
+
 Add Relation t Equal 
  reflexivity proved by eq_refl 
  symmetry proved by eq_sym
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 947dc818e1..bb2c01437d 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -102,6 +102,8 @@ exact sub_opp.
 exact add_opp.
 Qed.
 
+Typeclasses unfold NZadd NZmul NZsub NZeq.
+
 Add Ring BigZr : BigZring.
 
 (** Todo: tactic translating from [BigZ] to [Z] + omega *)
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index cbf6f701f2..5376027ddb 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -30,6 +30,7 @@ Module Make (N:NType) <: ZType.
   | Neg : N.t -> t_.
  
  Definition t := t_.
+ Typeclasses unfold t.
 
  Definition zero := Pos N.zero.
  Definition one  := Pos N.one.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 485480fa04..1e0b45cd2c 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -76,6 +76,8 @@ exact mul_assoc.
 exact mul_add_distr_r.
 Qed.
 
+Typeclasses unfold NZadd NZsub NZmul.
+
 Add Ring BigNr : BigNring.
 
 (** Todo: tactic translating from [BigN] to [Z] + omega *)
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 0baba94c6d..c360f53dc8 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -139,7 +139,7 @@ let _ =
   pr "";
   pr " Definition %s := %s_." t t;
   pr "";
-
+  pr " Typeclasses unfold %s." t;
   pr " Definition w_0 := w0_op.(znz_0).";
   pr "";