diff options
author | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /theories/Setoids/Setoid_Prop.v | |
parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'theories/Setoids/Setoid_Prop.v')
-rw-r--r-- | theories/Setoids/Setoid_Prop.v | 79 |
1 files changed, 0 insertions, 79 deletions
diff --git a/theories/Setoids/Setoid_Prop.v b/theories/Setoids/Setoid_Prop.v deleted file mode 100644 index 7300937e..00000000 --- a/theories/Setoids/Setoid_Prop.v +++ /dev/null @@ -1,79 +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_Prop.v 10739 2008-04-01 14:45:20Z herbelin $: i*) - -Require Import Setoid_tac. - -(** * A few examples on [iff] *) - -(** [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. - -(** [impl] as a relation *) - -Theorem impl_trans: transitive _ impl. -Proof. - hnf; unfold impl; tauto. -Qed. - -Add Relation Prop impl - reflexivity proved by impl_refl - transitivity proved by impl_trans -as impl_relation. - -(** [impl] is a morphism *) - -Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism. -Proof. - unfold impl; tauto. -Qed. - -(** [and] is a morphism *) - -Add Morphism and with signature iff ==> iff ==> iff as And_Morphism. - tauto. -Qed. - -(** [or] is a morphism *) - -Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism. -Proof. - tauto. -Qed. - -(** [not] is a morphism *) - -Add Morphism not with signature iff ==> iff as Not_Morphism. -Proof. - tauto. -Qed. - -(** The same examples on [impl] *) - -Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2. -Proof. - unfold impl; tauto. -Qed. - -Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2. -Proof. - unfold impl; tauto. -Qed. - -Add Morphism not with signature impl --> impl as Not_Morphism2. -Proof. - unfold impl; tauto. -Qed. - |