matita/library/technicalities/setoids.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti. C.Sacerdoti Coen.                          *)
   8 (*      ||A||       E.Tassi. S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* Code ported from the Coq theorem prover by Claudio Sacerdoti Coen *)
  16 (* Original author: Claudio Sacerdoti Coen. for the Coq system       *)
  17
  18 set "baseuri" "cic:/matita/technicalities/setoids".
  19
  20 include "higher_order_defs/relations.ma".
  21 include "datatypes/constructors.ma".
  22
  23 (* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *)
  24
  25 (* X will be used to distinguish covariant arguments whose type is an   *)
  26 (* Asymmetric* relation from contravariant arguments of the same type *)
  27 inductive X_Relation_Class (X: Type) : Type ≝
  28    SymmetricReflexive :
  29      ∀A,Aeq. symmetric A Aeq → reflexive ? Aeq → X_Relation_Class X
  30  | AsymmetricReflexive : X → ∀A,Aeq. reflexive A Aeq → X_Relation_Class X
  31  | SymmetricAreflexive : ∀A,Aeq. symmetric A Aeq → X_Relation_Class X
  32  | AsymmetricAreflexive : X → ∀A.∀Aeq : relation A. X_Relation_Class X
  33  | Leibniz : Type → X_Relation_Class X.
  34
  35 inductive variance : Set ≝
  36    Covariant : variance
  37  | Contravariant : variance.
  38
  39 definition Argument_Class ≝ X_Relation_Class variance.
  40 definition Relation_Class ≝ X_Relation_Class unit.
  41
  42 inductive Reflexive_Relation_Class : Type :=
  43    RSymmetric :
  44      ∀A,Aeq. symmetric A Aeq → reflexive ? Aeq → Reflexive_Relation_Class
  45  | RAsymmetric :
  46      ∀A,Aeq. reflexive A Aeq → Reflexive_Relation_Class
  47  | RLeibniz : Type → Reflexive_Relation_Class.
  48
  49 inductive Areflexive_Relation_Class  : Type :=
  50  | ASymmetric : ∀A,Aeq. symmetric A Aeq → Areflexive_Relation_Class
  51  | AAsymmetric : ∀A.∀Aeq : relation A. Areflexive_Relation_Class.
  52
  53 definition relation_class_of_argument_class : Argument_Class → Relation_Class.
  54  intro;
  55  unfold in a ⊢ %;
  56  elim a;
  57   [ apply (SymmetricReflexive ? ? ? H H1)
  58   | apply (AsymmetricReflexive ? something ? ? H)
  59   | apply (SymmetricAreflexive ? ? ? H)
  60   | apply (AsymmetricAreflexive ? something ? r)
  61   | apply (Leibniz ? T1)
  62   ]
  63 qed.
  64
  65 definition carrier_of_relation_class : ∀X. X_Relation_Class X → Type.
  66  intros;
  67  elim x;
  68  [1,2,3,4,5: exact T1]
  69 qed.
  70
  71 definition relation_of_relation_class :
  72  ∀X,R. carrier_of_relation_class X R → carrier_of_relation_class X R → Prop.
  73  intros 2;
  74  elim R 0;
  75  simplify;
  76   [1,2: intros 4; apply r
  77   |3,4: intros 3; apply r
  78   | apply eq
  79  ]
  80 qed.
  81
  82 lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
  83  ∀R.
  84   carrier_of_relation_class ? (relation_class_of_argument_class R) =
  85    carrier_of_relation_class ? R.
  86  intro;
  87  elim R;
  88  reflexivity.
  89  qed.
  90
  91 inductive nelistT (A : Type) : Type :=
  92    singl : A → nelistT A
  93  | cons : A → nelistT A → nelistT A.
  94
  95 definition Arguments := nelistT Argument_Class.
  96
  97 definition function_type_of_morphism_signature :
  98  Arguments → Relation_Class → Type.
  99   intros (In Out);
 100   elim In
 101    [ exact (carrier_of_relation_class ? t → carrier_of_relation_class ? Out)
 102    | exact (carrier_of_relation_class ? t → T)
 103    ]
 104 qed.
 105
 106 definition make_compatibility_goal_aux:
 107  ∀In,Out.∀f,g:function_type_of_morphism_signature In Out.Prop.
 108  intros 2;
 109  elim In (a); simplify in f f1;
 110  generalize in match f; clear f;
 111  generalize in match f1; clear f1;
 112   [ elim a; simplify in f f1;
 113      [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
 114      | elim t;
 115         [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
 116         | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2))
 117         ]
 118      | exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
 119      | elim t;
 120         [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
 121         | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2))
 122         ]
 123      | exact (∀x. relation_of_relation_class ? Out (f x) (f1 x))
 124      ]
 125   | change with
 126      ((carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) →
 127       (carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) →
 128       Prop).
 129     elim t; simplify in f f1;
 130      [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
 131      | elim t1;
 132         [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
 133         | exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))
 134         ]
 135      | exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
 136      | elim t1;
 137         [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
 138         | exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))
 139         ]
 140      | exact (∀x. R (f x) (f1 x))
 141      ]
 142   ]
 143 qed.
 144
 145 definition make_compatibility_goal :=
 146  λIn,Out,f. make_compatibility_goal_aux In Out f f.
 147
 148 record Morphism_Theory In Out : Type :=
 149  { Function : function_type_of_morphism_signature In Out;
 150    Compat : make_compatibility_goal In Out Function
 151  }.
 152
 153 definition list_of_Leibniz_of_list_of_types: nelistT Type → Arguments.
 154  induction 1.
 155    exact (singl (Leibniz ? a)).
 156    exact (cons (Leibniz ? a) IHX).
 157 qed.
 158
 159 (* every function is a morphism from Leibniz+ to Leibniz *)
 160 definition morphism_theory_of_function :
 161  ∀(In: nelistT Type) (Out: Type).
 162   let In' := list_of_Leibniz_of_list_of_types In in
 163   let Out' := Leibniz ? Out in
 164    function_type_of_morphism_signature In' Out' →
 165     Morphism_Theory In' Out'.
 166   intros.
 167   exists X.
 168   induction In;  unfold make_compatibility_goal; simpl.
 169     reflexivity.
 170     intro; apply (IHIn (X x)).
 171 qed.
 172
 173 (* THE iff RELATION CLASS *)
 174
 175 definition Iff_Relation_Class : Relation_Class.
 176  eapply (@SymmetricReflexive unit ? iff).
 177  exact iff_sym.
 178  exact iff_refl.
 179 qed.
 180
 181 (* THE impl RELATION CLASS *)
 182
 183 definition impl (A B: Prop) := A → B.
 184
 185 Theorem impl_refl: reflexive ? impl.
 186  hnf; unfold impl; tauto.
 187 Qed.
 188
 189 definition Impl_Relation_Class : Relation_Class.
 190  eapply (@AsymmetricReflexive unit tt ? impl).
 191  exact impl_refl.
 192 qed.
 193
 194 (* UTILITY FUNCTIONS TO PROVE THAT EVERY TRANSITIVE RELATION IS A MORPHISM *)
 195
 196 definition equality_morphism_of_symmetric_areflexive_transitive_relation:
 197  ∀(A: Type)(Aeq: relation A)(sym: symmetric ? Aeq)(trans: transitive ? Aeq).
 198   let ASetoidClass := SymmetricAreflexive ? sym in
 199    (Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class).
 200  intros.
 201  exists Aeq.
 202  unfold make_compatibility_goal; simpl; split; eauto.
 203 qed.
 204
 205 definition equality_morphism_of_symmetric_reflexive_transitive_relation:
 206  ∀(A: Type)(Aeq: relation A)(refl: reflexive ? Aeq)(sym: symmetric ? Aeq)
 207   (trans: transitive ? Aeq). let ASetoidClass := SymmetricReflexive ? sym refl in
 208    (Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class).
 209  intros.
 210  exists Aeq.
 211  unfold make_compatibility_goal; simpl; split; eauto.
 212 qed.
 213
 214 definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
 215  ∀(A: Type)(Aeq: relation A)(trans: transitive ? Aeq).
 216   let ASetoidClass1 := AsymmetricAreflexive Contravariant Aeq in
 217   let ASetoidClass2 := AsymmetricAreflexive Covariant Aeq in
 218    (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
 219  intros.
 220  exists Aeq.
 221  unfold make_compatibility_goal; simpl; unfold impl; eauto.
 222 qed.
 223
 224 definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
 225  ∀(A: Type)(Aeq: relation A)(refl: reflexive ? Aeq)(trans: transitive ? Aeq).
 226   let ASetoidClass1 := AsymmetricReflexive Contravariant refl in
 227   let ASetoidClass2 := AsymmetricReflexive Covariant refl in
 228    (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
 229  intros.
 230  exists Aeq.
 231  unfold make_compatibility_goal; simpl; unfold impl; eauto.
 232 qed.
 233
 234 (* iff AS A RELATION *)
 235
 236 Add Relation Prop iff
 237  reflexivity proved by iff_refl
 238  symmetry proved by iff_sym
 239  transitivity proved by iff_trans
 240  as iff_relation.
 241
 242 (* every predicate is  morphism from Leibniz+ to Iff_Relation_Class *)
 243 definition morphism_theory_of_predicate :
 244  ∀(In: nelistT Type).
 245   let In' := list_of_Leibniz_of_list_of_types In in
 246    function_type_of_morphism_signature In' Iff_Relation_Class →
 247     Morphism_Theory In' Iff_Relation_Class.
 248   intros.
 249   exists X.
 250   induction In;  unfold make_compatibility_goal; simpl.
 251     intro; apply iff_refl.
 252     intro; apply (IHIn (X x)).
 253 qed.
 254
 255 (* impl AS A RELATION *)
 256
 257 Theorem impl_trans: transitive ? impl.
 258  hnf; unfold impl; tauto.
 259 Qed.
 260
 261 Add Relation Prop impl
 262  reflexivity proved by impl_refl
 263  transitivity proved by impl_trans
 264  as impl_relation.
 265
 266 (* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *)
 267
 268 inductive rewrite_direction : Type :=
 269    Left2Right
 270  | Right2Left.
 271
 272 Implicit Type dir: rewrite_direction.
 273
 274 definition variance_of_argument_class : Argument_Class → option variance.
 275  destruct 1.
 276  exact None.
 277  exact (Some v).
 278  exact None.
 279  exact (Some v).
 280  exact None.
 281 qed.
 282
 283 definition opposite_direction :=
 284  fun dir =>
 285    match dir with
 286        Left2Right => Right2Left
 287      | Right2Left => Left2Right
 288    end.
 289
 290 Lemma opposite_direction_idempotent:
 291  ∀dir. (opposite_direction (opposite_direction dir)) = dir.
 292   destruct dir; reflexivity.
 293 Qed.
 294
 295 inductive check_if_variance_is_respected :
 296  option variance → rewrite_direction → rewrite_direction →  Prop
 297 :=
 298    MSNone : ∀dir dir'. check_if_variance_is_respected None dir dir'
 299  | MSCovariant : ∀dir. check_if_variance_is_respected (Some Covariant) dir dir
 300  | MSContravariant :
 301      ∀dir.
 302       check_if_variance_is_respected (Some Contravariant) dir (opposite_direction dir).
 303
 304 definition relation_class_of_reflexive_relation_class:
 305  Reflexive_Relation_Class → Relation_Class.
 306  induction 1.
 307    exact (SymmetricReflexive ? s r).
 308    exact (AsymmetricReflexive tt r).
 309    exact (Leibniz ? T).
 310 qed.
 311
 312 definition relation_class_of_areflexive_relation_class:
 313  Areflexive_Relation_Class → Relation_Class.
 314  induction 1.
 315    exact (SymmetricAreflexive ? s).
 316    exact (AsymmetricAreflexive tt Aeq).
 317 qed.
 318
 319 definition carrier_of_reflexive_relation_class :=
 320  fun R => carrier_of_relation_class (relation_class_of_reflexive_relation_class R).
 321
 322 definition carrier_of_areflexive_relation_class :=
 323  fun R => carrier_of_relation_class (relation_class_of_areflexive_relation_class R).
 324
 325 definition relation_of_areflexive_relation_class :=
 326  fun R => relation_of_relation_class (relation_class_of_areflexive_relation_class R).
 327
 328 inductive Morphism_Context Hole dir : Relation_Class → rewrite_direction →  Type :=
 329     App :
 330       ∀In Out dir'.
 331         Morphism_Theory In Out → Morphism_Context_List Hole dir dir' In →
 332            Morphism_Context Hole dir Out dir'
 333   | ToReplace : Morphism_Context Hole dir Hole dir
 334   | ToKeep :
 335      ∀S dir'.
 336       carrier_of_reflexive_relation_class S →
 337         Morphism_Context Hole dir (relation_class_of_reflexive_relation_class S) dir'
 338  | ProperElementToKeep :
 339      ∀S dir' (x: carrier_of_areflexive_relation_class S).
 340       relation_of_areflexive_relation_class S x x →
 341         Morphism_Context Hole dir (relation_class_of_areflexive_relation_class S) dir'
 342 with Morphism_Context_List Hole dir :
 343    rewrite_direction → Arguments → Type
 344 :=
 345     fcl_singl :
 346       ∀S dir' dir''.
 347        check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' →
 348         Morphism_Context Hole dir (relation_class_of_argument_class S) dir' →
 349          Morphism_Context_List Hole dir dir'' (singl S)
 350  | fcl_cons :
 351       ∀S L dir' dir''.
 352        check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' →
 353         Morphism_Context Hole dir (relation_class_of_argument_class S) dir' →
 354          Morphism_Context_List Hole dir dir'' L →
 355           Morphism_Context_List Hole dir dir'' (cons S L).
 356
 357 Scheme Morphism_Context_rect2 := Induction for Morphism_Context  Sort Type
 358 with Morphism_Context_List_rect2 := Induction for Morphism_Context_List Sort Type.
 359
 360 definition product_of_arguments : Arguments → Type.
 361  induction 1.
 362    exact (carrier_of_relation_class a).
 363    exact (prod (carrier_of_relation_class a) IHX).
 364 qed.
 365
 366 definition get_rewrite_direction: rewrite_direction → Argument_Class → rewrite_direction.
 367  intros dir R.
 368 destruct (variance_of_argument_class R).
 369    destruct v.
 370      exact dir.                                      (* covariant *)
 371      exact (opposite_direction dir). (* contravariant *)
 372    exact dir.                                       (* symmetric relation *)
 373 qed.
 374
 375 definition directed_relation_of_relation_class:
 376  ∀dir (R: Relation_Class).
 377    carrier_of_relation_class R → carrier_of_relation_class R → Prop.
 378  destruct 1.
 379    exact (@relation_of_relation_class unit).
 380    intros; exact (relation_of_relation_class ? X0 X).
 381 qed.
 382
 383 definition directed_relation_of_argument_class:
 384  ∀dir (R: Argument_Class).
 385    carrier_of_relation_class R → carrier_of_relation_class R → Prop.
 386   intros dir R.
 387   rewrite <-
 388    (about_carrier_of_relation_class_and_relation_class_of_argument_class R).
 389   exact (directed_relation_of_relation_class dir (relation_class_of_argument_class R)).
 390 qed.
 391
 392
 393 definition relation_of_product_of_arguments:
 394  ∀dir In.
 395   product_of_arguments In → product_of_arguments In → Prop.
 396  induction In.
 397    simpl.
 398    exact (directed_relation_of_argument_class (get_rewrite_direction dir a) a).
 399
 400    simpl; intros.
 401    destruct X; destruct X0.
 402    apply and.
 403      exact
 404       (directed_relation_of_argument_class (get_rewrite_direction dir a) a c c0).
 405      exact (IHIn p p0).
 406 qed.
 407
 408 definition apply_morphism:
 409  ∀In Out (m: function_type_of_morphism_signature In Out)
 410   (args: product_of_arguments In). carrier_of_relation_class Out.
 411  intros.
 412  induction In.
 413    exact (m args).
 414    simpl in m. args.
 415    destruct args.
 416    exact (IHIn (m c) p).
 417 qed.
 418
 419 Theorem apply_morphism_compatibility_Right2Left:
 420  ∀In Out (m1 m2: function_type_of_morphism_signature In Out)
 421    (args1 args2: product_of_arguments In).
 422      make_compatibility_goal_aux ? ? m1 m2 →
 423       relation_of_product_of_arguments Right2Left ? args1 args2 →
 424         directed_relation_of_relation_class Right2Left ?
 425          (apply_morphism ? ? m2 args1)
 426          (apply_morphism ? ? m1 args2).
 427   induction In; intros.
 428     simpl in m1. m2. args1. args2. H0 |- *.
 429     destruct a; simpl in H; hnf in H0.
 430           apply H; exact H0.
 431           destruct v; simpl in H0; apply H; exact H0.
 432           apply H; exact H0.
 433           destruct v; simpl in H0; apply H; exact H0.
 434           rewrite H0; apply H; exact H0.
 435
 436    simpl in m1. m2. args1. args2. H0 |- *.
 437    destruct args1; destruct args2; simpl.
 438    destruct H0.
 439    simpl in H.
 440    destruct a; simpl in H.
 441      apply IHIn.
 442        apply H; exact H0.
 443        exact H1.
 444      destruct v.
 445        apply IHIn.
 446          apply H; exact H0.
 447          exact H1.
 448        apply IHIn.
 449          apply H; exact H0.
 450           exact H1.
 451      apply IHIn.
 452        apply H; exact H0.
 453        exact H1.
 454      destruct v.
 455        apply IHIn.
 456          apply H; exact H0.
 457          exact H1.
 458        apply IHIn.
 459          apply H; exact H0.
 460           exact H1.
 461     rewrite H0; apply IHIn.
 462       apply H.
 463       exact H1.
 464 Qed.
 465
 466 Theorem apply_morphism_compatibility_Left2Right:
 467  ∀In Out (m1 m2: function_type_of_morphism_signature In Out)
 468    (args1 args2: product_of_arguments In).
 469      make_compatibility_goal_aux ? ? m1 m2 →
 470       relation_of_product_of_arguments Left2Right ? args1 args2 →
 471         directed_relation_of_relation_class Left2Right ?
 472          (apply_morphism ? ? m1 args1)
 473          (apply_morphism ? ? m2 args2).
 474   induction In; intros.
 475     simpl in m1. m2. args1. args2. H0 |- *.
 476     destruct a; simpl in H; hnf in H0.
 477           apply H; exact H0.
 478           destruct v; simpl in H0; apply H; exact H0.
 479           apply H; exact H0.
 480           destruct v; simpl in H0; apply H; exact H0.
 481           rewrite H0; apply H; exact H0.
 482
 483     simpl in m1. m2. args1. args2. H0 |- *.
 484    destruct args1; destruct args2; simpl.
 485    destruct H0.
 486    simpl in H.
 487    destruct a; simpl in H.
 488      apply IHIn.
 489        apply H; exact H0.
 490        exact H1.
 491      destruct v.
 492        apply IHIn.
 493          apply H; exact H0.
 494          exact H1.
 495        apply IHIn.
 496          apply H; exact H0.
 497           exact H1.
 498        apply IHIn.
 499          apply H; exact H0.
 500          exact H1.
 501        apply IHIn.
 502          destruct v; simpl in H. H0; apply H; exact H0.
 503           exact H1.
 504     rewrite H0; apply IHIn.
 505       apply H.
 506       exact H1.
 507 Qed.
 508
 509 definition interp :
 510  ∀Hole dir Out dir'. carrier_of_relation_class Hole →
 511   Morphism_Context Hole dir Out dir' → carrier_of_relation_class Out.
 512  intros Hole dir Out dir' H t.
 513  elim t using
 514   (@Morphism_Context_rect2 Hole dir (fun S ? ? => carrier_of_relation_class S)
 515     (fun ? L fcl => product_of_arguments L));
 516   intros.
 517    exact (apply_morphism ? ? (Function m) X).
 518    exact H.
 519    exact c.
 520    exact x.
 521    simpl;
 522      rewrite <-
 523        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 524      exact X.
 525    split.
 526      rewrite <-
 527        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 528        exact X.
 529        exact X0.
 530 qed.
 531
 532 (*CSC: interp and interp_relation_class_list should be mutually defined. since
 533    the proof term of each one contains the proof term of the other one. However
 534    I cannot do that interactively (I should write the Fix by hand) *)
 535 definition interp_relation_class_list :
 536  ∀Hole dir dir' (L: Arguments). carrier_of_relation_class Hole →
 537   Morphism_Context_List Hole dir dir' L → product_of_arguments L.
 538  intros Hole dir dir' L H t.
 539  elim t using
 540   (@Morphism_Context_List_rect2 Hole dir (fun S ? ? => carrier_of_relation_class S)
 541     (fun ? L fcl => product_of_arguments L));
 542  intros.
 543    exact (apply_morphism ? ? (Function m) X).
 544    exact H.
 545    exact c.
 546    exact x.
 547    simpl;
 548      rewrite <-
 549        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 550      exact X.
 551    split.
 552      rewrite <-
 553        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 554        exact X.
 555        exact X0.
 556 qed.
 557
 558 Theorem setoid_rewrite:
 559  ∀Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole)
 560   (E: Morphism_Context Hole dir Out dir').
 561    (directed_relation_of_relation_class dir Hole E1 E2) →
 562     (directed_relation_of_relation_class dir' Out (interp E1 E) (interp E2 E)).
 563  intros.
 564  elim E using
 565    (@Morphism_Context_rect2 Hole dir
 566      (fun S dir'' E => directed_relation_of_relation_class dir'' S (interp E1 E) (interp E2 E))
 567      (fun dir'' L fcl =>
 568         relation_of_product_of_arguments dir'' ?
 569          (interp_relation_class_list E1 fcl)
 570          (interp_relation_class_list E2 fcl))); intros.
 571    change (directed_relation_of_relation_class dir'0 Out0
 572     (apply_morphism ? ? (Function m) (interp_relation_class_list E1 m0))
 573     (apply_morphism ? ? (Function m) (interp_relation_class_list E2 m0))).
 574    destruct dir'0.
 575      apply apply_morphism_compatibility_Left2Right.
 576        exact (Compat m).
 577        exact H0.
 578      apply apply_morphism_compatibility_Right2Left.
 579        exact (Compat m).
 580        exact H0.
 581
 582    exact H.
 583
 584    unfold interp. Morphism_Context_rect2.
 585    (*CSC: reflexivity used here*)
 586    destruct S; destruct dir'0; simpl; (apply r || reflexivity).
 587
 588    destruct dir'0; exact r.
 589
 590   destruct S; unfold directed_relation_of_argument_class; simpl in H0 |- *;
 591    unfold get_rewrite_direction; simpl.
 592      destruct dir'0; destruct dir'';
 593        (exact H0 ||
 594         unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
 595      (* the following mess with generalize/clear/intros is to help Coq resolving *)
 596      (* second order unification problems.                                                                *)
 597      generalize m c H0; clear H0 m c; inversion c;
 598        generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
 599          (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
 600      destruct dir'0; destruct dir'';
 601        (exact H0 ||
 602         unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
 603 (* the following mess with generalize/clear/intros is to help Coq resolving *)
 604      (* second order unification problems.                                                                *)
 605      generalize m c H0; clear H0 m c; inversion c;
 606        generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
 607          (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
 608      destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0).
 609
 610   change
 611     (directed_relation_of_argument_class (get_rewrite_direction dir'' S) S
 612        (eq_rect ? (fun T : Type => T) (interp E1 m) ?
 613          (about_carrier_of_relation_class_and_relation_class_of_argument_class S))
 614        (eq_rect ? (fun T : Type => T) (interp E2 m) ?
 615          (about_carrier_of_relation_class_and_relation_class_of_argument_class S)) /\
 616      relation_of_product_of_arguments dir'' ?
 617        (interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)).
 618    split.
 619      clear m0 H1; destruct S; simpl in H0 |- *; unfold get_rewrite_direction; simpl.
 620         destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
 621         inversion c.
 622           rewrite <- H3; exact H0.
 623           rewrite (opposite_direction_idempotent dir'0); exact H0.
 624         destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
 625         inversion c.
 626           rewrite <- H3; exact H0.
 627           rewrite (opposite_direction_idempotent dir'0); exact H0.
 628         destruct dir''; destruct dir'0; (exact H0 || hnf; symmetry; exact H0).
 629      exact H1.
 630 Qed.
 631
 632 (* BEGIN OF UTILITY/BACKWARD COMPATIBILITY PART *)
 633
 634 record Setoid_Theory  (A: Type) (Aeq: relation A) : Prop :=
 635   {Seq_refl : ∀x:A. Aeq x x;
 636    Seq_sym : ∀x y:A. Aeq x y → Aeq y x;
 637    Seq_trans : ∀x y z:A. Aeq x y → Aeq y z → Aeq x z}.
 638
 639 (* END OF UTILITY/BACKWARD COMPATIBILITY PART *)
 640
 641 (* A FEW EXAMPLES ON iff *)
 642
 643 (* impl IS A MORPHISM *)
 644
 645 Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
 646 unfold impl; tauto.
 647 Qed.
 648
 649 (* and IS A MORPHISM *)
 650
 651 Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
 652  tauto.
 653 Qed.
 654
 655 (* or IS A MORPHISM *)
 656
 657 Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
 658  tauto.
 659 Qed.
 660
 661 (* not IS A MORPHISM *)
 662
 663 Add Morphism not with signature iff ==> iff as Not_Morphism.
 664  tauto.
 665 Qed.
 666
 667 (* THE SAME EXAMPLES ON impl *)
 668
 669 Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
 670  unfold impl; tauto.
 671 Qed.
 672
 673 Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
 674  unfold impl; tauto.
 675 Qed.
 676
 677 Add Morphism not with signature impl -→ impl as Not_Morphism2.
 678  unfold impl; tauto.
 679 Qed.
 680
 681 (* FOR BACKWARD COMPATIBILITY *)
 682 Implicit Arguments Setoid_Theory [].
 683 Implicit Arguments Seq_refl [].
 684 Implicit Arguments Seq_sym [].
 685 Implicit Arguments Seq_trans [].
 686
 687
 688 (* Some tactics for manipulating Setoid Theory not officially
 689    declared as Setoid. *)
 690
 691 Ltac trans_st x := match goal with
 692   | H : Setoid_Theory ? ?eqA |- ?eqA ? ? =>
 693      apply (Seq_trans ? ? H) with x; auto
 694  end.
 695
 696 Ltac sym_st := match goal with
 697   | H : Setoid_Theory ? ?eqA |- ?eqA ? ? =>
 698      apply (Seq_sym ? ? H); auto
 699  end.
 700
 701 Ltac refl_st := match goal with
 702   | H : Setoid_Theory ? ?eqA |- ?eqA ? ? =>
 703      apply (Seq_refl ? ? H); auto
 704  end.
 705
 706 definition gen_st : ∀A : Set. Setoid_Theory ? (@eq A).
 707 Proof. constructor; congruence. Qed.
 708