Mise en forme des theories

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

1 files changed, 360 insertions, 347 deletions

diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index b56818629..508a0231e 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -13,7 +13,7 @@ Require Export Relation_Definitions.
 
 Set Implicit Arguments.
 
-(* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *)
+(** * Definitions of [Relation_Class] and n-ary [Morphism_Theory] *)
 
 (* X will be used to distinguish covariant arguments whose type is an   *)
 (* Asymmetric* relation from contravariant arguments of the same type *)
@@ -46,39 +46,39 @@ Inductive Areflexive_Relation_Class  : Type :=
 Implicit Type Hole Out: Relation_Class.
 
 Definition relation_class_of_argument_class : Argument_Class -> Relation_Class.
- destruct 1.
- exact (SymmetricReflexive _ s r).
- exact (AsymmetricReflexive tt r).
- exact (SymmetricAreflexive _ s).
- exact (AsymmetricAreflexive tt Aeq).
- exact (Leibniz _ T).
+  destruct 1.
+  exact (SymmetricReflexive _ s r).
+  exact (AsymmetricReflexive tt r).
+  exact (SymmetricAreflexive _ s).
+  exact (AsymmetricAreflexive tt Aeq).
+  exact (Leibniz _ T).
 Defined.
 
 Definition carrier_of_relation_class : forall X, X_Relation_Class X -> Type.
- destruct 1.
- exact A.
- exact A.
- exact A.
- exact A.
- exact T.
+  destruct 1.
+  exact A.
+  exact A.
+  exact A.
+  exact A.
+  exact T.
 Defined.
 
 Definition relation_of_relation_class :
- forall X R, @carrier_of_relation_class X R -> carrier_of_relation_class R -> Prop.
- destruct R.
- exact Aeq.
- exact Aeq.
- exact Aeq.
- exact Aeq.
- exact (@eq T).
+  forall X R, @carrier_of_relation_class X R -> carrier_of_relation_class R -> Prop.
+  destruct R.
+  exact Aeq.
+  exact Aeq.
+  exact Aeq.
+  exact Aeq.
+  exact (@eq T).
 Defined.
 
 Lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
- forall R,
-  carrier_of_relation_class (relation_class_of_argument_class R) =
-   carrier_of_relation_class R.
- destruct R; reflexivity.
- Defined.
+  forall R,
+    carrier_of_relation_class (relation_class_of_argument_class R) =
+    carrier_of_relation_class R.
+  destruct R; reflexivity.
+Defined.
 
 Inductive nelistT (A : Type) : Type :=
    singl : A -> nelistT A
@@ -89,7 +89,7 @@ Definition Arguments := nelistT Argument_Class.
 Implicit Type In: Arguments.
 
 Definition function_type_of_morphism_signature :
- Arguments -> Relation_Class -> Type.
+  Arguments -> Relation_Class -> Type.
   intros In Out.
   induction In.
     exact (carrier_of_relation_class a -> carrier_of_relation_class Out).
@@ -97,12 +97,12 @@ Definition function_type_of_morphism_signature :
 Defined. 
 
 Definition make_compatibility_goal_aux:
- forall In Out
-  (f g: function_type_of_morphism_signature In Out), Prop.
- intros; induction In; simpl in f, g.
-   induction a; simpl in f, g.
-     exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)).
-     destruct x.
+  forall In Out
+    (f g: function_type_of_morphism_signature In Out), Prop.
+  intros; induction In; simpl in f, g.
+    induction a; simpl in f, g.
+      exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)).
+      destruct x.
         exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)).
         exact (forall x1 x2, Aeq x2 x1 -> relation_of_relation_class Out (f x1) (g x2)).
       exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)).
@@ -113,21 +113,45 @@ Definition make_compatibility_goal_aux:
   induction a; simpl in f, g.
     exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
     destruct x.
-       exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
-       exact (forall x1 x2, Aeq x2 x1 -> IHIn (f x1) (g x2)).
+      exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
+      exact (forall x1 x2, Aeq x2 x1 -> IHIn (f x1) (g x2)).
     exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
     destruct x.
-       exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
-       exact (forall x1 x2, Aeq x2 x1 -> IHIn (f x1) (g x2)).
+      exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
+      exact (forall x1 x2, Aeq x2 x1 -> IHIn (f x1) (g x2)).
     exact (forall x, IHIn (f x) (g x)).
 Defined. 
 
 Definition make_compatibility_goal :=
