helm/software/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 "datatypes/constructors.ma".
  21 include "logic/connectives2.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: Arguments) (Out: Relation_Class) : 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  intro;
 155  elim n;
 156   [ apply (singl ? (Leibniz ? t))
 157   | apply (cons ? (Leibniz ? t) a)
 158   ]
 159 qed.
 160
 161 (* every function is a morphism from Leibniz+ to Leibniz *)
 162 definition morphism_theory_of_function :
 163  ∀In: nelistT Type.∀Out: Type.
 164   let In' := list_of_Leibniz_of_list_of_types In in
 165   let Out' := Leibniz ? Out in
 166    function_type_of_morphism_signature In' Out' →
 167     Morphism_Theory In' Out'.
 168   intros;
 169   apply (mk_Morphism_Theory ? ? f);
 170   unfold In' in f; clear In';
 171   unfold Out' in f; clear Out';
 172   generalize in match f; clear f;
 173   elim In;
 174    [ unfold make_compatibility_goal;
 175      simplify;
 176      intros;
 177      whd;
 178      reflexivity
 179    | simplify;
 180      intro;
 181      unfold In' in f;
 182      unfold Out' in f;
 183      exact (H (f1 x))
 184    ]
 185 qed.
 186
 187 (* THE iff RELATION CLASS *)
 188
 189 definition Iff_Relation_Class : Relation_Class.
 190  apply (SymmetricReflexive unit ? iff);
 191   [ exact symmetric_iff
 192   | exact reflexive_iff
 193   ]
 194 qed.
 195
 196 (* THE impl RELATION CLASS *)
 197
 198 definition impl \def \lambda A,B:Prop. A → B.
 199
 200 theorem impl_refl: reflexive ? impl.
 201  unfold reflexive;
 202  intros;
 203  unfold impl;
 204  intro;
 205  assumption.
 206 qed.
 207
 208 definition Impl_Relation_Class : Relation_Class.
 209  unfold Relation_Class;
 210  apply (AsymmetricReflexive unit something ? impl);
 211  exact impl_refl.
 212 qed.
 213
 214 (* UTILITY FUNCTIONS TO PROVE THAT EVERY TRANSITIVE RELATION IS A MORPHISM *)
 215
 216 definition equality_morphism_of_symmetric_areflexive_transitive_relation:
 217  ∀A: Type.∀Aeq: relation A.∀sym: symmetric ? Aeq.∀trans: transitive ? Aeq.
 218   let ASetoidClass := SymmetricAreflexive ? ? ? sym in
 219    (Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass))
 220      Iff_Relation_Class).
 221  intros;
 222  apply mk_Morphism_Theory;
 223   [ exact Aeq
 224   | unfold make_compatibility_goal;
 225     simplify;
 226     intros;
 227     split;
 228     unfold transitive in H;
 229     unfold symmetric in sym;
 230     intro;
 231     auto
 232   ].
 233 qed.
 234
 235 definition equality_morphism_of_symmetric_reflexive_transitive_relation:
 236  ∀A: Type.∀Aeq: relation A.∀refl: reflexive ? Aeq.∀sym: symmetric ? Aeq.
 237   ∀trans: transitive ? Aeq.
 238    let ASetoidClass := SymmetricReflexive ? ? ? sym refl in
 239     (Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass)) Iff_Relation_Class).
 240  intros;
 241  apply mk_Morphism_Theory;
 242  reduce;
 243   [ exact Aeq
 244   | intros;
 245     split;
 246     intro;
 247     unfold transitive in H;
 248     auto
 249   ]
 250 qed.
 251
 252 definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
 253  ∀(A: Type)(Aeq: relation A)(trans: transitive ? Aeq).
 254   let ASetoidClass1 := AsymmetricAreflexive Contravariant Aeq in
 255   let ASetoidClass2 := AsymmetricAreflexive Covariant Aeq in
 256    (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
 257  intros.
 258  exists Aeq.
 259  unfold make_compatibility_goal; simpl; unfold impl; eauto.
 260 qed.
 261
 262 definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
 263  ∀(A: Type)(Aeq: relation A)(refl: reflexive ? Aeq)(trans: transitive ? Aeq).
 264   let ASetoidClass1 := AsymmetricReflexive Contravariant refl in
 265   let ASetoidClass2 := AsymmetricReflexive Covariant refl in
 266    (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
 267  intros.
 268  exists Aeq.
 269  unfold make_compatibility_goal; simpl; unfold impl; eauto.
 270 qed.
 271
 272 (* iff AS A RELATION *)
 273
 274 Add Relation Prop iff
 275  reflexivity proved by iff_refl
 276  symmetry proved by iff_sym
 277  transitivity proved by iff_trans
 278  as iff_relation.
 279
 280 (* every predicate is  morphism from Leibniz+ to Iff_Relation_Class *)
 281 definition morphism_theory_of_predicate :
 282  ∀(In: nelistT Type).
 283   let In' := list_of_Leibniz_of_list_of_types In in
 284    function_type_of_morphism_signature In' Iff_Relation_Class →
 285     Morphism_Theory In' Iff_Relation_Class.
 286   intros.
 287   exists X.
 288   induction In;  unfold make_compatibility_goal; simpl.
 289     intro; apply iff_refl.
 290     intro; apply (IHIn (X x)).
 291 qed.
 292
 293 (* impl AS A RELATION *)
 294
 295 Theorem impl_trans: transitive ? impl.
 296  hnf; unfold impl; tauto.
 297 Qed.
 298
 299 Add Relation Prop impl
 300  reflexivity proved by impl_refl
 301  transitivity proved by impl_trans
 302  as impl_relation.
 303
 304 (* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *)
 305
 306 inductive rewrite_direction : Type :=
 307    Left2Right
 308  | Right2Left.
 309
 310 Implicit Type dir: rewrite_direction.
 311
 312 definition variance_of_argument_class : Argument_Class → option variance.
 313  destruct 1.
 314  exact None.
 315  exact (Some v).
 316  exact None.
 317  exact (Some v).
 318  exact None.
 319 qed.
 320
 321 definition opposite_direction :=
 322  fun dir =>
 323    match dir with
 324        Left2Right => Right2Left
 325      | Right2Left => Left2Right
 326    end.
 327
 328 Lemma opposite_direction_idempotent:
 329  ∀dir. (opposite_direction (opposite_direction dir)) = dir.
 330   destruct dir; reflexivity.
 331 Qed.
 332
 333 inductive check_if_variance_is_respected :
 334  option variance → rewrite_direction → rewrite_direction →  Prop
 335 :=
 336    MSNone : ∀dir dir'. check_if_variance_is_respected None dir dir'
 337  | MSCovariant : ∀dir. check_if_variance_is_respected (Some Covariant) dir dir
 338  | MSContravariant :
 339      ∀dir.
 340       check_if_variance_is_respected (Some Contravariant) dir (opposite_direction dir).
 341
 342 definition relation_class_of_reflexive_relation_class:
 343  Reflexive_Relation_Class → Relation_Class.
 344  induction 1.
 345    exact (SymmetricReflexive ? s r).
 346    exact (AsymmetricReflexive tt r).
 347    exact (Leibniz ? T).
 348 qed.
 349
 350 definition relation_class_of_areflexive_relation_class:
 351  Areflexive_Relation_Class → Relation_Class.
 352  induction 1.
 353    exact (SymmetricAreflexive ? s).
 354    exact (AsymmetricAreflexive tt Aeq).
 355 qed.
 356
 357 definition carrier_of_reflexive_relation_class :=
 358  fun R => carrier_of_relation_class (relation_class_of_reflexive_relation_class R).
 359
 360 definition carrier_of_areflexive_relation_class :=
 361  fun R => carrier_of_relation_class (relation_class_of_areflexive_relation_class R).
 362
 363 definition relation_of_areflexive_relation_class :=
 364  fun R => relation_of_relation_class (relation_class_of_areflexive_relation_class R).
 365
 366 inductive Morphism_Context Hole dir : Relation_Class → rewrite_direction →  Type :=
 367     App :
 368       ∀In Out dir'.
 369         Morphism_Theory In Out → Morphism_Context_List Hole dir dir' In →
 370            Morphism_Context Hole dir Out dir'
 371   | ToReplace : Morphism_Context Hole dir Hole dir
 372   | ToKeep :
 373      ∀S dir'.
 374       carrier_of_reflexive_relation_class S →
 375         Morphism_Context Hole dir (relation_class_of_reflexive_relation_class S) dir'
 376  | ProperElementToKeep :
 377      ∀S dir' (x: carrier_of_areflexive_relation_class S).
 378       relation_of_areflexive_relation_class S x x →
 379         Morphism_Context Hole dir (relation_class_of_areflexive_relation_class S) dir'
 380 with Morphism_Context_List Hole dir :
 381    rewrite_direction → Arguments → Type
 382 :=
 383     fcl_singl :
 384       ∀S dir' dir''.
 385        check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' →
 386         Morphism_Context Hole dir (relation_class_of_argument_class S) dir' →
 387          Morphism_Context_List Hole dir dir'' (singl S)
 388  | fcl_cons :
 389       ∀S L dir' dir''.
 390        check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' →
 391         Morphism_Context Hole dir (relation_class_of_argument_class S) dir' →
 392          Morphism_Context_List Hole dir dir'' L →
 393           Morphism_Context_List Hole dir dir'' (cons S L).
 394
 395 Scheme Morphism_Context_rect2 := Induction for Morphism_Context  Sort Type
 396 with Morphism_Context_List_rect2 := Induction for Morphism_Context_List Sort Type.
 397
 398 definition product_of_arguments : Arguments → Type.
 399  induction 1.
 400    exact (carrier_of_relation_class a).
 401    exact (prod (carrier_of_relation_class a) IHX).
 402 qed.
 403
 404 definition get_rewrite_direction: rewrite_direction → Argument_Class → rewrite_direction.
 405  intros dir R.
 406 destruct (variance_of_argument_class R).
 407    destruct v.
 408      exact dir.                                      (* covariant *)
 409      exact (opposite_direction dir). (* contravariant *)
 410    exact dir.                                       (* symmetric relation *)
 411 qed.
 412
 413 definition directed_relation_of_relation_class:
 414  ∀dir (R: Relation_Class).
 415    carrier_of_relation_class R → carrier_of_relation_class R → Prop.
 416  destruct 1.
 417    exact (@relation_of_relation_class unit).
 418    intros; exact (relation_of_relation_class ? X0 X).
 419 qed.
 420
 421 definition directed_relation_of_argument_class:
 422  ∀dir (R: Argument_Class).
 423    carrier_of_relation_class R → carrier_of_relation_class R → Prop.
 424   intros dir R.
 425   rewrite <-
 426    (about_carrier_of_relation_class_and_relation_class_of_argument_class R).
 427   exact (directed_relation_of_relation_class dir (relation_class_of_argument_class R)).
 428 qed.
 429
 430
 431 definition relation_of_product_of_arguments:
 432  ∀dir In.
 433   product_of_arguments In → product_of_arguments In → Prop.
 434  induction In.
 435    simpl.
 436    exact (directed_relation_of_argument_class (get_rewrite_direction dir a) a).
 437
 438    simpl; intros.
 439    destruct X; destruct X0.
 440    apply and.
 441      exact
 442       (directed_relation_of_argument_class (get_rewrite_direction dir a) a c c0).
 443      exact (IHIn p p0).
 444 qed.
 445
 446 definition apply_morphism:
 447  ∀In Out (m: function_type_of_morphism_signature In Out)
 448   (args: product_of_arguments In). carrier_of_relation_class Out.
 449  intros.
 450  induction In.
 451    exact (m args).
 452    simpl in m. args.
 453    destruct args.
 454    exact (IHIn (m c) p).
 455 qed.
 456
 457 Theorem apply_morphism_compatibility_Right2Left:
 458  ∀In Out (m1 m2: function_type_of_morphism_signature In Out)
 459    (args1 args2: product_of_arguments In).
 460      make_compatibility_goal_aux ? ? m1 m2 →
 461       relation_of_product_of_arguments Right2Left ? args1 args2 →
 462         directed_relation_of_relation_class Right2Left ?
 463          (apply_morphism ? ? m2 args1)
 464          (apply_morphism ? ? m1 args2).
 465   induction In; intros.
 466     simpl in m1. m2. args1. args2. H0 |- *.
 467     destruct a; simpl in H; hnf in H0.
 468           apply H; exact H0.
 469           destruct v; simpl in H0; apply H; exact H0.
 470           apply H; exact H0.
 471           destruct v; simpl in H0; apply H; exact H0.
 472           rewrite H0; apply H; exact H0.
 473
 474    simpl in m1. m2. args1. args2. H0 |- *.
 475    destruct args1; destruct args2; simpl.
 476    destruct H0.
 477    simpl in H.
 478    destruct a; simpl in H.
 479      apply IHIn.
 480        apply H; exact H0.
 481        exact H1.
 482      destruct v.
 483        apply IHIn.
 484          apply H; exact H0.
 485          exact H1.
 486        apply IHIn.
 487          apply H; exact H0.
 488           exact H1.
 489      apply IHIn.
 490        apply H; exact H0.
 491        exact H1.
 492      destruct v.
 493        apply IHIn.
 494          apply H; exact H0.
 495          exact H1.
 496        apply IHIn.
 497          apply H; exact H0.
 498           exact H1.
 499     rewrite H0; apply IHIn.
 500       apply H.
 501       exact H1.
 502 Qed.
 503
 504 Theorem apply_morphism_compatibility_Left2Right:
 505  ∀In Out (m1 m2: function_type_of_morphism_signature In Out)
 506    (args1 args2: product_of_arguments In).
 507      make_compatibility_goal_aux ? ? m1 m2 →
 508       relation_of_product_of_arguments Left2Right ? args1 args2 →
 509         directed_relation_of_relation_class Left2Right ?
 510          (apply_morphism ? ? m1 args1)
 511          (apply_morphism ? ? m2 args2).
 512   induction In; intros.
 513     simpl in m1. m2. args1. args2. H0 |- *.
 514     destruct a; simpl in H; hnf in H0.
 515           apply H; exact H0.
 516           destruct v; simpl in H0; apply H; exact H0.
 517           apply H; exact H0.
 518           destruct v; simpl in H0; apply H; exact H0.
 519           rewrite H0; apply H; exact H0.
 520
 521     simpl in m1. m2. args1. args2. H0 |- *.
 522    destruct args1; destruct args2; simpl.
 523    destruct H0.
 524    simpl in H.
 525    destruct a; simpl in H.
 526      apply IHIn.
 527        apply H; exact H0.
 528        exact H1.
 529      destruct v.
 530        apply IHIn.
 531          apply H; exact H0.
 532          exact H1.
 533        apply IHIn.
 534          apply H; exact H0.
 535           exact H1.
 536        apply IHIn.
 537          apply H; exact H0.
 538          exact H1.
 539        apply IHIn.
 540          destruct v; simpl in H. H0; apply H; exact H0.
 541           exact H1.
 542     rewrite H0; apply IHIn.
 543       apply H.
 544       exact H1.
 545 Qed.
 546
 547 definition interp :
 548  ∀Hole dir Out dir'. carrier_of_relation_class Hole →
 549   Morphism_Context Hole dir Out dir' → carrier_of_relation_class Out.
 550  intros Hole dir Out dir' H t.
 551  elim t using
 552   (@Morphism_Context_rect2 Hole dir (fun S ? ? => carrier_of_relation_class S)
 553     (fun ? L fcl => product_of_arguments L));
 554   intros.
 555    exact (apply_morphism ? ? (Function m) X).
 556    exact H.
 557    exact c.
 558    exact x.
 559    simpl;
 560      rewrite <-
 561        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 562      exact X.
 563    split.
 564      rewrite <-
 565        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 566        exact X.
 567        exact X0.
 568 qed.
 569
 570 (*CSC: interp and interp_relation_class_list should be mutually defined. since
 571    the proof term of each one contains the proof term of the other one. However
 572    I cannot do that interactively (I should write the Fix by hand) *)
 573 definition interp_relation_class_list :
 574  ∀Hole dir dir' (L: Arguments). carrier_of_relation_class Hole →
 575   Morphism_Context_List Hole dir dir' L → product_of_arguments L.
 576  intros Hole dir dir' L H t.
 577  elim t using
 578   (@Morphism_Context_List_rect2 Hole dir (fun S ? ? => carrier_of_relation_class S)
 579     (fun ? L fcl => product_of_arguments L));
 580  intros.
 581    exact (apply_morphism ? ? (Function m) X).
 582    exact H.
 583    exact c.
 584    exact x.
 585    simpl;
 586      rewrite <-
 587        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 588      exact X.
 589    split.
 590      rewrite <-
 591        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 592        exact X.
 593        exact X0.
 594 qed.
 595
 596 Theorem setoid_rewrite:
 597  ∀Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole)
 598   (E: Morphism_Context Hole dir Out dir').
 599    (directed_relation_of_relation_class dir Hole E1 E2) →
 600     (directed_relation_of_relation_class dir' Out (interp E1 E) (interp E2 E)).
 601  intros.
 602  elim E using
 603    (@Morphism_Context_rect2 Hole dir
 604      (fun S dir'' E => directed_relation_of_relation_class dir'' S (interp E1 E) (interp E2 E))
 605      (fun dir'' L fcl =>
 606         relation_of_product_of_arguments dir'' ?
 607          (interp_relation_class_list E1 fcl)
 608          (interp_relation_class_list E2 fcl))); intros.
 609    change (directed_relation_of_relation_class dir'0 Out0
 610     (apply_morphism ? ? (Function m) (interp_relation_class_list E1 m0))
 611     (apply_morphism ? ? (Function m) (interp_relation_class_list E2 m0))).
 612    destruct dir'0.
 613      apply apply_morphism_compatibility_Left2Right.
 614        exact (Compat m).
 615        exact H0.
 616      apply apply_morphism_compatibility_Right2Left.
 617        exact (Compat m).
 618        exact H0.
 619
 620    exact H.
 621
 622    unfold interp. Morphism_Context_rect2.
 623    (*CSC: reflexivity used here*)
 624    destruct S; destruct dir'0; simpl; (apply r || reflexivity).
 625
 626    destruct dir'0; exact r.
 627
 628   destruct S; unfold directed_relation_of_argument_class; simpl in H0 |- *;
 629    unfold get_rewrite_direction; simpl.
 630      destruct dir'0; destruct dir'';
 631        (exact H0 ||
 632         unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
 633      (* the following mess with generalize/clear/intros is to help Coq resolving *)
 634      (* second order unification problems.                                                                *)
 635      generalize m c H0; clear H0 m c; inversion c;
 636        generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
 637          (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
 638      destruct dir'0; destruct dir'';
 639        (exact H0 ||
 640         unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
 641 (* the following mess with generalize/clear/intros is to help Coq resolving *)
 642      (* second order unification problems.                                                                *)
 643      generalize m c H0; clear H0 m c; inversion c;
 644        generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
 645          (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
 646      destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0).
 647
 648   change
 649     (directed_relation_of_argument_class (get_rewrite_direction dir'' S) S
 650        (eq_rect ? (fun T : Type => T) (interp E1 m) ?
 651          (about_carrier_of_relation_class_and_relation_class_of_argument_class S))
 652        (eq_rect ? (fun T : Type => T) (interp E2 m) ?
 653          (about_carrier_of_relation_class_and_relation_class_of_argument_class S)) /\
 654      relation_of_product_of_arguments dir'' ?
 655        (interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)).
 656    split.
 657      clear m0 H1; destruct S; simpl in H0 |- *; unfold get_rewrite_direction; simpl.
 658         destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
 659         inversion c.
 660           rewrite <- H3; exact H0.
 661           rewrite (opposite_direction_idempotent dir'0); exact H0.
 662         destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
 663         inversion c.
 664           rewrite <- H3; exact H0.
 665           rewrite (opposite_direction_idempotent dir'0); exact H0.
 666         destruct dir''; destruct dir'0; (exact H0 || hnf; symmetry; exact H0).
 667      exact H1.
 668 Qed.
 669
 670 (* BEGIN OF UTILITY/BACKWARD COMPATIBILITY PART *)
 671
 672 record Setoid_Theory  (A: Type) (Aeq: relation A) : Prop :=
 673   {Seq_refl : ∀x:A. Aeq x x;
 674    Seq_sym : ∀x y:A. Aeq x y → Aeq y x;
 675    Seq_trans : ∀x y z:A. Aeq x y → Aeq y z → Aeq x z}.
 676
 677 (* END OF UTILITY/BACKWARD COMPATIBILITY PART *)
 678
 679 (* A FEW EXAMPLES ON iff *)
 680
 681 (* impl IS A MORPHISM *)
 682
 683 Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
 684 unfold impl; tauto.
 685 Qed.
 686
 687 (* and IS A MORPHISM *)
 688
 689 Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
 690  tauto.
 691 Qed.
 692
 693 (* or IS A MORPHISM *)
 694
 695 Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
 696  tauto.
 697 Qed.
 698
 699 (* not IS A MORPHISM *)
 700
 701 Add Morphism not with signature iff ==> iff as Not_Morphism.
 702  tauto.
 703 Qed.
 704
 705 (* THE SAME EXAMPLES ON impl *)
 706
 707 Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
 708  unfold impl; tauto.
 709 Qed.
 710
 711 Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
 712  unfold impl; tauto.
 713 Qed.
 714
 715 Add Morphism not with signature impl -→ impl as Not_Morphism2.
 716  unfold impl; tauto.
 717 Qed.
 718
 719 (* FOR BACKWARD COMPATIBILITY *)
 720 Implicit Arguments Setoid_Theory [].
 721 Implicit Arguments Seq_refl [].
 722 Implicit Arguments Seq_sym [].
 723 Implicit Arguments Seq_trans [].
 724
 725
 726 (* Some tactics for manipulating Setoid Theory not officially
 727    declared as Setoid. *)
 728
 729 Ltac trans_st x := match goal with
 730   | H : Setoid_Theory ? ?eqA |- ?eqA ? ? =>
 731      apply (Seq_trans ? ? H) with x; auto
 732  end.
 733
 734 Ltac sym_st := match goal with
 735   | H : Setoid_Theory ? ?eqA |- ?eqA ? ? =>
 736      apply (Seq_sym ? ? H); auto
 737  end.
 738
 739 Ltac refl_st := match goal with
 740   | H : Setoid_Theory ? ?eqA |- ?eqA ? ? =>
 741      apply (Seq_refl ? ? H); auto
 742  end.
 743
 744 definition gen_st : ∀A : Set. Setoid_Theory ? (@eq A).
 745 Proof. constructor; congruence. Qed.
 746