diff options
Diffstat (limited to 'theories/Setoids/Setoid_tac.v')
| -rw-r--r-- | theories/Setoids/Setoid_tac.v | 595 |
1 files changed, 0 insertions, 595 deletions
diff --git a/theories/Setoids/Setoid_tac.v b/theories/Setoids/Setoid_tac.v deleted file mode 100644 index cdc4eafe..00000000 --- a/theories/Setoids/Setoid_tac.v +++ /dev/null @@ -1,595 +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: Setoid_tac.v 10739 2008-04-01 14:45:20Z herbelin $ i*) - -Require Export Relation_Definitions. - -Set Implicit Arguments. - -(** * 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 *) -Inductive X_Relation_Class (X: Type) : Type := - SymmetricReflexive : - forall A Aeq, symmetric A Aeq -> reflexive _ Aeq -> X_Relation_Class X - | AsymmetricReflexive : X -> forall A Aeq, reflexive A Aeq -> X_Relation_Class X - | SymmetricAreflexive : forall A Aeq, symmetric A Aeq -> X_Relation_Class X - | AsymmetricAreflexive : X -> forall A (Aeq : relation A), X_Relation_Class X - | Leibniz : Type -> X_Relation_Class X. - -Inductive variance : Set := - Covariant - | Contravariant. - -Definition Argument_Class := X_Relation_Class variance. -Definition Relation_Class := X_Relation_Class unit. - -Inductive Reflexive_Relation_Class : Type := - RSymmetric : - forall A Aeq, symmetric A Aeq -> reflexive _ Aeq -> Reflexive_Relation_Class - | RAsymmetric : - forall A Aeq, reflexive A Aeq -> Reflexive_Relation_Class - | RLeibniz : Type -> Reflexive_Relation_Class. - -Inductive Areflexive_Relation_Class : Type := - | ASymmetric : forall A Aeq, symmetric A Aeq -> Areflexive_Relation_Class - | AAsymmetric : forall A (Aeq : relation A), Areflexive_Relation_Class. - -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). -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. -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). -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. - -Inductive nelistT (A : Type) : Type := - singl : A -> nelistT A - | necons : A -> nelistT A -> nelistT A. - -Definition Arguments := nelistT Argument_Class. - -Implicit Type In: Arguments. - -Definition function_type_of_morphism_signature : - Arguments -> 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; 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)). - 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 x, relation_of_relation_class Out (f x) (g x)). - 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)). - 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 x, 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 }. - - -(** 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. - exact (singl (Leibniz _ a)). - exact (necons (Leibniz _ a) IHX). -Defined. - -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. - -(** Every predicate is a 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. - -(** * 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), - let ASetoidClass := SymmetricAreflexive _ sym in - (Morphism_Theory (necons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class). - intros. - exists Aeq. - unfold make_compatibility_goal; simpl; split; eauto. -Defined. - -Definition equality_morphism_of_symmetric_reflexive_transitive_relation: - forall (A: Type)(Aeq: relation A)(refl: reflexive _ Aeq)(sym: symmetric _ Aeq) - (trans: transitive _ Aeq), let ASetoidClass := SymmetricReflexive _ sym refl in - (Morphism_Theory (necons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class). - intros. - exists Aeq. - unfold make_compatibility_goal; simpl; split; eauto. -Defined. - -Definition equality_morphism_of_asymmetric_areflexive_transitive_relation: - forall (A: Type)(Aeq: relation A)(trans: transitive _ Aeq), - let ASetoidClass1 := AsymmetricAreflexive Contravariant Aeq in - let ASetoidClass2 := AsymmetricAreflexive Covariant Aeq in - (Morphism_Theory (necons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class). - intros. - exists Aeq. - unfold make_compatibility_goal; simpl; unfold impl; eauto. -Defined. - -Definition equality_morphism_of_asymmetric_reflexive_transitive_relation: - forall (A: Type)(Aeq: relation A)(refl: reflexive _ Aeq)(trans: transitive _ Aeq), - let ASetoidClass1 := AsymmetricReflexive Contravariant refl in - let ASetoidClass2 := AsymmetricReflexive Covariant refl in - (Morphism_Theory (necons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class). - intros. - exists Aeq. - unfold make_compatibility_goal; simpl; unfold impl; eauto. -Defined. - -(** * The CIC part of the reflexive tactic ([setoid_rewrite]) *) - -Inductive rewrite_direction : Type := - | 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. -Defined. - -Definition opposite_direction := - fun dir => - match dir with - | Left2Right => Right2Left - | Right2Left => Left2Right - end. - -Lemma opposite_direction_idempotent: - 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, - 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). -Defined. - -Definition relation_class_of_areflexive_relation_class: - 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). - -Definition carrier_of_areflexive_relation_class := - 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). - -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' - | ToReplace : Morphism_Context Hole dir Hole dir - | ToKeep : - 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), - relation_of_areflexive_relation_class S x x -> - Morphism_Context Hole dir (relation_class_of_areflexive_relation_class S) dir' -with Morphism_Context_List Hole dir : - rewrite_direction -> Arguments -> Type -:= - fcl_singl : - forall S dir' dir'', - check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' -> - Morphism_Context Hole dir (relation_class_of_argument_class S) dir' -> - Morphism_Context_List Hole dir dir'' (singl S) - | fcl_cons : - forall S L dir' dir'', - check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' -> - Morphism_Context Hole dir (relation_class_of_argument_class S) dir' -> - Morphism_Context_List Hole dir dir'' L -> - Morphism_Context_List Hole dir dir'' (necons S L). - -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). -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 *) -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). -Defined. - -Definition directed_relation_of_argument_class: - 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). - 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. - apply and. - exact - (directed_relation_of_argument_class (get_rewrite_direction dir a) a c c0). - exact (IHIn p p0). -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). -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). - 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. - exact H1. - apply IHIn. - apply H; exact H0. - exact H1. - 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. - rewrite H0; apply IHIn. - apply H. - exact H1. -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). -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. - 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. - exact H1. - rewrite H0; apply IHIn. - apply H. - exact H1. -Qed. - -Definition interp : - forall Hole dir Out dir', carrier_of_relation_class Hole -> - Morphism_Context Hole dir Out dir' -> carrier_of_relation_class Out. - intros Hole dir Out dir' H t. - elim t using - (@Morphism_Context_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. - -(* 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. -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) -> - (directed_relation_of_relation_class dir' Out (interp E1 E) (interp E2 E)). -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 - (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 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). - - change - (directed_relation_of_argument_class (get_rewrite_direction dir'' S) S - (eq_rect _ (fun T : Type => T) (interp E1 m) _ - (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'' _ - (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. |