- (fun In Out f => make_compatibility_goal_aux In Out f f).
+  (fun In Out f => make_compatibility_goal_aux In Out f f).
 
 Record Morphism_Theory In Out : Type :=
-   {Function : function_type_of_morphism_signature In Out;
-    Compat : make_compatibility_goal In Out Function}.
+  { Function : function_type_of_morphism_signature In Out;
+    Compat : make_compatibility_goal In Out Function }.
+
+(** The [iff] relation class *)
+
+Definition Iff_Relation_Class : Relation_Class.
+  eapply (@SymmetricReflexive unit _ iff).
+  exact iff_sym.
+  exact iff_refl.
+Defined.
+
+(** The [impl] relation class *)
+
+Definition impl (A B: Prop) := A -> B.
+
+Theorem impl_refl: reflexive _ impl.
+Proof.
+  hnf; unfold impl; tauto.
+Qed.
+
+Definition Impl_Relation_Class : Relation_Class.
+  eapply (@AsymmetricReflexive unit tt _ impl).
+  exact impl_refl.
+Defined.
+
+(** Every function is a morphism from Leibniz+ to Leibniz *)
 
 Definition list_of_Leibniz_of_list_of_types: nelistT Type -> Arguments.
  induction 1.
@@ -135,13 +159,12 @@ Definition list_of_Leibniz_of_list_of_types: nelistT Type -> Arguments.
    exact (necons (Leibniz _ a) IHX).
 Defined.
 
-(* every function is a morphism from Leibniz+ to Leibniz *)
 Definition morphism_theory_of_function :
- forall (In: nelistT Type) (Out: Type),
-  let In' := list_of_Leibniz_of_list_of_types In in
-  let Out' := Leibniz _ Out in
-   function_type_of_morphism_signature In' Out' ->
-    Morphism_Theory In' Out'.
+  forall (In: nelistT Type) (Out: Type),
+    let In' := list_of_Leibniz_of_list_of_types In in
+      let Out' := Leibniz _ Out in
+	function_type_of_morphism_signature In' Out' ->
+	Morphism_Theory In' Out'.
   intros.
   exists X.
   induction In;  unfold make_compatibility_goal; simpl.
@@ -149,28 +172,21 @@ Definition morphism_theory_of_function :
     intro; apply (IHIn (X x)).
 Defined.
 
-(* THE iff RELATION CLASS *)
-
-Definition Iff_Relation_Class : Relation_Class.
- eapply (@SymmetricReflexive unit _ iff).
- exact iff_sym.
- exact iff_refl.
-Defined.
-
-(* THE impl RELATION CLASS *)
+(** Every predicate is a morphism from Leibniz+ to Iff_Relation_Class *)
 
-Definition impl (A B: Prop) := A -> B.
-
-Theorem impl_refl: reflexive _ impl.
- hnf; unfold impl; tauto.
-Qed.
-
-Definition Impl_Relation_Class : Relation_Class.
- eapply (@AsymmetricReflexive unit tt _ impl).
- exact impl_refl.
+Definition morphism_theory_of_predicate :
+  forall (In: nelistT Type),
+    let In' := list_of_Leibniz_of_list_of_types In in
+      function_type_of_morphism_signature In' Iff_Relation_Class ->
+      Morphism_Theory In' Iff_Relation_Class.
+  intros.
+  exists X.
+  induction In;  unfold make_compatibility_goal; simpl.
+    intro; apply iff_refl.
+    intro; apply (IHIn (X x)).
 Defined.
 
-(* UTILITY FUNCTIONS TO PROVE THAT EVERY TRANSITIVE RELATION IS A MORPHISM *)
+(** * Utility functions to prove that every transitive relation is a morphism *)
 
 Definition equality_morphism_of_symmetric_areflexive_transitive_relation:
  forall (A: Type)(Aeq: relation A)(sym: symmetric _ Aeq)(trans: transitive _ Aeq),
@@ -210,114 +226,148 @@ Definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
  unfold make_compatibility_goal; simpl; unfold impl; eauto.
 Defined.
 
-(* iff AS A RELATION *)
+(** * A few examples on [iff] *)
 
