New reflexive implementation of setoid_rewrite. The new implementation

introduces a few backward incompatibilities:
 1. setoid_replace used to try to close the new goal using full_trivial.
    The new implementation does not try to close the goal.
    To fix the script it is sufficient to add a "; [ idtac | trivial ]."
    after every application of setoid_replace that used to generate just
    one goal.
 2. (setoid_replace c1 c2) used to replace either c1 with c2 or c2 with c1
    (if c1 did not occur in the goal). The new implementation only replaces
    c1 with c2.
    To fix the script it is sufficient to replace
    (setoid_replace c1 with c2) with
    (setoid_replace c1 with c2) || (setoid_replace c2 with c1)
    in those cases where it is unknown what should be substituted with what.
 3. the goal generated by the "Add Morphism" command has the hypothesis
    permutated w.r.t. the old implementation. I.e. the old implementation
    used to generate: forall x1 x2, forall x3 x4, x1=x2 -> x3=x4 -> ...
    whereas the new implementation generates
     forall x1 x2, x1=x2 -> forall x3 x4, x3 = x4 -> ...
    Fixing the script is usually trivial.
 4. the "Add Morphism P" command used to generate a non-standard goal in the
    case of P being a predicate (i.e. a function whose codomain is Prop).
    In that case the goal ended with an implication (instead of ending with
    a coimplication). The new implementation generates a standard goal that
    ends with a coimplication.
    To fix the script you can add the following line at the very beginning:
     cut <<old_goal>>; intro Hold; split; apply Hold;
      assumption || (symmetry;assumption).


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

1 files changed, 327 insertions, 45 deletions

diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index bca2bf9de..bf54f0567 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -1,3 +1,4 @@
+
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -8,64 +9,345 @@
 
 (*i $Id$: i*)
 
