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  intros;
 340  elim a;
 341   [ apply None
 342   | apply (Some ? t)
 343   | apply None
 344   | apply (Some ? t)
 345   | apply None
 346   ]
 347 qed.
 348
 349 definition opposite_direction :=
 350  λdir.
 351    match dir with
 352     [ Left2Right ⇒ Right2Left
 353     | Right2Left ⇒ Left2Right
 354     ].
 355
 356 lemma opposite_direction_idempotent:
 357  ∀dir. opposite_direction (opposite_direction dir) = dir.
 358   intros;
 359   elim dir;
 360   reflexivity.
 361 qed.
 362
 363 inductive check_if_variance_is_respected :
 364  option variance → rewrite_direction → rewrite_direction →  Prop
 365 :=
 366    MSNone : ∀dir,dir'. check_if_variance_is_respected (None ?) dir dir'
 367  | MSCovariant : ∀dir. check_if_variance_is_respected (Some ? Covariant) dir dir
 368  | MSContravariant :
 369      ∀dir.
 370       check_if_variance_is_respected (Some ? Contravariant) dir (opposite_direction dir).
 371
 372 definition relation_class_of_reflexive_relation_class:
 373  Reflexive_Relation_Class → Relation_Class.
 374  intro;
 375  elim r;
 376   [ apply (SymmetricReflexive ? ? ? H H1)
 377   | apply (AsymmetricReflexive ? something ? ? H)
 378   | apply (Leibniz ? T)
 379   ]
 380 qed.
 381
 382 definition relation_class_of_areflexive_relation_class:
 383  Areflexive_Relation_Class → Relation_Class.
 384  intro;
 385  elim a;
 386   [ apply (SymmetricAreflexive ? ? ? H)
 387   | apply (AsymmetricAreflexive ? something ? r)
 388   ]
 389 qed.
 390
 391 definition carrier_of_reflexive_relation_class :=
 392  λR.carrier_of_relation_class ? (relation_class_of_reflexive_relation_class R).
 393
 394 definition carrier_of_areflexive_relation_class :=
 395  λR.carrier_of_relation_class ? (relation_class_of_areflexive_relation_class R).
 396
 397 definition relation_of_areflexive_relation_class :=
 398  λR.relation_of_relation_class ? (relation_class_of_areflexive_relation_class R).
 399
 400 inductive Morphism_Context (Hole: Relation_Class) (dir:rewrite_direction) : Relation_Class → rewrite_direction →  Type :=
 401     App :
 402       ∀In,Out,dir'.
 403         Morphism_Theory In Out → Morphism_Context_List Hole dir dir' In →
 404            Morphism_Context Hole dir Out dir
 405   | ToReplace : Morphism_Context Hole dir Hole dir
 406   | ToKeep :
 407      ∀S,dir'.
 408       carrier_of_reflexive_relation_class S →
 409         Morphism_Context Hole dir (relation_class_of_reflexive_relation_class S) dir'
 410  | ProperElementToKeep :
 411      ∀S,dir'.∀x: carrier_of_areflexive_relation_class S.
 412       relation_of_areflexive_relation_class S x x →
 413         Morphism_Context Hole dir (relation_class_of_areflexive_relation_class S) dir'
 414 with Morphism_Context_List :
 415    rewrite_direction → Arguments → Type
 416 :=
 417     fcl_singl :
 418       ∀S,dir',dir''.
 419        check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' →
 420         Morphism_Context Hole dir (relation_class_of_argument_class S) dir' →
 421          Morphism_Context_List Hole dir dir'' (singl ? S)
 422  | fcl_cons :
 423       ∀S,L,dir',dir''.
 424        check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' →
 425         Morphism_Context Hole dir (relation_class_of_argument_class S) dir' →
 426          Morphism_Context_List Hole dir dir'' L →
 427           Morphism_Context_List Hole dir dir'' (cons ? S L).
 428
 429 definition product_of_arguments : Arguments → Type.
 430  intro;
 431  elim a;
 432   [ apply (carrier_of_relation_class ? t)
 433   | apply (Prod (carrier_of_relation_class ? t) T)
 434   ]
 435 qed.
 436
 437 definition get_rewrite_direction: rewrite_direction → Argument_Class → rewrite_direction.
 438  intros (dir R);
 439  cases (variance_of_argument_class R);
 440   [ cases a;
 441      [ exact dir                      (* covariant *)
 442      | exact (opposite_direction dir) (* contravariant *)
 443      ]
 444   | exact dir                         (* symmetric relation *)
 445   ]
 446 qed.
 447
 448 definition directed_relation_of_relation_class:
 449  ∀dir:rewrite_direction.∀R: Relation_Class.
 450    carrier_of_relation_class ? R → carrier_of_relation_class ? R → Prop.
 451  intros;
 452  cases r;
 453   [ exact (relation_of_relation_class ? ? c c1)
 454   | apply (relation_of_relation_class ? ? c1 c)
 455   ]
 456 qed.
 457
 458 definition directed_relation_of_argument_class:
 459  ∀dir:rewrite_direction.∀R: Argument_Class.
 460    carrier_of_relation_class ? R → carrier_of_relation_class ? R → Prop.
 461   intros (dir R);
 462   generalize in match
 463    (about_carrier_of_relation_class_and_relation_class_of_argument_class R);
 464   intro H;
 465   apply (directed_relation_of_relation_class dir (relation_class_of_argument_class R));
 466   apply (eq_rect ? ? (λX.X) ? ? (sym_eq ? ? ? H));
 467    [ apply c
 468    | apply c1
 469    ]
 470 qed.
 471
 472 definition relation_of_product_of_arguments:
 473  ∀dir:rewrite_direction.∀In.
 474   product_of_arguments In → product_of_arguments In → Prop.
 475  intros 2;
 476  elim In 0;
 477   [ simplify;
 478     intro;
 479     exact (directed_relation_of_argument_class (get_rewrite_direction r t) t)
 480   | intros;
 481     change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
 482     change in p1 with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
 483     cases p;
 484     cases p1;
 485    apply And;
 486     [ exact
 487       (directed_relation_of_argument_class (get_rewrite_direction r t) t a a1)
 488     | exact (R b b1)
 489     ]
 490   ]
 491 qed.
 492
 493 (*
 494 definition apply_morphism:
 495  ∀In Out (m: function_type_of_morphism_signature In Out)
 496   (args: product_of_arguments In). carrier_of_relation_class Out.
 497  intros.
 498  induction In.
 499    exact (m args).
 500    simpl in m. args.
 501    destruct args.
 502    exact (IHIn (m c) p).
 503 qed.
 504
 505 Theorem apply_morphism_compatibility_Right2Left:
 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 Right2Left ? args1 args2 →
 510         directed_relation_of_relation_class Right2Left ?
 511          (apply_morphism ? ? m2 args1)
 512          (apply_morphism ? ? m1 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      destruct v.
 541        apply IHIn.
 542          apply H; exact H0.
 543          exact H1.
 544        apply IHIn.
 545          apply H; exact H0.
 546           exact H1.
 547     rewrite H0; apply IHIn.
 548       apply H.
 549       exact H1.
 550 Qed.
 551
 552 Theorem apply_morphism_compatibility_Left2Right:
 553  ∀In Out (m1 m2: function_type_of_morphism_signature In Out)
 554    (args1 args2: product_of_arguments In).
 555      make_compatibility_goal_aux ? ? m1 m2 →
 556       relation_of_product_of_arguments Left2Right ? args1 args2 →
 557         directed_relation_of_relation_class Left2Right ?
 558          (apply_morphism ? ? m1 args1)
 559          (apply_morphism ? ? m2 args2).
 560   induction In; intros.
 561     simpl in m1. m2. args1. args2. H0 |- *.
 562     destruct a; simpl in H; hnf in H0.
 563           apply H; exact H0.
 564           destruct v; simpl in H0; apply H; exact H0.
 565           apply H; exact H0.
 566           destruct v; simpl in H0; apply H; exact H0.
 567           rewrite H0; apply H; exact H0.
 568
 569     simpl in m1. m2. args1. args2. H0 |- *.
 570    destruct args1; destruct args2; simpl.
 571    destruct H0.
 572    simpl in H.
 573    destruct a; simpl in H.
 574      apply IHIn.
 575        apply H; exact H0.
 576        exact H1.
 577      destruct v.
 578        apply IHIn.
 579          apply H; exact H0.
 580          exact H1.
 581        apply IHIn.
 582          apply H; exact H0.
 583           exact H1.
 584        apply IHIn.
 585          apply H; exact H0.
 586          exact H1.
 587        apply IHIn.
 588          destruct v; simpl in H. H0; apply H; exact H0.
 589           exact H1.
 590     rewrite H0; apply IHIn.
 591       apply H.
 592       exact H1.
 593 Qed.
 594
 595 definition interp :
 596  ∀Hole dir Out dir'. carrier_of_relation_class Hole →
 597   Morphism_Context Hole dir Out dir' → carrier_of_relation_class Out.
 598  intros Hole dir Out dir' H t.
 599  elim t using
 600   (@Morphism_Context_rect2 Hole dir (fun S ? ? => carrier_of_relation_class S)
 601     (fun ? L fcl => product_of_arguments L));
 602   intros.
 603    exact (apply_morphism ? ? (Function m) X).
 604    exact H.
 605    exact c.
 606    exact x.
 607    simpl;
 608      rewrite <-
 609        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 610      exact X.
 611    split.
 612      rewrite <-
 613        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 614        exact X.
 615        exact X0.
 616 qed.
 617
 618 (*CSC: interp and interp_relation_class_list should be mutually defined. since
 619    the proof term of each one contains the proof term of the other one. However
 620    I cannot do that interactively (I should write the Fix by hand) *)
 621 definition interp_relation_class_list :
 622  ∀Hole dir dir' (L: Arguments). carrier_of_relation_class Hole →
 623   Morphism_Context_List Hole dir dir' L → product_of_arguments L.
 624  intros Hole dir dir' L H t.
 625  elim t using
 626   (@Morphism_Context_List_rect2 Hole dir (fun S ? ? => carrier_of_relation_class S)
 627     (fun ? L fcl => product_of_arguments L));
 628  intros.
 629    exact (apply_morphism ? ? (Function m) X).
 630    exact H.
 631    exact c.
 632    exact x.
 633    simpl;
 634      rewrite <-
 635        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 636      exact X.
 637    split.
 638      rewrite <-
 639        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 640        exact X.
 641        exact X0.
 642 qed.
 643
 644 Theorem setoid_rewrite:
 645  ∀Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole)
 646   (E: Morphism_Context Hole dir Out dir').
 647    (directed_relation_of_relation_class dir Hole E1 E2) →
 648     (directed_relation_of_relation_class dir' Out (interp E1 E) (interp E2 E)).
 649  intros.
 650  elim E using
 651    (@Morphism_Context_rect2 Hole dir
 652      (fun S dir'' E => directed_relation_of_relation_class dir'' S (interp E1 E) (interp E2 E))
 653      (fun dir'' L fcl =>
 654         relation_of_product_of_arguments dir'' ?
 655          (interp_relation_class_list E1 fcl)
 656          (interp_relation_class_list E2 fcl))); intros.
 657    change (directed_relation_of_relation_class dir'0 Out0
 658     (apply_morphism ? ? (Function m) (interp_relation_class_list E1 m0))
 659     (apply_morphism ? ? (Function m) (interp_relation_class_list E2 m0))).
 660    destruct dir'0.
 661      apply apply_morphism_compatibility_Left2Right.
 662        exact (Compat m).
 663        exact H0.
 664      apply apply_morphism_compatibility_Right2Left.
 665        exact (Compat m).
 666        exact H0.
 667
 668    exact H.
 669
 670    unfold interp. Morphism_Context_rect2.
 671    (*CSC: reflexivity used here*)
 672    destruct S; destruct dir'0; simpl; (apply r || reflexivity).
 673
 674    destruct dir'0; exact r.
 675
 676   destruct S; unfold directed_relation_of_argument_class; simpl in H0 |- *;
 677    unfold get_rewrite_direction; simpl.
 678      destruct dir'0; destruct dir'';
 679        (exact H0 ||
 680         unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
 681      (* the following mess with generalize/clear/intros is to help Coq resolving *)
 682      (* second order unification problems.                                                                *)
 683      generalize m c H0; clear H0 m c; inversion c;
 684        generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
 685          (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
 686      destruct dir'0; destruct dir'';
 687        (exact H0 ||
 688         unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
 689 (* the following mess with generalize/clear/intros is to help Coq resolving *)
 690      (* second order unification problems.                                                                *)
 691      generalize m c H0; clear H0 m c; inversion c;
 692        generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
 693          (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
 694      destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0).
 695
 696   change
 697     (directed_relation_of_argument_class (get_rewrite_direction dir'' S) S
 698        (eq_rect ? (fun T : Type => T) (interp E1 m) ?
 699          (about_carrier_of_relation_class_and_relation_class_of_argument_class S))
 700        (eq_rect ? (fun T : Type => T) (interp E2 m) ?
 701          (about_carrier_of_relation_class_and_relation_class_of_argument_class S)) /\
 702      relation_of_product_of_arguments dir'' ?
 703        (interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)).
 704    split.
 705      clear m0 H1; destruct S; simpl in H0 |- *; unfold get_rewrite_direction; simpl.
 706         destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
 707         inversion c.
 708           rewrite <- H3; exact H0.
 709           rewrite (opposite_direction_idempotent dir'0); exact H0.
 710         destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
 711         inversion c.
 712           rewrite <- H3; exact H0.
 713           rewrite (opposite_direction_idempotent dir'0); exact H0.
 714         destruct dir''; destruct dir'0; (exact H0 || hnf; symmetry; exact H0).
 715      exact H1.
 716 Qed.
 717
 718 (* A FEW EXAMPLES ON iff *)
 719
 720 (* impl IS A MORPHISM *)
 721
 722 Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
 723 unfold impl; tauto.
 724 Qed.
 725
 726 (* and IS A MORPHISM *)
 727
 728 Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
 729  tauto.
 730 Qed.
 731
 732 (* or IS A MORPHISM *)
 733
 734 Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
 735  tauto.
 736 Qed.
 737
 738 (* not IS A MORPHISM *)
 739
 740 Add Morphism not with signature iff ==> iff as Not_Morphism.
 741  tauto.
 742 Qed.
 743
 744 (* THE SAME EXAMPLES ON impl *)
 745
 746 Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
 747  unfold impl; tauto.
 748 Qed.
 749
 750 Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
 751  unfold impl; tauto.
 752 Qed.
 753
 754 Add Morphism not with signature impl -→ impl as Not_Morphism2.
 755  unfold impl; tauto.
 756 Qed.
 757
 758 *)