From bef5058398fc59c4b010977967d9a58730e62e1b Mon Sep 17 00:00:00 2001 From: sacerdot Date: Wed, 29 Sep 2004 12:56:25 +0000 Subject: impl relation and impl/and/or/not morphisms over impl declared. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6153 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Setoids/Setoid.v | 30 +++++++++++++++++++++++++----- 1 file changed, 25 insertions(+), 5 deletions(-) (limited to 'theories/Setoids') diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index 7cf89bb74..7d8196a72 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -580,7 +580,7 @@ Defined. Add Morphism iff : Iff_Morphism. tauto. -Defined. +Qed. (* impl IS A MORPHISM *) @@ -588,25 +588,45 @@ Definition impl (A B: Prop) := A -> B. Add Morphism impl : Impl_Morphism. unfold impl; tauto. -Defined. +Qed. (* and IS A MORPHISM *) Add Morphism and : And_Morphism. tauto. -Defined. +Qed. (* or IS A MORPHISM *) Add Morphism or : Or_Morphism. tauto. -Defined. +Qed. (* not IS A MORPHISM *) Add Morphism not : Not_Morphism. tauto. -Defined. +Qed. + +(* THE ASYMMETRIC AREFLEXIVE RELATION impl WITH A FEW MORPHISMS *) + +Add Relation Prop 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. + +Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2. + unfold impl; tauto. +Qed. + +Add Morphism not with signature impl --> impl as Not_Morphism2. + unfold impl; tauto. +Qed. (* FOR BACKWARD COMPATIBILITY *) Implicit Arguments Setoid_Theory []. -- cgit v1.2.3