Proper implicit arguments handling for assumptions

(Axiom/Variable...). New tactic clapply to apply unapplied class methods
in tactic mode, simple solution to the fact that apply does not work
up-to classes yet. Add Functions.v for class definitions related to
functional morphisms.


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

6 files changed, 86 insertions, 15 deletions

diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
new file mode 100644
index 0000000000..7942d36427
--- /dev/null
+++ b/theories/Classes/Functions.v
@@ -0,0 +1,43 @@
+(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Functional morphisms.
+ 
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+   91405 Orsay, France *)
+
+(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+
+Require Import Coq.Program.Program.
+Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.Morphisms.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Injective :=
+  injective : forall x y : A, RB (f x) (f y) -> RA x y.
+
+Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Surjective :=
+  surjective : forall y, exists x : A, RB y (f x).
+
+Definition Bijective [ m : Morphism (A -> B) (RA ++> RB) (f : A -> B) ] :=
+  Injective m /\ Surjective m.
+
+Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism :=
+  monic :> Injective m.
+
+Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism :=
+  epic :> Surjective m.
+
+Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism :=
+  monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m.
+
+Class [ m : Morphism (A -> A) (eqA ++> eqA), ? IsoMorphism m ] => AutoMorphism.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index beeb745899..cb27fbc380 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -16,3 +16,6 @@
 (* $Id: Init.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
 (* Ltac typeclass_instantiation := typeclasses eauto || eauto. *)
+
+Tactic Notation "clapply" ident(c) :=
+  eapply @c ; eauto with typeclass_instances.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 3ba6c1824b..18dc3190f2 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -133,6 +133,13 @@ Program Instance (A : Type) (R : relation A) `B` (R' : relation B)
 
 Program Instance iff_iff_iff_impl_morphism : ? Morphism (iff ++> iff ++> iff) impl.
 
+Lemma reflexive_impl_iff [ Symmetric A R, ? Morphism (R ++> impl) m ] : Morphism (R ==> iff) m.
+Proof.
+  intros.
+  constructor ; simpl_relation.
+  split ; clapply respect ; [ idtac | sym ] ; auto.
+Qed.
+
 (** The complement of a relation conserves its morphisms. *)
 
 Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => 
@@ -158,6 +165,15 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] =>
     apply respect ; auto.
   Qed.
 
+Program Instance (A B C : Type) [ ? Morphism (RA ++> RB ++> RC) (f : A -> B -> C) ] => 
+  flip_morphism : ? Morphism (RB ++> RA ++> RC) (flip f).
+
+  Next Obligation.
+  Proof.
+    unfold flip. 
+    apply respect ; auto.
+  Qed.
+
 (* Definition respectful' A (R : relation A) B (R' : relation B) (f : A -> B) : relation A := *)
 (*   fun x y => R x y -> R' (f x) (f y). *)
 
diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v
index c05a4b1e12..0d21985dcf 100644
--- a/theories/Classes/Relations.v
+++ b/theories/Classes/Relations.v
@@ -17,7 +17,7 @@
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
 Require Import Coq.Program.Program.
-Require Import Coq.Classes.Init.
+Require Export Coq.Classes.Init.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -71,15 +71,15 @@ Program Instance [ Irreflexive A R ] => flip_irreflexive : Irreflexive A (flip R
 
 Program Instance [ Symmetric A R ] => flip_symmetric : Symmetric A (flip R).
 
-  Solve Obligations using unfold flip ; program_simpl ; apply symmetric ; eauto.
+  Solve Obligations using unfold flip ; program_simpl ; clapply symmetric.
 
 Program Instance [ Asymmetric A R ] => flip_asymmetric : Asymmetric A (flip R).
   
-  Solve Obligations using program_simpl ; unfold flip in * ; intros ; eapply asymmetric ; eauto.
+  Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetric.
 
 Program Instance [ Transitive A R ] => flip_transitive : Transitive A (flip R).
 
-  Solve Obligations using unfold flip ; program_simpl ; eapply transitive ; eauto.
+  Solve Obligations using unfold flip ; program_simpl ; clapply transitive.
 
 (** Have to do it again for Prop. *)
 
@@ -91,15 +91,15 @@ Program Instance [ Irreflexive A (R : relation A) ] => inverse_irreflexive : Irr
 
 Program Instance [ Symmetric A (R : relation A) ] => inverse_symmetric : Symmetric A (inverse R).
 
-  Solve Obligations using unfold inverse, flip ; program_simpl ; eapply symmetric ; eauto.
+  Solve Obligations using unfold inverse, flip ; program_simpl ; clapply symmetric.
 
 Program Instance [ Asymmetric A (R : relation A) ] => inverse_asymmetric : Asymmetric A (inverse R).
   
-  Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; eapply asymmetric ; eauto.
+  Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; clapply asymmetric.
 
 Program Instance [ Transitive A (R : relation A) ] => inverse_transitive : Transitive A (inverse R).
 
-  Solve Obligations using unfold inverse, flip ; program_simpl ; eapply transitive ; eauto.
+  Solve Obligations using unfold inverse, flip ; program_simpl ; clapply transitive.
 
 Program Instance [ Reflexive A (R : relation A) ] => 
   reflexive_complement_irreflexive : Irreflexive A (complement R).
@@ -190,6 +190,12 @@ Ltac relation_refl :=
 
     | [ |- ?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)
+
+    | [ |- ?R ?A ?B ?C ?D ?E ?F ?G ?X ?X ] => apply (reflexive (R:=R A B C D E F G) X)
+    | [ H : ?R ?A ?B ?C ?D ?E ?F ?G ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D E F G) H)
+
+    | [ |- ?R ?A ?B ?C ?D ?E ?F ?G ?H ?X ?X ] => apply (reflexive (R:=R A B C D E F G H) X)
+    | [ H : ?R ?A ?B ?C ?D ?E ?F ?G ?H ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D E F G H) H)
   end.
 
 Ltac refl := relation_refl.
@@ -284,6 +290,12 @@ Ltac trans Y := relation_transitive Y.
 
 Ltac relation_tac := relation_refl || relation_sym || relation_trans.
 
+(** Various combinations of reflexivity, symmetry and transitivity. *)
+
+Class PreOrder A (R : relation A) :=
+  preorder_refl :> Reflexive R ;
+  preorder_trans :> Transitive R.
+
 (** The [PER] typeclass. *)
 
 Class PER (carrier : Type) (pequiv : relation carrier) :=
@@ -340,3 +352,4 @@ Program Instance [ sa : Equivalence a R, sb : Equivalence b R' ] => equiv_setoid
   Equivalence (a -> b)
   (fun f g => forall (x y : a), R x y -> R' (f x) (g y)).
 *)
+
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index cd7737d06d..9ec955bcfe 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -24,6 +24,7 @@ Unset Strict Implicit.
 
 Require Export Coq.Classes.Relations.
 Require Export Coq.Classes.Morphisms.
+Require Export Coq.Classes.Functions.
 
 (** A setoid wraps an equivalence. *)
 
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index fb7f8827bf..953296c28c 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -25,17 +25,12 @@ Require Export Coq.Classes.SetoidClass.
 (* Application of the extensionality axiom to turn a goal on leibinz equality to 
    a setoid equivalence. *)
 
-Lemma setoideq_eq [ sa : Setoid a ] : forall x y : a, x == y -> x = y.
-Proof.
-  admit.
-Qed.
-
-Implicit Arguments setoideq_eq [[a] [sa]].
+Axiom setoideq_eq : forall [ sa : Setoid a ] (x y : a), x == y -> x = y.
 
 (** Application of the extensionality principle for setoids. *)
 
-Ltac setoideq_ext :=
+Ltac setoid_extensionality :=
   match goal with
-    [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) X Y)
+    [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y))
   end.