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 include "logic/coimplication.ma".
  23
  24 (* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *)
  25
  26 (* X will be used to distinguish covariant arguments whose type is an   *)
  27 (* Asymmetric* relation from contravariant arguments of the same type *)
  28 inductive X_Relation_Class (X: Type) : Type ≝
  29    SymmetricReflexive :
  30      ∀A,Aeq. symmetric A Aeq → reflexive ? Aeq → X_Relation_Class X
  31  | AsymmetricReflexive : X → ∀A,Aeq. reflexive A Aeq → X_Relation_Class X
  32  | SymmetricAreflexive : ∀A,Aeq. symmetric A Aeq → X_Relation_Class X
  33  | AsymmetricAreflexive : X → ∀A.∀Aeq : relation A. X_Relation_Class X
  34  | Leibniz : Type → X_Relation_Class X.
  35
  36 inductive variance : Set ≝
  37    Covariant : variance
  38  | Contravariant : variance.
  39
  40 definition Argument_Class ≝ X_Relation_Class variance.
  41 definition Relation_Class ≝ X_Relation_Class unit.
  42
  43 inductive Reflexive_Relation_Class : Type :=
  44    RSymmetric :
  45      ∀A,Aeq. symmetric A Aeq → reflexive ? Aeq → Reflexive_Relation_Class
  46  | RAsymmetric :
  47      ∀A,Aeq. reflexive A Aeq → Reflexive_Relation_Class
  48  | RLeibniz : Type → Reflexive_Relation_Class.
  49
  50 inductive Areflexive_Relation_Class  : Type :=
  51  | ASymmetric : ∀A,Aeq. symmetric A Aeq → Areflexive_Relation_Class
  52  | AAsymmetric : ∀A.∀Aeq : relation A. Areflexive_Relation_Class.
  53
  54 definition relation_class_of_argument_class : Argument_Class → Relation_Class.
  55  intros (a); cases a;
  56   [ apply (SymmetricReflexive ? ? ? H H1)
  57   | apply (AsymmetricReflexive ? something ? ? H)
  58   | apply (SymmetricAreflexive ? ? ? H)
  59   | apply (AsymmetricAreflexive ? something ? r)
  60   | apply (Leibniz ? T)
  61   ]
  62 qed.
  63
  64 definition carrier_of_relation_class : ∀X. X_Relation_Class X → Type.
  65  intros (X x); cases x (A o o o o A o o A o o o A o A); exact A.
  66 qed.
  67
  68 definition relation_of_relation_class:
  69  ∀X,R. carrier_of_relation_class X R → carrier_of_relation_class X R → Prop.
  70 intros 2; cases R; simplify; [1,2,3,4: assumption | apply (eq T) ]
  71 qed.
  72
  73 lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
  74  ∀R.
  75   carrier_of_relation_class ? (relation_class_of_argument_class R) =
  76    carrier_of_relation_class ? R.
  77 intro; cases R; reflexivity.
  78 qed.
  79
  80 inductive nelistT (A : Type) : Type :=
  81    singl : A → nelistT A
  82  | cons : A → nelistT A → nelistT A.
  83
  84 definition Arguments := nelistT Argument_Class.
  85
  86 definition function_type_of_morphism_signature :
  87  Arguments → Relation_Class → Type.
  88   intros (In Out); elim In;
  89   [ exact (carrier_of_relation_class ? t → carrier_of_relation_class ? Out)
  90   | exact (carrier_of_relation_class ? t → T)
  91   ]
  92 qed.
  93
  94 definition make_compatibility_goal_aux:
  95  ∀In,Out.∀f,g:function_type_of_morphism_signature In Out.Prop.
  96  intros 2;
  97  elim In (a); simplify in f f1;
  98  generalize in match f1; clear f1;
  99  generalize in match f; clear f;
 100   [ elim a; simplify in f f1;
 101      [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
 102      | cases t;
 103         [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
 104         | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2))
 105         ]
 106      | exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
 107      | cases t;
 108         [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
 109         | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2))
 110         ]
 111      | exact (∀x. relation_of_relation_class ? Out (f x) (f1 x))
 112      ]
 113   | change with
 114      ((carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) →
 115       (carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) →
 116       Prop).
 117     elim t; simplify in f f1;
 118      [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
 119      |2,4: cases t1;
 120         [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
 121         |2,4: exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))
 122         ]
 123      | exact (∀x. R (f x) (f1 x))
 124      ]
 125   ]
 126 qed.
 127
 128 definition make_compatibility_goal :=
 129  λIn,Out,f. make_compatibility_goal_aux In Out f f.
 130
 131 record Morphism_Theory (In: Arguments) (Out: Relation_Class) : Type :=
 132  { Function : function_type_of_morphism_signature In Out;
 133    Compat : make_compatibility_goal In Out Function
 134  }.
 135
 136 definition list_of_Leibniz_of_list_of_types: nelistT Type → Arguments.
 137  intro;
 138  elim n;
 139   [ apply (singl ? (Leibniz ? t))
 140   | apply (cons ? (Leibniz ? t) a)
 141   ]
 142 qed.
 143
 144 (* every function is a morphism from Leibniz+ to Leibniz *)
 145 definition morphism_theory_of_function :
 146  ∀In: nelistT Type.∀Out: Type.
 147   let In' := list_of_Leibniz_of_list_of_types In in
 148   let Out' := Leibniz ? Out in
 149    function_type_of_morphism_signature In' Out' →
 150     Morphism_Theory In' Out'.
 151   intros;
 152   apply (mk_Morphism_Theory ? ? f);
 153   unfold In' in f; clear In';
 154   unfold Out' in f; clear Out';
 155   generalize in match f; clear f;
 156   elim In;
 157    [ unfold make_compatibility_goal;
 158      whd; intros;
 159      reflexivity
 160    | simplify;
 161      intro;
 162      unfold In' in f;
 163      unfold Out' in f;
 164      exact (H (f1 x))
 165    ]
 166 qed.
 167
 168 (* THE iff RELATION CLASS *)
 169
 170 definition Iff_Relation_Class : Relation_Class.
 171  apply (SymmetricReflexive unit ? iff);
 172   [ exact symmetric_iff
 173   | exact reflexive_iff
 174   ]
 175 qed.
 176
 177 (* THE impl RELATION CLASS *)
 178
 179 definition impl \def \lambda A,B:Prop. A → B.
 180
 181 theorem impl_refl: reflexive ? impl.
 182  unfold reflexive;
 183  intros;
 184  unfold impl;
 185  intro;
 186  assumption.
 187 qed.
 188
 189 definition Impl_Relation_Class : Relation_Class.
 190  unfold Relation_Class;
 191  apply (AsymmetricReflexive unit something ? impl);
 192  exact impl_refl.
 193 qed.
 194
 195 (* UTILITY FUNCTIONS TO PROVE THAT EVERY TRANSITIVE RELATION IS A MORPHISM *)
 196
 197 definition equality_morphism_of_symmetric_areflexive_transitive_relation:
 198  ∀A: Type.∀Aeq: relation A.∀sym: symmetric ? Aeq.∀trans: transitive ? Aeq.
 199   let ASetoidClass := SymmetricAreflexive ? ? ? sym in
 200    (Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass))
 201      Iff_Relation_Class).
 202  intros;
 203  apply mk_Morphism_Theory;
 204   [ exact Aeq
 205   | unfold make_compatibility_goal;
 206     simplify;
 207     intros;
 208     split;
 209     unfold transitive in H;
 210     unfold symmetric in sym;
 211     intro;
 212     autobatch new
 213   ].
 214 qed.
 215
 216 definition equality_morphism_of_symmetric_reflexive_transitive_relation:
 217  ∀A: Type.∀Aeq: relation A.∀refl: reflexive ? Aeq.∀sym: symmetric ? Aeq.
 218   ∀trans: transitive ? Aeq.
 219    let ASetoidClass := SymmetricReflexive ? ? ? sym refl in
 220     (Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass)) Iff_Relation_Class).
 221  intros;
 222  apply mk_Morphism_Theory;
 223  reduce;
 224   [ exact Aeq
 225   | intros;
 226     split;
 227     intro;
 228     unfold transitive in H;
 229     unfold symmetric in sym;
 230     autobatch depth=4.
 231   ]
 232 qed.
 233
 234 definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
 235  ∀A: Type.∀Aeq: relation A.∀trans: transitive ? Aeq.
 236   let ASetoidClass1 := AsymmetricAreflexive ? Contravariant ? Aeq in
 237   let ASetoidClass2 := AsymmetricAreflexive ? Covariant ? Aeq in
 238    (Morphism_Theory (cons ? ASetoidClass1 (singl ? ASetoidClass2)) Impl_Relation_Class).
 239  intros;
 240  apply mk_Morphism_Theory;
 241  [ simplify;
 242    apply Aeq
 243  | simplify;
 244    intros;
 245    whd;
 246    intros;
 247    autobatch
 248  ].
 249 qed.
 250
 251 definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
 252  ∀A: Type.∀Aeq: relation A.∀refl: reflexive ? Aeq.∀trans: transitive ? Aeq.
 253   let ASetoidClass1 := AsymmetricReflexive ? Contravariant ? ? refl in
 254   let ASetoidClass2 := AsymmetricReflexive ? Covariant ? ? refl in
 255    (Morphism_Theory (cons ? ASetoidClass1 (singl ? ASetoidClass2)) Impl_Relation_Class).
 256  intros;
 257  apply mk_Morphism_Theory;
 258  [ simplify;
 259    apply Aeq
 260  | simplify;
 261    intros;
 262    whd;
 263    intro;
 264    autobatch
 265  ].
 266 qed.
 267
 268 (* iff AS A RELATION *)
 269
 270 (*DA PORTARE:Add Relation Prop iff
 271  reflexivity proved by iff_refl
 272  symmetry proved by iff_sym
 273  transitivity proved by iff_trans
 274  as iff_relation.*)
 275
 276 (* every predicate is  morphism from Leibniz+ to Iff_Relation_Class *)
 277 definition morphism_theory_of_predicate :
 278  ∀(In: nelistT Type).
 279   let In' := list_of_Leibniz_of_list_of_types In in
 280    function_type_of_morphism_signature In' Iff_Relation_Class →
 281     Morphism_Theory In' Iff_Relation_Class.
 282   intros;
 283   apply mk_Morphism_Theory;
 284   [ apply f
 285   | generalize in match f; clear f;
 286     unfold In'; clear In';
 287     elim In;
 288      [ reduce;
 289        intro;
 290        apply iff_refl
 291      | simplify;
 292        intro x;
 293        apply (H (f1 x))
 294      ]
 295   ].
 296 qed.
 297
 298 (* impl AS A RELATION *)
 299
 300 theorem impl_trans: transitive ? impl.
 301  whd;
 302  unfold impl;
 303  intros;
 304  autobatch.
 305 qed.
 306
 307 (*DA PORTARE: Add Relation Prop impl
 308  reflexivity proved by impl_refl
 309  transitivity proved by impl_trans
 310  as impl_relation.*)
 311
 312 (* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *)
 313
 314 inductive rewrite_direction : Type :=
 315    Left2Right: rewrite_direction
 316  | Right2Left: rewrite_direction.
 317
 318 definition variance_of_argument_class : Argument_Class → option variance.
 319  intros;
 320  elim a;
 321   [ apply None
 322   | apply (Some ? t)
 323   | apply None
 324   | apply (Some ? t)
 325   | apply None
 326   ]
 327 qed.
 328
 329 definition opposite_direction :=
 330  λdir.
 331    match dir with
 332     [ Left2Right ⇒ Right2Left
 333     | Right2Left ⇒ Left2Right
 334     ].
 335
 336 lemma opposite_direction_idempotent:
 337  ∀dir. opposite_direction (opposite_direction dir) = dir.
 338   intros;
 339   elim dir;
 340   reflexivity.
 341 qed.
 342
 343 inductive check_if_variance_is_respected :
 344  option variance → rewrite_direction → rewrite_direction →  Prop
 345 :=
 346    MSNone : ∀dir,dir'. check_if_variance_is_respected (None ?) dir dir'
 347  | MSCovariant : ∀dir. check_if_variance_is_respected (Some ? Covariant) dir dir
 348  | MSContravariant :
 349      ∀dir.
 350       check_if_variance_is_respected (Some ? Contravariant) dir (opposite_direction dir).
 351
 352 definition relation_class_of_reflexive_relation_class:
 353  Reflexive_Relation_Class → Relation_Class.
 354  intro;
 355  elim r;
 356   [ apply (SymmetricReflexive ? ? ? H H1)
 357   | apply (AsymmetricReflexive ? something ? ? H)
 358   | apply (Leibniz ? T)
 359   ]
 360 qed.
 361
 362 definition relation_class_of_areflexive_relation_class:
 363  Areflexive_Relation_Class → Relation_Class.
 364  intro;
 365  elim a;
 366   [ apply (SymmetricAreflexive ? ? ? H)
 367   | apply (AsymmetricAreflexive ? something ? r)
 368   ]
 369 qed.
 370
 371 definition carrier_of_reflexive_relation_class :=
 372  λR.carrier_of_relation_class ? (relation_class_of_reflexive_relation_class R).
 373
 374 definition carrier_of_areflexive_relation_class :=
 375  λR.carrier_of_relation_class ? (relation_class_of_areflexive_relation_class R).
 376
 377 definition relation_of_areflexive_relation_class :=
 378  λR.relation_of_relation_class ? (relation_class_of_areflexive_relation_class R).
 379
 380 inductive Morphism_Context (Hole: Relation_Class) (dir:rewrite_direction) : Relation_Class → rewrite_direction →  Type :=
 381     App :
 382       ∀In,Out,dir'.
 383         Morphism_Theory In Out → Morphism_Context_List Hole dir dir' In →
 384            Morphism_Context Hole dir Out dir'
 385   | ToReplace : Morphism_Context Hole dir Hole dir
 386   | ToKeep :
 387      ∀S,dir'.
 388       carrier_of_reflexive_relation_class S →
 389         Morphism_Context Hole dir (relation_class_of_reflexive_relation_class S) dir'
 390  | ProperElementToKeep :
 391      ∀S,dir'.∀x: carrier_of_areflexive_relation_class S.
 392       relation_of_areflexive_relation_class S x x →
 393         Morphism_Context Hole dir (relation_class_of_areflexive_relation_class S) dir'
 394 with Morphism_Context_List :
 395    rewrite_direction → Arguments → Type
 396 :=
 397     fcl_singl :
 398       ∀S,dir',dir''.
 399        check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' →
 400         Morphism_Context Hole dir (relation_class_of_argument_class S) dir' →
 401          Morphism_Context_List Hole dir dir'' (singl ? S)
 402  | fcl_cons :
 403       ∀S,L,dir',dir''.
 404        check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' →
 405         Morphism_Context Hole dir (relation_class_of_argument_class S) dir' →
 406          Morphism_Context_List Hole dir dir'' L →
 407           Morphism_Context_List Hole dir dir'' (cons ? S L).
 408
 409 lemma Morphism_Context_rect2:
 410  ∀Hole,dir.
 411  ∀P:
 412   ∀r:Relation_Class.∀r0:rewrite_direction.Morphism_Context Hole dir r r0 → Type.
 413  ∀P0:
 414   ∀r:rewrite_direction.∀a:Arguments.Morphism_Context_List Hole dir r a → Type.
 415  (∀In,Out,dir'.
 416    ∀m:Morphism_Theory In Out.∀m0:Morphism_Context_List Hole dir dir' In.
 417     P0 dir' In m0 → P Out dir' (App Hole ? ? ? ? m m0)) →
 418  P Hole dir (ToReplace Hole dir) →
 419  (∀S:Reflexive_Relation_Class.∀dir'.∀c:carrier_of_reflexive_relation_class S.
 420    P (relation_class_of_reflexive_relation_class S) dir'
 421     (ToKeep Hole dir S dir' c)) →
 422  (∀S:Areflexive_Relation_Class.∀dir'.
 423    ∀x:carrier_of_areflexive_relation_class S.
 424     ∀r:relation_of_areflexive_relation_class S x x.
 425      P (relation_class_of_areflexive_relation_class S) dir'
 426       (ProperElementToKeep Hole dir S dir' x r)) →
 427  (∀S:Argument_Class.∀dir',dir''.
 428    ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
 429     ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
 430      P (relation_class_of_argument_class S) dir' m ->
 431       P0 dir'' (singl ? S) (fcl_singl ? ? S ? ? c m)) →
 432  (∀S:Argument_Class.∀L:Arguments.∀dir',dir''.
 433    ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
 434     ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
 435      P (relation_class_of_argument_class S) dir' m →
 436       ∀m0:Morphism_Context_List Hole dir dir'' L.
 437        P0 dir'' L m0 → P0 dir'' (cons ? S L) (fcl_cons ? ? S ? ? ? c m m0)) →
 438  ∀r:Relation_Class.∀r0:rewrite_direction.∀m:Morphism_Context Hole dir r r0.
 439   P r r0 m
 440 ≝
 441  λHole,dir,P,P0,f,f0,f1,f2,f3,f4.
 442  let rec
 443   F (rc:Relation_Class) (r0:rewrite_direction)
 444    (m:Morphism_Context Hole dir rc r0) on m : P rc r0 m
 445  ≝
 446   match m return λrc.λr0.λm0.P rc r0 m0 with
 447   [ App In Out dir' m0 m1 ⇒ f In Out dir' m0 m1 (F0 dir' In m1)
 448   | ToReplace ⇒ f0
 449   | ToKeep S dir' c ⇒ f1 S dir' c
 450   | ProperElementToKeep S dir' x r1 ⇒ f2 S dir' x r1
 451   ]
 452  and
 453   F0 (r:rewrite_direction) (a:Arguments)
 454    (m:Morphism_Context_List Hole dir r a) on m : P0 r a m
 455  ≝
 456   match m return λr.λa.λm0.P0 r a m0 with
 457   [ fcl_singl S dir' dir'' c m0 ⇒
 458       f3 S dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
 459   | fcl_cons S L dir' dir'' c m0 m1 ⇒
 460       f4 S L dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
 461         m1 (F0 dir'' L m1)
 462   ]
 463 in F.
 464
 465 lemma Morphism_Context_List_rect2:
 466  ∀Hole,dir.
 467  ∀P:
 468   ∀r:Relation_Class.∀r0:rewrite_direction.Morphism_Context Hole dir r r0 → Type.
 469  ∀P0:
 470   ∀r:rewrite_direction.∀a:Arguments.Morphism_Context_List Hole dir r a → Type.
 471  (∀In,Out,dir'.
 472    ∀m:Morphism_Theory In Out.∀m0:Morphism_Context_List Hole dir dir' In.
 473     P0 dir' In m0 → P Out dir' (App Hole ? ? ? ? m m0)) →
 474  P Hole dir (ToReplace Hole dir) →
 475  (∀S:Reflexive_Relation_Class.∀dir'.∀c:carrier_of_reflexive_relation_class S.
 476    P (relation_class_of_reflexive_relation_class S) dir'
 477     (ToKeep Hole dir S dir' c)) →
 478  (∀S:Areflexive_Relation_Class.∀dir'.
 479    ∀x:carrier_of_areflexive_relation_class S.
 480     ∀r:relation_of_areflexive_relation_class S x x.
 481      P (relation_class_of_areflexive_relation_class S) dir'
 482       (ProperElementToKeep Hole dir S dir' x r)) →
 483  (∀S:Argument_Class.∀dir',dir''.
 484    ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
 485     ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
 486      P (relation_class_of_argument_class S) dir' m ->
 487       P0 dir'' (singl ? S) (fcl_singl ? ? S ? ? c m)) →
 488  (∀S:Argument_Class.∀L:Arguments.∀dir',dir''.
 489    ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
 490     ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
 491      P (relation_class_of_argument_class S) dir' m →
 492       ∀m0:Morphism_Context_List Hole dir dir'' L.
 493        P0 dir'' L m0 → P0 dir'' (cons ? S L) (fcl_cons ? ? S ? ? ? c m m0)) →
 494  ∀r:rewrite_direction.∀a:Arguments.∀m:Morphism_Context_List Hole dir r a.
 495   P0 r a m
 496 ≝
 497  λHole,dir,P,P0,f,f0,f1,f2,f3,f4.
 498  let rec
 499   F (rc:Relation_Class) (r0:rewrite_direction)
 500    (m:Morphism_Context Hole dir rc r0) on m : P rc r0 m
 501  ≝
 502   match m return λrc.λr0.λm0.P rc r0 m0 with
 503   [ App In Out dir' m0 m1 ⇒ f In Out dir' m0 m1 (F0 dir' In m1)
 504   | ToReplace ⇒ f0
 505   | ToKeep S dir' c ⇒ f1 S dir' c
 506   | ProperElementToKeep S dir' x r1 ⇒ f2 S dir' x r1
 507   ]
 508  and
 509   F0 (r:rewrite_direction) (a:Arguments)
 510    (m:Morphism_Context_List Hole dir r a) on m : P0 r a m
 511  ≝
 512   match m return λr.λa.λm0.P0 r a m0 with
 513   [ fcl_singl S dir' dir'' c m0 ⇒
 514       f3 S dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
 515   | fcl_cons S L dir' dir'' c m0 m1 ⇒
 516       f4 S L dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
 517         m1 (F0 dir'' L m1)
 518   ]
 519 in F0.
 520
 521 definition product_of_arguments : Arguments → Type.
 522  intro;
 523  elim a;
 524   [ apply (carrier_of_relation_class ? t)
 525   | apply (Prod (carrier_of_relation_class ? t) T)
 526   ]
 527 qed.
 528
 529 definition get_rewrite_direction: rewrite_direction → Argument_Class → rewrite_direction.
 530  intros (dir R);
 531  cases (variance_of_argument_class R) (a);
 532   [ exact dir
 533   | cases a;
 534      [ exact dir                      (* covariant *)
 535      | exact (opposite_direction dir) (* contravariant *)
 536      ]
 537   ]
 538 qed.
 539
 540 definition directed_relation_of_relation_class:
 541  ∀dir:rewrite_direction.∀R: Relation_Class.
 542    carrier_of_relation_class ? R → carrier_of_relation_class ? R → Prop.
 543  intros;
 544  cases r;
 545   [ exact (relation_of_relation_class ? ? c c1)
 546   | apply (relation_of_relation_class ? ? c1 c)
 547   ]
 548 qed.
 549
 550 definition directed_relation_of_argument_class:
 551  ∀dir:rewrite_direction.∀R: Argument_Class.
 552    carrier_of_relation_class ? R → carrier_of_relation_class ? R → Prop.
 553   intros (dir R c c1);
 554   rewrite < (about_carrier_of_relation_class_and_relation_class_of_argument_class R) in c c1;
 555   exact (directed_relation_of_relation_class dir (relation_class_of_argument_class R)  c c1).
 556 qed.
 557
 558
 559 definition relation_of_product_of_arguments:
 560  ∀dir:rewrite_direction.∀In.
 561   product_of_arguments In → product_of_arguments In → Prop.
 562  intros 2;
 563  elim In 0;
 564   [ simplify;
 565     intro;
 566     exact (directed_relation_of_argument_class (get_rewrite_direction r t) t)
 567   | intros;
 568     change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
 569     change in p1 with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
 570     cases p (c p2);
 571     cases p1 (c1 p3);
 572    apply And;
 573     [ exact
 574       (directed_relation_of_argument_class (get_rewrite_direction r t) t c c1)
 575     | exact (R p2 p3)
 576     ]
 577   ]
 578 qed.
 579
 580 definition apply_morphism:
 581  ∀In,Out.∀m: function_type_of_morphism_signature In Out.
 582   ∀args: product_of_arguments In. carrier_of_relation_class ? Out.
 583  intro;
 584  elim In;
 585   [ exact (f p)
 586   | change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
 587    elim p;
 588    change in f1 with (carrier_of_relation_class variance t → function_type_of_morphism_signature n Out);
 589    exact (f ? (f1 t1) t2)
 590   ]
 591 qed.
 592
 593 theorem apply_morphism_compatibility_Right2Left:
 594  ∀In,Out.∀m1,m2: function_type_of_morphism_signature In Out.
 595   ∀args1,args2: product_of_arguments In.
 596      make_compatibility_goal_aux ? ? m1 m2 →
 597       relation_of_product_of_arguments Right2Left ? args1 args2 →
 598         directed_relation_of_relation_class Right2Left ?
 599          (apply_morphism ? ? m2 args1)
 600          (apply_morphism ? ? m1 args2).
 601   intro;
 602   elim In;
 603    [ simplify in m1 m2 args1 args2 ⊢ %;
 604      change in H1 with
 605       (directed_relation_of_argument_class
 606         (get_rewrite_direction Right2Left t) t args1 args2);
 607      generalize in match H1; clear H1;
 608      generalize in match H; clear H;
 609      generalize in match args2; clear args2;
 610      generalize in match args1; clear args1;
 611      generalize in match m2; clear m2;
 612      generalize in match m1; clear m1;
 613      elim t 0; simplify;
 614       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
 615         apply H;
 616         exact H1
 617       | intros 8 (v T1 r Hr m1 m2 args1 args2);
 618         cases v;
 619         simplify;
 620         intros (H H1);
 621         apply (H ? ? H1);
 622       | intros;
 623         apply H1;
 624         exact H2
 625       | intros 7 (v);
 626         cases v; simplify;
 627         intros (H H1);
 628         apply H;
 629         exact H1
 630       | intros;
 631         simplify in H1;
 632         rewrite > H1;
 633         apply H;
 634         exact H1
 635       ]
 636    | change in m1 with
 637       (carrier_of_relation_class variance t →
 638         function_type_of_morphism_signature n Out);
 639      change in m2 with
 640       (carrier_of_relation_class variance t →
 641         function_type_of_morphism_signature n Out);
 642      change in args1 with
 643       ((carrier_of_relation_class ? t) × (product_of_arguments n));
 644      change in args2 with
 645       ((carrier_of_relation_class ? t) × (product_of_arguments n));
 646      generalize in match H2; clear H2;
 647      elim args2 0; clear args2;
 648      elim args1; clear args1;
 649      elim H2; clear H2;
 650      change in H4 with
 651       (relation_of_product_of_arguments Right2Left n t2 t4);
 652      change with
 653       (relation_of_relation_class unit Out (apply_morphism n Out (m1 t3) t4)
 654         (apply_morphism n Out (m2 t1) t2));
 655      generalize in match H3; clear H3;
 656      generalize in match t3; clear t3;
 657      generalize in match t1; clear t1;
 658      generalize in match H1; clear H1;
 659      generalize in match m2; clear m2;
 660      generalize in match m1; clear m1;
 661      elim t 0;
 662       [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
 663         simplify in H3;
 664         change in H1 with
 665          (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 666      | intro v;
 667        elim v 0;
 668        [ intros (T1 r Hr m1 m2 H1 t1 t3 H3);
 669          simplify in H3;
 670          change in H1 with
 671           (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 672        | intros (T1 r Hr m1 m2 H1 t1 t3 H3);
 673          simplify in H3;
 674          change in H1 with
 675           (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 676        ]
 677      | intros (T1 r Hs m1 m2 H1 t1 t3 H3);
 678        simplify in H3;
 679        change in H1 with
 680         (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 681      | intro v;
 682        elim v 0;
 683         [ intros (T1 r m1 m2 H1 t1 t3 H3);
 684           simplify in H3;
 685           change in H1 with
 686            (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 687         | intros (T1 r m1 m2 H1 t1 t3 H3);
 688           simplify in H3;
 689           change in H1 with
 690            (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 691         ]
 692      | intros (T m1 m2 H1 t1 t3 H3);
 693        simplify in H3;
 694        change in H1 with
 695         (∀x:T. make_compatibility_goal_aux n Out (m1 x) (m2 x));
 696        rewrite > H3;
 697        simplify in H;
 698        apply H;
 699         [ apply H1
 700         | assumption
 701         ]
 702      ] ;
 703      simplify in H;
 704      apply H;
 705       [1,3,5,7,9,11:
 706         apply H1;
 707         assumption
 708       |2,4,6,8,10,12:
 709         assumption
 710       ]
 711    ]
 712 qed.
 713
 714 theorem apply_morphism_compatibility_Left2Right:
 715  ∀In,Out.∀m1,m2: function_type_of_morphism_signature In Out.
 716   ∀args1,args2: product_of_arguments In.
 717      make_compatibility_goal_aux ? ? m1 m2 →
 718       relation_of_product_of_arguments Left2Right ? args1 args2 →
 719         directed_relation_of_relation_class Left2Right ?
 720          (apply_morphism ? ? m1 args1)
 721          (apply_morphism ? ? m2 args2).
 722   intro;
 723   elim In 0; simplify; intros;
 724    [ change in H1 with
 725       (directed_relation_of_argument_class
 726         (get_rewrite_direction Left2Right t) t args1 args2);
 727      generalize in match H1; clear H1;
 728      generalize in match H; clear H;
 729      generalize in match args2; clear args2;
 730      generalize in match args1; clear args1;
 731      generalize in match m2; clear m2;
 732      generalize in match m1; clear m1;
 733      elim t 0; simplify;
 734       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
 735         apply H;
 736         exact H1
 737       | intros 8 (v T1 r Hr m1 m2 args1 args2);
 738         cases v;
 739         intros (H H1);
 740         simplify in H1;
 741         apply H;
 742         exact H1
 743       | intros;
 744         apply H1;
 745         exact H2
 746       | intros 7 (v);
 747         cases v;
 748         intros (H H1);
 749         simplify in H1;
 750         apply H;
 751         exact H1
 752       | intros;
 753         simplify in H1;
 754         rewrite > H1;
 755         apply H;
 756         exact H1
 757       ]
 758    | change in m1 with
 759       (carrier_of_relation_class variance t →
 760         function_type_of_morphism_signature n Out);
 761      change in m2 with
 762       (carrier_of_relation_class variance t →
 763         function_type_of_morphism_signature n Out);
 764      change in args1 with
 765       ((carrier_of_relation_class ? t) × (product_of_arguments n));
 766      change in args2 with
 767       ((carrier_of_relation_class ? t) × (product_of_arguments n));
 768      generalize in match H2; clear H2;
 769      elim args2 0; clear args2;
 770      elim args1; clear args1;
 771      elim H2; clear H2;
 772      change in H4 with
 773       (relation_of_product_of_arguments Left2Right n t2 t4);
 774      change with
 775       (relation_of_relation_class unit Out (apply_morphism n Out (m1 t1) t2)
 776         (apply_morphism n Out (m2 t3) t4));
 777      generalize in match H3; clear H3;
 778      generalize in match t3; clear t3;
 779      generalize in match t1; clear t1;
 780      generalize in match H1; clear H1;
 781      generalize in match m2; clear m2;
 782      generalize in match m1; clear m1;
 783      elim t 0;
 784       [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
 785         change in H1 with
 786          (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 787      | intro v;
 788        elim v 0;
 789        [ intros (T1 r Hr m1 m2 H1 t1 t3 H3);
 790          simplify in H3;
 791          change in H1 with
 792           (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 793        | intros (T1 r Hr m1 m2 H1 t1 t3 H3);
 794          simplify in H3;
 795          change in H1 with
 796           (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 797        ]
 798      | intros (T1 r Hs m1 m2 H1 t1 t3 H3);
 799        simplify in H3;
 800        change in H1 with
 801         (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 802      | intro v;
 803        elim v 0;
 804         [ intros (T1 r m1 m2 H1 t1 t3 H3);
 805           simplify in H3;
 806           change in H1 with
 807            (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 808         | intros (T1 r m1 m2 H1 t1 t3 H3);
 809           simplify in H3;
 810           change in H1 with
 811            (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 812         ]
 813      | intros (T m1 m2 H1 t1 t3 H3);
 814        simplify in H3;
 815        change in H1 with
 816         (∀x:T. make_compatibility_goal_aux n Out (m1 x) (m2 x));
 817        rewrite > H3;
 818        simplify in H;
 819        apply H;
 820         [ apply H1
 821         | assumption
 822         ]
 823      ] ;
 824      simplify in H;
 825      apply H;
 826       [1,3,5,7,9,11:
 827         apply H1;
 828         assumption
 829       |2,4,6,8,10,12:
 830         assumption
 831       ]
 832    ]
 833 qed.
 834
 835 definition interp :
 836  ∀Hole,dir,Out,dir'. carrier_of_relation_class ? Hole →
 837   Morphism_Context Hole dir Out dir' → carrier_of_relation_class ? Out.
 838  intros (Hole dir Out dir' H t).
 839  apply
 840   (Morphism_Context_rect2 Hole dir (λS,xx,yy. carrier_of_relation_class ? S)
 841     (λxx,L,fcl.product_of_arguments L));
 842   intros;
 843    [8: apply t
 844    |7: skip
 845    | exact (apply_morphism ? ? (Function ? ? m) p)
 846    | exact H
 847    | exact c
 848    | exact x
 849    | simplify;
 850      rewrite <
 851        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 852      exact c1
 853    | split;
 854       [ rewrite <
 855          (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 856         exact c1
 857       | exact p
 858       ]
 859    ]
 860 qed.
 861
 862
 863 (*CSC: interp and interp_relation_class_list should be mutually defined. since
 864    the proof term of each one contains the proof term of the other one. However
 865    I cannot do that interactively (I should write the Fix by hand) *)
 866 definition interp_relation_class_list :
 867  ∀Hole,dir,dir'.∀L: Arguments. carrier_of_relation_class ? Hole →
 868   Morphism_Context_List Hole dir dir' L → product_of_arguments L.
 869  intros (Hole dir dir' L H t);
 870  apply
 871   (Morphism_Context_List_rect2 Hole dir (λS,xx,yy.carrier_of_relation_class ? S)
 872     (λxx,L,fcl.product_of_arguments L));
 873  intros;
 874   [8: apply t
 875   |7: skip
 876   | exact (apply_morphism ? ? (Function ? ? m) p)
 877   | exact H
 878   | exact c
 879   | exact x
 880   | simplify;
 881      rewrite <
 882        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 883      exact c1
 884   | split;
 885      [ rewrite <
 886         (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
 887        exact c1
 888      | exact p
 889      ]
 890   ]
 891 qed.
 892
 893 (*
 894 Theorem setoid_rewrite:
 895  ∀Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole)
 896   (E: Morphism_Context Hole dir Out dir').
 897    (directed_relation_of_relation_class dir Hole E1 E2) →
 898     (directed_relation_of_relation_class dir' Out (interp E1 E) (interp E2 E)).
 899  intros.
 900  elim E using
 901    (@Morphism_Context_rect2 Hole dir
 902      (fun S dir'' E => directed_relation_of_relation_class dir'' S (interp E1 E) (interp E2 E))
 903      (fun dir'' L fcl =>
 904         relation_of_product_of_arguments dir'' ?
 905          (interp_relation_class_list E1 fcl)
 906          (interp_relation_class_list E2 fcl))); intros.
 907    change (directed_relation_of_relation_class dir'0 Out0
 908     (apply_morphism ? ? (Function m) (interp_relation_class_list E1 m0))
 909     (apply_morphism ? ? (Function m) (interp_relation_class_list E2 m0))).
 910    destruct dir'0.
 911      apply apply_morphism_compatibility_Left2Right.
 912        exact (Compat m).
 913        exact H0.
 914      apply apply_morphism_compatibility_Right2Left.
 915        exact (Compat m).
 916        exact H0.
 917
 918    exact H.
 919
 920    unfold interp. Morphism_Context_rect2.
 921    (*CSC: reflexivity used here*)
 922    destruct S; destruct dir'0; simpl; (apply r || reflexivity).
 923
 924    destruct dir'0; exact r.
 925
 926   destruct S; unfold directed_relation_of_argument_class; simpl in H0 |- *;
 927    unfold get_rewrite_direction; simpl.
 928      destruct dir'0; destruct dir'';
 929        (exact H0 ||
 930         unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
 931      (* the following mess with generalize/clear/intros is to help Coq resolving *)
 932      (* second order unification problems.                                                                *)
 933      generalize m c H0; clear H0 m c; inversion c;
 934        generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
 935          (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
 936      destruct dir'0; destruct dir'';
 937        (exact H0 ||
 938         unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
 939 (* the following mess with generalize/clear/intros is to help Coq resolving *)
 940      (* second order unification problems.                                                                *)
 941      generalize m c H0; clear H0 m c; inversion c;
 942        generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
 943          (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
 944      destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0).
 945
 946   change
 947     (directed_relation_of_argument_class (get_rewrite_direction dir'' S) S
 948        (eq_rect ? (fun T : Type => T) (interp E1 m) ?
 949          (about_carrier_of_relation_class_and_relation_class_of_argument_class S))
 950        (eq_rect ? (fun T : Type => T) (interp E2 m) ?
 951          (about_carrier_of_relation_class_and_relation_class_of_argument_class S)) /\
 952      relation_of_product_of_arguments dir'' ?
 953        (interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)).
 954    split.
 955      clear m0 H1; destruct S; simpl in H0 |- *; unfold get_rewrite_direction; simpl.
 956         destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
 957         inversion c.
 958           rewrite <- H3; exact H0.
 959           rewrite (opposite_direction_idempotent dir'0); exact H0.
 960         destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
 961         inversion c.
 962           rewrite <- H3; exact H0.
 963           rewrite (opposite_direction_idempotent dir'0); exact H0.
 964         destruct dir''; destruct dir'0; (exact H0 || hnf; symmetry; exact H0).
 965      exact H1.
 966 Qed.
 967
 968 (* A FEW EXAMPLES ON iff *)
 969
 970 (* impl IS A MORPHISM *)
 971
 972 Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
 973 unfold impl; tautobatch.
 974 Qed.
 975
 976 (* and IS A MORPHISM *)
 977
 978 Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
 979  tautobatch.
 980 Qed.
 981
 982 (* or IS A MORPHISM *)
 983
 984 Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
 985  tautobatch.
 986 Qed.
 987
 988 (* not IS A MORPHISM *)
 989
 990 Add Morphism not with signature iff ==> iff as Not_Morphism.
 991  tautobatch.
 992 Qed.
 993
 994 (* THE SAME EXAMPLES ON impl *)
 995
 996 Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
 997  unfold impl; tautobatch.
 998 Qed.
 999
1000 Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
1001  unfold impl; tautobatch.
1002 Qed.
1003
1004 Add Morphism not with signature impl -→ impl as Not_Morphism2.
1005  unfold impl; tautobatch.
1006 Qed.
1007
1008 *)