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