-Add Relation Prop iff
- reflexivity proved by iff_refl
- symmetry proved by iff_sym
- transitivity proved by iff_trans
- as iff_relation.
+(** [iff] as a relation *)
 
-(* every predicate is  morphism from Leibniz+ to Iff_Relation_Class *)
-Definition morphism_theory_of_predicate :
- forall (In: nelistT Type),
-  let In' := list_of_Leibniz_of_list_of_types In in
-   function_type_of_morphism_signature In' Iff_Relation_Class ->
-    Morphism_Theory In' Iff_Relation_Class.
-  intros.
-  exists X.
-  induction In;  unfold make_compatibility_goal; simpl.
-    intro; apply iff_refl.
-    intro; apply (IHIn (X x)).
-Defined.
+Add Relation Prop iff
+  reflexivity proved by iff_refl
+  symmetry proved by iff_sym
+  transitivity proved by iff_trans
+as iff_relation.
 
-(* impl AS A RELATION *)
+(** [impl] as a relation *)
 
 Theorem impl_trans: transitive _ impl.
- hnf; unfold impl; tauto.
+Proof.
+  hnf; unfold impl; tauto.
 Qed.
 
 Add Relation Prop impl
- reflexivity proved by impl_refl
- transitivity proved by impl_trans
- as impl_relation.
+  reflexivity proved by impl_refl
+  transitivity proved by impl_trans
+as impl_relation.
+
+(** [impl] is a morphism *)
+
+Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
+Proof.
+  unfold impl; tauto.
+Qed.
+
+(** [and] is a morphism *)
+
+Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
+ tauto.
+Qed.
+
+(** [or] is a morphism *)
 
-(* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *)
+Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
+Proof.
+  tauto.
+Qed.
+
+(** [not] is a morphism *)
+
+Add Morphism not with signature iff ==> iff as Not_Morphism.
+Proof.
+  tauto.
+Qed.
+
+(** The same examples on [impl] *)
+
+Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
+Proof.
+  unfold impl; tauto.
+Qed.
+
+Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
+Proof.
+  unfold impl; tauto.
+Qed.
+
+Add Morphism not with signature impl --> impl as Not_Morphism2.
+Proof.
+  unfold impl; tauto.
+Qed.
+
+(** * The CIC part of the reflexive tactic ([setoid_rewrite]) *)
 
 Inductive rewrite_direction : Type :=
-   Left2Right
- | Right2Left.
+  | Left2Right
+  | Right2Left.
 
 Implicit Type dir: rewrite_direction.
 
 Definition variance_of_argument_class : Argument_Class -> option variance.
- destruct 1.
- exact None.
- exact (Some v).
- exact None.
- exact (Some v).
- exact None.
+  destruct 1.
+  exact None.
+  exact (Some v).
+  exact None.
+  exact (Some v).
+  exact None.
 Defined.
 
 Definition opposite_direction :=
- fun dir =>
-   match dir with
-       Left2Right => Right2Left
-     | Right2Left => Left2Right
+  fun dir =>
+    match dir with
+      | Left2Right => Right2Left
+      | Right2Left => Left2Right
    end.
 
 Lemma opposite_direction_idempotent:
- forall dir, (opposite_direction (opposite_direction dir)) = dir.
+  forall dir, (opposite_direction (opposite_direction dir)) = dir.
+Proof.
   destruct dir; reflexivity.
 Qed.
 
 Inductive check_if_variance_is_respected :
- option variance -> rewrite_direction -> rewrite_direction ->  Prop
-:=
-   MSNone : forall dir dir', check_if_variance_is_respected None dir dir'
- | MSCovariant : forall dir, check_if_variance_is_respected (Some Covariant) dir dir
- | MSContravariant :
-     forall dir,
+  option variance -> rewrite_direction -> rewrite_direction ->  Prop :=
+  | MSNone : forall dir dir', check_if_variance_is_respected None dir dir'
+  | MSCovariant : forall dir, check_if_variance_is_respected (Some Covariant) dir dir
+  | MSContravariant :
+    forall dir,
       check_if_variance_is_respected (Some Contravariant) dir (opposite_direction dir).
 
 Definition relation_class_of_reflexive_relation_class:
