Suppression des fichiers .v en ancienne syntaxe

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

2 files changed, 0 insertions, 356 deletions

diff --git a/theories7/Setoids/.cvsignore b/theories7/Setoids/.cvsignore
deleted file mode 100644
index c446fcb878..0000000000
--- a/theories7/Setoids/.cvsignore
+++ /dev/null
@@ -1 +0,0 @@
-*.v8
diff --git a/theories7/Setoids/Setoid.v b/theories7/Setoids/Setoid.v
deleted file mode 100644
index 189f2c09ee..0000000000
--- a/theories7/Setoids/Setoid.v
+++ /dev/null
@@ -1,355 +0,0 @@
-
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(*i $Id$: i*)
-
-(*
-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.
-
-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.
-
-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}.
-
-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 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.
-
-(* END OF UTILITY/BACKWARD COMPATIBILITY PART *)
-
-(* A FEW EXAMPLES *)
-
-Add Morphism iff : Iff_Morphism.
- tauto.
-Defined.
-
-(* impl IS A MORPHISM *)
-
-Definition impl (A B: Prop) := A -> B.
-
-Add Morphism impl : Impl_Morphism.
-unfold impl; tauto.
-Defined.
-
-(* and IS A MORPHISM *)
-
-Add Morphism and : And_Morphism.
- tauto.
-Defined.
-
-(* 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 [].
-*)