diff options
Diffstat (limited to 'theories/Setoids/Setoid.v')
| -rw-r--r-- | theories/Setoids/Setoid.v | 675 |
1 files changed, 634 insertions, 41 deletions
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index 63f21fed..6ff73438 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 *) @@ -6,66 +7,658 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Setoid.v,v 1.5.2.1 2004/07/16 19:31:17 herbelin Exp $: i*) +(*i $Id: Setoid.v 6306 2004-11-16 16:11:10Z sacerdot $: 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 + | cons : 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}. + +Definition list_of_Leibniz_of_list_of_types: nelistT Type -> Arguments. + 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 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. + hnf; unfold impl; tauto. +Qed. + +Definition Impl_Relation_Class : Relation_Class. + eapply (@AsymmetricReflexive unit tt _ impl). + exact impl_refl. +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 (cons 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 (cons 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 (cons 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 (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class). + intros. + exists Aeq. + unfold make_compatibility_goal; simpl; unfold impl; eauto. +Defined. + +(* iff AS A RELATION *) + +Add Relation Prop iff + reflexivity proved by iff_refl + symmetry proved by iff_sym + transitivity proved by iff_trans + as iff_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. + +(* impl AS A RELATION *) + +Theorem impl_trans: transitive _ impl. + hnf; unfold impl; tauto. +Qed. + +Add Relation Prop impl + reflexivity proved by impl_refl + transitivity proved by impl_trans + as impl_relation. + +(* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *) -Section Setoid. +Inductive rewrite_direction : Type := + Left2Right + | Right2Left. -Variable A : Type. -Variable Aeq : A -> A -> Prop. +Implicit Type dir: rewrite_direction. -Record Setoid_Theory : Prop := +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. + 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'' (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. + +Definition product_of_arguments : Arguments -> Type. + induction 1. + exact (carrier_of_relation_class a). + exact (prodT (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). + 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)). + 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. + +(* BEGIN OF UTILITY/BACKWARD COMPATIBILITY PART *) + +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 Setoid. +(* END OF UTILITY/BACKWARD COMPATIBILITY PART *) + +(* A FEW EXAMPLES ON iff *) -Definition Prop_S : Setoid_Theory Prop iff. -split; [ exact iff_refl | exact iff_sym | exact iff_trans ]. +(* impl IS A MORPHISM *) + +Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism. +unfold impl; tauto. Qed. -Add Setoid Prop iff Prop_S. +(* and IS A MORPHISM *) -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. +Add Morphism and with signature iff ==> iff ==> iff as And_Morphism. + tauto. +Qed. -Add Morphism or : or_ext. -intros. -inversion H1. -left. -inversion H. -apply (H3 H2). +(* or IS A MORPHISM *) -right. -inversion H0. -apply (H3 H2). +Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism. + tauto. Qed. -Add Morphism and : and_ext. -intros. -inversion H1. -split. -inversion H. -apply (H4 H2). +(* not IS A MORPHISM *) -inversion H0. -apply (H4 H3). +Add Morphism not with signature iff ==> iff as Not_Morphism. + tauto. Qed. -Add Morphism not : not_ext. -red in |- *; intros. -apply H0. -inversion H. -apply (H3 H1). +(* THE SAME EXAMPLES ON impl *) + +Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2. + unfold impl; tauto. Qed. -Definition fleche (A B:Prop) := A -> B. +Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2. + unfold impl; tauto. +Qed. -Add Morphism fleche : fleche_ext. -unfold fleche in |- *. -intros. -inversion H0. -inversion H. -apply (H3 (H1 (H6 H2))). +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 []. |