- Reflexive_Relation_Class -> Relation_Class.
- induction 1.
-   exact (SymmetricReflexive _ s r).
-   exact (AsymmetricReflexive tt r).
-   exact (Leibniz _ T).
+  Reflexive_Relation_Class -> Relation_Class.
+  induction 1.
+  exact (SymmetricReflexive _ s r).
+  exact (AsymmetricReflexive tt r).
+  exact (Leibniz _ T).
 Defined.
 
 Definition relation_class_of_areflexive_relation_class:
- Areflexive_Relation_Class -> Relation_Class.
- induction 1.
-   exact (SymmetricAreflexive _ s).
-   exact (AsymmetricAreflexive tt Aeq).
+  Areflexive_Relation_Class -> Relation_Class.
+  induction 1.
+    exact (SymmetricAreflexive _ s).
+    exact (AsymmetricAreflexive tt Aeq).
 Defined.
 
 Definition carrier_of_reflexive_relation_class :=
- fun R => carrier_of_relation_class (relation_class_of_reflexive_relation_class R).
+  fun R => carrier_of_relation_class (relation_class_of_reflexive_relation_class R).
 
 Definition carrier_of_areflexive_relation_class :=
- fun R => carrier_of_relation_class (relation_class_of_areflexive_relation_class R).
+  fun R => carrier_of_relation_class (relation_class_of_areflexive_relation_class R).
 
 Definition relation_of_areflexive_relation_class :=
- fun R => relation_of_relation_class (relation_class_of_areflexive_relation_class R).
+  fun R => relation_of_relation_class (relation_class_of_areflexive_relation_class R).
 
 Inductive Morphism_Context Hole dir : Relation_Class -> rewrite_direction ->  Type :=
-    App :
-      forall In Out dir',
-        Morphism_Theory In Out -> Morphism_Context_List Hole dir dir' In ->
-           Morphism_Context Hole dir Out dir'
+  | App :
+    forall In Out dir',
+      Morphism_Theory In Out -> Morphism_Context_List Hole dir dir' In ->
+      Morphism_Context Hole dir Out dir'
   | ToReplace : Morphism_Context Hole dir Hole dir
   | ToKeep :
-     forall S dir',
+    forall S dir',
       carrier_of_reflexive_relation_class S ->
-        Morphism_Context Hole dir (relation_class_of_reflexive_relation_class S) dir'
- | ProperElementToKeep :
-     forall S dir' (x: carrier_of_areflexive_relation_class S),
+      Morphism_Context Hole dir (relation_class_of_reflexive_relation_class S) dir'
+  | ProperElementToKeep :
+    forall S dir' (x: carrier_of_areflexive_relation_class S),
       relation_of_areflexive_relation_class S x x ->
-        Morphism_Context Hole dir (relation_class_of_areflexive_relation_class S) dir'
+      Morphism_Context Hole dir (relation_class_of_areflexive_relation_class S) dir'
 with Morphism_Context_List Hole dir :
    rewrite_direction -> Arguments -> Type
 :=
@@ -337,47 +387,47 @@ Scheme Morphism_Context_rect2 := Induction for Morphism_Context  Sort Type
 with Morphism_Context_List_rect2 := Induction for Morphism_Context_List Sort Type.
 
 Definition product_of_arguments : Arguments -> Type.
- induction 1.
-   exact (carrier_of_relation_class a).
-   exact (prod (carrier_of_relation_class a) IHX).
+  induction 1.
+  exact (carrier_of_relation_class a).
+  exact (prod (carrier_of_relation_class a) IHX).
 Defined.
 
 Definition get_rewrite_direction: rewrite_direction -> Argument_Class -> rewrite_direction.
- intros dir R.
-destruct (variance_of_argument_class R).
-   destruct v.
-     exact dir.                                      (* covariant *)
-     exact (opposite_direction dir). (* contravariant *)
-   exact dir.                                       (* symmetric relation *)
+  intros dir R.
+  destruct (variance_of_argument_class R).
+  destruct v.
+    exact dir.                      (* covariant *)
+    exact (opposite_direction dir). (* contravariant *)
+   exact dir.                       (* symmetric relation *)
 Defined.
 
 Definition directed_relation_of_relation_class:
