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