-Section Setoid.
+Set Implicit Arguments.
+
+(* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *)
+
+Definition is_reflexive (A: Type) (Aeq: A -> A -> Prop) : Prop :=
+ forall x:A, Aeq x x.
+
+Definition is_symmetric (A: Type) (Aeq: A -> A -> Prop) : Prop :=
+ forall (x y:A), Aeq x y -> Aeq y x.
+
+Inductive Relation_Class : Type :=
+   Reflexive : forall A Aeq, (@is_reflexive A Aeq) -> Relation_Class
+ | Leibniz : Type -> Relation_Class.
+
+Implicit Type Hole Out: Relation_Class.
+
+Definition carrier_of_relation_class : Relation_Class -> Type.
+ intro; case X; intros.
+ exact A.
+ exact T.
+Defined.
+
+Inductive nelistT (A : Type) : Type :=
+   singl : A -> (nelistT A)
+ | cons : A -> (nelistT A) -> (nelistT A).
+
+Implicit Type In: (nelistT Relation_Class).
+
+Definition function_type_of_morphism_signature :
+ (nelistT Relation_Class) -> Relation_Class -> Type.
+  intros In Out.
+  induction In.
+    exact (carrier_of_relation_class a -> carrier_of_relation_class Out).
+    exact (carrier_of_relation_class a -> IHIn).
+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; destruct Out; simpl in f, g.
+     exact (forall (x1 x2: A), (Aeq x1 x2) -> (Aeq0 (f x1) (g x2))).
+     exact (forall (x1 x2: A), (Aeq x1 x2) -> f x1 = g x2).
+     exact (forall (x: T), (Aeq (f x) (g x))).
+     exact (forall (x: T), f x = g x).
+  induction a; simpl in f, g.
+    exact (forall (x1 x2: A), (Aeq x1 x2) -> IHIn (f x1) (g x2)).
+    exact (forall (x: T), IHIn (f x) (g x)).
+Defined. 
+
+Definition make_compatibility_goal :=
+ (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}.
+
+Definition list_of_Leibniz_of_list_of_types:
+ nelistT Type -> nelistT Relation_Class.
+ induction 1.
+   exact (singl (Leibniz a)).
+   exact (cons (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'.
+  intros.
+  exists X.
+  induction In;  unfold make_compatibility_goal; simpl.
+    reflexivity.
+    intro; apply (IHIn (X x)).
+Defined.
+
+(* THE Prop RELATION CLASS *)
+
+Add Relation Prop iff reflexivity proved by iff_refl symmetry proved by iff_sym.
+
+Definition Prop_Relation_Class : Relation_Class.
+ eapply (@Reflexive _ iff).
+ exact iff_refl.
+Defined.
+
+(* every predicate is  morphism from Leibniz+ to Prop_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' Prop_Relation_Class ->
+    Morphism_Theory In' Prop_Relation_Class.
+  intros.
+  exists X.
+  induction In;  unfold make_compatibility_goal; simpl.
+    intro; apply iff_refl.
+    intro; apply (IHIn (X x)).
+Defined.
+
+(* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *)
+
+Inductive Morphism_Context Hole : Relation_Class -> Type :=
+    App : forall In Out,
+                Morphism_Theory In Out ->  Morphism_Context_List Hole In ->
+                  Morphism_Context Hole Out
+  | Toreplace : Morphism_Context Hole Hole
+  | Tokeep :
+     forall (S: Relation_Class),
+      carrier_of_relation_class S -> Morphism_Context Hole S
+  | Imp :
+      Morphism_Context Hole Prop_Relation_Class ->
+       Morphism_Context Hole Prop_Relation_Class ->
+        Morphism_Context Hole Prop_Relation_Class
+with Morphism_Context_List Hole: nelistT Relation_Class -> Type :=
+    fcl_singl :
+      forall (S: Relation_Class), Morphism_Context Hole S ->
+       Morphism_Context_List Hole (singl S)
+ | fcl_cons :
+      forall (S: Relation_Class) (L: nelistT Relation_Class),
+       Morphism_Context Hole S -> Morphism_Context_List Hole L ->
+        Morphism_Context_List Hole (cons S L).
+
+Scheme Morphism_Context_rect2 := Induction for Morphism_Context  Sort Type
+with Morphism_Context_List_rect2 := Induction for Morphism_Context_List Sort Type.
+
+Inductive prodT (A B: Type) : Type :=
+ pairT : A -> B -> prodT A B.
+
+Definition product_of_relation_class_list : nelistT Relation_Class -> Type.
+ induction 1.
+   exact (carrier_of_relation_class a).
+   exact (prodT (carrier_of_relation_class a) IHX).
+Defined.
 
-Variable A : Type.
-Variable Aeq : A -> A -> Prop.
+Definition relation_of_relation_class:
+ forall Out,
+  carrier_of_relation_class Out -> carrier_of_relation_class Out -> Prop.
+ destruct Out.
+   exact Aeq.
+   exact (@eq T).
+Defined.
 
-Record Setoid_Theory : Prop := 
+Definition relation_of_product_of_relation_class_list:
+ forall In,
+  product_of_relation_class_list In -> product_of_relation_class_list In -> Prop.
+ induction In.
+   exact (relation_of_relation_class a).
+
+   simpl; intros.
+   destruct X; destruct X0.
+   exact (relation_of_relation_class a c c0 /\ IHIn p p0).
+Defined. 
+
+Definition apply_morphism:
+ forall In Out (m: function_type_of_morphism_signature In Out)
+  (args: product_of_relation_class_list 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:
+ forall In Out (m1 m2: function_type_of_morphism_signature In Out)
+   (args1 args2: product_of_relation_class_list In),
+     make_compatibility_goal_aux _ _ m1 m2 ->
+      relation_of_product_of_relation_class_list _ args1 args2 ->
+        relation_of_relation_class _
+         (apply_morphism _ _ m1 args1)
+         (apply_morphism _ _ m2 args2).
+  intros.
+  induction In.
+    simpl; simpl in m1, m2, args1, args2, H0.
+    destruct a; destruct Out.
+      apply H; exact H0.
+      simpl; apply H; exact H0.
+      simpl; rewrite H0; apply H.
+      simpl; rewrite H0; apply H.
+   simpl in 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.
+    rewrite H0; apply IHIn.
+      apply H.
+      exact H1.
+Qed.
+
+Definition interp :
+ forall Hole Out, carrier_of_relation_class Hole ->
+  Morphism_Context Hole Out -> carrier_of_relation_class Out.
+ intros Hole Out H t.
+ elim t using
+  (@Morphism_Context_rect2 Hole (fun S _ => carrier_of_relation_class S)
+    (fun L fcl => product_of_relation_class_list L));
+  intros.
+   exact (apply_morphism _ _ (Function m) X).
+   exact H.
+   exact c.
+   exact (X -> X0).
+   exact X.
+   split; [ exact X | exact X0 ].
+Defined.
+
+(*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 (L: nelistT Relation_Class), carrier_of_relation_class Hole ->
+  Morphism_Context_List Hole L -> product_of_relation_class_list L.
+ intros Hole L H t.
+ elim t using
+  (@Morphism_Context_List_rect2 Hole (fun S _ => carrier_of_relation_class S)
+    (fun L fcl => product_of_relation_class_list L));
+ intros.
+   exact (apply_morphism _ _ (Function m) X).
+   exact H.
+   exact c.
+   exact (X -> X0).
+   exact X.
+   split; [ exact X | exact X0 ].
+Defined.
+
+Theorem setoid_rewrite:
+ forall Hole Out (E1 E2: carrier_of_relation_class Hole)
+  (E: Morphism_Context Hole Out),
+   (relation_of_relation_class Hole E1 E2) ->
+    (relation_of_relation_class Out (interp E1 E) (interp E2 E)).
+ intros.
+ elim E using
+   (@Morphism_Context_rect2 Hole
+     (fun S E => relation_of_relation_class S (interp E1 E) (interp E2 E))
+     (fun L fcl =>
+       relation_of_product_of_relation_class_list _
+        (interp_relation_class_list E1 fcl)
+        (interp_relation_class_list E2 fcl)));
+ intros.
+   change (relation_of_relation_class Out0
+    (apply_morphism _ _ (Function m) (interp_relation_class_list E1 m0))
+    (apply_morphism _ _ (Function m) (interp_relation_class_list E2 m0))).
+   apply apply_morphism_compatibility.
+     exact (Compat m).
+     exact H0.
+
+   exact H.
+
+   unfold interp, Morphism_Context_rect2.
+   (*CSC: reflexivity used here*)
+   destruct S.
+     apply i.
+     simpl; reflexivity.
+
+   change
+     (relation_of_relation_class Prop_Relation_Class
+       (interp E1 m -> interp E1 m0) (interp E2 m -> interp E2 m0)).
+   simpl; simpl in H0, H1.
+   tauto.
+
+  exact H0.
+
+  change
+    (relation_of_relation_class _ (interp E1 m) (interp E2 m) /\
+     relation_of_product_of_relation_class_list _
+       (interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)).
+   split.
+     exact H0.
+     exact H1.
+Qed.
+
+(* BEGIN OF UTILITY/BACKWARD COMPATIBILITY PART *)
+
+Record Setoid_Theory  (A: Type) (Aeq: A -> A -> Prop) : 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 Setoid.
+Definition relation_class_of_setoid_theory:
+ forall (A: Type) (Aeq: A -> A -> Prop),
+  Setoid_Theory Aeq -> Relation_Class.
+ intros.
+ apply (@Reflexive _ Aeq).
+ exact (Seq_refl H).
+Defined.
 
-Definition Prop_S : Setoid_Theory Prop iff.
-split; [ exact iff_refl | exact iff_sym | exact iff_trans ].
-Qed.
+Definition equality_morphism_of_setoid_theory:
+ forall (A: Type) (Aeq: A -> A -> Prop) (ST: Setoid_Theory Aeq),
+   let ASetoidClass := relation_class_of_setoid_theory ST in 
+    (Morphism_Theory (cons ASetoidClass (singl ASetoidClass))
+      Prop_Relation_Class).
+ intros.
+ exists Aeq.
+ pose (sym   := Seq_sym ST);  clearbody sym.
+ pose (trans := Seq_trans ST); clearbody trans.
+ (*CSC: symmetry and transitivity used here *)
+ unfold make_compatibility_goal; simpl; split; eauto.
+Defined.
 
-Add Setoid Prop iff Prop_S.
+(* END OF UTILITY/BACKWARD COMPATIBILITY PART *)
 
-Hint Resolve (Seq_refl Prop iff Prop_S): setoid.
-Hint Resolve (Seq_sym Prop iff Prop_S): setoid.
-Hint Resolve (Seq_trans Prop iff Prop_S): setoid.
+(* A FEW EXAMPLES *)
 
-Add Morphism or : or_ext.
-intros.
-inversion H1.
-left.
-inversion H.
-apply (H3 H2).
+Add Morphism iff : Iff_Morphism.
+ tauto.
+Defined.
 
-right.
-inversion H0.
-apply (H3 H2).
-Qed.
+(* impl IS A MORPHISM *)
 
-Add Morphism and : and_ext.
-intros.
-inversion H1.
-split.
-inversion H.
-apply (H4 H2).
+Definition impl (A B: Prop) := A -> B.
 
-inversion H0.
-apply (H4 H3).
-Qed.
+Add Morphism impl : Impl_Morphism.
+unfold impl; tauto.
+Defined.
 
-Add Morphism not : not_ext.
-red in |- *; intros.
-apply H0.
-inversion H.
-apply (H3 H1).
-Qed.
+(* and IS A MORPHISM *)
 
-Definition fleche (A B:Prop) := A -> B.
+Add Morphism and : And_Morphism.
+ tauto.
+Defined.
 
-Add Morphism fleche : fleche_ext.
-unfold fleche in |- *.
-intros.
-inversion H0.
-inversion H.
-apply (H3 (H1 (H6 H2))).
-Qed.
+(* or IS A MORPHISM *)
+
+Add Morphism or : Or_Morphism.
+ tauto.
+Defined.
+
+(* not IS A MORPHISM *)
+
+Add Morphism not : Not_Morphism.
+ tauto.
+Defined.
+
+(* FOR BACKWARD COMPATIBILITY *)
+Implicit Arguments Setoid_Theory [].
+Implicit Arguments Seq_refl [].
+Implicit Arguments Seq_sym [].
+Implicit Arguments Seq_trans [].