- forall dir (R: Relation_Class),
-   carrier_of_relation_class R -> carrier_of_relation_class R -> Prop.
- destruct 1.
-   exact (@relation_of_relation_class unit).
-   intros; exact (relation_of_relation_class _ X0 X).
+  forall dir (R: Relation_Class),
+    carrier_of_relation_class R -> carrier_of_relation_class R -> Prop.
+  destruct 1.
+    exact (@relation_of_relation_class unit).
+    intros; exact (relation_of_relation_class _ X0 X).
 Defined.
 
 Definition directed_relation_of_argument_class:
- forall dir (R: Argument_Class),
-   carrier_of_relation_class R -> carrier_of_relation_class R -> Prop.
+  forall dir (R: Argument_Class),
+    carrier_of_relation_class R -> carrier_of_relation_class R -> Prop.
   intros dir R.
   rewrite <-
-   (about_carrier_of_relation_class_and_relation_class_of_argument_class R).
+    (about_carrier_of_relation_class_and_relation_class_of_argument_class R).
   exact (directed_relation_of_relation_class dir (relation_class_of_argument_class R)).
 Defined.
 
 
 Definition relation_of_product_of_arguments:
- forall dir In,
-  product_of_arguments In -> product_of_arguments In -> Prop.
- induction In.
-   simpl.
-   exact (directed_relation_of_argument_class (get_rewrite_direction dir a) a).
-
-   simpl; intros.
-   destruct X; destruct X0.
+  forall dir In,
+    product_of_arguments In -> product_of_arguments In -> Prop.
+  induction In.
+    simpl.
+      exact (directed_relation_of_argument_class (get_rewrite_direction dir a) a).
+
+    simpl; intros.
+      destruct X; destruct X0.
    apply and.
      exact
       (directed_relation_of_argument_class (get_rewrite_direction dir a) a c c0).
@@ -385,32 +435,32 @@ Definition relation_of_product_of_arguments:
 Defined. 
 
 Definition apply_morphism:
- forall In Out (m: function_type_of_morphism_signature In Out)
-  (args: product_of_arguments In), carrier_of_relation_class Out.
- intros.
- induction In.
-   exact (m args).
-   simpl in m, args.
-   destruct args.
-   exact (IHIn (m c) p).
+  forall In Out (m: function_type_of_morphism_signature In Out)
+    (args: product_of_arguments In), carrier_of_relation_class Out.
+  intros.
+  induction In.
+    exact (m args).
+    simpl in m, args.
+    destruct args.
+    exact (IHIn (m c) p).
 Defined.
 
 Theorem apply_morphism_compatibility_Right2Left:
- forall In Out (m1 m2: function_type_of_morphism_signature In Out)
-   (args1 args2: product_of_arguments In),
-     make_compatibility_goal_aux _ _ m1 m2 ->
-      relation_of_product_of_arguments Right2Left _ args1 args2 ->
-        directed_relation_of_relation_class Right2Left _
-         (apply_morphism _ _ m2 args1)
-         (apply_morphism _ _ m1 args2).
+  forall In Out (m1 m2: function_type_of_morphism_signature In Out)
+    (args1 args2: product_of_arguments In),
+    make_compatibility_goal_aux _ _ m1 m2 ->
+    relation_of_product_of_arguments Right2Left _ args1 args2 ->
+    directed_relation_of_relation_class Right2Left _
+    (apply_morphism _ _ m2 args1)
+    (apply_morphism _ _ m1 args2).
   induction In; intros.
     simpl in m1, m2, args1, args2, H0 |- *.
     destruct a; simpl in H; hnf in H0.
-          apply H; exact H0.
-          destruct v; simpl in H0; apply H; exact H0.
-          apply H; exact H0.
-          destruct v; simpl in H0; apply H; exact H0.
-          rewrite H0; apply H; exact H0.
+      apply H; exact H0.
+      destruct v; simpl in H0; apply H; exact H0.
+      apply H; exact H0.
+      destruct v; simpl in H0; apply H; exact H0.
+      rewrite H0; apply H; exact H0.
 
    simpl in m1, m2, args1, args2, H0 |- *.
    destruct args1; destruct args2; simpl.
@@ -443,46 +493,47 @@ Theorem apply_morphism_compatibility_Right2Left:
 Qed.
 
 Theorem apply_morphism_compatibility_Left2Right:
