helm/software/matita/nlibrary/overlap/o-algebra.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "sets/categories2.ma".
  16
  17 (*
  18 interpretation "unary morphism comprehension with no proof" 'comprehension T P =
  19   (mk_unary_morphism T ? P ?).
  20 interpretation "unary morphism1 comprehension with no proof" 'comprehension T P =
  21   (mk_unary_morphism1 T ? P ?).
  22
  23 notation > "hvbox({ ident i ∈ s | term 19 p | by })" with precedence 90
  24 for @{ 'comprehension_by $s (λ${ident i}. $p) $by}.
  25 notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
  26 for @{ 'comprehension_by $s (λ${ident i}:$_. $p) $by}.
  27
  28 interpretation "unary morphism comprehension with proof" 'comprehension_by s \eta.f p =
  29   (mk_unary_morphism s ? f p).
  30 interpretation "unary morphism1 comprehension with proof" 'comprehension_by s \eta.f p =
  31   (mk_unary_morphism1 s ? f p).
  32 *)
  33
  34 (* per il set-indexing vedere capitolo BPTools (foundational tools), Sect. 0.3.4 complete
  35    lattices, Definizione 0.9 *)
  36 (* USARE L'ESISTENZIALE DEBOLE *)
  37 nrecord OAlgebra : Type[2] := {
  38   oa_P :> setoid1;
  39   oa_leq : binary_morphism1 oa_P oa_P CPROP; (*CSC: dovrebbe essere CProp bug refiner*)
  40   oa_overlap: binary_morphism1 oa_P oa_P CPROP;
  41   binary_meet: binary_morphism1 oa_P oa_P oa_P;
  42 (*CSC:  oa_join: ∀I:setoid.unary_morphism1 (setoid1_of_setoid … I ⇒ oa_P) oa_P;*)
  43   oa_one: oa_P;
  44   oa_zero: oa_P;
  45   oa_leq_refl: ∀a:oa_P. oa_leq a a;
  46   oa_leq_antisym: ∀a,b:oa_P.oa_leq a b → oa_leq b a → a = b;
  47   oa_leq_trans: ∀a,b,c:oa_P.oa_leq a b → oa_leq b c → oa_leq a c;
  48   oa_overlap_sym: ∀a,b:oa_P.oa_overlap a b → oa_overlap b a;
  49 (*CSC:  oa_join_sup: ∀I:setoid.∀p_i:I ⇒ oa_P.∀p:oa_P.oa_leq (oa_join I p_i) p = (∀i:I.oa_leq (p_i i) p);*)
  50   oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
  51   oa_one_top: ∀p:oa_P.oa_leq p oa_one;
  52   oa_overlap_preservers_meet: ∀p,q:oa_P.oa_overlap p q → oa_overlap p (binary_meet p q);
  53 (*CSC:  oa_join_split:
  54       ∀I:SET.∀p.∀q:I ⇒ oa_P.
  55        oa_overlap p (oa_join I q) = (∃i:I.oa_overlap p (q i));*)
  56   (*oa_base : setoid;
  57   1) enum non e' il nome giusto perche' non e' suriettiva
  58   2) manca (vedere altro capitolo) la "suriettivita'" come immagine di insiemi di oa_base
  59   oa_enum : ums oa_base oa_P;
  60   oa_density: ∀p,q.(∀i.oa_overlap p (oa_enum i) → oa_overlap q (oa_enum i)) → oa_leq p q
  61   *)
  62   oa_density:
  63       ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q
  64 }.
  65
  66 interpretation "o-algebra leq" 'leq a b = (fun21 ??? (oa_leq ?) a b).
  67
  68 notation "hovbox(a mpadded width -150% (>)< b)" non associative with precedence 45
  69 for @{ 'overlap $a $b}.
  70 interpretation "o-algebra overlap" 'overlap a b = (fun21 ??? (oa_overlap ?) a b).
  71
  72 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)"
  73 non associative with precedence 50 for @{ 'oa_meet $p }.
  74 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈  I) break term 90 p)"
  75 non associative with precedence 50 for @{ 'oa_meet_mk (λ${ident i}:$I.$p) }.
  76
  77 (*notation > "hovbox(∧ f)" non associative with precedence 60
  78 for @{ 'oa_meet $f }.
  79 interpretation "o-algebra meet" 'oa_meet f =
  80   (fun12 ?? (oa_meet ??) f).
  81 interpretation "o-algebra meet with explicit function" 'oa_meet_mk f =
  82   (fun12 ?? (oa_meet ??) (mk_unary_morphism ?? f ?)).
  83 *)
  84 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)"
  85 non associative with precedence 50 for @{ 'oa_join $p }.
  86 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈  I) break term 90 p)"
  87 non associative with precedence 50 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }.
  88
  89 (*CSC
  90 notation > "hovbox(∨ f)" non associative with precedence 60
  91 for @{ 'oa_join $f }.
  92 interpretation "o-algebra join" 'oa_join f =
  93   (fun12 ?? (oa_join ??) f).
  94 interpretation "o-algebra join with explicit function" 'oa_join_mk f =
  95   (fun12 ?? (oa_join ??) (mk_unary_morphism ?? f ?)).
  96 *)
  97 (*definition binary_meet : ∀O:OAlgebra. binary_morphism1 O O O.
  98 intros; split;
  99 [ intros (p q);
 100   apply (∧ { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p ? p q });
 101 | intros; lapply (prop12 ? O (oa_meet O BOOL));
 102    [2: apply ({ x ∈ BOOL | match x with [ true ⇒ a | false ⇒ b ] | IF_THEN_ELSE_p ? a b });
 103    |3: apply ({ x ∈ BOOL | match x with [ true ⇒ a' | false ⇒ b' ] | IF_THEN_ELSE_p ? a' b' });
 104    | apply Hletin;]
 105   intro x; simplify; cases x; simplify; assumption;]
 106 qed.*)
 107
 108 interpretation "o-algebra binary meet" 'and a b =
 109   (fun21 ??? (binary_meet ?) a b).
 110
 111 (*
 112 prefer coercion Type1_OF_OAlgebra.
 113
 114 definition binary_join : ∀O:OAlgebra. binary_morphism1 O O O.
 115 intros; split;
 116 [ intros (p q);
 117   apply (∨ { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p ? p q });
 118 | intros; lapply (prop12 ? O (oa_join O BOOL));
 119    [2: apply ({ x ∈ BOOL | match x with [ true ⇒ a | false ⇒ b ] | IF_THEN_ELSE_p ? a b });
 120    |3: apply ({ x ∈ BOOL | match x with [ true ⇒ a' | false ⇒ b' ] | IF_THEN_ELSE_p ? a' b' });
 121    | apply Hletin;]
 122   intro x; simplify; cases x; simplify; assumption;]
 123 qed.
 124
 125 interpretation "o-algebra binary join" 'or a b =
 126   (fun21 ??? (binary_join ?) a b).
 127 *)
 128 (*
 129 lemma oa_overlap_preservers_meet: ∀O:OAlgebra.∀p,q:O.p >< q → p >< (p ∧ q).
 130 (* next change to avoid universe inconsistency *)
 131 change in ⊢ (?→%→%→?) with (Type1_OF_OAlgebra O);
 132 intros;  lapply (oa_overlap_preserves_meet_ O p q f);
 133 lapply (prop21 O O CPROP (oa_overlap O) p p ? (p ∧ q) # ?);
 134 [3: apply (if ?? (Hletin1)); apply Hletin;|skip] apply refl1;
 135 qed.
 136 *)
 137 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)"
 138 non associative with precedence 49 for @{ 'oa_join $p }.
 139 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈  I) break term 90 p)"
 140 non associative with precedence 49 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }.
 141 notation < "hovbox(a ∨ b)" left associative with precedence 49
 142 for @{ 'oa_join_mk (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
 143
 144 notation > "hovbox(∨ f)" non associative with precedence 59
 145 for @{ 'oa_join $f }.
 146 notation > "hovbox(a ∨ b)" left associative with precedence 49
 147 for @{ 'oa_join (mk_unary_morphism BOOL ? (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) (IF_THEN_ELSE_p ? $a $b)) }.
 148
 149 (*interpretation "o-algebra join" 'oa_join f =
 150   (fun12 ?? (oa_join ??) f).
 151 interpretation "o-algebra join with explicit function" 'oa_join_mk f =
 152   (fun12 ?? (oa_join ??) (mk_unary_morphism ?? f ?)).
 153 *)
 154 nrecord ORelation (P,Q : OAlgebra) : Type[1] ≝ {
 155   or_f :> P ⇒ Q;
 156   or_f_minus_star : P ⇒ Q;
 157   or_f_star : Q ⇒ P;
 158   or_f_minus : Q ⇒ P;
 159   or_prop1 : ∀p,q. (or_f p ≤ q) = (p ≤ or_f_star q);
 160   or_prop2 : ∀p,q. (or_f_minus p ≤ q) = (p ≤ or_f_minus_star q);
 161   or_prop3 : ∀p,q. (or_f p >< q) = (p >< or_f_minus q)
 162 }.
 163
 164 notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}.
 165 notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}.
 166
 167 notation "r \sup (⎻* )" non associative with precedence 90 for @{'OR_f_minus_star $r}.
 168 notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r}.
 169
 170 notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
 171 notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
 172
 173 interpretation "o-relation f⎻*" 'OR_f_minus_star r = (or_f_minus_star ? ? r).
 174 interpretation "o-relation f⎻" 'OR_f_minus r = (or_f_minus ? ? r).
 175 interpretation "o-relation f*" 'OR_f_star r = (or_f_star ? ? r).
 176
 177
 178 ndefinition ORelation_setoid : OAlgebra → OAlgebra → setoid1.
 179 #P; #Q; @ (ORelation P Q); @
 180  [ napply (λp,q.p = q)
 181  | #x; napply refl1
 182  | #x; #y; napply sym1
 183  | #x; #y; #z; napply trans1 ]
 184 nqed.
 185
 186 unification hint 0 ≔ P, Q ;
 187   R ≟ (ORelation_setoid P Q)
 188 (* -------------------------- *) ⊢
 189     carr1 R ≡ ORelation P Q.
 190
 191 ndefinition or_f_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
 192  (unary_morphism1_setoid1 P Q).
 193  #P; #Q; @
 194   [ napply or_f
 195   | #a; #a'; #e; nassumption]
 196 nqed.
 197
 198 unification hint 0 ≔ P, Q, r;
 199  R ≟ (mk_unary_morphism1 … (or_f …) (prop11 … (or_f_morphism1 …)))
 200 (* ------------------------ *) ⊢
 201   fun11 … R r ≡ or_f P Q r.
 202
 203 nlemma ORelation_eq_respects_leq_or_f_minus_:
 204  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
 205   r=r' → ∀x. r⎻ x ≤ r'⎻ x.
 206  #P; #Q; #a; #a'; #e; #x;
 207  napply oa_density; #r; #H;
 208  napply oa_overlap_sym;
 209  napply (. (or_prop3 … a' …)^-1); (*CSC: why a'? *)
 210  napply (. ?‡#)
 211   [##2: napply (a r)
 212   | ngeneralize in match r in ⊢ %;
 213     nchange with (or_f … a' = or_f … a);
 214     napply (.= †e^-1);
 215     napply #]
 216  napply (. (or_prop3 …));
 217  napply oa_overlap_sym;
 218  nassumption.
 219 nqed.
 220
 221 nlemma ORelation_eq2:
 222  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
 223   r=r' → r⎻ = r'⎻.
 224  #P; #Q; #a; #a'; #e; #x;
 225  napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_
 226   [ napply e | napply e^-1]
 227 nqed.
 228
 229 ndefinition or_f_minus_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
 230  (unary_morphism1_setoid1 Q P).
 231  #P; #Q; @
 232   [ napply or_f_minus
 233   | napply ORelation_eq2]
 234 nqed.
 235
 236 unification hint 0 ≔ P, Q, r;
 237  R ≟ (mk_unary_morphism1 … (or_f_minus …) (prop11 … (or_f_minus_morphism1 …)))
 238 (* ------------------------ *) ⊢
 239   fun11 … R r ≡ or_f_minus P Q r.
 240
 241 naxiom daemon : False.
 242
 243 nlemma ORelation_eq_respects_leq_or_f_star_:
 244  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
 245   r=r' → ∀x. r* x ≤ r'* x.
 246  #P; #Q; #a; #a'; #e; #x; (*CSC: una schifezza *)
 247  ncases daemon.
 248  (*
 249  ngeneralize in match (. (or_prop1 P Q a' (a* x) x)^-1) in ⊢ %; #H; napply H;
 250  nchange with (or_f P Q a' (a* x) ≤ x);
 251  napply (. ?‡#)
 252   [##2: napply (a (a* x))
 253   | ngeneralize in match (a* x);
 254     nchange with (or_f P Q a' = or_f P Q a);
 255     napply (.= †e^-1); napply #]
 256  napply (. (or_prop1 …));
 257  napply oa_leq_refl.*)
 258 nqed.
 259
 260 nlemma ORelation_eq3:
 261  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
 262   r=r' → r* = r'*.
 263  #P; #Q; #a; #a'; #e; #x;
 264  napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_star_
 265   [ napply e | napply e^-1]
 266 nqed.
 267
 268 ndefinition or_f_star_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
 269  (unary_morphism1_setoid1 Q P).
 270  #P; #Q; @
 271   [ napply or_f_star
 272   | napply ORelation_eq3]
 273 nqed.
 274
 275 unification hint 0 ≔ P, Q, r;
 276  R ≟ (mk_unary_morphism1 … (or_f_star …) (prop11 … (or_f_star_morphism1 …)))
 277 (* ------------------------ *) ⊢
 278   fun11 … R r ≡ or_f_star P Q r.
 279
 280 nlemma ORelation_eq_respects_leq_or_f_minus_star_:
 281  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
 282   r=r' → ∀x. r⎻* x ≤ r'⎻* x.
 283  #P; #Q; #a; #a'; #e; #x; (*CSC: una schifezza *)
 284  ncases daemon. (*
 285  ngeneralize in match (. (or_prop2 P Q a' (a⎻* x) x)^-1) in ⊢ %; #H; napply H;
 286  nchange with (or_f_minus P Q a' (a⎻* x) ≤ x);
 287  napply (. ?‡#)
 288   [##2: napply (a⎻ (a⎻* x))
 289   | ngeneralize in match (a⎻* x);
 290     nchange with (a'⎻ = a⎻);
 291     napply (.= †e^-1); napply #]
 292  napply (. (or_prop2 …));
 293  napply oa_leq_refl.*)
 294 nqed.
 295
 296 nlemma ORelation_eq4:
 297  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
 298   r=r' → r⎻* = r'⎻*.
 299  #P; #Q; #a; #a'; #e; #x;
 300  napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_star_
 301   [ napply e | napply e^-1]
 302 nqed.
 303
 304 ndefinition or_f_minus_star_morphism1:
 305  ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q) (unary_morphism1_setoid1 P Q).
 306  #P; #Q; @
 307   [ napply or_f_minus_star
 308   | napply ORelation_eq4]
 309 nqed.
 310
 311
 312 unification hint 0 ≔ P, Q, r;
 313  R ≟ (mk_unary_morphism1 … (or_f_minus_star …) (prop11 … (or_f_minus_star_morphism1 …)))
 314 (* ------------------------ *) ⊢
 315   fun11 … R r ≡ or_f_minus_star P Q r.
 316
 317 (* qui la notazione non va *)
 318 (*CSC
 319 nlemma leq_to_eq_join: ∀S:OAlgebra.∀p,q:S. p ≤ q → q = (binary_join ? p q).
 320  intros;
 321  apply oa_leq_antisym;
 322   [ apply oa_density; intros;
 323     apply oa_overlap_sym;
 324     unfold binary_join; simplify;
 325     apply (. (oa_join_split : ?));
 326     exists; [ apply false ]
 327     apply oa_overlap_sym;
 328     assumption
 329   | unfold binary_join; simplify;
 330     apply (. (oa_join_sup : ?)); intro;
 331     cases i; whd in ⊢ (? ? ? ? ? % ?);
 332      [ assumption | apply oa_leq_refl ]]
 333 qed.
 334
 335 nlemma overlap_monotone_left: ∀S:OAlgebra.∀p,q,r:S. p ≤ q → p >< r → q >< r.
 336  #S; #p; #q; #r; #H1; #H2;
 337  apply (. (leq_to_eq_join : ?)‡#);
 338   [ apply f;
 339   | skip
 340   | apply oa_overlap_sym;
 341     unfold binary_join; simplify;
 342     apply (. (oa_join_split : ?));
 343     exists [ apply true ]
 344     apply oa_overlap_sym;
 345     assumption; ]
 346 qed.*)
 347
 348 (* Part of proposition 9.9 *)
 349 nlemma f_minus_image_monotone: ∀S,T.∀R:ORelation S T.∀p,q. p ≤ q → R⎻ p ≤ R⎻ q.
 350  #S; #T; #R; #p; #q; #H;
 351  napply (. (or_prop2 …));
 352  napply oa_leq_trans; ##[##2: napply H; ##| ##skip |
 353   napply (. (or_prop2 … q …)^ -1);(*CSC: why q?*) napply oa_leq_refl]
 354 nqed.
 355
 356 (* Part of proposition 9.9 *)
 357 nlemma f_minus_star_image_monotone: ∀S,T.∀R:ORelation S T.∀p,q. p ≤ q → R⎻* p ≤ R⎻* q.
 358  #S; #T; #R; #p; #q; #H;
 359  napply (. (or_prop2 … (R⎻* p) q)^ -1); (*CSC: why ?*)
 360  napply oa_leq_trans; ##[##3: napply H; ##| ##skip | napply (. (or_prop2 …)); napply oa_leq_refl]
 361 nqed.
 362
 363 (* Part of proposition 9.9 *)
 364 nlemma f_image_monotone: ∀S,T.∀R:ORelation S T.∀p,q. p ≤ q → R p ≤ R q.
 365  #S; #T; #R; #p; #q; #H;
 366  napply (. (or_prop1 …));
 367  napply oa_leq_trans; ##[##2: napply H; ##| ##skip | napply (. (or_prop1 … q …)^ -1); napply oa_leq_refl]
 368 nqed.
 369
 370 (* Part of proposition 9.9 *)
 371 nlemma f_star_image_monotone: ∀S,T.∀R:ORelation S T.∀p,q. p ≤ q → R* p ≤ R* q.
 372  #S; #T; #R; #p; #q; #H;
 373  napply (. (or_prop1 … (R* p) q)^ -1);
 374  napply oa_leq_trans; ##[##3: napply H; ##| ##skip | napply (. (or_prop1 …)); napply oa_leq_refl]
 375 nqed.
 376
 377 nlemma lemma_10_2_a: ∀S,T.∀R:ORelation S T.∀p. p ≤ R⎻* (R⎻ p).
 378  #S; #T; #R; #p;
 379  napply (. (or_prop2 … p …)^-1);
 380  napply oa_leq_refl.
 381 nqed.
 382
 383 nlemma lemma_10_2_b: ∀S,T.∀R:ORelation S T.∀p. R⎻ (R⎻* p) ≤ p.
 384  #S; #T; #R; #p;
 385  napply (. (or_prop2 …));
 386  napply oa_leq_refl.
 387 nqed.
 388
 389 nlemma lemma_10_2_c: ∀S,T.∀R:ORelation S T.∀p. p ≤ R* (R p).
 390  #S; #T; #R; #p;
 391  napply (. (or_prop1 … p …)^-1);
 392  napply oa_leq_refl.
 393 nqed.
 394
 395 nlemma lemma_10_2_d: ∀S,T.∀R:ORelation S T.∀p. R (R* p) ≤ p.
 396  #S; #T; #R; #p;
 397  napply (. (or_prop1 …));
 398  napply oa_leq_refl.
 399 nqed.
 400
 401 nlemma lemma_10_3_a: ∀S,T.∀R:ORelation S T.∀p. R⎻ (R⎻* (R⎻ p)) = R⎻ p.
 402  #S; #T; #R; #p; napply oa_leq_antisym
 403   [ napply lemma_10_2_b
 404   | napply f_minus_image_monotone;
 405     napply lemma_10_2_a ]
 406 nqed.
 407
 408 nlemma lemma_10_3_b: ∀S,T.∀R:ORelation S T.∀p. R* (R (R* p)) = R* p.
 409  #S; #T; #R; #p; napply oa_leq_antisym
 410   [ napply f_star_image_monotone;
 411     napply (lemma_10_2_d ?? R p)
 412   | napply lemma_10_2_c ]
 413 nqed.
 414
 415 nlemma lemma_10_3_c: ∀S,T.∀R:ORelation S T.∀p. R (R* (R p)) = R p.
 416  #S; #T; #R; #p; napply oa_leq_antisym
 417   [ napply lemma_10_2_d
 418   | napply f_image_monotone;
 419     napply (lemma_10_2_c ?? R p) ]
 420 nqed.
 421
 422 nlemma lemma_10_3_d: ∀S,T.∀R:ORelation S T.∀p. R⎻* (R⎻ (R⎻* p)) = R⎻* p.
 423  #S; #T; #R; #p; napply oa_leq_antisym
 424   [ napply f_minus_star_image_monotone;
 425     napply (lemma_10_2_b ?? R p)
 426   | napply lemma_10_2_a ]
 427 nqed.
 428
 429 nlemma lemma_10_4_a: ∀S,T.∀R:ORelation S T.∀p. R⎻* (R⎻ (R⎻* (R⎻ p))) = R⎻* (R⎻ p).
 430  #S; #T; #R; #p; napply (†(lemma_10_3_a …)).
 431 nqed.
 432
 433 nlemma lemma_10_4_b: ∀S,T.∀R:ORelation S T.∀p. R (R* (R (R* p))) = R (R* p).
 434  #S; #T; #R; #p; napply (†(lemma_10_3_b …));
 435 nqed.
 436
 437 nlemma oa_overlap_sym': ∀o:OAlgebra.∀U,V:o. (U >< V) = (V >< U).
 438  #o; #U; #V; @; #H; napply oa_overlap_sym; nassumption.
 439 nqed.
 440
 441 (******************* CATEGORIES **********************)
 442
 443 ninductive one : Type[0] ≝ unit : one.
 444
 445 ndefinition force : ∀S:Type[2]. S → ∀T:Type[2]. T → one → Type[2] ≝
 446  λS,s,T,t,lock. match lock with [ unit => S ].
 447
 448 ndefinition enrich_as :
 449  ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one.force S s T t lock ≝
 450  λS,s,T,t,lock. match lock return λlock.match lock with [ unit ⇒ S ]
 451                     with [ unit ⇒ s ].
 452
 453 ncoercion enrich_as : ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one. force S s T t lock
 454  ≝ enrich_as on t: ? to force ? ? ? ? ?.
 455
 456 (* does not work here
 457 nlemma foo : ∀A,B,C:setoid1.∀f:B ⇒ C.∀g:A ⇒ B. unary_morphism1 A C.
 458 #A; #B; #C; #f; #g; napply(f \circ g).
 459 nqed.*)
 460
 461 (* This precise hint does not leave spurious metavariables *)
 462 unification hint 0 ≔ A,B,C : setoid1, f:B ⇒ C, g: A ⇒ B;
 463    lock ≟ unit
 464 (* --------------------------------------------------------------- *) ⊢
 465   (unary_morphism1 A C)
 466  ≡
 467   (force (unary_morphism1 A C) (comp1_unary_morphisms A B C f g)
 468    (carr1 A → carr1 C) (composition1 A B C f g)  lock)
 469   .
 470
 471 (* This uniform hint opens spurious metavariables
 472 unification hint 0 ≔ A,B,C : setoid1, f:B ⇒ C, g: A ⇒ B, X;
 473    lock ≟ unit
 474 (* --------------------------------------------------------------- *) ⊢
 475   (unary_morphism1 A C)
 476  ≡
 477   (force (unary_morphism1 A C) X (carr1 A → carr1 C) (fun11 … X)  lock)
 478   .
 479 *)
 480
 481 nlemma foo : ∀A,B,C:setoid1.∀f:B ⇒ C.∀g:A ⇒ B. unary_morphism1 A C.
 482 #A; #B; #C; #f; #g; napply(f ∘ g).
 483 nqed.
 484
 485 (*
 486
 487 ndefinition uffa: ∀A,B. ∀U: unary_morphism1 A B. (A → B) → CProp[0].
 488  #A;#B;#_;#_; napply True.
 489 nqed.
 490 ndefinition mk_uffa: ∀A,B.∀U: unary_morphism1 A B. ∀f: (A → B). uffa A B U f.
 491  #A; #B; #U; #f; napply I.
 492 nqed.
 493
 494 ndefinition coerc_to_unary_morphism1:
 495  ∀A,B. ∀U: unary_morphism1 A B. uffa A B U (fun11 … U) → unary_morphism1 A B.
 496  #A; #B; #U; #_; nassumption.
 497 nqed.
 498
 499 ncheck (λA,B,C,f,g.coerc_to_unary_morphism1 ??? (mk_uffa ??? (composition1 A B C f g))).
 500 *)
 501 ndefinition ORelation_composition : ∀P,Q,R.
 502   binary_morphism1 (ORelation_setoid P Q) (ORelation_setoid Q R) (ORelation_setoid P R).
 503 #P; #Q; #R; @
 504 [ #F; #G; @
 505   [ napply (G ∘ F) (* napply (comp1_unary_morphisms … G F) (*CSC: was (G ∘ F);*) *)
 506   | napply (G⎻* ∘ F⎻* ) (* napply (comp1_unary_morphisms … G⎻* F⎻* ) (*CSC: was (G⎻* ∘ F⎻* );*)*)
 507   | napply (comp1_unary_morphisms … F* G* ) (*CSC: was (F* ∘ G* );*)
 508   | napply (comp1_unary_morphisms … F⎻ G⎻) (*CSC: was (F⎻ ∘ G⎻);*)
 509   | #p; #q; nnormalize;
 510     napply (.= (or_prop1 … G …)); (*CSC: it used to understand without G *)
 511     napply (or_prop1 …)
 512   | #p; #q; nnormalize;
 513     napply (.= (or_prop2 … F …));
 514     napply or_prop2
 515   | #p; #q; nnormalize;
 516     napply (.= (or_prop3 … G …));
 517     napply or_prop3
 518   ]
 519 ##| #a;#a';#b;#b';#e;#e1;#x;nnormalize;napply (.= †(e x));napply e1]
 520 nqed.
 521
 522 (*
 523 ndefinition OA : category2.
 524 split;
 525 [ apply (OAlgebra);
 526 | intros; apply (ORelation_setoid o o1);
 527 | intro O; split;
 528   [1,2,3,4: apply id2;
 529   |5,6,7:intros; apply refl1;]
 530 | apply ORelation_composition;
 531 | intros (P Q R S F G H); split;
 532    [ change with (H⎻* ∘ G⎻* ∘ F⎻* = H⎻* ∘ (G⎻* ∘ F⎻* ));
 533      apply (comp_assoc2 ????? (F⎻* ) (G⎻* ) (H⎻* ));
 534    | apply ((comp_assoc2 ????? (H⎻) (G⎻) (F⎻))^-1);
 535    | apply ((comp_assoc2 ????? F G H)^-1);
 536    | apply ((comp_assoc2 ????? H* G* F* ));]
 537 | intros; split; unfold ORelation_composition; simplify; apply id_neutral_left2;
 538 | intros; split; unfold ORelation_composition; simplify; apply id_neutral_right2;]
 539 qed.
 540
 541 definition OAlgebra_of_objs2_OA: objs2 OA → OAlgebra ≝ λx.x.
 542 coercion OAlgebra_of_objs2_OA.
 543
 544 definition ORelation_setoid_of_arrows2_OA:
 545   ∀P,Q. arrows2 OA P Q → ORelation_setoid P Q ≝ λP,Q,c.c.
 546 coercion ORelation_setoid_of_arrows2_OA.
 547
 548 prefer coercion Type_OF_objs2.
 549 *)
 550 (* alias symbol "eq" = "setoid1 eq". *)