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