From 8d065d79d7b358d85a335a581933e1a3d67ef863 Mon Sep 17 00:00:00 2001 From: sacerdot Date: Wed, 8 Sep 2004 16:21:50 +0000 Subject: * cleaning/renaming * reuse of definitions already given in the standard library git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6083 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Setoids/Setoid.v | 72 ++++++++++++++++++++--------------------------- 1 file changed, 31 insertions(+), 41 deletions(-) (limited to 'theories/Setoids') diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index 91745c98b..7cf89bb74 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -9,24 +9,20 @@ (*i $Id$: i*) +Require Export Relation_Definitions. + Set Implicit Arguments. (* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *) -Definition is_reflexive (A: Type) (Aeq: A -> A -> Prop) : Prop := - forall x:A, Aeq x x. - -Definition is_symmetric (A: Type) (Aeq: A -> A -> Prop) : Prop := - forall (x y:A), Aeq x y -> Aeq y x. - -(* X will be used to distinguish covariant arguments whose type is an *) -(* AsymmetricReflexive relation from covariant arguments of the same type*) +(* X will be used to distinguish covariant arguments whose type is an *) +(* Asymmetric* relation from contravariant arguments of the same type *) Inductive X_Relation_Class (X: Type) : Type := SymmetricReflexive : - forall A Aeq, @is_symmetric A Aeq -> is_reflexive Aeq -> X_Relation_Class X - | AsymmetricReflexive : X -> forall A Aeq, @is_reflexive A Aeq -> X_Relation_Class X - | Symmetric : forall A Aeq, @is_symmetric A Aeq -> X_Relation_Class X - | Asymmetric : X -> forall A (Aeq : A -> A -> Prop), X_Relation_Class X + forall A Aeq, symmetric A Aeq -> reflexive _ Aeq -> X_Relation_Class X + | AsymmetricReflexive : X -> forall A Aeq, reflexive A Aeq -> X_Relation_Class X + | SymmetricAreflexive : forall A Aeq, symmetric A Aeq -> X_Relation_Class X + | AsymmetricAreflexive : X -> forall A (Aeq : relation A), X_Relation_Class X | Leibniz : Type -> X_Relation_Class X. Inductive variance : Set := @@ -40,10 +36,10 @@ Implicit Type Hole Out: Relation_Class. Definition relation_class_of_argument_class : Argument_Class -> Relation_Class. destruct 1. - exact (SymmetricReflexive _ i i0). - exact (AsymmetricReflexive tt i). - exact (Symmetric _ i). - exact (Asymmetric tt Aeq). + exact (SymmetricReflexive _ s r). + exact (AsymmetricReflexive tt r). + exact (SymmetricAreflexive _ s). + exact (AsymmetricAreflexive tt Aeq). exact (Leibniz _ T). Defined. @@ -204,29 +200,29 @@ Inductive check_if_variance_is_respected : check_if_variance_is_respected (Some Contravariant) dir (opposite_direction dir). Inductive Reflexive_Relation_Class : Type := - RSymmetricReflexive : - forall A Aeq, @is_symmetric A Aeq -> is_reflexive Aeq -> Reflexive_Relation_Class - | RAsymmetricReflexive : - forall A Aeq, @is_reflexive A Aeq -> Reflexive_Relation_Class + RSymmetric : + forall A Aeq, symmetric A Aeq -> reflexive _ Aeq -> Reflexive_Relation_Class + | RAsymmetric : + forall A Aeq, reflexive A Aeq -> Reflexive_Relation_Class | RLeibniz : Type -> Reflexive_Relation_Class. Inductive Areflexive_Relation_Class : Type := - | ASymmetric : forall A Aeq, @is_symmetric A Aeq -> Areflexive_Relation_Class - | AAsymmetric : forall A (Aeq : A -> A -> Prop), Areflexive_Relation_Class. + | ASymmetric : forall A Aeq, symmetric A Aeq -> Areflexive_Relation_Class + | AAsymmetric : forall A (Aeq : relation A), Areflexive_Relation_Class. Definition relation_class_of_reflexive_relation_class: Reflexive_Relation_Class -> Relation_Class. induction 1. - exact (SymmetricReflexive _ i i0). - exact (AsymmetricReflexive tt i). + exact (SymmetricReflexive _ s r). + exact (AsymmetricReflexive tt r). exact (Leibniz _ T). Defined. Definition relation_class_of_areflexive_relation_class: Areflexive_Relation_Class -> Relation_Class. induction 1. - exact (Symmetric _ i). - exact (Asymmetric tt Aeq). + exact (SymmetricAreflexive _ s). + exact (AsymmetricAreflexive tt Aeq). Defined. Definition carrier_of_reflexive_relation_class := @@ -499,21 +495,15 @@ Theorem setoid_rewrite: unfold interp, Morphism_Context_rect2. (*CSC: reflexivity used here*) - destruct S; destruct dir'0; simpl. - apply i0. - apply i0. - apply i. - apply i. - reflexivity. - reflexivity. + destruct S; destruct dir'0; simpl; (apply r || reflexivity). - destruct dir'0; exact r. + destruct dir'0; exact r. destruct S; unfold directed_relation_of_argument_class; simpl in H0 |- *; unfold get_rewrite_direction; simpl. destruct dir'0; destruct dir''; (exact H0 || - unfold directed_relation_of_argument_class; simpl; apply i; exact H0). + unfold directed_relation_of_argument_class; simpl; apply s; exact H0). (* the following mess with generalize/clear/intros is to help Coq resolving *) (* second order unification problems. *) generalize m c H0; clear H0 m c; inversion c; @@ -521,7 +511,7 @@ Theorem setoid_rewrite: (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3). destruct dir'0; destruct dir''; (exact H0 || - unfold directed_relation_of_argument_class; simpl; apply i; exact H0). + unfold directed_relation_of_argument_class; simpl; apply s; exact H0). (* the following mess with generalize/clear/intros is to help Coq resolving *) (* second order unification problems. *) generalize m c H0; clear H0 m c; inversion c; @@ -539,11 +529,11 @@ Theorem setoid_rewrite: (interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)). split. clear m0 H1; destruct S; simpl in H0 |- *; unfold get_rewrite_direction; simpl. - destruct dir''; destruct dir'0; (exact H0 || hnf; apply i; exact H0). + destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0). inversion c. rewrite <- H3; exact H0. rewrite (opposite_direction_idempotent dir'0); exact H0. - destruct dir''; destruct dir'0; (exact H0 || hnf; apply i; exact H0). + destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0). inversion c. rewrite <- H3; exact H0. rewrite (opposite_direction_idempotent dir'0); exact H0. @@ -553,13 +543,13 @@ Qed. (* BEGIN OF UTILITY/BACKWARD COMPATIBILITY PART *) -Record Setoid_Theory (A: Type) (Aeq: A -> A -> Prop) : Prop := +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}. Definition argument_class_of_setoid_theory: - forall (A: Type) (Aeq: A -> A -> Prop), + forall (A: Type) (Aeq: relation A), Setoid_Theory Aeq -> Argument_Class. intros. apply (@SymmetricReflexive variance _ Aeq). @@ -573,7 +563,7 @@ Definition relation_class_of_setoid_theory := (@argument_class_of_setoid_theory A Aeq Setoid). Definition equality_morphism_of_setoid_theory: - forall (A: Type) (Aeq: A -> A -> Prop) (ST: Setoid_Theory Aeq), + 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)) Prop_Relation_Class). -- cgit v1.2.3