From 2eccf8b0a25257574a8c3893add06166b2ed0c7d Mon Sep 17 00:00:00 2001 From: sacerdot Date: Thu, 7 Oct 2004 08:53:18 +0000 Subject: iff and impl are now declared as transitive relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6192 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Setoids/Setoid.v | 127 ++++++++++++++++++++++++---------------------- 1 file changed, 66 insertions(+), 61 deletions(-) (limited to 'theories/Setoids') diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index c0ab8aa55..2d48e82df 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -140,14 +140,73 @@ Defined. (* THE iff RELATION CLASS *) -Add Relation Prop iff reflexivity proved by iff_refl symmetry proved by iff_sym as iff_relation. - 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), @@ -161,24 +220,16 @@ Definition morphism_theory_of_predicate : intro; apply (IHIn (X x)). Defined. -(* THE impl RELATION CLASS *) - -Definition impl (A B: Prop) := A -> B. - -Theorem impl_refl: reflexive _ impl. - hnf; unfold impl; tauto. -Qed. +(* impl AS A RELATION *) Theorem impl_trans: transitive _ impl. hnf; unfold impl; tauto. Qed. -Add Relation Prop impl reflexivity proved by impl_refl as impl_relation. - -Definition Impl_Relation_Class : Relation_Class. - eapply (@AsymmetricReflexive unit tt _ impl). - exact impl_refl. -Defined. +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) *) @@ -593,52 +644,10 @@ Definition equality_morphism_of_setoid_theory: unfold make_compatibility_goal; simpl; split; eauto. Defined. -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. - (* END OF UTILITY/BACKWARD COMPATIBILITY PART *) (* A FEW EXAMPLES ON iff *) -Add Morphism iff with signature iff ==> iff ==> iff as Iff_Morphism. - tauto. -Qed. - (* impl IS A MORPHISM *) Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism. @@ -665,10 +674,6 @@ Qed. (* THE SAME EXAMPLES ON impl *) -Add Morphism impl with signature impl --> impl ++> impl as Impl_Morphism2. - unfold impl; tauto. -Qed. - Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2. unfold impl; tauto. Qed. -- cgit v1.2.3