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 lemma Morphism_Context_rect2:
 430  ∀Hole,dir.
 431  ∀P:
 432   ∀r:Relation_Class.∀r0:rewrite_direction.Morphism_Context Hole dir r r0 → Type.
 433  ∀P0:
 434   ∀r:rewrite_direction.∀a:Arguments.Morphism_Context_List Hole dir r a → Type.
 435  (∀In,Out,dir'.
 436    ∀m:Morphism_Theory In Out.∀m0:Morphism_Context_List Hole dir dir' In.
 437     P0 dir' In m0 → P Out dir' (App Hole ? ? ? ? m m0)) →
 438  P Hole dir (ToReplace Hole dir) →
 439  (∀S:Reflexive_Relation_Class.∀dir'.∀c:carrier_of_reflexive_relation_class S.
 440    P (relation_class_of_reflexive_relation_class S) dir'
 441     (ToKeep Hole dir S dir' c)) →
 442  (∀S:Areflexive_Relation_Class.∀dir'.
 443    ∀x:carrier_of_areflexive_relation_class S.
 444     ∀r:relation_of_areflexive_relation_class S x x.
 445      P (relation_class_of_areflexive_relation_class S) dir'
 446       (ProperElementToKeep Hole dir S dir' x r)) →
 447  (∀S:Argument_Class.∀dir',dir''.
 448    ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
 449     ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
 450      P (relation_class_of_argument_class S) dir' m ->
 451       P0 dir'' (singl ? S) (fcl_singl ? ? S ? ? c m)) →
 452  (∀S:Argument_Class.∀L:Arguments.∀dir',dir''.
 453    ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
 454     ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
 455      P (relation_class_of_argument_class S) dir' m →
 456       ∀m0:Morphism_Context_List Hole dir dir'' L.
 457        P0 dir'' L m0 → P0 dir'' (cons ? S L) (fcl_cons ? ? S ? ? ? c m m0)) →
 458  ∀r:Relation_Class.∀r0:rewrite_direction.∀m:Morphism_Context Hole dir r r0.
 459   P r r0 m
 460 ≝
 461  λHole,dir,P,P0,f,f0,f1,f2,f3,f4.
 462  let rec
 463   F (rc:Relation_Class) (r0:rewrite_direction)
 464    (m:Morphism_Context Hole dir rc r0) on m : P rc r0 m
 465  ≝
 466   match m return λrc.λr0.λm0.P rc r0 m0 with
 467   [ App In Out dir' m0 m1 ⇒ f In Out dir' m0 m1 (F0 dir' In m1)
 468   | ToReplace ⇒ f0
 469   | ToKeep S dir' c ⇒ f1 S dir' c
 470   | ProperElementToKeep S dir' x r1 ⇒ f2 S dir' x r1
 471   ]
 472  and
 473   F0 (r:rewrite_direction) (a:Arguments)
 474    (m:Morphism_Context_List Hole dir r a) on m : P0 r a m
 475  ≝
 476   match m return λr.λa.λm0.P0 r a m0 with
 477   [ fcl_singl S dir' dir'' c m0 ⇒
 478       f3 S dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
 479   | fcl_cons S L dir' dir'' c m0 m1 ⇒
 480       f4 S L dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
 481         m1 (F0 dir'' L m1)
 482   ]
 483 in F.
 484
 485 lemma Morphism_Context_List_rect2:
 486  ∀Hole,dir.
 487  ∀P:
 488   ∀r:Relation_Class.∀r0:rewrite_direction.Morphism_Context Hole dir r r0 → Type.
 489  ∀P0:
 490   ∀r:rewrite_direction.∀a:Arguments.Morphism_Context_List Hole dir r a → Type.
 491  (∀In,Out,dir'.
 492    ∀m:Morphism_Theory In Out.∀m0:Morphism_Context_List Hole dir dir' In.
 493     P0 dir' In m0 → P Out dir' (App Hole ? ? ? ? m m0)) →
 494  P Hole dir (ToReplace Hole dir) →
 495  (∀S:Reflexive_Relation_Class.∀dir'.∀c:carrier_of_reflexive_relation_class S.
 496    P (relation_class_of_reflexive_relation_class S) dir'
 497     (ToKeep Hole dir S dir' c)) →
 498  (∀S:Areflexive_Relation_Class.∀dir'.
 499    ∀x:carrier_of_areflexive_relation_class S.
 500     ∀r:relation_of_areflexive_relation_class S x x.
 501      P (relation_class_of_areflexive_relation_class S) dir'
 502       (ProperElementToKeep Hole dir S dir' x r)) →
 503  (∀S:Argument_Class.∀dir',dir''.
 504    ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
 505     ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
 506      P (relation_class_of_argument_class S) dir' m ->
 507       P0 dir'' (singl ? S) (fcl_singl ? ? S ? ? c m)) →
 508  (∀S:Argument_Class.∀L:Arguments.∀dir',dir''.
 509    ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
 510     ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
 511      P (relation_class_of_argument_class S) dir' m →
 512       ∀m0:Morphism_Context_List Hole dir dir'' L.
 513        P0 dir'' L m0 → P0 dir'' (cons ? S L) (fcl_cons ? ? S ? ? ? c m m0)) →
 514  ∀r:rewrite_direction.∀a:Arguments.∀m:Morphism_Context_List Hole dir r a.
 515   P0 r a m
 516 ≝
 517  λHole,dir,P,P0,f,f0,f1,f2,f3,f4.
 518  let rec
 519   F (rc:Relation_Class) (r0:rewrite_direction)
 520    (m:Morphism_Context Hole dir rc r0) on m : P rc r0 m
 521  ≝
 522   match m return λrc.λr0.λm0.P rc r0 m0 with
 523   [ App In Out dir' m0 m1 ⇒ f In Out dir' m0 m1 (F0 dir' In m1)
 524   | ToReplace ⇒ f0
 525   | ToKeep S dir' c ⇒ f1 S dir' c
 526   | ProperElementToKeep S dir' x r1 ⇒ f2 S dir' x r1
 527   ]
 528  and
 529   F0 (r:rewrite_direction) (a:Arguments)
 530    (m:Morphism_Context_List Hole dir r a) on m : P0 r a m
 531  ≝
 532   match m return λr.λa.λm0.P0 r a m0 with
 533   [ fcl_singl S dir' dir'' c m0 ⇒
 534       f3 S dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
 535   | fcl_cons S L dir' dir'' c m0 m1 ⇒
 536       f4 S L dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
 537         m1 (F0 dir'' L m1)
 538   ]
 539 in F0.
 540
 541 definition product_of_arguments : Arguments → Type.
 542  intro;
 543  elim a;
 544   [ apply (carrier_of_relation_class ? t)
 545   | apply (Prod (carrier_of_relation_class ? t) T)
 546   ]
 547 qed.
 548
 549 definition get_rewrite_direction: rewrite_direction → Argument_Class → rewrite_direction.
 550  intros (dir R);
 551  cases (variance_of_argument_class R);
 552   [ exact dir
 553   | cases a;
 554      [ exact dir                      (* covariant *)
 555      | exact (opposite_direction dir) (* contravariant *)
 556      ]
 557   ]
 558 qed.
 559
 560 definition directed_relation_of_relation_class:
 561  ∀dir:rewrite_direction.∀R: Relation_Class.
 562    carrier_of_relation_class ? R → carrier_of_relation_class ? R → Prop.
 563  intros;
 564  cases r;
 565   [ exact (relation_of_relation_class ? ? c c1)
 566   | apply (relation_of_relation_class ? ? c1 c)
 567   ]
 568 qed.
 569
 570 definition directed_relation_of_argument_class:
 571  ∀dir:rewrite_direction.∀R: Argument_Class.
 572    carrier_of_relation_class ? R → carrier_of_relation_class ? R → Prop.
 573   intros (dir R);
 574   generalize in match
 575    (about_carrier_of_relation_class_and_relation_class_of_argument_class R);
 576   intro H;
 577   apply (directed_relation_of_relation_class dir (relation_class_of_argument_class R));
 578   apply (eq_rect ? ? (λX.X) ? ? (sym_eq ? ? ? H));
 579    [ apply c
 580    | apply c1
 581    ]
 582 qed.
 583
 584 definition relation_of_product_of_arguments:
 585  ∀dir:rewrite_direction.∀In.
 586   product_of_arguments In → product_of_arguments In → Prop.
 587  intros 2;
 588  elim In 0;
 589   [ simplify;
 590     intro;
 591     exact (directed_relation_of_argument_class (get_rewrite_direction r t) t)
 592   | intros;
 593     change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
 594     change in p1 with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
 595     cases p;
 596     cases p1;
 597    apply And;
 598     [ exact
 599       (directed_relation_of_argument_class (get_rewrite_direction r t) t a a1)
 600     | exact (R b b1)
 601     ]
 602   ]
 603 qed.
 604
 605 definition apply_morphism:
 606  ∀In,Out.∀m: function_type_of_morphism_signature In Out.
 607   ∀args: product_of_arguments In. carrier_of_relation_class ? Out.
 608  intro;
 609  elim In;
 610   [ exact (f p)
 611   | change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
 612    elim p;
 613    change in f1 with (carrier_of_relation_class variance t → function_type_of_morphism_signature n Out);
 614    exact (f ? (f1 t1) t2)
 615   ]
 616 qed.
 617
 618 theorem apply_morphism_compatibility_Right2Left:
 619  ∀In,Out.∀m1,m2: function_type_of_morphism_signature In Out.
 620   ∀args1,args2: product_of_arguments In.
 621      make_compatibility_goal_aux ? ? m1 m2 →
 622       relation_of_product_of_arguments Right2Left ? args1 args2 →
 623         directed_relation_of_relation_class Right2Left ?
 624          (apply_morphism ? ? m2 args1)
 625          (apply_morphism ? ? m1 args2).
 626   intro;
 627   elim In;
 628    [ simplify in m1 m2 args1 args2 ⊢ %;
 629      change in H1 with
 630       (directed_relation_of_argument_class
 631         (get_rewrite_direction Right2Left t) t args1 args2);
 632      generalize in match H1; clear H1;
 633      generalize in match H; clear H;
 634      generalize in match args2; clear args2;
 635      generalize in match args1; clear args1;
 636      generalize in match m2; clear m2;
 637      generalize in match m1; clear m1;
 638      elim t 0;
 639       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
 640         simplify in H;
 641         simplify in H1;
 642         simplify;
 643         apply H;
 644         exact H1
 645       | intros 8 (v T1 r Hr m1 m2 args1 args2);
 646         cases v;
 647         intros (H H1);
 648         simplify in H1;
 649         apply H;
 650         exact H1
 651       | intros;
 652         apply H1;
 653         exact H2
 654       | intros 7 (v);
 655         cases v;
 656         intros (H H1);
 657         simplify in H1;
 658         apply H;
 659         exact H1
 660       | intros;
 661         simplify in H1;
 662         rewrite > H1;
 663         apply H;
 664         exact H1
 665       ]
 666    | change in m1 with
 667       (carrier_of_relation_class variance t →
 668         function_type_of_morphism_signature n Out);
 669      change in m2 with
 670       (carrier_of_relation_class variance t →
 671         function_type_of_morphism_signature n Out);
 672      change in args1 with
 673       ((carrier_of_relation_class ? t) × (product_of_arguments n));
 674      change in args2 with
 675       ((carrier_of_relation_class ? t) × (product_of_arguments n));
 676      generalize in match H2; clear H2;
 677      elim args2 0; clear args2;
 678      elim args1; clear args1;
 679      elim H2; clear H2;
 680      change in H4 with
 681       (relation_of_product_of_arguments Right2Left n t2 t4);
 682      change with
 683       (relation_of_relation_class unit Out (apply_morphism n Out (m1 t3) t4)
 684         (apply_morphism n Out (m2 t1) t2));
 685      generalize in match H3; clear H3;
 686      generalize in match t3; clear t3;
 687      generalize in match t1; clear t1;
 688      generalize in match H1; clear H1;
 689      generalize in match m2; clear m2;
 690      generalize in match m1; clear m1;
 691      elim t 0;
 692       [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
 693         simplify in H3;
 694         change in H1 with
 695          (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 696      | intro v;
 697        elim v 0;
 698        [ intros (T1 r Hr m1 m2 H1 t1 t3 H3);
 699          simplify in H3;
 700          change in H1 with
 701           (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 702        | intros (T1 r Hr m1 m2 H1 t1 t3 H3);
 703          simplify in H3;
 704          change in H1 with
 705           (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 706        ]
 707      | intros (T1 r Hs m1 m2 H1 t1 t3 H3);
 708        simplify in H3;
 709        change in H1 with
 710         (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 711      | intro v;
 712        elim v 0;
 713         [ intros (T1 r m1 m2 H1 t1 t3 H3);
 714           simplify in H3;
 715           change in H1 with
 716            (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 717         | intros (T1 r m1 m2 H1 t1 t3 H3);
 718           simplify in H3;
 719           change in H1 with
 720            (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 721         ]
 722      | intros (T m1 m2 H1 t1 t3 H3);
 723        simplify in H3;
 724        change in H1 with
 725         (∀x:T. make_compatibility_goal_aux n Out (m1 x) (m2 x));
 726        rewrite > H3;
 727        simplify in H;
 728        apply H;
 729         [ apply H1
 730         | assumption
 731         ]
 732      ] ;
 733      simplify in H;
 734      apply H;
 735       [1,3,5,7,9,11:
 736         apply H1;
 737         assumption
 738       |2,4,6,8,10,12:
 739         assumption
 740       ]
 741    ]
 742 qed.
 743
 744 theorem apply_morphism_compatibility_Left2Right:
 745  ∀In,Out.∀m1,m2: function_type_of_morphism_signature In Out.
 746   ∀args1,args2: product_of_arguments In.
 747      make_compatibility_goal_aux ? ? m1 m2 →
 748       relation_of_product_of_arguments Left2Right ? args1 args2 →
 749         directed_relation_of_relation_class Left2Right ?
 750          (apply_morphism ? ? m1 args1)
 751          (apply_morphism ? ? m2 args2).
 752   intro;
 753   elim In;
 754    [ simplify in m1 m2 args1 args2 ⊢ %;
 755      change in H1 with
 756       (directed_relation_of_argument_class
 757         (get_rewrite_direction Left2Right t) t args1 args2);
 758      generalize in match H1; clear H1;
 759      generalize in match H; clear H;
 760      generalize in match args2; clear args2;
 761      generalize in match args1; clear args1;
 762      generalize in match m2; clear m2;
 763      generalize in match m1; clear m1;
 764      elim t 0;
 765       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
 766         simplify in H;
 767         simplify in H1;
 768         simplify;
 769         apply H;
 770         exact H1
 771       | intros 8 (v T1 r Hr m1 m2 args1 args2);
 772         cases v;
 773         intros (H H1);
 774         simplify in H1;
 775         apply H;
 776         exact H1
 777       | intros;
 778         apply H1;
 779         exact H2
 780       | intros 7 (v);
 781         cases v;
 782         intros (H H1);
 783         simplify in H1;
 784         apply H;
 785         exact H1
 786       | intros;
 787         simplify in H1;
 788         rewrite > H1;
 789         apply H;
 790         exact H1
 791       ]
 792    | change in m1 with
 793       (carrier_of_relation_class variance t →
 794         function_type_of_morphism_signature n Out);
 795      change in m2 with
 796       (carrier_of_relation_class variance t →
 797         function_type_of_morphism_signature n Out);
 798      change in args1 with
 799       ((carrier_of_relation_class ? t) × (product_of_arguments n));
 800      change in args2 with
 801       ((carrier_of_relation_class ? t) × (product_of_arguments n));
 802      generalize in match H2; clear H2;
 803      elim args2 0; clear args2;
 804      elim args1; clear args1;
 805      elim H2; clear H2;
 806      change in H4 with
 807       (relation_of_product_of_arguments Left2Right n t2 t4);
 808      change with
 809       (relation_of_relation_class unit Out (apply_morphism n Out (m1 t1) t2)
 810         (apply_morphism n Out (m2 t3) t4));
 811      generalize in match H3; clear H3;
 812      generalize in match t3; clear t3;
 813      generalize in match t1; clear t1;
 814      generalize in match H1; clear H1;
 815      generalize in match m2; clear m2;
 816      generalize in match m1; clear m1;
 817      elim t 0;
 818       [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
 819         simplify in H3;
 820         change in H1 with
 821          (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 822      | intro v;
 823        elim v 0;
 824        [ intros (T1 r Hr m1 m2 H1 t1 t3 H3);
 825          simplify in H3;
 826          change in H1 with
 827           (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 828        | intros (T1 r Hr m1 m2 H1 t1 t3 H3);
 829          simplify in H3;
 830          change in H1 with
 831           (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 832        ]
 833      | intros (T1 r Hs m1 m2 H1 t1 t3 H3);
 834        simplify in H3;
 835        change in H1 with
 836         (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 837      | intro v;
 838        elim v 0;
 839         [ intros (T1 r m1 m2 H1 t1 t3 H3);
 840           simplify in H3;
 841           change in H1 with
 842            (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 843         | intros (T1 r m1 m2 H1 t1 t3 H3);
 844           simplify in H3;
 845           change in H1 with
 846            (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 847         ]
 848      | intros (T m1 m2 H1 t1 t3 H3);
 849        simplify in H3;
 850        change in H1 with
 851         (∀x:T. make_compatibility_goal_aux n Out (m1 x) (m2 x));
 852        rewrite > H3;
 853        simplify in H;
 854        apply H;
 855         [ apply H1
 856         | assumption
 857         ]
 858      ] ;
 859      simplify in H;
 860      apply H;
 861       [1,3,5,7,9,11:
 862         apply H1;
 863         assumption
 864       |2,4,6,8,10,12:
 865         assumption
 866       ]
 867    ]
 868 qed.
 869
 870 definition interp :
 871  ∀Hole,dir,Out,dir'. carrier_of_relation_class ? Hole →
 872   Morphism_Context Hole dir Out dir' → carrier_of_relation_class ? Out.
 873  intros (Hole dir Out dir' H t).
 874  apply
 875   (Morphism_Context_rect2 Hole dir (λS,xx,yy. carrier_of_relation_class ? S)
 876     (λxx,L,fcl.product_of_arguments L));
 877   intros;
 878    [8: apply t
 879    |7: skip
 880    | exact (apply_morphism ? ? (Function ? ? m) p)
 881    | exact H
 882    | exact c
 883    | exact x
 884    | simplify;
 885      rewrite <
 886        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 887      exact c1
 888    | split;
 889       [ rewrite <
 890          (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 891         exact c1
 892       | exact p
 893       ]
 894    ]
 895 qed.
 896
 897
 898 (*CSC: interp and interp_relation_class_list should be mutually defined. since
 899    the proof term of each one contains the proof term of the other one. However
 900    I cannot do that interactively (I should write the Fix by hand) *)
 901 definition interp_relation_class_list :
 902  ∀Hole,dir,dir'.∀L: Arguments. carrier_of_relation_class ? Hole →
 903   Morphism_Context_List Hole dir dir' L → product_of_arguments L.
 904  intros (Hole dir dir' L H t);
 905  apply
 906   (Morphism_Context_List_rect2 Hole dir (λS,xx,yy.carrier_of_relation_class ? S)
 907     (λxx,L,fcl.product_of_arguments L));
 908  intros;
 909   [8: apply t
 910   |7: skip
 911   | exact (apply_morphism ? ? (Function ? ? m) p)
 912   | exact H
 913   | exact c
 914   | exact x
 915   | simplify;
 916      rewrite <
 917        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 918      exact c1
 919   | split;
 920      [ rewrite <
 921         (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 922        exact c1
 923      | exact p
 924      ]
 925   ]
 926 qed.
 927
 928 (*
 929 Theorem setoid_rewrite:
 930  ∀Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole)
 931   (E: Morphism_Context Hole dir Out dir').
 932    (directed_relation_of_relation_class dir Hole E1 E2) →
 933     (directed_relation_of_relation_class dir' Out (interp E1 E) (interp E2 E)).
 934  intros.
 935  elim E using
 936    (@Morphism_Context_rect2 Hole dir
 937      (fun S dir'' E => directed_relation_of_relation_class dir'' S (interp E1 E) (interp E2 E))
 938      (fun dir'' L fcl =>
 939         relation_of_product_of_arguments dir'' ?
 940          (interp_relation_class_list E1 fcl)
 941          (interp_relation_class_list E2 fcl))); intros.
 942    change (directed_relation_of_relation_class dir'0 Out0
 943     (apply_morphism ? ? (Function m) (interp_relation_class_list E1 m0))
 944     (apply_morphism ? ? (Function m) (interp_relation_class_list E2 m0))).
 945    destruct dir'0.
 946      apply apply_morphism_compatibility_Left2Right.
 947        exact (Compat m).
 948        exact H0.
 949      apply apply_morphism_compatibility_Right2Left.
 950        exact (Compat m).
 951        exact H0.
 952
 953    exact H.
 954
 955    unfold interp. Morphism_Context_rect2.
 956    (*CSC: reflexivity used here*)
 957    destruct S; destruct dir'0; simpl; (apply r || reflexivity).
 958
 959    destruct dir'0; exact r.
 960
 961   destruct S; unfold directed_relation_of_argument_class; simpl in H0 |- *;
 962    unfold get_rewrite_direction; simpl.
 963      destruct dir'0; destruct dir'';
 964        (exact H0 ||
 965         unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
 966      (* the following mess with generalize/clear/intros is to help Coq resolving *)
 967      (* second order unification problems.                                                                *)
 968      generalize m c H0; clear H0 m c; inversion c;
 969        generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
 970          (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
 971      destruct dir'0; destruct dir'';
 972        (exact H0 ||
 973         unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
 974 (* the following mess with generalize/clear/intros is to help Coq resolving *)
 975      (* second order unification problems.                                                                *)
 976      generalize m c H0; clear H0 m c; inversion c;
 977        generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
 978          (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
 979      destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0).
 980
 981   change
 982     (directed_relation_of_argument_class (get_rewrite_direction dir'' S) S
 983        (eq_rect ? (fun T : Type => T) (interp E1 m) ?
 984          (about_carrier_of_relation_class_and_relation_class_of_argument_class S))
 985        (eq_rect ? (fun T : Type => T) (interp E2 m) ?
 986          (about_carrier_of_relation_class_and_relation_class_of_argument_class S)) /\
 987      relation_of_product_of_arguments dir'' ?
 988        (interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)).
 989    split.
 990      clear m0 H1; destruct S; simpl in H0 |- *; unfold get_rewrite_direction; simpl.
 991         destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
 992         inversion c.
 993           rewrite <- H3; exact H0.
 994           rewrite (opposite_direction_idempotent dir'0); exact H0.
 995         destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
 996         inversion c.
 997           rewrite <- H3; exact H0.
 998           rewrite (opposite_direction_idempotent dir'0); exact H0.
 999         destruct dir''; destruct dir'0; (exact H0 || hnf; symmetry; exact H0).
1000      exact H1.
1001 Qed.
1002
1003 (* A FEW EXAMPLES ON iff *)
1004
1005 (* impl IS A MORPHISM *)
1006
1007 Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
1008 unfold impl; tauto.
1009 Qed.
1010
1011 (* and IS A MORPHISM *)
1012
1013 Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
1014  tauto.
1015 Qed.
1016
1017 (* or IS A MORPHISM *)
1018
1019 Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
1020  tauto.
1021 Qed.
1022
1023 (* not IS A MORPHISM *)
1024
1025 Add Morphism not with signature iff ==> iff as Not_Morphism.
1026  tauto.
1027 Qed.
1028
1029 (* THE SAME EXAMPLES ON impl *)
1030
1031 Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
1032  unfold impl; tauto.
1033 Qed.
1034
1035 Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
1036  unfold impl; tauto.
1037 Qed.
1038
1039 Add Morphism not with signature impl -→ impl as Not_Morphism2.
1040  unfold impl; tauto.
1041 Qed.
1042
1043 *)