Reorganize Program and Classes theories. Requiring Setoid no longer sets

implicits for left, inl or eq, hence some theories had to be changed
again. It should make some user contribs compile again too. Also
do not import functional extensionality when importing Program.Basics,
add a Combinators file for proofs requiring it and a Syntax file for the
implicit settings. Move Classes.Relations to Classes.RelationClasses to
avoid name clash warnings as advised by Hugo and Pierre.


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

Author: msozeau

Makefile.common

@@ -748,7 +748,7 @@ SETOIDSVO:= theories/Setoids/Setoid.vo # theories/Setoids/Setoid_tac.vo theories
 
 UNICODEVO:= theories/Unicode/Utf8.vo
 
-CLASSESVO:= theories/Classes/Init.vo theories/Classes/Relations.vo theories/Classes/Morphisms.vo \
+CLASSESVO:= theories/Classes/Init.vo theories/Classes/RelationClasses.vo theories/Classes/Morphisms.vo \
 	theories/Classes/Functions.vo theories/Classes/Equivalence.vo theories/Classes/SetoidTactics.vo \
 	theories/Classes/SetoidClass.vo theories/Classes/SetoidAxioms.vo theories/Classes/SetoidDec.vo
 
@@ -806,8 +806,9 @@ CCVO:=
 DPVO:=contrib/dp/Dp.vo
 
 SUBTACVO:=theories/Program/Tactics.vo theories/Program/Equality.vo theories/Program/Subset.vo \
-	theories/Program/Utils.vo theories/Program/Wf.vo theories/Program/Program.vo \
-	theories/Program/FunctionalExtensionality.vo theories/Program/Basics.vo
+	theories/Program/Utils.vo theories/Program/Wf.vo theories/Program/Basics.vo \
+	theories/Program/FunctionalExtensionality.vo theories/Program/Combinators.vo \
+	theories/Program/Syntax.vo theories/Program/Program.vo 
 
 RTAUTOVO:= \
  contrib/rtauto/Bintree.vo contrib/rtauto/Rtauto.vo

contrib/rtauto/Bintree.v

@@ -107,7 +107,7 @@ intro ne;right;congruence.
 left;reflexivity.
 Defined.
 
-Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left (refl_equal m).
+Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left _ (refl_equal m).
 fix 1;intros [mm|mm|].
 simpl; rewrite  pos_eq_dec_refl; reflexivity.
 simpl; rewrite  pos_eq_dec_refl; reflexivity.
@@ -116,7 +116,7 @@ Qed.
 
 Theorem pos_eq_dec_ex : forall m n,
  pos_eq m n =true -> exists h:m=n,
- pos_eq_dec m n = left h.
+ pos_eq_dec m n = left _ h.
 fix 1;intros [mm|mm|] [nn|nn|];try (simpl;congruence).
 simpl;intro e.
 elim (pos_eq_dec_ex _ _ e).

tactics/class_tactics.ml4

@@ -360,28 +360,25 @@ let impl = lazy (gen_constant ["Program"; "Basics"] "impl")
 let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow")
 let coq_id = lazy (gen_constant ["Program"; "Basics"] "id")
 
-let reflexive_type = lazy (gen_constant ["Classes"; "Relations"] "Reflexive")
-let reflexive_proof = lazy (gen_constant ["Classes"; "Relations"] "reflexive")
+let reflexive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Reflexive")
+let reflexive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "reflexive")
 
-let symmetric_type = lazy (gen_constant ["Classes"; "Relations"] "Symmetric")
-let symmetric_proof = lazy (gen_constant ["Classes"; "Relations"] "symmetric")
+let symmetric_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Symmetric")
+let symmetric_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "symmetric")
 
-let transitive_type = lazy (gen_constant ["Classes"; "Relations"] "Transitive")
-let transitive_proof = lazy (gen_constant ["Classes"; "Relations"] "transitive")
+let transitive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Transitive")
+let transitive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "transitive")
 
-let inverse = lazy (gen_constant ["Classes"; "Relations"] "inverse")
+let inverse = lazy (gen_constant ["Classes"; "RelationClasses"] "inverse")
 
 let respectful_dep = lazy (gen_constant ["Classes"; "Morphisms"] "respectful_dep")
 let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful")
 
-let equivalence = lazy (gen_constant ["Classes"; "Relations"] "Equivalence")
-let default_relation = lazy (gen_constant ["Classes"; "Relations"] "DefaultRelation")
+let equivalence = lazy (gen_constant ["Classes"; "RelationClasses"] "Equivalence")
+let default_relation = lazy (gen_constant ["Classes"; "RelationClasses"] "DefaultRelation")
 
