diff options
author | clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-19 12:03:50 +0000 |
---|---|---|
committer | clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-19 12:03:50 +0000 |
commit | d35d4a8c279cc39d54037ceb97510b56d12e6a1a (patch) | |
tree | 17924b1167bc2ac4e09ad457f5ca50e1373306c5 /theories/Setoids | |
parent | 70d71580aed122f4966de27fcacdd8b3997d7a9c (diff) |
Deplacement des setoides.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1992 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Setoids')
-rw-r--r-- | theories/Setoids/Setoid.v | 75 |
1 files changed, 75 insertions, 0 deletions
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v new file mode 100644 index 000000000..80dfe2d63 --- /dev/null +++ b/theories/Setoids/Setoid.v @@ -0,0 +1,75 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$: *) + +Require Export Setoid_replace. + +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]. +Save. + +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). +Save. + +Add Morphism and : and_ext. +Intros. +Inversion H1. +Split. +Inversion H. +Apply (H4 H2). + +Inversion H0. +Apply (H4 H3). +Save. + +Add Morphism not : not_ext. +Red ; Intros. +Apply H0. +Inversion H. +Apply (H3 H1). +Save. + +Definition fleche [A,B:Prop] := A -> B. + +Add Morphism fleche : fleche_ext. +Unfold fleche. +Intros. +Inversion H0. +Inversion H. +Apply (H3 (H1 (H6 H2))). +Save. + |