diff options
Diffstat (limited to 'theories/Setoids')
-rw-r--r-- | theories/Setoids/Setoid.v | 100 |
1 files changed, 70 insertions, 30 deletions
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index bde24eded..c0ab8aa55 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -138,22 +138,22 @@ Definition morphism_theory_of_function : intro; apply (IHIn (X x)). Defined. -(* THE Prop RELATION CLASS *) +(* THE iff RELATION CLASS *) -Add Relation Prop iff reflexivity proved by iff_refl symmetry proved by iff_sym. +Add Relation Prop iff reflexivity proved by iff_refl symmetry proved by iff_sym as iff_relation. -Definition Prop_Relation_Class : Relation_Class. +Definition Iff_Relation_Class : Relation_Class. eapply (@SymmetricReflexive unit _ iff). exact iff_sym. exact iff_refl. Defined. -(* every predicate is morphism from Leibniz+ to Prop_Relation_Class *) +(* 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' Prop_Relation_Class -> - Morphism_Theory In' Prop_Relation_Class. + 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. @@ -161,6 +161,25 @@ 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. + +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. + (* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *) Inductive rewrite_direction : Type := @@ -566,7 +585,7 @@ Definition equality_morphism_of_setoid_theory: forall (A: Type) (Aeq: relation A) (ST: Setoid_Theory Aeq), let ASetoidClass := argument_class_of_setoid_theory ST in (Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) - Prop_Relation_Class). + Iff_Relation_Class). intros. exists Aeq. pose (sym := Seq_sym ST); clearbody sym. @@ -574,56 +593,77 @@ Definition equality_morphism_of_setoid_theory: unfold make_compatibility_goal; simpl; split; eauto. Defined. -Lemma eq_setoid : forall R, Setoid_Theory (@eq R). -Proof - (fun R => - Build_Setoid_Theory (@eq R) (@refl_equal R) (@sym_eq R) (@trans_eq R)). +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 *) +(* A FEW EXAMPLES ON iff *) -Add Morphism iff : Iff_Morphism. +Add Morphism iff with signature iff ==> iff ==> iff as Iff_Morphism. tauto. Qed. (* impl IS A MORPHISM *) -Definition impl (A B: Prop) := A -> B. - -Add Morphism impl : Impl_Morphism. +Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism. unfold impl; tauto. Qed. (* and IS A MORPHISM *) -Add Morphism and : And_Morphism. +Add Morphism and with signature iff ==> iff ==> iff as And_Morphism. tauto. Qed. (* or IS A MORPHISM *) -Add Morphism or : Or_Morphism. +Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism. tauto. Qed. (* not IS A MORPHISM *) -Add Morphism not : Not_Morphism. +Add Morphism not with signature iff ==> iff as Not_Morphism. tauto. Qed. -Theorem impl_refl: reflexive _ impl. - hnf; unfold impl; tauto. -Qed. - -Theorem impl_trans: transitive _ impl. - hnf; unfold impl; tauto. -Qed. - -(* THE ASYMMETRIC AREFLEXIVE RELATION impl WITH A FEW MORPHISMS *) - -Add Relation Prop impl reflexivity proved by impl_refl. +(* THE SAME EXAMPLES ON impl *) Add Morphism impl with signature impl --> impl ++> impl as Impl_Morphism2. unfold impl; tauto. |