-let iff_equiv = lazy (gen_constant ["Classes"; "Relations"] "iff_equivalence")
-let eq_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_equivalence")
-
-(* let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") *)
-let coq_relation = lazy (gen_constant ["Classes";"Relations"] "relation")
+(* let coq_relation = lazy (gen_constant ["RelationClasses";"Relation_Definitions"] "relation") *)
+let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation")
 let coq_relation a = mkApp (Lazy.force coq_relation, [| a |])
 let coq_relationT = lazy (gen_constant ["Classes";"Relations"] "relationT")
 

theories/Classes/Equivalence.v

@@ -8,7 +8,6 @@
 (************************************************************************)
 
 (* Typeclass-based setoids, tactics and standard instances.
-   TODO: explain clrewrite, clsubstitute and so on.
  
    Author: Matthieu Sozeau
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
@@ -17,10 +16,10 @@
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
 Require Export Coq.Program.Basics.
-Require Import Coq.Program.Program.
+Require Import Coq.Program.Tactics.
 
 Require Import Coq.Classes.Init.
-Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
 Require Export Coq.Classes.SetoidTactics.
 

theories/Classes/Functions.v

@@ -16,7 +16,7 @@
 (* $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.RelationClasses.
 Require Export Coq.Classes.Morphisms.
 
 Set Implicit Arguments.

theories/Classes/Morphisms.v

@@ -15,8 +15,9 @@
 
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
-Require Import Coq.Program.Program.
-Require Export Coq.Classes.Relations.
+Require Import Coq.Program.Basics.
+Require Import Coq.Program.Tactics.
+Require Export Coq.Classes.RelationClasses.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -53,6 +54,7 @@ Class Morphism A (R : relation A) (m : A) :=
 Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := 
   { morph : A -> B | respectful R R' morph morph }.
 
+
 Ltac obligations_tactic ::= program_simpl.
 
 Program Instance [ Equivalence A R, Equivalence B R' ] => 
@@ -180,8 +182,6 @@ Hint Resolve @subrelation_morphism 4 : typeclass_instances.
 
 (* Hint Resolve @subrelation_morphism 4 : typeclass_instances. *)
 
-
-
 (* Program Instance `A` (R : relation A) `B` (R' : relation B) *)
 (*   [ ? Morphism (R ==> R' ==> iff) m ] => *)
 (*   iff_impl_binary_morphism : ? Morphism (R ==> R' ==> impl) m. *)
@@ -381,7 +381,7 @@ Program Instance (A B : Type) (R : relation A) (R' : relation B)
    to get an [R y z] goal. *)
 
 Program Instance [ ! Transitive A R ] => 
-  trans_co_eq_inv_impl_morphism : Morphism (R ==> eq ==> inverse impl) R.
+  trans_co_eq_inv_impl_morphism : Morphism (R ==> (@eq A) ==> inverse impl) R.
 
   Next Obligation.
   Proof with auto.
@@ -390,7 +390,7 @@ Program Instance [ ! Transitive A R ] =>
   Qed.
 
 Program Instance [ ! Transitive A R ] => 
-  trans_contra_eq_impl_morphism : Morphism (R --> eq ==> impl) R.
+  trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R.
 
   Next Obligation.
   Proof with auto.

theories/Classes/Relations.v theories/Classes/RelationClasses.v

@@ -17,15 +17,13 @@
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
 Require Export Coq.Classes.Init.
-Require Import Coq.Program.Program.
+Require Import Coq.Program.Basics.
+Require Import Coq.Program.Tactics.
+Require Export Coq.Relations.Relation_Definitions.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(* Notation "'relation' A " := (A -> A -> Prop) (at level 0). *)
-
-Definition relation A := A -> A -> Prop.
-
 (** Default relation on a given support. *)
 
 Class DefaultRelation A (R : relation A).
@@ -35,14 +33,12 @@ Class DefaultRelation A (R : relation A).
 Definition default_relation [ DefaultRelation A R ] : relation A := R.
 
 (** A notation for applying the default relation to [x] and [y]. *)
-Notation " x ===def y " := (default_relation x y) (at level 70, no associativity).
 
-Definition inverse A (R : relation A) : relation A := fun x y => R y x.
+Notation " x ===def y " := (default_relation x y) (at level 70, no associativity).
 
-Lemma inverse_inverse : forall A (R : relation A), inverse (inverse R) = R.
-Proof. intros ; unfold inverse. apply (flip_flip R). Qed.
+Definition inverse {A} : relation A -> relation A := flip.
 
-Definition complement A (R : relation A) : relation A := fun x y => R x y -> False.
+Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False.
 
 (** These are convertible. *)
 
@@ -355,7 +351,7 @@ Program Instance [ eq : Equivalence A eqA, Antisymmetric eq (R : relation A) ] =
 
 (** Leibinz equality [eq] is an equivalence relation. *)
 
-Program Instance eq_equivalence : Equivalence A eq.
+Program Instance eq_equivalence : Equivalence A (@eq A).
 
 (** Logical equivalence [iff] is an equivalence relation. *)
 

theories/Classes/SetoidClass.v

@@ -22,7 +22,7 @@ Require Import Coq.Classes.Init.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
 Require Export Coq.Classes.Functions.
 

theories/Classes/SetoidTactics.v

@@ -15,7 +15,7 @@
 
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
-Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
 
 Set Implicit Arguments.

theories/FSets/FMapFacts.v

@@ -675,7 +675,7 @@ rewrite (In_iff m Hk), in_find_iff, in_find_iff, Hm; intuition.
 Qed.
 
 Add Morphism (@MapsTo elt)
- with signature E.eq ==> Logic.eq ==> Equal ==> iff as MapsTo_m.
+ with signature E.eq ==> @Logic.eq _ ==> Equal ==> iff as MapsTo_m.
 Proof.
 unfold Equal; intros k k' Hk e m m' Hm.
 rewrite (MapsTo_iff m e Hk), find_mapsto_iff, find_mapsto_iff, Hm; 
@@ -689,19 +689,19 @@ rewrite <-Hm in H0; eauto.
 rewrite Hm in H0; eauto.
 Qed.
 
-Add Morphism (@is_empty elt) with signature Equal ==> Logic.eq as is_empty_m.
+Add Morphism (@is_empty elt) with signature Equal ==> @Logic.eq _ as is_empty_m.
 Proof.
 intros m m' Hm.
 rewrite eq_bool_alt, <-is_empty_iff, <-is_empty_iff, Hm; intuition.
 Qed.
 
-Add Morphism (@mem elt) with signature E.eq ==> Equal ==> Logic.eq as mem_m.
+Add Morphism (@mem elt) with signature E.eq ==> Equal ==> @Logic.eq _ as mem_m.
 Proof.
 intros k k' Hk m m' Hm.
 rewrite eq_bool_alt, <- mem_in_iff, <-mem_in_iff, Hk, Hm; intuition.
 Qed.
 
-Add Morphism (@find elt) with signature E.eq ==> Equal ==> Logic.eq as find_m.
+Add Morphism (@find elt) with signature E.eq ==> Equal ==> @Logic.eq _ as find_m.
 Proof.
 intros k k' Hk m m' Hm.
 generalize (find_mapsto_iff m k)(find_mapsto_iff m' k')
@@ -713,7 +713,7 @@ symmetry; rewrite <- H2, <-Hk, <-Hm, H1; auto.
 Qed.
 
 Add Morphism (@add elt) with signature 
- E.eq ==> Logic.eq ==> Equal ==> Equal as add_m.
+ E.eq ==> @Logic.eq _ ==> Equal ==> Equal as add_m.
 Proof.
 intros k k' Hk e m m' Hm y.
 rewrite add_o, add_o; do 2 destruct eq_dec; auto.
@@ -730,7 +730,7 @@ elim n; rewrite <-Hk; auto.
 elim n; rewrite Hk; auto.
 Qed.
 
-Add Morphism (@map elt elt') with signature Logic.eq ==> Equal ==> Equal as map_m.
+Add Morphism (@map elt elt') with signature @Logic.eq _ ==> Equal ==> Equal as map_m.
 Proof.
 intros f m m' Hm y.
 rewrite map_o, map_o, Hm; auto.
@@ -1104,7 +1104,7 @@ Module WProperties (E:DecidableType)(M:WSfun E).
 
  End Elt.
 
- Add Morphism (@cardinal elt) with signature Equal ==> Logic.eq as cardinal_m.
+ Add Morphism (@cardinal elt) with signature Equal ==> @Logic.eq _ as cardinal_m.
  Proof. intros; apply Equal_cardinal; auto. Qed.
 
 End WProperties.

theories/Numbers/Natural/Abstract/NBase.v

@@ -81,7 +81,7 @@ function (by recursion) that maps 0 to false and the successor to true *)
 Definition if_zero (A : Set) (a b : A) (n : N) : A :=
   recursion a (fun _ _ => b) n.
 
-Add Morphism (if_zero A) with signature (eq ==> eq ==> Neq ==> eq) as if_zero_wd.
+Add Morphism (if_zero A) with signature ((@eq (A:Set)) ==> (@eq A) ==> Neq ==> (@eq A)) as if_zero_wd.
 Proof.
 intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)).
 reflexivity. unfold fun2_eq; now intros. assumption.