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

9 files changed, 101 insertions, 23 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.
 
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 6e07ea43a9..87cd9becc0 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -157,7 +157,7 @@ Section Well_founded_2.
    P x x' :=
     F
       (fun (y:A) (y':B) (h:R (y, y') (x, x')) =>
-         Acc_iter_2 (x:=y) (x':=y') (Acc_inv a (y, y') h)).
+         Acc_iter_2 (x:=y) (x':=y') (Acc_inv a h)).
   End Acc_iter_2.
 
   Hypothesis Rwf : well_founded R.
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 3040dd04ba..8a3e5dccd9 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -1,3 +1,4 @@
+(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -18,7 +19,7 @@ Unset Strict Implicit.
 
 Require Export Coq.Program.FunctionalExtensionality.
 
-Notation  "'λ' x : T , y" := (fun x:T => y) (at level 1, x,T,y at level 10) : program_scope.
+Notation  " 'λ' x : T , y " := (fun x:T => y) (at level 100, x,T,y at level 10, no associativity) : program_scope.
 
 Open Scope program_scope.
 
@@ -45,7 +46,7 @@ Proof.
 Qed.
 
 Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D), 
-  h ∘ (g ∘ f) = h ∘ g ∘ f.
+  h ∘ g ∘ f = h ∘ (g ∘ f).
 Proof.
   intros.
   reflexivity.
@@ -117,7 +118,7 @@ Qed.
 
 (** Useful implicits and notations for lists. *)
 
-Require Export Coq.Lists.List.
+Require Import Coq.Lists.List.
 
 Implicit Arguments nil [[A]].
 Implicit Arguments cons [[A]].
@@ -141,3 +142,9 @@ Tactic Notation "exist" constr(x) := exists x.
 Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y.
 Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z.
 Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w.
+
+(* Notation " 'Σ' x : T , p" := (sigT (fun x : T => p)) *)
+(*   (at level 200, x ident, y ident, right associativity) : program_scope. *)
+
+(* Notation " 'Π' x : T , p " := (forall x : T, p) *)
+(*   (at level 200, x ident, right associativity) : program_scope. *)
\ No newline at end of file
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 70b1b1b5a2..98b18f9030 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -17,7 +17,7 @@ Section Well_founded.
     
     Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x :=
       F_sub x (fun y: { y : A | R y x}  => Fix_F_sub (proj1_sig y) 
-        (Acc_inv r (proj1_sig y) (proj2_sig y))).
+        (Acc_inv r (proj2_sig y))).
     
     Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
   End Acc.
@@ -38,7 +38,7 @@ Section Well_founded.
 
     Lemma Fix_F_eq :
       forall (x:A) (r:Acc R x),
-        F_sub x (fun (y:A|R y x) => Fix_F (`y) (Acc_inv r (proj1_sig y) (proj2_sig y))) = Fix_F x r.
+        F_sub x (fun (y:A|R y x) => Fix_F (`y) (Acc_inv r (proj2_sig y))) = Fix_F x r.
     Proof. 
       destruct r using Acc_inv_dep; auto.
     Qed.
@@ -89,7 +89,7 @@ Section Well_founded_measure.
     
     Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x :=
       F_sub x (fun y: { y : A | m y < m x}  => Fix_measure_F_sub (proj1_sig y) 
-        (Acc_inv r (m (proj1_sig y)) (proj2_sig y))).
+        (@Acc_inv _ _ _ r (m (proj1_sig y)) (proj2_sig y))).
     
     Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)).
   
@@ -111,7 +111,7 @@ Section Well_founded_measure.
 
     Lemma Fix_measure_F_eq :
       forall (x:A) (r:Acc lt (m x)),
-        F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (m (proj1_sig y)) (proj2_sig y))) = Fix_F x r.
+        F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (proj2_sig y))) = Fix_F x r.
     Proof.
       intros x.
       set (y := m x).