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   [ exact dir
 441   | cases a;
 442      [ exact dir                      (* covariant *)
 443      | exact (opposite_direction dir) (* contravariant *)
 444      ]
 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 definition apply_morphism:
 494  ∀In,Out.∀m: function_type_of_morphism_signature In Out.
 495   ∀args: product_of_arguments In. carrier_of_relation_class ? Out.
 496  intro;
 497  elim In;
 498   [ exact (f p)
 499   | change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
 500    elim p;
 501    change in f1 with (carrier_of_relation_class variance t → function_type_of_morphism_signature n Out);
 502    exact (f ? (f1 t1) t2)
 503   ]
 504 qed.
 505
 506 theorem apply_morphism_compatibility_Right2Left:
 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 Right2Left ? args1 args2 →
 511         directed_relation_of_relation_class Right2Left ?
 512          (apply_morphism ? ? m2 args1)
 513          (apply_morphism ? ? m1 args2).
 514   intro;
 515   elim In;
 516    [ simplify in m1 m2 args1 args2 ⊢ %;
 517      change in H1 with
 518       (directed_relation_of_argument_class
 519         (get_rewrite_direction Right2Left t) t args1 args2);
 520      generalize in match H1; clear H1;
 521      generalize in match H; clear H;
 522      generalize in match args2; clear args2;
 523      generalize in match args1; clear args1;
 524      generalize in match m2; clear m2;
 525      generalize in match m1; clear m1;
 526      elim t 0;
 527       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
 528         simplify in H;
 529         simplify in H1;
 530         simplify;
 531         apply H;
 532         exact H1
 533       | intros 8 (v T1 r Hr m1 m2 args1 args2);
 534         cases v;
 535         intros (H H1);
 536         simplify in H1;
 537         apply H;
 538         exact H1
 539       | intros;
 540         apply H1;
 541         exact H2
 542       | intros 7 (v);
 543         cases v;
 544         intros (H H1);
 545         simplify in H1;
 546         apply H;
 547         exact H1
 548       | intros;
 549         simplify in H1;
 550         rewrite > H1;
 551         apply H;
 552         exact H1
 553       ]
 554    | change in m1 with
 555       (carrier_of_relation_class variance t →
 556         function_type_of_morphism_signature n Out);
 557      change in m2 with
 558       (carrier_of_relation_class variance t →
 559         function_type_of_morphism_signature n Out);
 560      change in args1 with
 561       ((carrier_of_relation_class ? t) × (product_of_arguments n));
 562      change in args2 with
 563       ((carrier_of_relation_class ? t) × (product_of_arguments n));
 564      generalize in match H2; clear H2;
 565      elim args2 0; clear args2;
 566      elim args1; clear args1;
 567      elim H2; clear H2;
 568      change in H4 with
 569       (relation_of_product_of_arguments Right2Left n t2 t4);
 570      change with
 571       (relation_of_relation_class unit Out (apply_morphism n Out (m1 t3) t4)
 572         (apply_morphism n Out (m2 t1) t2));
 573      generalize in match H3; clear H3;
 574      generalize in match t3; clear t3;
 575      generalize in match t1; clear t1;
 576      generalize in match H1; clear H1;
 577      generalize in match m2; clear m2;
 578      generalize in match m1; clear m1;
 579      elim t 0;
 580       [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
 581         simplify in H3;
 582         change in H1 with
 583          (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 584      | intro v;
 585        elim v 0;
 586        [ intros (T1 r Hr m1 m2 H1 t1 t3 H3);
 587          simplify in H3;
 588          change in H1 with
 589           (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 590        | intros (T1 r Hr m1 m2 H1 t1 t3 H3);
 591          simplify in H3;
 592          change in H1 with
 593           (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 594        ]
 595      | intros (T1 r Hs m1 m2 H1 t1 t3 H3);
 596        simplify in H3;
 597        change in H1 with
 598         (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 599      | intro v;
 600        elim v 0;
 601         [ intros (T1 r m1 m2 H1 t1 t3 H3);
 602           simplify in H3;
 603           change in H1 with
 604            (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 605         | intros (T1 r m1 m2 H1 t1 t3 H3);
 606           simplify in H3;
 607           change in H1 with
 608            (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 609         ]
 610      | intros (T m1 m2 H1 t1 t3 H3);
 611        simplify in H3;
 612        change in H1 with
 613         (∀x:T. make_compatibility_goal_aux n Out (m1 x) (m2 x));
 614        rewrite > H3;
 615        simplify in H;
 616        apply H;
 617         [ apply H1
 618         | assumption
 619         ]
 620      ] ;
 621      simplify in H;
 622      apply H;
 623       [1,3,5,7,9,11:
 624         apply H1;
 625         assumption
 626       |2,4,6,8,10,12:
 627         assumption
 628       ]
 629    ]
 630 qed.
 631
 632 (*
 633 Theorem apply_morphism_compatibility_Left2Right:
 634  ∀In Out (m1 m2: function_type_of_morphism_signature In Out)
 635    (args1 args2: product_of_arguments In).
 636      make_compatibility_goal_aux ? ? m1 m2 →
 637       relation_of_product_of_arguments Left2Right ? args1 args2 →
 638         directed_relation_of_relation_class Left2Right ?
 639          (apply_morphism ? ? m1 args1)
 640          (apply_morphism ? ? m2 args2).
 641   induction In; intros.
 642     simpl in m1. m2. args1. args2. H0 |- *.
 643     destruct a; simpl in H; hnf in H0.
 644           apply H; exact H0.
 645           destruct v; simpl in H0; apply H; exact H0.
 646           apply H; exact H0.
 647           destruct v; simpl in H0; apply H; exact H0.
 648           rewrite H0; apply H; exact H0.
 649
 650     simpl in m1. m2. args1. args2. H0 |- *.
 651    destruct args1; destruct args2; simpl.
 652    destruct H0.
 653    simpl in H.
 654    destruct a; simpl in H.
 655      apply IHIn.
 656        apply H; exact H0.
 657        exact H1.
 658      destruct v.
 659        apply IHIn.
 660          apply H; exact H0.
 661          exact H1.
 662        apply IHIn.
 663          apply H; exact H0.
 664           exact H1.
 665        apply IHIn.
 666          apply H; exact H0.
 667          exact H1.
 668        apply IHIn.
 669          destruct v; simpl in H. H0; apply H; exact H0.
 670           exact H1.
 671     rewrite H0; apply IHIn.
 672       apply H.
 673       exact H1.
 674 Qed.
 675
 676 definition interp :
 677  ∀Hole dir Out dir'. carrier_of_relation_class Hole →
 678   Morphism_Context Hole dir Out dir' → carrier_of_relation_class Out.
 679  intros Hole dir Out dir' H t.
 680  elim t using
 681   (@Morphism_Context_rect2 Hole dir (fun S ? ? => carrier_of_relation_class S)
 682     (fun ? L fcl => product_of_arguments L));
 683   intros.
 684    exact (apply_morphism ? ? (Function m) X).
 685    exact H.
 686    exact c.
 687    exact x.
 688    simpl;
 689      rewrite <-
 690        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 691      exact X.
 692    split.
 693      rewrite <-
 694        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 695        exact X.
 696        exact X0.
 697 qed.
 698
 699 (*CSC: interp and interp_relation_class_list should be mutually defined. since
 700    the proof term of each one contains the proof term of the other one. However
 701    I cannot do that interactively (I should write the Fix by hand) *)
 702 definition interp_relation_class_list :
 703  ∀Hole dir dir' (L: Arguments). carrier_of_relation_class Hole →
 704   Morphism_Context_List Hole dir dir' L → product_of_arguments L.
 705  intros Hole dir dir' L H t.
 706  elim t using
 707   (@Morphism_Context_List_rect2 Hole dir (fun S ? ? => carrier_of_relation_class S)
 708     (fun ? L fcl => product_of_arguments L));
 709  intros.
 710    exact (apply_morphism ? ? (Function m) X).
 711    exact H.
 712    exact c.
 713    exact x.
 714    simpl;
 715      rewrite <-
 716        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 717      exact X.
 718    split.
 719      rewrite <-
 720        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 721        exact X.
 722        exact X0.
 723 qed.
 724
 725 Theorem setoid_rewrite:
 726  ∀Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole)
 727   (E: Morphism_Context Hole dir Out dir').
 728    (directed_relation_of_relation_class dir Hole E1 E2) →
 729     (directed_relation_of_relation_class dir' Out (interp E1 E) (interp E2 E)).
 730  intros.
 731  elim E using
 732    (@Morphism_Context_rect2 Hole dir
 733      (fun S dir'' E => directed_relation_of_relation_class dir'' S (interp E1 E) (interp E2 E))
 734      (fun dir'' L fcl =>
 735         relation_of_product_of_arguments dir'' ?
 736          (interp_relation_class_list E1 fcl)
 737          (interp_relation_class_list E2 fcl))); intros.
 738    change (directed_relation_of_relation_class dir'0 Out0
 739     (apply_morphism ? ? (Function m) (interp_relation_class_list E1 m0))
 740     (apply_morphism ? ? (Function m) (interp_relation_class_list E2 m0))).
 741    destruct dir'0.
 742      apply apply_morphism_compatibility_Left2Right.
 743        exact (Compat m).
 744        exact H0.
 745      apply apply_morphism_compatibility_Right2Left.
 746        exact (Compat m).
 747        exact H0.
 748
 749    exact H.
 750
 751    unfold interp. Morphism_Context_rect2.
 752    (*CSC: reflexivity used here*)
 753    destruct S; destruct dir'0; simpl; (apply r || reflexivity).
 754
 755    destruct dir'0; exact r.
 756
 757   destruct S; unfold directed_relation_of_argument_class; simpl in H0 |- *;
 758    unfold get_rewrite_direction; simpl.
 759      destruct dir'0; destruct dir'';
 760        (exact H0 ||
 761         unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
 762      (* the following mess with generalize/clear/intros is to help Coq resolving *)
 763      (* second order unification problems.                                                                *)
 764      generalize m c H0; clear H0 m c; inversion c;
 765        generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
 766          (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
 767      destruct dir'0; destruct dir'';
 768        (exact H0 ||
 769         unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
 770 (* the following mess with generalize/clear/intros is to help Coq resolving *)
 771      (* second order unification problems.                                                                *)
 772      generalize m c H0; clear H0 m c; inversion c;
 773        generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
 774          (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
 775      destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0).
 776
 777   change
 778     (directed_relation_of_argument_class (get_rewrite_direction dir'' S) S
 779        (eq_rect ? (fun T : Type => T) (interp E1 m) ?
 780          (about_carrier_of_relation_class_and_relation_class_of_argument_class S))
 781        (eq_rect ? (fun T : Type => T) (interp E2 m) ?
 782          (about_carrier_of_relation_class_and_relation_class_of_argument_class S)) /\
 783      relation_of_product_of_arguments dir'' ?
 784        (interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)).
 785    split.
 786      clear m0 H1; destruct S; simpl in H0 |- *; unfold get_rewrite_direction; simpl.
 787         destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
 788         inversion c.
 789           rewrite <- H3; exact H0.
 790           rewrite (opposite_direction_idempotent dir'0); exact H0.
 791         destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
 792         inversion c.
 793           rewrite <- H3; exact H0.
 794           rewrite (opposite_direction_idempotent dir'0); exact H0.
 795         destruct dir''; destruct dir'0; (exact H0 || hnf; symmetry; exact H0).
 796      exact H1.
 797 Qed.
 798
 799 (* A FEW EXAMPLES ON iff *)
 800
 801 (* impl IS A MORPHISM *)
 802
 803 Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
 804 unfold impl; tauto.
 805 Qed.
 806
 807 (* and IS A MORPHISM *)
 808
 809 Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
 810  tauto.
 811 Qed.
 812
 813 (* or IS A MORPHISM *)
 814
 815 Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
 816  tauto.
 817 Qed.
 818
 819 (* not IS A MORPHISM *)
 820
 821 Add Morphism not with signature iff ==> iff as Not_Morphism.
 822  tauto.
 823 Qed.
 824
 825 (* THE SAME EXAMPLES ON impl *)
 826
 827 Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
 828  unfold impl; tauto.
 829 Qed.
 830
 831 Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
 832  unfold impl; tauto.
 833 Qed.
 834
 835 Add Morphism not with signature impl -→ impl as Not_Morphism2.
 836  unfold impl; tauto.
 837 Qed.
 838
 839 *)