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