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