From a7313888d9d9531bbcce3857842785ee49469c6d Mon Sep 17 00:00:00 2001 From: sacerdot Date: Mon, 18 Oct 2004 16:32:44 +0000 Subject: * Code simplification and clean-up. In particular there is no more code duplicated between add_relation and add_setoid. * Less ad-hoc backward compatibility lemmas for setoids required in Setoid.v * Term size reduction (first part): when a relation is registered, we add to the environment a definition that gives back either the relation as an argument or as a relation class. The definition is used to reduce the term size. [ Note: we could save a bit more by defining two definitions in place of one. However, we suppose that the lambda term fragments generated can be shared quite effectively. Thus we would recive almost no benefit by sharing in terms of size. What about proof checking time? ] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6238 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Setoids/Setoid.v | 26 -------------------------- 1 file changed, 26 deletions(-) (limited to 'theories/Setoids') diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index 2d48e82df..51703b23e 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -618,32 +618,6 @@ Record Setoid_Theory (A: Type) (Aeq: relation A) : Prop := 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}. -Definition argument_class_of_setoid_theory: - forall (A: Type) (Aeq: relation A), - Setoid_Theory Aeq -> Argument_Class. - intros. - apply (@SymmetricReflexive variance _ Aeq). - exact (Seq_sym H). - exact (Seq_refl H). -Defined. - -Definition relation_class_of_setoid_theory := - fun A Aeq Setoid => - relation_class_of_argument_class - (@argument_class_of_setoid_theory A Aeq Setoid). - -Definition equality_morphism_of_setoid_theory: - forall (A: Type) (Aeq: relation A) (ST: Setoid_Theory Aeq), - let ASetoidClass := argument_class_of_setoid_theory ST in - (Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) - Iff_Relation_Class). - intros. - exists Aeq. - pose (sym := Seq_sym ST); clearbody sym. - pose (trans := Seq_trans ST); clearbody trans. - unfold make_compatibility_goal; simpl; split; eauto. -Defined. - (* END OF UTILITY/BACKWARD COMPATIBILITY PART *) (* A FEW EXAMPLES ON iff *) -- cgit v1.2.3