From fc3f8eb9bcb6645a97a35335d588dbd50231689b Mon Sep 17 00:00:00 2001 From: msozeau Date: Tue, 8 Apr 2008 16:15:23 +0000 Subject: - A little cleanup in Classes/*. Separate standard morphisms on relf/sym/trans relations from morphisms on prop connectives and relations. - Add general order theory on predicates, instantiated for relations. Derives equivalence, implication, conjunction and disjunction as liftings from propositional connectives. Can be used for n-ary homogeneous predicates thanks to a bit of metaprogramming with lists of types. - Rebind Setoid_Theory to use the Equivalence record type instead of declaring an isomorphic one. One needs to do "red" after constructor to get the same statements when building objects of type Setoid_Theory, so scripts break. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10765 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Setoids/Setoid.v | 20 ++++++++------------ 1 file changed, 8 insertions(+), 12 deletions(-) (limited to 'theories/Setoids') diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index 983c651ab..8f59c048f 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -8,22 +8,18 @@ (*i $Id$: i*) -Set Implicit Arguments. - Require Export Coq.Classes.SetoidTactics. (** For backward compatibility *) -Record Setoid_Theory (A: Type) (Aeq: relation A) : Prop := - { Seq_refl : forall x:A, Aeq x x; - Seq_sym : forall x y:A, Aeq x y -> Aeq y x; - Seq_trans : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z }. - -Implicit Arguments Setoid_Theory []. -Implicit Arguments Seq_refl []. -Implicit Arguments Seq_sym []. -Implicit Arguments Seq_trans []. - +Definition Setoid_Theory := @Equivalence. +Definition Build_Setoid_Theory := @Build_Equivalence. +Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x := + Eval compute in reflexivity. +Definition Seq_sym A Aeq (s : Setoid_Theory A Aeq) : forall x y:A, Aeq x y -> Aeq y x := + Eval compute in symmetry. +Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z := + Eval compute in transitivity. (** Some tactics for manipulating Setoid Theory not officially declared as Setoid. *) -- cgit v1.2.3