New tactics [conv] to test convertibility (actually, unification) of two

terms and [head_of_constr id] to put the head of a constr in some new
hypothesis. Both are used in a new tactic to deal with partial
applications in setoid_rewrite. Also fix bug #1905 by using
[subrelation] to take care of [Morphism (R ==> R') id] constraints.


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

8 files changed, 131 insertions, 46 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 700ce5895a..5cd656e910 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -760,11 +760,11 @@ let allowK = true
 
 let refresh_hypinfo env sigma hypinfo = 
   if !hypinfo.abs = None then
-    let {l2r=l2r; c = c} = !hypinfo in
+    let {l2r=l2r; c = c;cl=cl} = !hypinfo in
       match c with 
 	| Some c ->
 	    (* Refresh the clausenv to not get the same meta twice in the goal. *)
-	    hypinfo := decompose_setoid_eqhyp env sigma c l2r;
+	    hypinfo := decompose_setoid_eqhyp cl.env (Evd.evars_of cl.evd) c l2r;
 	| _ -> ()
   else ()
 
@@ -1723,6 +1723,21 @@ TACTIC EXTEND apply_typeclasses
    ]
 END
 
+let rec head_of_constr t =
+  let t = strip_outer_cast(collapse_appl t) in
+    match kind_of_term t with
+    | Prod (_,_,c2)  -> head_of_constr c2 
+    | LetIn (_,_,_,c2) -> head_of_constr c2
+    | App (f,args)  -> head_of_constr f
+    | _      -> t
+      
+TACTIC EXTEND head_of_constr
+  [ "head_of_constr" ident(h) constr(c) ] -> [
+    let c = head_of_constr c in
+      letin_tac None (Name h) c allHyps
+  ]
+END
+
 (* TACTIC EXTEND solve_evar *)
 (*   [ "solve_evar" int_or_var(n) ] -> [ fun gl -> *)
 (*     let n = match n with ArgArg i -> pred i | _ -> assert false in *)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 5d374215de..19ce087113 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -504,3 +504,6 @@ TACTIC EXTEND generalize_eqs
 | ["generalize_eqs" hyp(id) ] -> [ abstract_generalize id ]
 END
 
+TACTIC EXTEND conv
+| ["conv" constr(x) constr(y) ] -> [ conv x y ]
+END
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8c84b40d15..586283d5a3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -689,6 +689,13 @@ let simplest_case c = general_case_analysis false (c,NoBindings)
 (*            Resolution tactics                    *)
 (****************************************************)
 
+let resolve_classes gl =
+  let env = pf_env gl and evd = project gl in
+    if evd = Evd.empty then tclIDTAC gl
+    else
+      let evd' = Typeclasses.resolve_typeclasses env (Evd.create_evar_defs evd) in
+	(tclTHEN (tclEVARS (Evd.evars_of evd')) tclNORMEVAR) gl
+
 (* Resolution with missing arguments *)
 
 let general_apply with_delta with_destruct with_evars (c,lbind) gl =
@@ -2925,3 +2932,8 @@ let admit_as_an_axiom gl =
     (applist (axiom, 
               List.rev (Array.to_list (instance_from_named_context sign))))
     gl
+
+let conv x y gl =
+  try let evd = Evarconv.the_conv_x_leq (pf_env gl) x y (Evd.create_evar_defs (project gl)) in
+	tclEVARS (Evd.evars_of evd) gl
+  with _ -> tclFAIL 0 (str"Not convertible") gl
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 700c25f6e8..cbf27b0320 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -339,6 +339,8 @@ val generalize      : constr list -> tactic
 val generalize_gen  : ((occurrences * constr) * name) list -> tactic
 val generalize_dep  : constr  -> tactic
 
+val conv            : constr -> constr -> tactic
+
 val tclABSTRACT : identifier option -> tactic -> tactic
 
 val admit_as_an_axiom : tactic
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index d77704c12a..84aa9cf06b 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -54,6 +54,9 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
 
 Program Instance equiv_reflexive [ sa : Equivalence A ] : Reflexive equiv.
 
+  Next Obligation.
+  Proof. reflexivity. Qed.
+
 Program Instance equiv_symmetric [ sa : Equivalence A ] : Symmetric equiv.
 
   Next Obligation.
@@ -116,7 +119,7 @@ Section Respecting.
   Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := 
     { morph : A -> B | respectful R R' morph morph }.
   
-  Program Instance respecting_equiv [ Equivalence A R, Equivalence B R' ] :
+  Program Instance respecting_equiv [ eqa : Equivalence A R, eqb : Equivalence B R' ] :
     Equivalence respecting
     (fun (f g : respecting) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
 
@@ -124,19 +127,24 @@ Section Respecting.
 
   Next Obligation.
   Proof. 
-    unfold respecting in *. program_simpl. red in H2,H3,H4. 
-    transitivity (y x0) ; auto.
+    unfold respecting in *. program_simpl. destruct eqa ; destruct eqb. red in H2,H1 ; auto.
+  Qed.
+
+  Next Obligation.
+  Proof.
+    unfold respecting in *. program_simpl. destruct eqa ; destruct eqb. red in H2,H3,H4.
     transitivity (y y0) ; auto.
-    symmetry. auto.
   Qed.
 
 End Respecting.
 
 (** The default equivalence on function spaces, with higher-priority than [eq]. *)
 
-Program Instance pointwise_equivalence [ Equivalence B eqB ] :
+Program Instance pointwise_equivalence [ eqb : Equivalence B eqB ] :
   Equivalence (A -> B) (pointwise_relation eqB) | 9.
 
+  Solve Obligations using simpl_relation ; first [ reflexivity | (symmetry ; auto) ].
+
   Next Obligation.
   Proof.
     transitivity (y x0) ; auto.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 43320dcebc..54c97ae7b5 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -19,3 +19,16 @@
 
 Tactic Notation "clapply" ident(c) :=
   eapply @c ; eauto with typeclass_instances.
+
+(** The unconvertible typeclass, to test that two objects of the same type are 
+   actually different. *)
+
+Class Unconvertible (A : Type) (a b : A).
+
+Ltac unconvertible :=
+  match goal with
+    | |- @Unconvertible _ ?x ?y => conv x y ; fail 1 "Convertible"
+    | |- _ => apply Build_Unconvertible 
+  end.
+
+Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances.
\ No newline at end of file
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 2c1a7deb99..0a099e135b 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-name: "coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *)
+(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -87,19 +87,28 @@ 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. *)
 
+Hint Unfold Reflexive : core.
+Hint Unfold Symmetric : core.
+Hint Unfold Transitive : core.
+
 Program Instance respectful_per [ PER A (R : relation A), PER B (R' : relation B) ] : 
   PER (A -> B) (R ==> R').
 
   Next Obligation.
   Proof with auto.
+    destruct PER0 ; destruct PER1 ; auto.
+  Qed.
+
+  Next Obligation.
+  Proof with auto. destruct PER0 ; destruct PER1.
     assert(R x0 x0). 
     transitivity y0... symmetry...
     transitivity (y x0)...
   Qed.
 
-(** Subrelations induce a morphism on the identity, not used for morphism search yet. *)
+(** Subrelations induce a morphism on the identity. *)
 
-Lemma subrelation_id_morphism [ subrelation A R₁ R₂ ] : Morphism (R₁ ==> R₂) id.
+Instance subrelation_id_morphism [ subrelation A R₁ R₂ ] : Morphism (R₁ ==> R₂) id.
 Proof. firstorder. Qed.
 
 (** The subrelation property goes through products as usual. *)
@@ -115,7 +124,8 @@ Proof. simpl_relation. Qed.
 
 (** [Morphism] is itself a covariant morphism for [subrelation]. *)
 
-Lemma subrelation_morphism [ mor : Morphism A R₁ m, sub : subrelation A R₁ R₂ ] : Morphism R₂ m.
+Lemma subrelation_morphism [ mor : Morphism A R₁ m, unc : Unconvertible (relation A) R₁ R₂,
+  sub : subrelation A R₁ R₂ ] : Morphism R₂ m.
 Proof.
   intros. apply sub. apply mor.
 Qed.
@@ -256,19 +266,8 @@ Program Instance PER_morphism [ PER A R ] : Morphism (R ==> R ==> iff) R | 1.
     transitivity y... transitivity y0... symmetry...
   Qed.
 
-(** In case the rewrite happens at top level. *)
-
-Program Instance iff_inverse_impl_id :
-  Morphism (iff ==> inverse impl) id.
-
-Program Instance inverse_iff_inverse_impl_id :
-  Morphism (iff --> inverse impl) id.
-  
-Program Instance iff_impl_id :
-  Morphism (iff ==> impl) id.
-
-Program Instance inverse_iff_impl_id :
-  Morphism (iff --> impl) id.
+Lemma symmetric_equiv_inverse [ Symmetric A R ] : relation_equivalence R (flip R).
+Proof. firstorder. Qed.
   
 Program Instance compose_morphism A B C R₀ R₁ R₂ :
   Morphism ((R₁ ==> R₂) ==> (R₀ ==> R₁) ==> (R₀ ==> R₂)) (@compose A B C).
@@ -282,10 +281,6 @@ Program Instance compose_morphism A B C R₀ R₁ R₂ :
 (** Coq functions are morphisms for leibniz equality, 
    applied only if really needed. *)
 
-(* Instance (A : Type) [ Reflexive B R ] => *)
-(*   eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *)
-(* Proof. simpl_relation. Qed. *)
-
 Instance reflexive_eq_dom_reflexive (A : Type) [ Reflexive B R' ] :
   Reflexive (@Logic.eq A ==> R').
 Proof. simpl_relation. Qed.
@@ -334,32 +329,69 @@ Lemma Reflexive_partial_app_morphism [ Morphism (A -> B) (R ==> R') m, MorphismP
    Morphism R' (m x).
 Proof. simpl_relation. Qed.
 
+Class Params {A : Type} (of : A) (arity : nat).
+
+Class PartialApplication.
+
 Ltac partial_application_tactic := 
-  let tac x :=
-    match type of x with
-      | Type => fail 1
-      | _ => eapply @Reflexive_partial_app_morphism
+  let rec do_partial_apps H m :=
+    match m with
+      | ?m' ?x => eapply @Reflexive_partial_app_morphism ; [do_partial_apps H m'|clear H]
+      | _ => idtac
     end
   in
-  let on_morphism m :=
-    match m with
-      | ?m' ?x => tac x
-      | ?m' _ ?x => tac x
-      | ?m' _ _ ?x => tac x
-      | ?m' _ _ _ ?x => tac x
-      | ?m' _ _ _ _ ?x => tac x
-      | ?m' _ _ _ _ _ ?x => tac x
-      | ?m' _ _ _ _ _ _ ?x => tac x
-      | ?m' _ _ _ _ _ _ _ ?x => tac x
-      | ?m' _ _ _ _ _ _ _ _ ?x => tac x
+  let rec do_partial H ar m :=
+    match ar with
+      | 0 => do_partial_apps H m
+      | S ?n' => 
+        match m with
+          ?m' ?x => do_partial H n' m'
+        end
     end
   in
+  let on_morphism m :=
+    let m' := fresh in head_of_constr m' m ;
+    let n := fresh in evar (n:nat) ;
+    let v := eval compute in n in clear n ;
+    let H := fresh in
+      assert(H:Params m' v) by typeclasses eauto ;
+      let v' := eval compute in v in 
+      do_partial H v' m
+ in
   match goal with
     | [ _ : subrelation_done |- _ ] => fail 1
-    | [ _ : normalization_done |- _ ] => fail 1      
-    | [ |- @Morphism _ _ ?m ] => on_morphism m
+    | [ _ : normalization_done |- _ ] => fail 1
+    | [ _ : @Params _ _ _ |- _ ] => fail 1
+    | [ |- @Morphism ?T _ (?m ?x) ] => 
+      match goal with 
+        | [ _ : PartialApplication |- _ ] => 
+          eapply @Reflexive_partial_app_morphism
+        | _ => 
+          on_morphism (m x) || 
+            (eapply @Reflexive_partial_app_morphism ;
+              [ pose Build_PartialApplication | idtac ])
+      end
   end.
 
+Section PartialAppTest.
+  Instance and_ar : Params and 0.
+
+  Goal Morphism (iff) (and True True).
+    partial_application_tactic.
+  Admitted.
+
+  Goal Morphism (iff) (or True True).
+    partial_application_tactic.
+    partial_application_tactic. 
+  Admitted.
+
+  Goal Morphism (iff ==> iff) (iff True).
+    partial_application_tactic.
+    (*partial_application_tactic. *)
+   Admitted.
+
+End PartialAppTest.
+
 Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances.
 
 Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index ddd7b38da4..bdd7b4b1d1 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -367,7 +367,7 @@ Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Q
    We give an equivalent definition, up-to an equivalence relation 
    on the carrier. *)
 
-Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder :=
+Class [ equ : Equivalence A eqA, preo : PreOrder A R ] => PartialOrder :=
   partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)).
 
 (** The equivalence proof is sufficient for proving that [R] must be a morphism