diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 70b9be8acc1d1ada178a95c1cd4013506e9d0d1b (patch) | |
tree | f672a286d962cc67c95874b3b60402fc957870b6 /theories/Setoids/Setoid.v | |
parent | a5bd4e097a94cc4f863bf4d4bcc5ce592c30ba47 (diff) | |
parent | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff) |
Merge commit 'upstream/8.1.gamma' into 8.1
Diffstat (limited to 'theories/Setoids/Setoid.v')
-rw-r--r-- | theories/Setoids/Setoid.v | 723 |
1 files changed, 368 insertions, 355 deletions
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index b670fc19..84af7d5d 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -7,13 +7,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Setoid.v 8866 2006-05-28 16:21:04Z herbelin $: i*) +(*i $Id: Setoid.v 9245 2006-10-17 12:53:34Z notin $: i*) Require Export Relation_Definitions. Set Implicit Arguments. -(* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *) +(** * Definitions of [Relation_Class] and n-ary [Morphism_Theory] *) (* X will be used to distinguish covariant arguments whose type is an *) (* Asymmetric* relation from contravariant arguments of the same type *) @@ -46,50 +46,50 @@ Inductive Areflexive_Relation_Class : Type := Implicit Type Hole Out: Relation_Class. Definition relation_class_of_argument_class : Argument_Class -> Relation_Class. - destruct 1. - exact (SymmetricReflexive _ s r). - exact (AsymmetricReflexive tt r). - exact (SymmetricAreflexive _ s). - exact (AsymmetricAreflexive tt Aeq). - exact (Leibniz _ T). + destruct 1. + exact (SymmetricReflexive _ s r). + exact (AsymmetricReflexive tt r). + exact (SymmetricAreflexive _ s). + exact (AsymmetricAreflexive tt Aeq). + exact (Leibniz _ T). Defined. Definition carrier_of_relation_class : forall X, X_Relation_Class X -> Type. - destruct 1. - exact A. - exact A. - exact A. - exact A. - exact T. + destruct 1. + exact A. + exact A. + exact A. + exact A. + exact T. Defined. Definition relation_of_relation_class : - forall X R, @carrier_of_relation_class X R -> carrier_of_relation_class R -> Prop. - destruct R. - exact Aeq. - exact Aeq. - exact Aeq. - exact Aeq. - exact (@eq T). + forall X R, @carrier_of_relation_class X R -> carrier_of_relation_class R -> Prop. + destruct R. + exact Aeq. + exact Aeq. + exact Aeq. + exact Aeq. + exact (@eq T). Defined. Lemma about_carrier_of_relation_class_and_relation_class_of_argument_class : - forall R, - carrier_of_relation_class (relation_class_of_argument_class R) = - carrier_of_relation_class R. - destruct R; reflexivity. - Defined. + forall R, + carrier_of_relation_class (relation_class_of_argument_class R) = + carrier_of_relation_class R. + destruct R; reflexivity. +Defined. Inductive nelistT (A : Type) : Type := singl : A -> nelistT A - | cons : A -> nelistT A -> nelistT A. + | necons : A -> nelistT A -> nelistT A. Definition Arguments := nelistT Argument_Class. Implicit Type In: Arguments. Definition function_type_of_morphism_signature : - Arguments -> Relation_Class -> Type. + Arguments -> Relation_Class -> Type. intros In Out. induction In. exact (carrier_of_relation_class a -> carrier_of_relation_class Out). @@ -97,12 +97,12 @@ Definition function_type_of_morphism_signature : Defined. Definition make_compatibility_goal_aux: - forall In Out - (f g: function_type_of_morphism_signature In Out), Prop. - intros; induction In; simpl in f, g. - induction a; simpl in f, g. - exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)). - destruct x. + forall In Out + (f g: function_type_of_morphism_signature In Out), Prop. + intros; induction In; simpl in f, g. + induction a; simpl in f, g. + exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)). + destruct x. exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)). exact (forall x1 x2, Aeq x2 x1 -> relation_of_relation_class Out (f x1) (g x2)). exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)). @@ -113,35 +113,58 @@ Definition make_compatibility_goal_aux: induction a; simpl in f, g. exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)). destruct x. - exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)). - exact (forall x1 x2, Aeq x2 x1 -> IHIn (f x1) (g x2)). + exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)). + exact (forall x1 x2, Aeq x2 x1 -> IHIn (f x1) (g x2)). exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)). destruct x. - exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)). - exact (forall x1 x2, Aeq x2 x1 -> IHIn (f x1) (g x2)). + exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)). + exact (forall x1 x2, Aeq x2 x1 -> IHIn (f x1) (g x2)). exact (forall x, IHIn (f x) (g x)). Defined. Definition make_compatibility_goal := - (fun In Out f => make_compatibility_goal_aux In Out f f). + (fun In Out f => make_compatibility_goal_aux In Out f f). Record Morphism_Theory In Out : Type := - {Function : function_type_of_morphism_signature In Out; - Compat : make_compatibility_goal In Out Function}. + { Function : function_type_of_morphism_signature In Out; + Compat : make_compatibility_goal In Out Function }. + +(** The [iff] relation class *) + +Definition Iff_Relation_Class : Relation_Class. + eapply (@SymmetricReflexive unit _ iff). + exact iff_sym. + exact iff_refl. +Defined. + +(** The [impl] relation class *) + +Definition impl (A B: Prop) := A -> B. + +Theorem impl_refl: reflexive _ impl. +Proof. + hnf; unfold impl; tauto. +Qed. + +Definition Impl_Relation_Class : Relation_Class. + eapply (@AsymmetricReflexive unit tt _ impl). + exact impl_refl. +Defined. + +(** Every function is a morphism from Leibniz+ to Leibniz *) Definition list_of_Leibniz_of_list_of_types: nelistT Type -> Arguments. induction 1. exact (singl (Leibniz _ a)). - exact (cons (Leibniz _ a) IHX). + exact (necons (Leibniz _ a) IHX). Defined. -(* every function is a morphism from Leibniz+ to Leibniz *) Definition morphism_theory_of_function : - forall (In: nelistT Type) (Out: Type), - let In' := list_of_Leibniz_of_list_of_types In in - let Out' := Leibniz _ Out in - function_type_of_morphism_signature In' Out' -> - Morphism_Theory In' Out'. + forall (In: nelistT Type) (Out: Type), + let In' := list_of_Leibniz_of_list_of_types In in + let Out' := Leibniz _ Out in + function_type_of_morphism_signature In' Out' -> + Morphism_Theory In' Out'. intros. exists X. induction In; unfold make_compatibility_goal; simpl. @@ -149,33 +172,26 @@ Definition morphism_theory_of_function : intro; apply (IHIn (X x)). Defined. -(* THE iff RELATION CLASS *) - -Definition Iff_Relation_Class : Relation_Class. - eapply (@SymmetricReflexive unit _ iff). - exact iff_sym. - exact iff_refl. -Defined. - -(* THE impl RELATION CLASS *) +(** Every predicate is a morphism from Leibniz+ to Iff_Relation_Class *) -Definition impl (A B: Prop) := A -> B. - -Theorem impl_refl: reflexive _ impl. - hnf; unfold impl; tauto. -Qed. - -Definition Impl_Relation_Class : Relation_Class. - eapply (@AsymmetricReflexive unit tt _ impl). - exact impl_refl. +Definition morphism_theory_of_predicate : + forall (In: nelistT Type), + let In' := list_of_Leibniz_of_list_of_types In in + function_type_of_morphism_signature In' Iff_Relation_Class -> + Morphism_Theory In' Iff_Relation_Class. + intros. + exists X. + induction In; unfold make_compatibility_goal; simpl. + intro; apply iff_refl. + intro; apply (IHIn (X x)). Defined. -(* UTILITY FUNCTIONS TO PROVE THAT EVERY TRANSITIVE RELATION IS A MORPHISM *) +(** * Utility functions to prove that every transitive relation is a morphism *) Definition equality_morphism_of_symmetric_areflexive_transitive_relation: forall (A: Type)(Aeq: relation A)(sym: symmetric _ Aeq)(trans: transitive _ Aeq), let ASetoidClass := SymmetricAreflexive _ sym in - (Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class). + (Morphism_Theory (necons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class). intros. exists Aeq. unfold make_compatibility_goal; simpl; split; eauto. @@ -184,7 +200,7 @@ Defined. Definition equality_morphism_of_symmetric_reflexive_transitive_relation: forall (A: Type)(Aeq: relation A)(refl: reflexive _ Aeq)(sym: symmetric _ Aeq) (trans: transitive _ Aeq), let ASetoidClass := SymmetricReflexive _ sym refl in - (Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class). + (Morphism_Theory (necons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class). intros. exists Aeq. unfold make_compatibility_goal; simpl; split; eauto. @@ -194,7 +210,7 @@ Definition equality_morphism_of_asymmetric_areflexive_transitive_relation: forall (A: Type)(Aeq: relation A)(trans: transitive _ Aeq), let ASetoidClass1 := AsymmetricAreflexive Contravariant Aeq in let ASetoidClass2 := AsymmetricAreflexive Covariant Aeq in - (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class). + (Morphism_Theory (necons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class). intros. exists Aeq. unfold make_compatibility_goal; simpl; unfold impl; eauto. @@ -204,120 +220,154 @@ Definition equality_morphism_of_asymmetric_reflexive_transitive_relation: forall (A: Type)(Aeq: relation A)(refl: reflexive _ Aeq)(trans: transitive _ Aeq), let ASetoidClass1 := AsymmetricReflexive Contravariant refl in let ASetoidClass2 := AsymmetricReflexive Covariant refl in - (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class). + (Morphism_Theory (necons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class). intros. exists Aeq. unfold make_compatibility_goal; simpl; unfold impl; eauto. Defined. -(* iff AS A RELATION *) +(** * A few examples on [iff] *) -Add Relation Prop iff - reflexivity proved by iff_refl - symmetry proved by iff_sym - transitivity proved by iff_trans - as iff_relation. +(** [iff] as a relation *) -(* every predicate is morphism from Leibniz+ to Iff_Relation_Class *) -Definition morphism_theory_of_predicate : - forall (In: nelistT Type), - let In' := list_of_Leibniz_of_list_of_types In in - function_type_of_morphism_signature In' Iff_Relation_Class -> - Morphism_Theory In' Iff_Relation_Class. - intros. - exists X. - induction In; unfold make_compatibility_goal; simpl. - intro; apply iff_refl. - intro; apply (IHIn (X x)). -Defined. +Add Relation Prop iff + reflexivity proved by iff_refl + symmetry proved by iff_sym + transitivity proved by iff_trans +as iff_relation. -(* impl AS A RELATION *) +(** [impl] as a relation *) Theorem impl_trans: transitive _ impl. - hnf; unfold impl; tauto. +Proof. + hnf; unfold impl; tauto. Qed. Add Relation Prop impl - reflexivity proved by impl_refl - transitivity proved by impl_trans - as impl_relation. + reflexivity proved by impl_refl + transitivity proved by impl_trans +as impl_relation. + +(** [impl] is a morphism *) + +Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism. +Proof. + unfold impl; tauto. +Qed. + +(** [and] is a morphism *) + +Add Morphism and with signature iff ==> iff ==> iff as And_Morphism. + tauto. +Qed. + +(** [or] is a morphism *) -(* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *) +Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism. +Proof. + tauto. +Qed. + +(** [not] is a morphism *) + +Add Morphism not with signature iff ==> iff as Not_Morphism. +Proof. + tauto. +Qed. + +(** The same examples on [impl] *) + +Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2. +Proof. + unfold impl; tauto. +Qed. + +Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2. +Proof. + unfold impl; tauto. +Qed. + +Add Morphism not with signature impl --> impl as Not_Morphism2. +Proof. + unfold impl; tauto. +Qed. + +(** * The CIC part of the reflexive tactic ([setoid_rewrite]) *) Inductive rewrite_direction : Type := - Left2Right - | Right2Left. + | Left2Right + | Right2Left. Implicit Type dir: rewrite_direction. Definition variance_of_argument_class : Argument_Class -> option variance. - destruct 1. - exact None. - exact (Some v). - exact None. - exact (Some v). - exact None. + destruct 1. + exact None. + exact (Some v). + exact None. + exact (Some v). + exact None. Defined. Definition opposite_direction := - fun dir => - match dir with - Left2Right => Right2Left - | Right2Left => Left2Right + fun dir => + match dir with + | Left2Right => Right2Left + | Right2Left => Left2Right end. Lemma opposite_direction_idempotent: - forall dir, (opposite_direction (opposite_direction dir)) = dir. + forall dir, (opposite_direction (opposite_direction dir)) = dir. +Proof. destruct dir; reflexivity. Qed. Inductive check_if_variance_is_respected : - option variance -> rewrite_direction -> rewrite_direction -> Prop -:= - MSNone : forall dir dir', check_if_variance_is_respected None dir dir' - | MSCovariant : forall dir, check_if_variance_is_respected (Some Covariant) dir dir - | MSContravariant : - forall dir, + option variance -> rewrite_direction -> rewrite_direction -> Prop := + | MSNone : forall dir dir', check_if_variance_is_respected None dir dir' + | MSCovariant : forall dir, check_if_variance_is_respected (Some Covariant) dir dir + | MSContravariant : + forall dir, check_if_variance_is_respected (Some Contravariant) dir (opposite_direction dir). Definition relation_class_of_reflexive_relation_class: - Reflexive_Relation_Class -> Relation_Class. - induction 1. - exact (SymmetricReflexive _ s r). - exact (AsymmetricReflexive tt r). - exact (Leibniz _ T). + Reflexive_Relation_Class -> Relation_Class. + induction 1. + 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 (SymmetricAreflexive _ s). - exact (AsymmetricAreflexive tt Aeq). + Areflexive_Relation_Class -> Relation_Class. + induction 1. + exact (SymmetricAreflexive _ s). + exact (AsymmetricAreflexive tt Aeq). Defined. Definition carrier_of_reflexive_relation_class := - fun R => carrier_of_relation_class (relation_class_of_reflexive_relation_class R). + fun R => carrier_of_relation_class (relation_class_of_reflexive_relation_class R). Definition carrier_of_areflexive_relation_class := - fun R => carrier_of_relation_class (relation_class_of_areflexive_relation_class R). + fun R => carrier_of_relation_class (relation_class_of_areflexive_relation_class R). Definition relation_of_areflexive_relation_class := - fun R => relation_of_relation_class (relation_class_of_areflexive_relation_class R). + fun R => relation_of_relation_class (relation_class_of_areflexive_relation_class R). Inductive Morphism_Context Hole dir : Relation_Class -> rewrite_direction -> Type := - App : - forall In Out dir', - Morphism_Theory In Out -> Morphism_Context_List Hole dir dir' In -> - Morphism_Context Hole dir Out dir' + | App : + forall In Out dir', + Morphism_Theory In Out -> Morphism_Context_List Hole dir dir' In -> + Morphism_Context Hole dir Out dir' | ToReplace : Morphism_Context Hole dir Hole dir | ToKeep : - forall S dir', + forall S dir', carrier_of_reflexive_relation_class S -> - Morphism_Context Hole dir (relation_class_of_reflexive_relation_class S) dir' - | ProperElementToKeep : - forall S dir' (x: carrier_of_areflexive_relation_class S), + Morphism_Context Hole dir (relation_class_of_reflexive_relation_class S) dir' + | ProperElementToKeep : + forall S dir' (x: carrier_of_areflexive_relation_class S), relation_of_areflexive_relation_class S x x -> - Morphism_Context Hole dir (relation_class_of_areflexive_relation_class S) dir' + Morphism_Context Hole dir (relation_class_of_areflexive_relation_class S) dir' with Morphism_Context_List Hole dir : rewrite_direction -> Arguments -> Type := @@ -331,53 +381,53 @@ with Morphism_Context_List Hole dir : check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' -> Morphism_Context Hole dir (relation_class_of_argument_class S) dir' -> Morphism_Context_List Hole dir dir'' L -> - Morphism_Context_List Hole dir dir'' (cons S L). + Morphism_Context_List Hole dir dir'' (necons S L). Scheme Morphism_Context_rect2 := Induction for Morphism_Context Sort Type with Morphism_Context_List_rect2 := Induction for Morphism_Context_List Sort Type. Definition product_of_arguments : Arguments -> Type. - induction 1. - exact (carrier_of_relation_class a). - exact (prod (carrier_of_relation_class a) IHX). + induction 1. + exact (carrier_of_relation_class a). + exact (prod (carrier_of_relation_class a) IHX). Defined. Definition get_rewrite_direction: rewrite_direction -> Argument_Class -> rewrite_direction. - intros dir R. -destruct (variance_of_argument_class R). - destruct v. - exact dir. (* covariant *) - exact (opposite_direction dir). (* contravariant *) - exact dir. (* symmetric relation *) + intros dir R. + destruct (variance_of_argument_class R). + destruct v. + exact dir. (* covariant *) + exact (opposite_direction dir). (* contravariant *) + exact dir. (* symmetric relation *) Defined. Definition directed_relation_of_relation_class: - forall dir (R: Relation_Class), - carrier_of_relation_class R -> carrier_of_relation_class R -> Prop. - destruct 1. - exact (@relation_of_relation_class unit). - intros; exact (relation_of_relation_class _ X0 X). + forall dir (R: Relation_Class), + carrier_of_relation_class R -> carrier_of_relation_class R -> Prop. + destruct 1. + exact (@relation_of_relation_class unit). + intros; exact (relation_of_relation_class _ X0 X). Defined. Definition directed_relation_of_argument_class: - forall dir (R: Argument_Class), - carrier_of_relation_class R -> carrier_of_relation_class R -> Prop. + forall dir (R: Argument_Class), + carrier_of_relation_class R -> carrier_of_relation_class R -> Prop. intros dir R. rewrite <- - (about_carrier_of_relation_class_and_relation_class_of_argument_class R). + (about_carrier_of_relation_class_and_relation_class_of_argument_class R). exact (directed_relation_of_relation_class dir (relation_class_of_argument_class R)). Defined. Definition relation_of_product_of_arguments: - forall dir In, - product_of_arguments In -> product_of_arguments In -> Prop. - induction In. - simpl. - exact (directed_relation_of_argument_class (get_rewrite_direction dir a) a). - - simpl; intros. - destruct X; destruct X0. + forall dir In, + product_of_arguments In -> product_of_arguments In -> Prop. + induction In. + simpl. + exact (directed_relation_of_argument_class (get_rewrite_direction dir a) a). + + simpl; intros. + destruct X; destruct X0. apply and. exact (directed_relation_of_argument_class (get_rewrite_direction dir a) a c c0). @@ -385,32 +435,32 @@ Definition relation_of_product_of_arguments: Defined. Definition apply_morphism: - forall In Out (m: function_type_of_morphism_signature In Out) - (args: product_of_arguments In), carrier_of_relation_class Out. - intros. - induction In. - exact (m args). - simpl in m, args. - destruct args. - exact (IHIn (m c) p). + forall In Out (m: function_type_of_morphism_signature In Out) + (args: product_of_arguments In), carrier_of_relation_class Out. + intros. + induction In. + exact (m args). + simpl in m, args. + destruct args. + exact (IHIn (m c) p). Defined. Theorem apply_morphism_compatibility_Right2Left: - forall In Out (m1 m2: function_type_of_morphism_signature In Out) - (args1 args2: product_of_arguments In), - make_compatibility_goal_aux _ _ m1 m2 -> - relation_of_product_of_arguments Right2Left _ args1 args2 -> - directed_relation_of_relation_class Right2Left _ - (apply_morphism _ _ m2 args1) - (apply_morphism _ _ m1 args2). + forall In Out (m1 m2: function_type_of_morphism_signature In Out) + (args1 args2: product_of_arguments In), + make_compatibility_goal_aux _ _ m1 m2 -> + relation_of_product_of_arguments Right2Left _ args1 args2 -> + directed_relation_of_relation_class Right2Left _ + (apply_morphism _ _ m2 args1) + (apply_morphism _ _ m1 args2). induction In; intros. simpl in m1, m2, args1, args2, H0 |- *. destruct a; simpl in H; hnf in H0. - apply H; exact H0. - destruct v; simpl in H0; apply H; exact H0. - apply H; exact H0. - destruct v; simpl in H0; apply H; exact H0. - rewrite H0; apply H; exact H0. + apply H; exact H0. + destruct v; simpl in H0; apply H; exact H0. + apply H; exact H0. + destruct v; simpl in H0; apply H; exact H0. + rewrite H0; apply H; exact H0. simpl in m1, m2, args1, args2, H0 |- *. destruct args1; destruct args2; simpl. @@ -443,46 +493,47 @@ Theorem apply_morphism_compatibility_Right2Left: Qed. Theorem apply_morphism_compatibility_Left2Right: - forall In Out (m1 m2: function_type_of_morphism_signature In Out) - (args1 args2: product_of_arguments In), - make_compatibility_goal_aux _ _ m1 m2 -> - relation_of_product_of_arguments Left2Right _ args1 args2 -> - directed_relation_of_relation_class Left2Right _ - (apply_morphism _ _ m1 args1) - (apply_morphism _ _ m2 args2). + forall In Out (m1 m2: function_type_of_morphism_signature In Out) + (args1 args2: product_of_arguments In), + make_compatibility_goal_aux _ _ m1 m2 -> + relation_of_product_of_arguments Left2Right _ args1 args2 -> + directed_relation_of_relation_class Left2Right _ + (apply_morphism _ _ m1 args1) + (apply_morphism _ _ m2 args2). +Proof. induction In; intros. simpl in m1, m2, args1, args2, H0 |- *. destruct a; simpl in H; hnf in H0. + apply H; exact H0. + destruct v; simpl in H0; apply H; exact H0. + apply H; exact H0. + destruct v; simpl in H0; apply H; exact H0. + rewrite H0; apply H; exact H0. + + simpl in m1, m2, args1, args2, H0 |- *. + destruct args1; destruct args2; simpl. + destruct H0. + simpl in H. + destruct a; simpl in H. + apply IHIn. + apply H; exact H0. + exact H1. + destruct v. + apply IHIn. apply H; exact H0. - destruct v; simpl in H0; apply H; exact H0. - apply H; exact H0. - destruct v; simpl in H0; apply H; exact H0. - rewrite H0; apply H; exact H0. - - simpl in m1, m2, args1, args2, H0 |- *. - destruct args1; destruct args2; simpl. - destruct H0. - simpl in H. - destruct a; simpl in H. - apply IHIn. - apply H; exact H0. - exact H1. - destruct v. - apply IHIn. - apply H; exact H0. - exact H1. - apply IHIn. - apply H; exact H0. exact H1. - apply IHIn. - apply H; exact H0. - exact H1. - apply IHIn. - destruct v; simpl in H, H0; apply H; exact H0. + apply IHIn. + apply H; exact H0. + exact H1. + apply IHIn. + apply H; exact H0. exact H1. - rewrite H0; apply IHIn. - apply H. - exact H1. + apply IHIn. + destruct v; simpl in H, H0; apply H; exact H0. + exact H1. + rewrite H0; apply IHIn. + apply H. + exact H1. Qed. Definition interp : @@ -508,83 +559,84 @@ Definition interp : exact X0. Defined. -(*CSC: interp and interp_relation_class_list should be mutually defined, since +(* CSC: interp and interp_relation_class_list should be mutually defined, since the proof term of each one contains the proof term of the other one. However I cannot do that interactively (I should write the Fix by hand) *) Definition interp_relation_class_list : - forall Hole dir dir' (L: Arguments), carrier_of_relation_class Hole -> - Morphism_Context_List Hole dir dir' L -> product_of_arguments L. - intros Hole dir dir' L H t. - elim t using - (@Morphism_Context_List_rect2 Hole dir (fun S _ _ => carrier_of_relation_class S) - (fun _ L fcl => product_of_arguments L)); - intros. - exact (apply_morphism _ _ (Function m) X). - exact H. - exact c. - exact x. - simpl; - rewrite <- - (about_carrier_of_relation_class_and_relation_class_of_argument_class S); - exact X. - split. - rewrite <- - (about_carrier_of_relation_class_and_relation_class_of_argument_class S); - exact X. - exact X0. + forall Hole dir dir' (L: Arguments), carrier_of_relation_class Hole -> + Morphism_Context_List Hole dir dir' L -> product_of_arguments L. + intros Hole dir dir' L H t. + elim t using + (@Morphism_Context_List_rect2 Hole dir (fun S _ _ => carrier_of_relation_class S) + (fun _ L fcl => product_of_arguments L)); + intros. + exact (apply_morphism _ _ (Function m) X). + exact H. + exact c. + exact x. + simpl; + rewrite <- + (about_carrier_of_relation_class_and_relation_class_of_argument_class S); + exact X. + split. + rewrite <- + (about_carrier_of_relation_class_and_relation_class_of_argument_class S); + exact X. + exact X0. Defined. Theorem setoid_rewrite: - forall Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole) - (E: Morphism_Context Hole dir Out dir'), - (directed_relation_of_relation_class dir Hole E1 E2) -> + forall Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole) + (E: Morphism_Context Hole dir Out dir'), + (directed_relation_of_relation_class dir Hole E1 E2) -> (directed_relation_of_relation_class dir' Out (interp E1 E) (interp E2 E)). - intros. - elim E using - (@Morphism_Context_rect2 Hole dir - (fun S dir'' E => directed_relation_of_relation_class dir'' S (interp E1 E) (interp E2 E)) - (fun dir'' L fcl => +Proof. + intros. + elim E using + (@Morphism_Context_rect2 Hole dir + (fun S dir'' E => directed_relation_of_relation_class dir'' S (interp E1 E) (interp E2 E)) + (fun dir'' L fcl => relation_of_product_of_arguments dir'' _ - (interp_relation_class_list E1 fcl) - (interp_relation_class_list E2 fcl))); intros. - change (directed_relation_of_relation_class dir'0 Out0 + (interp_relation_class_list E1 fcl) + (interp_relation_class_list E2 fcl))); intros. + change (directed_relation_of_relation_class dir'0 Out0 (apply_morphism _ _ (Function m) (interp_relation_class_list E1 m0)) (apply_morphism _ _ (Function m) (interp_relation_class_list E2 m0))). - destruct dir'0. - apply apply_morphism_compatibility_Left2Right. - exact (Compat m). - exact H0. - apply apply_morphism_compatibility_Right2Left. - exact (Compat m). - exact H0. - - exact H. - - unfold interp, Morphism_Context_rect2. - (*CSC: reflexivity used here*) - destruct S; destruct dir'0; simpl; (apply r || reflexivity). - - destruct dir'0; exact r. + destruct dir'0. + apply apply_morphism_compatibility_Left2Right. + exact (Compat m). + exact H0. + apply apply_morphism_compatibility_Right2Left. + exact (Compat m). + exact H0. + + exact H. + + unfold interp, Morphism_Context_rect2. + (* CSC: reflexivity used here *) + destruct S; destruct dir'0; simpl; (apply r || reflexivity). + + 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 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; - generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros; - (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 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; - generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros; - (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3). - destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0). + unfold get_rewrite_direction; simpl. + destruct dir'0; destruct dir''; + (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; + generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros; + (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 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; + generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros; + (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3). + destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0). change (directed_relation_of_argument_class (get_rewrite_direction dir'' S) S @@ -592,96 +644,57 @@ Theorem setoid_rewrite: (about_carrier_of_relation_class_and_relation_class_of_argument_class S)) (eq_rect _ (fun T : Type => T) (interp E2 m) _ (about_carrier_of_relation_class_and_relation_class_of_argument_class S)) /\ - relation_of_product_of_arguments dir'' _ + relation_of_product_of_arguments dir'' _ (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 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 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; symmetry; exact H0). - exact H1. -Qed. - -(* BEGIN OF UTILITY/BACKWARD COMPATIBILITY PART *) + split. + clear m0 H1; destruct S; simpl in H0 |- *; unfold get_rewrite_direction; simpl. + 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 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; symmetry; exact H0). + exact H1. + Qed. + +(** * Miscelenous *) + +(** For backwark 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}. - -(* END OF UTILITY/BACKWARD COMPATIBILITY PART *) - -(* A FEW EXAMPLES ON iff *) - -(* impl IS A MORPHISM *) + { 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 }. -Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism. -unfold impl; tauto. -Qed. - -(* and IS A MORPHISM *) - -Add Morphism and with signature iff ==> iff ==> iff as And_Morphism. - tauto. -Qed. - -(* or IS A MORPHISM *) - -Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism. - tauto. -Qed. - -(* not IS A MORPHISM *) - -Add Morphism not with signature iff ==> iff as Not_Morphism. - tauto. -Qed. - -(* THE SAME EXAMPLES ON impl *) - -Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2. - unfold impl; tauto. -Qed. - -Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2. - unfold impl; tauto. -Qed. - -Add Morphism not with signature impl --> impl as Not_Morphism2. - unfold impl; tauto. -Qed. - -(* FOR BACKWARD COMPATIBILITY *) Implicit Arguments Setoid_Theory []. Implicit Arguments Seq_refl []. Implicit Arguments Seq_sym []. Implicit Arguments Seq_trans []. -(* Some tactics for manipulating Setoid Theory not officially - declared as Setoid. *) +(** Some tactics for manipulating Setoid Theory not officially + declared as Setoid. *) Ltac trans_st x := match goal with - | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => - apply (Seq_trans _ _ H) with x; auto - end. + | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => + apply (Seq_trans _ _ H) with x; auto + end. Ltac sym_st := match goal with - | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => - apply (Seq_sym _ _ H); auto - end. + | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => + apply (Seq_sym _ _ H); auto + end. Ltac refl_st := match goal with - | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => - apply (Seq_refl _ _ H); auto - end. + | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => + apply (Seq_refl _ _ H); auto + end. Definition gen_st : forall A : Set, Setoid_Theory _ (@eq A). -Proof. constructor; congruence. Qed. - +Proof. + constructor; congruence. +Qed. + |