- forall In Out (m1 m2: function_type_of_morphism_signature In Out)
-   (args1 args2: product_of_arguments In),
-     make_compatibility_goal_aux _ _ m1 m2 ->
-      relation_of_product_of_arguments Left2Right _ args1 args2 ->
-        directed_relation_of_relation_class Left2Right _
-         (apply_morphism _ _ m1 args1)
-         (apply_morphism _ _ m2 args2).
+  forall In Out (m1 m2: function_type_of_morphism_signature In Out)
+    (args1 args2: product_of_arguments In),
+    make_compatibility_goal_aux _ _ m1 m2 ->
+    relation_of_product_of_arguments Left2Right _ args1 args2 ->
+    directed_relation_of_relation_class Left2Right _
+    (apply_morphism _ _ m1 args1)
+    (apply_morphism _ _ m2 args2).
+Proof.
   induction In; intros.
     simpl in m1, m2, args1, args2, H0 |- *.
     destruct a; simpl in H; hnf in H0.
+      apply H; exact H0.
+      destruct v; simpl in H0; apply H; exact H0.
+      apply H; exact H0.
+      destruct v; simpl in H0; apply H; exact H0.
+      rewrite H0; apply H; exact H0.
+
+  simpl in m1, m2, args1, args2, H0 |- *.
+    destruct args1; destruct args2; simpl.
+    destruct H0.
+    simpl in H.
+    destruct a; simpl in H.
+      apply IHIn.
+        apply H; exact H0.
+        exact H1.
+      destruct v.
+        apply IHIn.
           apply H; exact H0.
-          destruct v; simpl in H0; apply H; exact H0.
-          apply H; exact H0.
-          destruct v; simpl in H0; apply H; exact H0.
-          rewrite H0; apply H; exact H0.
-
-    simpl in m1, m2, args1, args2, H0 |- *.
-   destruct args1; destruct args2; simpl.
-   destruct H0.
-   simpl in H.
-   destruct a; simpl in H.
-     apply IHIn.
-       apply H; exact H0.
-       exact H1.
-     destruct v.
-       apply IHIn.
-         apply H; exact H0.
-         exact H1.
-       apply IHIn.
-         apply H; exact H0.       
           exact H1.
-       apply IHIn.
-         apply H; exact H0.
-         exact H1.
-       apply IHIn.
-         destruct v; simpl in H, H0; apply H; exact H0. 
+        apply IHIn.
+          apply H; exact H0.       
+           exact H1.
+        apply IHIn.
+          apply H; exact H0.
           exact H1.
-    rewrite H0; apply IHIn.
-      apply H.
-      exact H1.
+        apply IHIn.
+          destruct v; simpl in H, H0; apply H; exact H0. 
+            exact H1.
+      rewrite H0; apply IHIn.
+        apply H.
+        exact H1.
 Qed.
 
 Definition interp :
@@ -508,83 +559,84 @@ Definition interp :
        exact X0.
 Defined.
 
