diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 16:15:58 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 16:15:58 +0000 |
commit | 9058fb97426307536f56c3e7447be2f70798e081 (patch) | |
tree | b9a5fcf2ace7ecec13ed264b93c33fc04b0f220f /theories7/Setoids/Setoid.v | |
parent | 95ad10e5eb2efc9b63382e0e6a2f9ada8da2ea2d (diff) |
Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et states7
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5026 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories7/Setoids/Setoid.v')
-rw-r--r-- | theories7/Setoids/Setoid.v | 73 |
1 files changed, 73 insertions, 0 deletions
diff --git a/theories7/Setoids/Setoid.v b/theories7/Setoids/Setoid.v new file mode 100644 index 000000000..8a5a9892a --- /dev/null +++ b/theories7/Setoids/Setoid.v @@ -0,0 +1,73 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$: i*) + +Section Setoid. + +Variable A : Type. +Variable Aeq : A -> A -> Prop. + +Record Setoid_Theory : Prop := +{ Seq_refl : (x:A) (Aeq x x); + Seq_sym : (x,y:A) (Aeq x y) -> (Aeq y x); + Seq_trans : (x,y,z:A) (Aeq x y) -> (Aeq y z) -> (Aeq x z) +}. + +End Setoid. + +Definition Prop_S : (Setoid_Theory Prop iff). +Split; [Exact iff_refl | Exact iff_sym | Exact iff_trans]. +Qed. + +Add Setoid Prop iff Prop_S. + +Hint prop_set : setoid := Resolve (Seq_refl Prop iff Prop_S). +Hint prop_set : setoid := Resolve (Seq_sym Prop iff Prop_S). +Hint prop_set : setoid := Resolve (Seq_trans Prop iff Prop_S). + +Add Morphism or : or_ext. +Intros. +Inversion H1. +Left. +Inversion H. +Apply (H3 H2). + +Right. +Inversion H0. +Apply (H3 H2). +Qed. + +Add Morphism and : and_ext. +Intros. +Inversion H1. +Split. +Inversion H. +Apply (H4 H2). + +Inversion H0. +Apply (H4 H3). +Qed. + +Add Morphism not : not_ext. +Red ; Intros. +Apply H0. +Inversion H. +Apply (H3 H1). +Qed. + +Definition fleche [A,B:Prop] := A -> B. + +Add Morphism fleche : fleche_ext. +Unfold fleche. +Intros. +Inversion H0. +Inversion H. +Apply (H3 (H1 (H6 H2))). +Qed. + |