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