-(*CSC: interp and interp_relation_class_list should be mutually defined, since
+(* CSC: interp and interp_relation_class_list should be mutually defined, since
    the proof term of each one contains the proof term of the other one. However
    I cannot do that interactively (I should write the Fix by hand) *)
 Definition interp_relation_class_list :
- forall Hole dir dir' (L: Arguments), carrier_of_relation_class Hole ->
-  Morphism_Context_List Hole dir dir' L -> product_of_arguments L.
- intros Hole dir dir' L H t.
- elim t using
-  (@Morphism_Context_List_rect2 Hole dir (fun S _ _ => carrier_of_relation_class S)
-    (fun _ L fcl => product_of_arguments L));
- intros.
-   exact (apply_morphism _ _ (Function m) X).
-   exact H.
-   exact c.
-   exact x.
-   simpl;
-     rewrite <-
-       (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
-     exact X.
-   split.
-     rewrite <-
-       (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
-       exact X.
-       exact X0.
+  forall Hole dir dir' (L: Arguments), carrier_of_relation_class Hole ->
+    Morphism_Context_List Hole dir dir' L -> product_of_arguments L.
+  intros Hole dir dir' L H t.
+  elim t using
+    (@Morphism_Context_List_rect2 Hole dir (fun S _ _ => carrier_of_relation_class S)
+      (fun _ L fcl => product_of_arguments L));
+    intros.
+  exact (apply_morphism _ _ (Function m) X).
+  exact H.
+  exact c.
+  exact x.
+  simpl;
+    rewrite <-
+      (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
+      exact X.
+  split.
+  rewrite <-
+    (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
+    exact X.
+  exact X0.
 Defined.
 
 Theorem setoid_rewrite:
- forall Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole)
-  (E: Morphism_Context Hole dir Out dir'),
-   (directed_relation_of_relation_class dir Hole E1 E2) ->
+  forall Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole)
+    (E: Morphism_Context Hole dir Out dir'),
+    (directed_relation_of_relation_class dir Hole E1 E2) ->
     (directed_relation_of_relation_class dir' Out (interp E1 E) (interp E2 E)).
- intros.
- elim E using
-   (@Morphism_Context_rect2 Hole dir
-     (fun S dir'' E => directed_relation_of_relation_class dir'' S (interp E1 E) (interp E2 E))
-     (fun dir'' L fcl =>
+Proof.
+  intros.
+  elim E using
+    (@Morphism_Context_rect2 Hole dir
+      (fun S dir'' E => directed_relation_of_relation_class dir'' S (interp E1 E) (interp E2 E))
+      (fun dir'' L fcl =>
         relation_of_product_of_arguments dir'' _
-         (interp_relation_class_list E1 fcl)
-         (interp_relation_class_list E2 fcl))); intros.
-   change (directed_relation_of_relation_class dir'0 Out0
+        (interp_relation_class_list E1 fcl)
+        (interp_relation_class_list E2 fcl))); intros.
+  change (directed_relation_of_relation_class dir'0 Out0
     (apply_morphism _ _ (Function m) (interp_relation_class_list E1 m0))
     (apply_morphism _ _ (Function m) (interp_relation_class_list E2 m0))).
-   destruct dir'0.
-     apply apply_morphism_compatibility_Left2Right.
-       exact (Compat m).
-       exact H0.
-     apply apply_morphism_compatibility_Right2Left.
-       exact (Compat m).
-       exact H0.
-
-   exact H.
-
-   unfold interp, Morphism_Context_rect2.
-   (*CSC: reflexivity used here*)
-   destruct S; destruct dir'0; simpl; (apply r || reflexivity).
-
-   destruct dir'0; exact r.
+  destruct dir'0.
+    apply apply_morphism_compatibility_Left2Right.
+      exact (Compat m).
+      exact H0.
+    apply apply_morphism_compatibility_Right2Left.
+      exact (Compat m).
+      exact H0.
+
+  exact H.
+
+  unfold interp, Morphism_Context_rect2.
+  (* CSC: reflexivity used here *)
+  destruct S; destruct dir'0; simpl; (apply r || reflexivity).
+  
+  destruct dir'0; exact r.
 
   destruct S; unfold directed_relation_of_argument_class; simpl in H0 |- *;
-   unfold get_rewrite_direction; simpl.
-     destruct dir'0; destruct dir'';
-       (exact H0 ||
-        unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
-     (* the following mess with generalize/clear/intros is to help Coq resolving *)
-     (* second order unification problems.                                                                *)
-     generalize m c H0; clear H0 m c; inversion c;
-       generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
-         (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
-     destruct dir'0; destruct dir'';
-       (exact H0 ||
-        unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
-(* the following mess with generalize/clear/intros is to help Coq resolving *)
-     (* second order unification problems.                                                                *)
-     generalize m c H0; clear H0 m c; inversion c;
-       generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
-         (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
-     destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0).
+    unfold get_rewrite_direction; simpl.
+  destruct dir'0; destruct dir'';
+    (exact H0 ||
+      unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
+  (* the following mess with generalize/clear/intros is to help Coq resolving *)
+  (* second order unification problems.                                       *)
+  generalize m c H0; clear H0 m c; inversion c;
+    generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
+      (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
+  destruct dir'0; destruct dir'';
+    (exact H0 ||
+      unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
+  (* the following mess with generalize/clear/intros is to help Coq resolving *)
+  (* second order unification problems.                                       *)
+  generalize m c H0; clear H0 m c; inversion c;
+    generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
+      (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
+  destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0).
 
   change
     (directed_relation_of_argument_class (get_rewrite_direction dir'' S) S
@@ -592,96 +644,57 @@ Theorem setoid_rewrite:
          (about_carrier_of_relation_class_and_relation_class_of_argument_class S))
        (eq_rect _ (fun T : Type => T) (interp E2 m) _
          (about_carrier_of_relation_class_and_relation_class_of_argument_class S)) /\
-     relation_of_product_of_arguments dir'' _
+       relation_of_product_of_arguments dir'' _
        (interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)).
-   split.
-     clear m0 H1; destruct S; simpl in H0 |- *; unfold get_rewrite_direction; simpl.
-        destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
-        inversion c.
-          rewrite <- H3; exact H0.
-          rewrite (opposite_direction_idempotent dir'0); exact H0.
-        destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
-        inversion c.
-          rewrite <- H3; exact H0.
-          rewrite (opposite_direction_idempotent dir'0); exact H0.
-        destruct dir''; destruct dir'0; (exact H0 || hnf; symmetry; exact H0).
-     exact H1.
-Qed.
-
-(* BEGIN OF UTILITY/BACKWARD COMPATIBILITY PART *)
+  split.
+  clear m0 H1; destruct S; simpl in H0 |- *; unfold get_rewrite_direction; simpl.
+    destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
+      inversion c.
+        rewrite <- H3; exact H0.
+        rewrite (opposite_direction_idempotent dir'0); exact H0.
+      destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
+      inversion c.
+        rewrite <- H3; exact H0.
+        rewrite (opposite_direction_idempotent dir'0); exact H0.
+      destruct dir''; destruct dir'0; (exact H0 || hnf; symmetry; exact H0).
+    exact H1.
+  Qed.
+
+(** * Miscelenous *)
+
+(** For backwark compatibility *)
 
 Record Setoid_Theory  (A: Type) (Aeq: relation A) : Prop := 
-  {Seq_refl : forall x:A, Aeq x x;
-   Seq_sym : forall x y:A, Aeq x y -> Aeq y x;
-   Seq_trans : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z}.
-
-(* END OF UTILITY/BACKWARD COMPATIBILITY PART *)
-
-(* A FEW EXAMPLES ON iff *)
-
-(* impl IS A MORPHISM *)
+  { Seq_refl : forall x:A, Aeq x x;
+    Seq_sym : forall x y:A, Aeq x y -> Aeq y x;
+    Seq_trans : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z }.
 
-Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
-unfold impl; tauto.
-Qed.
-
-(* and IS A MORPHISM *)
-
-Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
- tauto.
-Qed.
-
-(* or IS A MORPHISM *)
-
-Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
- tauto.
-Qed.
-
-(* not IS A MORPHISM *)
-
-Add Morphism not with signature iff ==> iff as Not_Morphism.
- tauto.
-Qed.
-
-(* THE SAME EXAMPLES ON impl *)
-
-Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
- unfold impl; tauto.
-Qed.
-
-Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
- unfold impl; tauto.
-Qed.
-
-Add Morphism not with signature impl --> impl as Not_Morphism2.
- unfold impl; tauto.
-Qed.
-
-(* FOR BACKWARD COMPATIBILITY *)
 Implicit Arguments Setoid_Theory [].
 Implicit Arguments Seq_refl [].
 Implicit Arguments Seq_sym [].
 Implicit Arguments Seq_trans [].
 
 
-(* Some tactics for manipulating Setoid Theory not officially 
-   declared as Setoid. *)
+(** Some tactics for manipulating Setoid Theory not officially 
+    declared as Setoid. *)
 
 Ltac trans_st x := match goal with 
-  | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
-     apply (Seq_trans _ _ H) with x; auto
- end.
+		     | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
+		       apply (Seq_trans _ _ H) with x; auto
+		   end.
 
 Ltac sym_st := match goal with 
-  | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
-     apply (Seq_sym _ _ H); auto
- end.
+		 | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
+		   apply (Seq_sym _ _ H); auto
+	       end.
 
 Ltac refl_st := match goal with 
-  | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
-     apply (Seq_refl _ _ H); auto
- end.
+		  | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
+		    apply (Seq_refl _ _ H); auto
+		end.
 
 Definition gen_st : forall A : Set, Setoid_Theory _ (@eq A).
-Proof. constructor; congruence. Qed.
-
+Proof. 
+  constructor; congruence. 
+Qed.
+