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