matita/library/technicalities/setoids.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti. C.Sacerdoti Coen.                          *)
   8 (*      ||A||       E.Tassi. S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* Code ported from the Coq theorem prover by Claudio Sacerdoti Coen *)
  16 (* Original author: Claudio Sacerdoti Coen. for the Coq system       *)
  17
  18 set "baseuri" "cic:/matita/technicalities/setoids".
  19
  20 include "datatypes/constructors.ma".
  21 include "logic/connectives2.ma".
  22
  23 (* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *)
  24
  25 (* X will be used to distinguish covariant arguments whose type is an   *)
  26 (* Asymmetric* relation from contravariant arguments of the same type *)
  27 inductive X_Relation_Class (X: Type) : Type ≝
  28    SymmetricReflexive :
  29      ∀A,Aeq. symmetric A Aeq → reflexive ? Aeq → X_Relation_Class X
  30  | AsymmetricReflexive : X → ∀A,Aeq. reflexive A Aeq → X_Relation_Class X
  31  | SymmetricAreflexive : ∀A,Aeq. symmetric A Aeq → X_Relation_Class X
  32  | AsymmetricAreflexive : X → ∀A.∀Aeq : relation A. X_Relation_Class X
  33  | Leibniz : Type → X_Relation_Class X.
  34
  35 inductive variance : Set ≝
  36    Covariant : variance
  37  | Contravariant : variance.
  38
  39 definition Argument_Class ≝ X_Relation_Class variance.
  40 definition Relation_Class ≝ X_Relation_Class unit.
  41
  42 inductive Reflexive_Relation_Class : Type :=
  43    RSymmetric :
  44      ∀A,Aeq. symmetric A Aeq → reflexive ? Aeq → Reflexive_Relation_Class
  45  | RAsymmetric :
  46      ∀A,Aeq. reflexive A Aeq → Reflexive_Relation_Class
  47  | RLeibniz : Type → Reflexive_Relation_Class.
  48
  49 inductive Areflexive_Relation_Class  : Type :=
  50  | ASymmetric : ∀A,Aeq. symmetric A Aeq → Areflexive_Relation_Class
  51  | AAsymmetric : ∀A.∀Aeq : relation A. Areflexive_Relation_Class.
  52
  53 definition relation_class_of_argument_class : Argument_Class → Relation_Class.
  54  intro;
  55  unfold in a ⊢ %;
  56  elim a;
  57   [ apply (SymmetricReflexive ? ? ? H H1)
  58   | apply (AsymmetricReflexive ? something ? ? H)
  59   | apply (SymmetricAreflexive ? ? ? H)
  60   | apply (AsymmetricAreflexive ? something ? r)
  61   | apply (Leibniz ? T1)
  62   ]
  63 qed.
  64
  65 definition carrier_of_relation_class : ∀X. X_Relation_Class X → Type.
  66  intros;
  67  elim x;
  68  [1,2,3,4,5: exact T1]
  69 qed.
  70
  71 definition relation_of_relation_class:
  72  ∀X,R. carrier_of_relation_class X R → carrier_of_relation_class X R → Prop.
  73  intros 2;
  74  elim R 0;
  75  simplify;
  76   [1,2: intros 4; apply r
  77   |3,4: intros 3; apply r
  78   | intros 1 (T1); apply (eq T1).
  79     (* this eta expansion is needed to avoid a universe inconsistency *)
  80  ]
  81 qed.
  82
  83 definition relation_of_relation_classCOQ:
  84  ∀X,R. carrier_of_relation_class X R → carrier_of_relation_class X R → Prop.
  85  intros 2;
  86  exact (
  87  match
  88   R
  89   return
  90     (λ x.carrier_of_relation_class X x -> carrier_of_relation_class X x -> Prop)
  91 with [
  92  SymmetricReflexive A Aeq _ _ => Aeq
  93 | AsymmetricReflexive _ A Aeq _ => Aeq
  94 | SymmetricAreflexive A Aeq _ => Aeq
  95 | AsymmetricAreflexive _ A Aeq => Aeq
  96 | Leibniz T => eq T]).
  97 qed.
  98
  99 lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
 100  ∀R.
 101   carrier_of_relation_class ? (relation_class_of_argument_class R) =
 102    carrier_of_relation_class ? R.
 103  intro;
 104  elim R;
 105  reflexivity.
 106  qed.
 107
 108 inductive nelistT (A : Type) : Type :=
 109    singl : A → nelistT A
 110  | cons : A → nelistT A → nelistT A.
 111
 112 definition Arguments := nelistT Argument_Class.
 113
 114 definition function_type_of_morphism_signature :
 115  Arguments → Relation_Class → Type.
 116   intros (In Out);
 117   elim In
 118    [ exact (carrier_of_relation_class ? t → carrier_of_relation_class ? Out)
 119    | exact (carrier_of_relation_class ? t → T)
 120    ]
 121 qed.
 122
 123 definition make_compatibility_goal_aux:
 124  ∀In,Out.∀f,g:function_type_of_morphism_signature In Out.Prop.
 125  intros 2;
 126  elim In (a); simplify in f f1;
 127  generalize in match f1; clear f1;
 128  generalize in match f; clear f;
 129   [ elim a; simplify in f f1;
 130      [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
 131      | elim t;
 132         [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
 133         | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2))
 134         ]
 135      | exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
 136      | elim t;
 137         [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
 138         | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2))
 139         ]
 140      | exact (∀x. relation_of_relation_class ? Out (f x) (f1 x))
 141      ]
 142   | change with
 143      ((carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) →
 144       (carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) →
 145       Prop).
 146     elim t; simplify in f f1;
 147      [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
 148      | elim t1;
 149         [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
 150         | exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))
 151         ]
 152      | exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
 153      | elim t1;
 154         [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
 155         | exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))
 156         ]
 157      | exact (∀x. R (f x) (f1 x))
 158      ]
 159   ]
 160 qed.
 161
 162 definition make_compatibility_goal :=
 163  λIn,Out,f. make_compatibility_goal_aux In Out f f.
 164
 165 record Morphism_Theory (In: Arguments) (Out: Relation_Class) : Type :=
 166  { Function : function_type_of_morphism_signature In Out;
 167    Compat : make_compatibility_goal In Out Function
 168  }.
 169
 170 definition list_of_Leibniz_of_list_of_types: nelistT Type → Arguments.
 171  intro;
 172  elim n;
 173   [ apply (singl ? (Leibniz ? t))
 174   | apply (cons ? (Leibniz ? t) a)
 175   ]
 176 qed.
 177
 178 (* every function is a morphism from Leibniz+ to Leibniz *)
 179 definition morphism_theory_of_function :
 180  ∀In: nelistT Type.∀Out: Type.
 181   let In' := list_of_Leibniz_of_list_of_types In in
 182   let Out' := Leibniz ? Out in
 183    function_type_of_morphism_signature In' Out' →
 184     Morphism_Theory In' Out'.
 185   intros;
 186   apply (mk_Morphism_Theory ? ? f);
 187   unfold In' in f; clear In';
 188   unfold Out' in f; clear Out';
 189   generalize in match f; clear f;
 190   elim In;
 191    [ unfold make_compatibility_goal;
 192      simplify;
 193      intros;
 194      whd;
 195      reflexivity
 196    | simplify;
 197      intro;
 198      unfold In' in f;
 199      unfold Out' in f;
 200      exact (H (f1 x))
 201    ]
 202 qed.
 203
 204 (* THE iff RELATION CLASS *)
 205
 206 definition Iff_Relation_Class : Relation_Class.
 207  apply (SymmetricReflexive unit ? iff);
 208   [ exact symmetric_iff
 209   | exact reflexive_iff
 210   ]
 211 qed.
 212
 213 (* THE impl RELATION CLASS *)
 214
 215 definition impl \def \lambda A,B:Prop. A → B.
 216
 217 theorem impl_refl: reflexive ? impl.
 218  unfold reflexive;
 219  intros;
 220  unfold impl;
 221  intro;
 222  assumption.
 223 qed.
 224
 225 definition Impl_Relation_Class : Relation_Class.
 226  unfold Relation_Class;
 227  apply (AsymmetricReflexive unit something ? impl);
 228  exact impl_refl.
 229 qed.
 230
 231 (* UTILITY FUNCTIONS TO PROVE THAT EVERY TRANSITIVE RELATION IS A MORPHISM *)
 232
 233 definition equality_morphism_of_symmetric_areflexive_transitive_relation:
 234  ∀A: Type.∀Aeq: relation A.∀sym: symmetric ? Aeq.∀trans: transitive ? Aeq.
 235   let ASetoidClass := SymmetricAreflexive ? ? ? sym in
 236    (Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass))
 237      Iff_Relation_Class).
 238  intros;
 239  apply mk_Morphism_Theory;
 240   [ exact Aeq
 241   | unfold make_compatibility_goal;
 242     simplify;
 243     intros;
 244     split;
 245     unfold transitive in H;
 246     unfold symmetric in sym;
 247     intro;
 248     auto new
 249   ].
 250 qed.
 251
 252 definition equality_morphism_of_symmetric_reflexive_transitive_relation:
 253  ∀A: Type.∀Aeq: relation A.∀refl: reflexive ? Aeq.∀sym: symmetric ? Aeq.
 254   ∀trans: transitive ? Aeq.
 255    let ASetoidClass := SymmetricReflexive ? ? ? sym refl in
 256     (Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass)) Iff_Relation_Class).
 257  intros;
 258  apply mk_Morphism_Theory;
 259  reduce;
 260   [ exact Aeq
 261   | intros;
 262     split;
 263     intro;
 264     unfold transitive in H;
 265     unfold symmetric in sym;
 266     auto depth=4.
 267   ]
 268 qed.
 269
 270 definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
 271  ∀A: Type.∀Aeq: relation A.∀trans: transitive ? Aeq.
 272   let ASetoidClass1 := AsymmetricAreflexive ? Contravariant ? Aeq in
 273   let ASetoidClass2 := AsymmetricAreflexive ? Covariant ? Aeq in
 274    (Morphism_Theory (cons ? ASetoidClass1 (singl ? ASetoidClass2)) Impl_Relation_Class).
 275  intros;
 276  apply mk_Morphism_Theory;
 277  [ simplify;
 278    apply Aeq
 279  | simplify;
 280    intros;
 281    whd;
 282    intros;
 283    auto
 284  ].
 285 qed.
 286
 287 definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
 288  ∀A: Type.∀Aeq: relation A.∀refl: reflexive ? Aeq.∀trans: transitive ? Aeq.
 289   let ASetoidClass1 := AsymmetricReflexive ? Contravariant ? ? refl in
 290   let ASetoidClass2 := AsymmetricReflexive ? Covariant ? ? refl in
 291    (Morphism_Theory (cons ? ASetoidClass1 (singl ? ASetoidClass2)) Impl_Relation_Class).
 292  intros;
 293  apply mk_Morphism_Theory;
 294  [ simplify;
 295    apply Aeq
 296  | simplify;
 297    intros;
 298    whd;
 299    intro;
 300    auto
 301  ].
 302 qed.
 303
 304 (* iff AS A RELATION *)
 305
 306 (*DA PORTARE:Add Relation Prop iff
 307  reflexivity proved by iff_refl
 308  symmetry proved by iff_sym
 309  transitivity proved by iff_trans
 310  as iff_relation.*)
 311
 312 (* every predicate is  morphism from Leibniz+ to Iff_Relation_Class *)
 313 definition morphism_theory_of_predicate :
 314  ∀(In: nelistT Type).
 315   let In' := list_of_Leibniz_of_list_of_types In in
 316    function_type_of_morphism_signature In' Iff_Relation_Class →
 317     Morphism_Theory In' Iff_Relation_Class.
 318   intros;
 319   apply mk_Morphism_Theory;
 320   [ apply f
 321   | generalize in match f; clear f;
 322     unfold In'; clear In';
 323     elim In;
 324      [ reduce;
 325        intro;
 326        alias id "iff_refl" = "cic:/matita/logic/coimplication/iff_refl.con".
 327        apply iff_refl
 328      | simplify;
 329        intro x;
 330        apply (H (f1 x))
 331      ]
 332   ].
 333 qed.
 334
 335 (* impl AS A RELATION *)
 336
 337 theorem impl_trans: transitive ? impl.
 338  whd;
 339  unfold impl;
 340  intros;
 341  auto.
 342 qed.
 343
 344 (*DA PORTARE: Add Relation Prop impl
 345  reflexivity proved by impl_refl
 346  transitivity proved by impl_trans
 347  as impl_relation.*)
 348
 349 (* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *)
 350
 351 inductive rewrite_direction : Type :=
 352    Left2Right: rewrite_direction
 353  | Right2Left: rewrite_direction.
 354
 355 definition variance_of_argument_class : Argument_Class → option variance.
 356  intros;
 357  elim a;
 358   [ apply None
 359   | apply (Some ? t)
 360   | apply None
 361   | apply (Some ? t)
 362   | apply None
 363   ]
 364 qed.
 365
 366 definition opposite_direction :=
 367  λdir.
 368    match dir with
 369     [ Left2Right ⇒ Right2Left
 370     | Right2Left ⇒ Left2Right
 371     ].
 372
 373 lemma opposite_direction_idempotent:
 374  ∀dir. opposite_direction (opposite_direction dir) = dir.
 375   intros;
 376   elim dir;
 377   reflexivity.
 378 qed.
 379
 380 inductive check_if_variance_is_respected :
 381  option variance → rewrite_direction → rewrite_direction →  Prop
 382 :=
 383    MSNone : ∀dir,dir'. check_if_variance_is_respected (None ?) dir dir'
 384  | MSCovariant : ∀dir. check_if_variance_is_respected (Some ? Covariant) dir dir
 385  | MSContravariant :
 386      ∀dir.
 387       check_if_variance_is_respected (Some ? Contravariant) dir (opposite_direction dir).
 388
 389 definition relation_class_of_reflexive_relation_class:
 390  Reflexive_Relation_Class → Relation_Class.
 391  intro;
 392  elim r;
 393   [ apply (SymmetricReflexive ? ? ? H H1)
 394   | apply (AsymmetricReflexive ? something ? ? H)
 395   | apply (Leibniz ? T)
 396   ]
 397 qed.
 398
 399 definition relation_class_of_areflexive_relation_class:
 400  Areflexive_Relation_Class → Relation_Class.
 401  intro;
 402  elim a;
 403   [ apply (SymmetricAreflexive ? ? ? H)
 404   | apply (AsymmetricAreflexive ? something ? r)
 405   ]
 406 qed.
 407
 408 definition carrier_of_reflexive_relation_class :=
 409  λR.carrier_of_relation_class ? (relation_class_of_reflexive_relation_class R).
 410
 411 definition carrier_of_areflexive_relation_class :=
 412  λR.carrier_of_relation_class ? (relation_class_of_areflexive_relation_class R).
 413
 414 definition relation_of_areflexive_relation_class :=
 415  λR.relation_of_relation_class ? (relation_class_of_areflexive_relation_class R).
 416
 417 inductive Morphism_Context (Hole: Relation_Class) (dir:rewrite_direction) : Relation_Class → rewrite_direction →  Type :=
 418     App :
 419       ∀In,Out,dir'.
 420         Morphism_Theory In Out → Morphism_Context_List Hole dir dir' In →
 421            Morphism_Context Hole dir Out dir'
 422   | ToReplace : Morphism_Context Hole dir Hole dir
 423   | ToKeep :
 424      ∀S,dir'.
 425       carrier_of_reflexive_relation_class S →
 426         Morphism_Context Hole dir (relation_class_of_reflexive_relation_class S) dir'
 427  | ProperElementToKeep :
 428      ∀S,dir'.∀x: carrier_of_areflexive_relation_class S.
 429       relation_of_areflexive_relation_class S x x →
 430         Morphism_Context Hole dir (relation_class_of_areflexive_relation_class S) dir'
 431 with Morphism_Context_List :
 432    rewrite_direction → Arguments → Type
 433 :=
 434     fcl_singl :
 435       ∀S,dir',dir''.
 436        check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' →
 437         Morphism_Context Hole dir (relation_class_of_argument_class S) dir' →
 438          Morphism_Context_List Hole dir dir'' (singl ? S)
 439  | fcl_cons :
 440       ∀S,L,dir',dir''.
 441        check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' →
 442         Morphism_Context Hole dir (relation_class_of_argument_class S) dir' →
 443          Morphism_Context_List Hole dir dir'' L →
 444           Morphism_Context_List Hole dir dir'' (cons ? S L).
 445
 446 lemma Morphism_Context_rect2:
 447  ∀Hole,dir.
 448  ∀P:
 449   ∀r:Relation_Class.∀r0:rewrite_direction.Morphism_Context Hole dir r r0 → Type.
 450  ∀P0:
 451   ∀r:rewrite_direction.∀a:Arguments.Morphism_Context_List Hole dir r a → Type.
 452  (∀In,Out,dir'.
 453    ∀m:Morphism_Theory In Out.∀m0:Morphism_Context_List Hole dir dir' In.
 454     P0 dir' In m0 → P Out dir' (App Hole ? ? ? ? m m0)) →
 455  P Hole dir (ToReplace Hole dir) →
 456  (∀S:Reflexive_Relation_Class.∀dir'.∀c:carrier_of_reflexive_relation_class S.
 457    P (relation_class_of_reflexive_relation_class S) dir'
 458     (ToKeep Hole dir S dir' c)) →
 459  (∀S:Areflexive_Relation_Class.∀dir'.
 460    ∀x:carrier_of_areflexive_relation_class S.
 461     ∀r:relation_of_areflexive_relation_class S x x.
 462      P (relation_class_of_areflexive_relation_class S) dir'
 463       (ProperElementToKeep Hole dir S dir' x r)) →
 464  (∀S:Argument_Class.∀dir',dir''.
 465    ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
 466     ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
 467      P (relation_class_of_argument_class S) dir' m ->
 468       P0 dir'' (singl ? S) (fcl_singl ? ? S ? ? c m)) →
 469  (∀S:Argument_Class.∀L:Arguments.∀dir',dir''.
 470    ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
 471     ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
 472      P (relation_class_of_argument_class S) dir' m →
 473       ∀m0:Morphism_Context_List Hole dir dir'' L.
 474        P0 dir'' L m0 → P0 dir'' (cons ? S L) (fcl_cons ? ? S ? ? ? c m m0)) →
 475  ∀r:Relation_Class.∀r0:rewrite_direction.∀m:Morphism_Context Hole dir r r0.
 476   P r r0 m
 477 ≝
 478  λHole,dir,P,P0,f,f0,f1,f2,f3,f4.
 479  let rec
 480   F (rc:Relation_Class) (r0:rewrite_direction)
 481    (m:Morphism_Context Hole dir rc r0) on m : P rc r0 m
 482  ≝
 483   match m return λrc.λr0.λm0.P rc r0 m0 with
 484   [ App In Out dir' m0 m1 ⇒ f In Out dir' m0 m1 (F0 dir' In m1)
 485   | ToReplace ⇒ f0
 486   | ToKeep S dir' c ⇒ f1 S dir' c
 487   | ProperElementToKeep S dir' x r1 ⇒ f2 S dir' x r1
 488   ]
 489  and
 490   F0 (r:rewrite_direction) (a:Arguments)
 491    (m:Morphism_Context_List Hole dir r a) on m : P0 r a m
 492  ≝
 493   match m return λr.λa.λm0.P0 r a m0 with
 494   [ fcl_singl S dir' dir'' c m0 ⇒
 495       f3 S dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
 496   | fcl_cons S L dir' dir'' c m0 m1 ⇒
 497       f4 S L dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
 498         m1 (F0 dir'' L m1)
 499   ]
 500 in F.
 501
 502 lemma Morphism_Context_List_rect2:
 503  ∀Hole,dir.
 504  ∀P:
 505   ∀r:Relation_Class.∀r0:rewrite_direction.Morphism_Context Hole dir r r0 → Type.
 506  ∀P0:
 507   ∀r:rewrite_direction.∀a:Arguments.Morphism_Context_List Hole dir r a → Type.
 508  (∀In,Out,dir'.
 509    ∀m:Morphism_Theory In Out.∀m0:Morphism_Context_List Hole dir dir' In.
 510     P0 dir' In m0 → P Out dir' (App Hole ? ? ? ? m m0)) →
 511  P Hole dir (ToReplace Hole dir) →
 512  (∀S:Reflexive_Relation_Class.∀dir'.∀c:carrier_of_reflexive_relation_class S.
 513    P (relation_class_of_reflexive_relation_class S) dir'
 514     (ToKeep Hole dir S dir' c)) →
 515  (∀S:Areflexive_Relation_Class.∀dir'.
 516    ∀x:carrier_of_areflexive_relation_class S.
 517     ∀r:relation_of_areflexive_relation_class S x x.
 518      P (relation_class_of_areflexive_relation_class S) dir'
 519       (ProperElementToKeep Hole dir S dir' x r)) →
 520  (∀S:Argument_Class.∀dir',dir''.
 521    ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
 522     ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
 523      P (relation_class_of_argument_class S) dir' m ->
 524       P0 dir'' (singl ? S) (fcl_singl ? ? S ? ? c m)) →
 525  (∀S:Argument_Class.∀L:Arguments.∀dir',dir''.
 526    ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
 527     ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
 528      P (relation_class_of_argument_class S) dir' m →
 529       ∀m0:Morphism_Context_List Hole dir dir'' L.
 530        P0 dir'' L m0 → P0 dir'' (cons ? S L) (fcl_cons ? ? S ? ? ? c m m0)) →
 531  ∀r:rewrite_direction.∀a:Arguments.∀m:Morphism_Context_List Hole dir r a.
 532   P0 r a m
 533 ≝
 534  λHole,dir,P,P0,f,f0,f1,f2,f3,f4.
 535  let rec
 536   F (rc:Relation_Class) (r0:rewrite_direction)
 537    (m:Morphism_Context Hole dir rc r0) on m : P rc r0 m
 538  ≝
 539   match m return λrc.λr0.λm0.P rc r0 m0 with
 540   [ App In Out dir' m0 m1 ⇒ f In Out dir' m0 m1 (F0 dir' In m1)
 541   | ToReplace ⇒ f0
 542   | ToKeep S dir' c ⇒ f1 S dir' c
 543   | ProperElementToKeep S dir' x r1 ⇒ f2 S dir' x r1
 544   ]
 545  and
 546   F0 (r:rewrite_direction) (a:Arguments)
 547    (m:Morphism_Context_List Hole dir r a) on m : P0 r a m
 548  ≝
 549   match m return λr.λa.λm0.P0 r a m0 with
 550   [ fcl_singl S dir' dir'' c m0 ⇒
 551       f3 S dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
 552   | fcl_cons S L dir' dir'' c m0 m1 ⇒
 553       f4 S L dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
 554         m1 (F0 dir'' L m1)
 555   ]
 556 in F0.
 557
 558 definition product_of_arguments : Arguments → Type.
 559  intro;
 560  elim a;
 561   [ apply (carrier_of_relation_class ? t)
 562   | apply (Prod (carrier_of_relation_class ? t) T)
 563   ]
 564 qed.
 565
 566 definition get_rewrite_direction: rewrite_direction → Argument_Class → rewrite_direction.
 567  intros (dir R);
 568  cases (variance_of_argument_class R);
 569   [ exact dir
 570   | cases a;
 571      [ exact dir                      (* covariant *)
 572      | exact (opposite_direction dir) (* contravariant *)
 573      ]
 574   ]
 575 qed.
 576
 577 definition directed_relation_of_relation_class:
 578  ∀dir:rewrite_direction.∀R: Relation_Class.
 579    carrier_of_relation_class ? R → carrier_of_relation_class ? R → Prop.
 580  intros;
 581  cases r;
 582   [ exact (relation_of_relation_class ? ? c c1)
 583   | apply (relation_of_relation_class ? ? c1 c)
 584   ]
 585 qed.
 586
 587 definition directed_relation_of_argument_class:
 588  ∀dir:rewrite_direction.∀R: Argument_Class.
 589    carrier_of_relation_class ? R → carrier_of_relation_class ? R → Prop.
 590   intros (dir R c c1);
 591   rewrite < (about_carrier_of_relation_class_and_relation_class_of_argument_class R) in c c1;
 592   exact (directed_relation_of_relation_class dir (relation_class_of_argument_class R)  c c1).
 593 qed.
 594
 595
 596 definition relation_of_product_of_arguments:
 597  ∀dir:rewrite_direction.∀In.
 598   product_of_arguments In → product_of_arguments In → Prop.
 599  intros 2;
 600  elim In 0;
 601   [ simplify;
 602     intro;
 603     exact (directed_relation_of_argument_class (get_rewrite_direction r t) t)
 604   | intros;
 605     change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
 606     change in p1 with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
 607     cases p;
 608     cases p1;
 609    apply And;
 610     [ exact
 611       (directed_relation_of_argument_class (get_rewrite_direction r t) t a a1)
 612     | exact (R b b1)
 613     ]
 614   ]
 615 qed.
 616
 617 definition apply_morphism:
 618  ∀In,Out.∀m: function_type_of_morphism_signature In Out.
 619   ∀args: product_of_arguments In. carrier_of_relation_class ? Out.
 620  intro;
 621  elim In;
 622   [ exact (f p)
 623   | change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
 624    elim p;
 625    change in f1 with (carrier_of_relation_class variance t → function_type_of_morphism_signature n Out);
 626    exact (f ? (f1 t1) t2)
 627   ]
 628 qed.
 629
 630 theorem apply_morphism_compatibility_Right2Left:
 631  ∀In,Out.∀m1,m2: function_type_of_morphism_signature In Out.
 632   ∀args1,args2: product_of_arguments In.
 633      make_compatibility_goal_aux ? ? m1 m2 →
 634       relation_of_product_of_arguments Right2Left ? args1 args2 →
 635         directed_relation_of_relation_class Right2Left ?
 636          (apply_morphism ? ? m2 args1)
 637          (apply_morphism ? ? m1 args2).
 638   intro;
 639   elim In;
 640    [ simplify in m1 m2 args1 args2 ⊢ %;
 641      change in H1 with
 642       (directed_relation_of_argument_class
 643         (get_rewrite_direction Right2Left t) t args1 args2);
 644      generalize in match H1; clear H1;
 645      generalize in match H; clear H;
 646      generalize in match args2; clear args2;
 647      generalize in match args1; clear args1;
 648      generalize in match m2; clear m2;
 649      generalize in match m1; clear m1;
 650      elim t 0;
 651       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
 652         simplify in H;
 653         simplify in H1;
 654         simplify;
 655         apply H;
 656         exact H1
 657       | intros 8 (v T1 r Hr m1 m2 args1 args2);
 658         cases v;
 659         intros (H H1);
 660         simplify in H1;
 661         apply H;
 662         exact H1
 663       | intros;
 664         apply H1;
 665         exact H2
 666       | intros 7 (v);
 667         cases v;
 668         intros (H H1);
 669         simplify in H1;
 670         apply H;
 671         exact H1
 672       | intros;
 673         simplify in H1;
 674         rewrite > H1;
 675         apply H;
 676         exact H1
 677       ]
 678    | change in m1 with
 679       (carrier_of_relation_class variance t →
 680         function_type_of_morphism_signature n Out);
 681      change in m2 with
 682       (carrier_of_relation_class variance t →
 683         function_type_of_morphism_signature n Out);
 684      change in args1 with
 685       ((carrier_of_relation_class ? t) × (product_of_arguments n));
 686      change in args2 with
 687       ((carrier_of_relation_class ? t) × (product_of_arguments n));
 688      generalize in match H2; clear H2;
 689      elim args2 0; clear args2;
 690      elim args1; clear args1;
 691      elim H2; clear H2;
 692      change in H4 with
 693       (relation_of_product_of_arguments Right2Left n t2 t4);
 694      change with
 695       (relation_of_relation_class unit Out (apply_morphism n Out (m1 t3) t4)
 696         (apply_morphism n Out (m2 t1) t2));
 697      generalize in match H3; clear H3;
 698      generalize in match t3; clear t3;
 699      generalize in match t1; clear t1;
 700      generalize in match H1; clear H1;
 701      generalize in match m2; clear m2;
 702      generalize in match m1; clear m1;
 703      elim t 0;
 704       [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
 705         simplify in H3;
 706         change in H1 with
 707          (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 708      | intro v;
 709        elim v 0;
 710        [ intros (T1 r Hr m1 m2 H1 t1 t3 H3);
 711          simplify in H3;
 712          change in H1 with
 713           (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 714        | intros (T1 r Hr m1 m2 H1 t1 t3 H3);
 715          simplify in H3;
 716          change in H1 with
 717           (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 718        ]
 719      | intros (T1 r Hs m1 m2 H1 t1 t3 H3);
 720        simplify in H3;
 721        change in H1 with
 722         (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 723      | intro v;
 724        elim v 0;
 725         [ intros (T1 r m1 m2 H1 t1 t3 H3);
 726           simplify in H3;
 727           change in H1 with
 728            (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 729         | intros (T1 r m1 m2 H1 t1 t3 H3);
 730           simplify in H3;
 731           change in H1 with
 732            (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
 733         ]
 734      | intros (T m1 m2 H1 t1 t3 H3);
 735        simplify in H3;
 736        change in H1 with
 737         (∀x:T. make_compatibility_goal_aux n Out (m1 x) (m2 x));
 738        rewrite > H3;
 739        simplify in H;
 740        apply H;
 741         [ apply H1
 742         | assumption
 743         ]
 744      ] ;
 745      simplify in H;
 746      apply H;
 747       [1,3,5,7,9,11:
 748         apply H1;
 749         assumption
 750       |2,4,6,8,10,12:
 751         assumption
 752       ]
 753    ]
 754 qed.
 755
 756 theorem apply_morphism_compatibility_Left2Right:
 757  ∀In,Out.∀m1,m2: function_type_of_morphism_signature In Out.
 758   ∀args1,args2: product_of_arguments In.
 759      make_compatibility_goal_aux ? ? m1 m2 →
 760       relation_of_product_of_arguments Left2Right ? args1 args2 →
 761         directed_relation_of_relation_class Left2Right ?
 762          (apply_morphism ? ? m1 args1)
 763          (apply_morphism ? ? m2 args2).
 764   intro;
 765   elim In;
 766    [ simplify in m1 m2 args1 args2 ⊢ %;
 767      change in H1 with
 768       (directed_relation_of_argument_class
 769         (get_rewrite_direction Left2Right t) t args1 args2);
 770      generalize in match H1; clear H1;
 771      generalize in match H; clear H;
 772      generalize in match args2; clear args2;
 773      generalize in match args1; clear args1;
 774      generalize in match m2; clear m2;
 775      generalize in match m1; clear m1;
 776      elim t 0;
 777       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
 778         simplify in H;
 779         simplify in H1;
 780         simplify;
 781         apply H;
 782         exact H1
 783       | intros 8 (v T1 r Hr m1 m2 args1 args2);
 784         cases v;
 785         intros (H H1);
 786         simplify in H1;
 787         apply H;
 788         exact H1
 789       | intros;
 790         apply H1;
 791         exact H2
 792       | intros 7 (v);
 793         cases v;
 794         intros (H H1);
 795         simplify in H1;
 796         apply H;
 797         exact H1
 798       | intros;
 799         simplify in H1;
 800         rewrite > H1;
 801         apply H;
 802         exact H1
 803       ]
 804    | change in m1 with
 805       (carrier_of_relation_class variance t →
 806         function_type_of_morphism_signature n Out);
 807      change in m2 with
 808       (carrier_of_relation_class variance t →
 809         function_type_of_morphism_signature n Out);
 810      change in args1 with
 811       ((carrier_of_relation_class ? t) × (product_of_arguments n));
 812      change in args2 with
 813       ((carrier_of_relation_class ? t) × (product_of_arguments n));
 814      generalize in match H2; clear H2;
 815      elim args2 0; clear args2;
 816      elim args1; clear args1;
 817      elim H2; clear H2;
 818      change in H4 with
 819       (relation_of_product_of_arguments Left2Right n t2 t4);
 820      change with
 821       (relation_of_relation_class unit Out (apply_morphism n Out (m1 t1) t2)
 822         (apply_morphism n Out (m2 t3) t4));
 823      generalize in match H3; clear H3;
 824      generalize in match t3; clear t3;
 825      generalize in match t1; clear t1;
 826      generalize in match H1; clear H1;
 827      generalize in match m2; clear m2;
 828      generalize in match m1; clear m1;
 829      elim t 0;
 830       [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
 831         simplify in 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    | 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   | 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; tauto.
1021 Qed.
1022
1023 (* and IS A MORPHISM *)
1024
1025 Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
1026  tauto.
1027 Qed.
1028
1029 (* or IS A MORPHISM *)
1030
1031 Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
1032  tauto.
1033 Qed.
1034
1035 (* not IS A MORPHISM *)
1036
1037 Add Morphism not with signature iff ==> iff as Not_Morphism.
1038  tauto.
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; tauto.
1045 Qed.
1046
1047 Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
1048  unfold impl; tauto.
1049 Qed.
1050
1051 Add Morphism not with signature impl -→ impl as Not_Morphism2.
1052  unfold impl; tauto.
1053 Qed.
1054
1055 *)