helm/software/matita/dama/lattice.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 "excess.ma".
  16
  17 record semi_lattice_base : Type ≝ {
  18   sl_carr:> apartness;
  19   sl_op: sl_carr → sl_carr → sl_carr;
  20   sl_op_refl: ∀x.sl_op x x ≈ x;
  21   sl_op_comm: ∀x,y:sl_carr. sl_op x y ≈ sl_op y x;
  22   sl_op_assoc: ∀x,y,z:sl_carr. sl_op x (sl_op y z) ≈ sl_op (sl_op x y) z;
  23   sl_strong_extop: ∀x.strong_ext ? (sl_op x)
  24 }.
  25
  26 notation "a \cross b" left associative with precedence 50 for @{ 'op $a $b }.
  27 interpretation "semi lattice base operation" 'op a b = (cic:/matita/lattice/sl_op.con _ a b).
  28
  29 lemma excess_of_semi_lattice_base: semi_lattice_base → excess.
  30 intro l;
  31 apply mk_excess;
  32 [1: apply mk_excess_;
  33     [1: apply mk_excess_dual_smart;
  34
  35   apply (mk_excess_base (sl_carr l));
  36     [1: apply (λa,b:sl_carr l.a # (a ✗ b));
  37     |2: unfold; intros 2 (x H); simplify in H;
  38         lapply (Ap≪ ? (sl_op_refl ??) H) as H1; clear H;
  39         apply (ap_coreflexive ?? H1);
  40     |3: unfold; simplify; intros (x y z H1);
  41         cases (ap_cotransitive ??? ((x ✗ z) ✗ y) H1) (H2 H2);[2:
  42           lapply (Ap≪ ? (sl_op_comm ???) H2) as H21;
  43           lapply (Ap≫ ? (sl_op_comm ???) H21) as H22; clear H21 H2;
  44           lapply (sl_strong_extop ???? H22); clear H22;
  45           left; apply ap_symmetric; assumption;]
  46         cases (ap_cotransitive ??? (x ✗ z) H2) (H3 H3);[left;assumption]
  47         right; lapply (Ap≫ ? (sl_op_assoc ????) H3) as H31;
  48         apply (sl_strong_extop ???? H31);]
  49
  50     |2:
  51     apply apartness_of_excess_base;
  52
  53   apply (mk_excess_base (sl_carr l));
  54     [1: apply (λa,b:sl_carr l.a # (a ✗ b));
  55     |2: unfold; intros 2 (x H); simplify in H;
  56         lapply (Ap≪ ? (sl_op_refl ??) H) as H1; clear H;
  57         apply (ap_coreflexive ?? H1);
  58     |3: unfold; simplify; intros (x y z H1);
  59         cases (ap_cotransitive ??? ((x ✗ z) ✗ y) H1) (H2 H2);[2:
  60           lapply (Ap≪ ? (sl_op_comm ???) H2) as H21;
  61           lapply (Ap≫ ? (sl_op_comm ???) H21) as H22; clear H21 H2;
  62           lapply (sl_strong_extop ???? H22); clear H22;
  63           left; apply ap_symmetric; assumption;]
  64         cases (ap_cotransitive ??? (x ✗ z) H2) (H3 H3);[left;assumption]
  65         right; lapply (Ap≫ ? (sl_op_assoc ????) H3) as H31;
  66         apply (sl_strong_extop ???? H31);]
  67
  68     |3: apply refl_eq;]
  69 |2,3: intros (x y H); assumption;]
  70 qed.
  71
  72 record semi_lattice : Type ≝ {
  73   sl_exc:> excess;
  74   sl_meet: sl_exc → sl_exc → sl_exc;
  75   sl_meet_refl: ∀x.sl_meet x x ≈ x;
  76   sl_meet_comm: ∀x,y. sl_meet x y ≈ sl_meet y x;
  77   sl_meet_assoc: ∀x,y,z. sl_meet x (sl_meet y z) ≈ sl_meet (sl_meet x y) z;
  78   sl_strong_extm: ∀x.strong_ext ? (sl_meet x);
  79   sl_le_to_eqm: ∀x,y.x ≤ y → x ≈ sl_meet x y;
  80   sl_lem: ∀x,y.(sl_meet x y) ≤ y
  81 }.
  82
  83 interpretation "semi lattice meet" 'and a b = (cic:/matita/lattice/sl_meet.con _ a b).
  84
  85 lemma sl_feq_ml: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
  86 intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
  87 intro H1; apply H; clear H; apply (sl_strong_extm ???? H1);
  88 qed.
  89
  90 lemma sl_feq_mr: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (a ∧ c) ≈ (b ∧ c).
  91 intros (l a b c H);
  92 apply (Eq≈ ? (sl_meet_comm ???)); apply (Eq≈ ?? (sl_meet_comm ???));
  93 apply sl_feq_ml; assumption;
  94 qed.
  95
  96
  97 (*
  98 lemma semi_lattice_of_semi_lattice_base: semi_lattice_base → semi_lattice.
  99 intro slb; apply (mk_semi_lattice (excess_of_semi_lattice_base slb));
 100 [1: apply (sl_op slb);
 101 |2: intro x; apply (eq_trans (excess_of_semi_lattice_base slb)); [2:
 102       apply (sl_op_refl slb);|1:skip] (sl_op slb x x)); ? (sl_op_refl slb x));
 103
 104  unfold excess_of_semi_lattice_base; simplify;
 105     intro H; elim H;
 106     [
 107
 108
 109     lapply (ap_rewl (excess_of_semi_lattice_base slb) x ? (sl_op slb x x)
 110       (eq_sym (excess_of_semi_lattice_base slb) ?? (sl_op_refl slb x)) t);
 111     change in x with (sl_carr slb);
 112     apply (Ap≪ (x ✗ x)); (sl_op_refl slb x));
 113
 114 whd in H; elim H; clear H;
 115     [ apply (ap_coreflexive (excess_of_semi_lattice_base slb) (x ✗ x) t);
 116
 117 prelattice (excess_of_directed l_)); [apply (sl_op l_);]
 118 unfold excess_of_directed; try unfold apart_of_excess; simplify;
 119 unfold excl; simplify;
 120 [intro x; intro H; elim H; clear H;
 121  [apply (sl_op_refl l_ x);
 122   lapply (Ap≫ ? (sl_op_comm ???) t) as H; clear t;
 123   lapply (sl_strong_extop l_ ??? H); apply ap_symmetric; assumption
 124  | lapply (Ap≪ ? (sl_op_refl ?x) t) as H; clear t;
 125    lapply (sl_strong_extop l_ ??? H); apply (sl_op_refl l_ x);
 126    apply ap_symmetric; assumption]
 127 |intros 3 (x y H); cases H (H1 H2); clear H;
 128  [lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ x y)) H1) as H; clear H1;
 129   lapply (sl_strong_extop l_ ??? H) as H1; clear H;
 130   lapply (Ap≪ ? (sl_op_comm ???) H1); apply (ap_coreflexive ?? Hletin);
 131  |lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ y x)) H2) as H; clear H2;
 132   lapply (sl_strong_extop l_ ??? H) as H1; clear H;
 133   lapply (Ap≪ ? (sl_op_comm ???) H1);apply (ap_coreflexive ?? Hletin);]
 134 |intros 4 (x y z H); cases H (H1 H2); clear H;
 135  [lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ x (sl_op l_ y z))) H1) as H; clear H1;
 136   lapply (sl_strong_extop l_ ??? H) as H1; clear H;
 137   lapply (Ap≪ ? (eq_sym ??? (sl_op_assoc ?x y z)) H1) as H; clear H1;
 138   apply (ap_coreflexive ?? H);
 139  |lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ (sl_op l_ x y) z)) H2) as H; clear H2;
 140   lapply (sl_strong_extop l_ ??? H) as H1; clear H;
 141   lapply (Ap≪ ? (sl_op_assoc ?x y z) H1) as H; clear H1;
 142   apply (ap_coreflexive ?? H);]
 143 |intros (x y z H); elim H (H1 H1); clear H;
 144  lapply (Ap≪ ? (sl_op_refl ??) H1) as H; clear H1;
 145  lapply (sl_strong_extop l_ ??? H) as H1; clear H;
 146  lapply (sl_strong_extop l_ ??? H1) as H; clear H1;
 147  cases (ap_cotransitive ??? (sl_op l_ y z) H);[left|right|right|left] try assumption;
 148  [apply ap_symmetric;apply (Ap≪ ? (sl_op_comm ???));
 149  |apply (Ap≫ ? (sl_op_comm ???));
 150  |apply ap_symmetric;] assumption;
 151 |intros 4 (x y H H1); apply H; clear H; elim H1 (H H);
 152  lapply (Ap≪ ? (sl_op_refl ??) H) as H1; clear H;
 153  lapply (sl_strong_extop l_ ??? H1) as H; clear H1;[2: apply ap_symmetric]
 154  assumption
 155 |intros 3 (x y H);
 156  cut (sl_op l_ x y ≈ sl_op l_ x (sl_op l_ y y)) as H1;[2:
 157    intro; lapply (sl_strong_extop ???? a); apply (sl_op_refl l_ y);
 158    apply ap_symmetric; assumption;]
 159  lapply (Ap≪ ? (eq_sym ??? H1) H); apply (sl_op_assoc l_ x y y);
 160  assumption; ]
 161 qed.
 162 *)
 163
 164 (* ED(≰,≱) → EB(≰') → ED(≰',≱') *)
 165 lemma subst_excess_base: excess_dual → excess_base → excess_dual.
 166 intros; apply (mk_excess_dual_smart e1);
 167 qed.
 168
 169 (* E_(ED(≰,≱),AP(#),c ED = c AP) → ED' → c DE' = c E_ → E_(ED',#,p) *)
 170 lemma subst_dual_excess: ∀e:excess_.∀e1:excess_dual.exc_carr e = exc_carr e1 → excess_.
 171 intros (e e1 p); apply (mk_excess_ e1 e); cases p; reflexivity;
 172 qed.
 173
 174 (* E(E_,H1,H2) → E_' → H1' → H2' → E(E_',H1',H2') *)
 175 alias symbol "nleq" = "Excess excess_".
 176 lemma subst_excess_: ∀e:excess. ∀e1:excess_.
 177   (∀y,x:e1. y # x → y ≰ x ∨ x ≰ y) →
 178   (∀y,x:e1.y ≰ x ∨ x ≰ y →  y # x) →
 179   excess.
 180 intros (e e1 H1 H2); apply (mk_excess e1 H1 H2);
 181 qed.
 182
 183 (* SL(E,M,H2-5(#),H67(≰)) → E' → c E = c E' → H67'(≰') → SL(E,M,p2-5,H67') *)
 184 lemma subst_excess:
 185   ∀l:semi_lattice.
 186   ∀e:excess.
 187   ∀p:exc_ap l = exc_ap e.
 188   (∀x,y:e.(le (exc_dual_base e)) x y → x ≈ (?(sl_meet l)) x y) →
 189   (∀x,y:e.(le (exc_dual_base e)) ((?(sl_meet l)) x y) y) →
 190   semi_lattice.
 191 [1,2:intro M;
 192  change with ((λx.ap_carr x) e -> (λx.ap_carr x) e -> (λx.ap_carr x) e);
 193  cases p; apply M;
 194 |intros (l e p H1 H2);
 195  apply (mk_semi_lattice e);
 196    [ change with ((λx.ap_carr x) e -> (λx.ap_carr x) e -> (λx.ap_carr x) e);
 197      cases p; simplify; apply (sl_meet l);
 198    |2: change in ⊢ (% → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_refl;
 199    |3: change in ⊢ (% → % → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_comm;
 200    |4: change in ⊢ (% → % → % → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_assoc;
 201    |5: change in ⊢ (% → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_strong_extm;
 202    |6: clear H2; apply H1;
 203    |7: clear H1; apply H2;]]
 204 qed.
 205
 206 lemma excess_of_excess_base: excess_base → excess.
 207 intro eb;
 208 apply mk_excess;
 209   [apply (mk_excess_ (mk_excess_dual_smart eb));
 210     [apply (apartness_of_excess_base eb);
 211     |reflexivity]
 212   |2,3: intros; assumption]
 213 qed.
 214
 215 lemma subst_excess_base_in_semi_lattice:
 216   ∀sl:semi_lattice.
 217   ∀eb:excess_base.
 218   ∀p:exc_carr sl = exc_carr eb.
 219
 220   mancano le 4 proprietà riscritte con p
 221
 222   semi_lattice.
 223 intros (l eb H); apply (subst_excess l);
 224   [apply (subst_excess_ l);
 225     [apply (subst_dual_excess l);
 226       [apply (subst_excess_base l eb);
 227       |apply H;]
 228     | change in \vdash (% -> % -> ?) with (exc_carr eb);
 229     letin xxx \def (ap2exc l); clearbody xxx;
 230     change in xxx:(%→%→?) with (Type_OF_semi_lattice l);
 231     whd in ⊢ (?→?→? (? %) ? ?→?);
 232     unfold exc_ap;
 233     simplify in ⊢ (?→?→%→?);
 234
 235 intros 2;
 236 generalize in ⊢ (% -> ?); intro P;
 237 generalize in match x in ⊢ % as x;
 238 generalize in match y in ⊢ % as y; clear x y;
 239
 240
 241 cases H; simplify;
 242
 243
 244 cut (Πy:exc_carr eb
 245 .Πx:exc_carr eb
 246  .match
 247   (match H
 248    in eq
 249    return
 250   λright_1:Type
 251   .(λmatched:eq Type (Type_OF_excess_ (excess__OF_semi_lattice l)) right_1
 252     .eq Type (Type_OF_excess_ (excess__OF_semi_lattice l)) right_1)
 253    with
 254   [refl_eq⇒refl_eq Type (Type_OF_excess_ (excess__OF_semi_lattice l))])
 255    in eq
 256    return
 257   λright_1:Type
 258   .(λmatched:eq Type (ap_carr (exc_ap (excess__OF_semi_lattice l))) right_1
 259     .right_1→right_1→Type)
 260    with
 261   [refl_eq⇒ap_apart (exc_ap (excess__OF_semi_lattice l))] y x);[2:
 262
 263
 264     change in ⊢ (?→?→? % ? ?→?) with (exc_ap_ (excess__OF_semi_lattice l));
 265     generalize in match H in \vdash (? -> %); cases H;
 266     cases H;
 267
 268
 269 normalize in ⊢ (?→?→?→? (? (? (? ? (% ? ?) ?)) ? ?) ?);
 270 whd in ⊢ (?→?→? % ? ?→?); change in ⊢ (?→?→? (? % ? ? ? ?) ? ?→?) with (exc_carr eb);
 271 cases H;
 272       change in ⊢ (?→?→? % ? ?→?) with (exc_ap l);
 273 (subst_dual_excess (excess__OF_semi_lattice l)
 274  (subst_excess_base (excess_dual_OF_semi_lattice l) eb) H)
 275
 276
 277        unfold subst_excess_base;
 278         unfold mk_excess_dual_smart;
 279         unfold excess__OF_semi_lattice;
 280         unfold excess_dual_OF_semi_lattice;
 281         unfold excess_dual_OF_semi_lattice;
 282
 283       reflexivity]
 284 *)
 285
 286 record lattice_ : Type ≝ {
 287   latt_mcarr:> semi_lattice;
 288   latt_jcarr_: semi_lattice;
 289 (*  latt_with1:   (subst_excess_
 290                   (subst_dual_excess
 291                     (subst_excess_base
 292                       (excess_dual_OF_excess (sl_exc latt_jcarr_))
 293                       (excess_base_OF_excess (sl_exc latt_mcarr))))) =
 294                 sl_exc latt_jcarr_;
 295
 296 *)
 297   latt_with1: excess_base_OF_excess1 (sl_exc latt_jcarr_) =  excess_base_OF_excess (sl_exc latt_mcarr);
 298   latt_with2: excess_base_OF_excess (sl_exc latt_jcarr_) =  excess_base_OF_excess1 (sl_exc latt_mcarr);
 299   latt_with3: apartness_OF_excess (sl_exc latt_jcarr_) = apartness_OF_excess (sl_exc latt_mcarr)
 300 }.
 301
 302 axiom FALSE: False.
 303
 304 lemma latt_jcarr : lattice_ → semi_lattice.
 305 intro l;
 306 apply mk_semi_lattice;
 307   [apply mk_excess;
 308     [apply mk_excess_;
 309       [apply (mk_excess_dual_smart l);
 310       |apply (exc_ap l);
 311       |reflexivity]
 312     |unfold mk_excess_dual_smart; simplify;
 313      intros (x y H); cases (ap2exc ??? H); [right|left]  assumption;
 314     |unfold mk_excess_dual_smart; simplify;
 315      intros (x y H);cases H; apply exc2ap;[right|left] assumption;]]
 316 unfold mk_excess_dual_smart; simplify;
 317 [1: change with ((λx.ap_carr x) l → (λx.ap_carr x) l → (λx.ap_carr x) l);
 318     simplify; unfold apartness_OF_lattice_;
 319     cases (latt_with3 l); apply (sl_meet (latt_jcarr_ l));
 320 |2: change in ⊢ (%→?) with ((λx.ap_carr x) l); simplify;
 321     unfold apartness_OF_lattice_;
 322     cases (latt_with3 l); apply (sl_meet_refl (latt_jcarr_ l));
 323 |3: change in ⊢ (%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_;
 324     cases (latt_with3 l); apply (sl_meet_comm (latt_jcarr_ l));
 325 |4: change in ⊢ (%→%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_;
 326     cases (latt_with3 l); apply (sl_meet_assoc (latt_jcarr_ l));
 327 |5: change in ⊢ (%→%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_;
 328     cases (latt_with3 l); apply (sl_strong_extm (latt_jcarr_ l));
 329 |7:
 330 (*
 331 unfold excess_base_OF_lattice_;
 332     change in ⊢ (?→?→? ? (% ? ?) ?)
 333     with (match latt_with3 l
 334  in eq
 335  return
 336 λright_1:apartness
 337 .(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right_1
 338   .ap_carr right_1→ap_carr right_1→ap_carr right_1)
 339  with
 340 [refl_eq⇒sl_meet (latt_jcarr_ l)]
 341  : ?
 342 );
 343   change in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?)
 344   with ((λx.exc_carr x) (excess_base_OF_semi_lattice (latt_mcarr l)));
 345   unfold excess_base_OF_lattice_ in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?);
 346   simplify in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?);
 347 change in ⊢ (?→?→? ? (% ? ?) ?) with
 348   (match refl_eq ? (excess__OF_semi_lattice (latt_mcarr l)) in eq
 349    return (λR.λE:eq ? (excess_base_OF_semi_lattice (latt_mcarr l)) R.R → R → R)
 350    with [refl_eq⇒
 351      (match latt_with3 l in eq
 352      return
 353        (λright:apartness
 354         .(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right
 355           .ap_carr right→ap_carr right→ap_carr right))
 356      with [refl_eq⇒ sl_meet (latt_jcarr_ l)]
 357      :
 358      exc_carr (excess_base_OF_semi_lattice (latt_mcarr l))
 359       →exc_carr (excess_base_OF_semi_lattice (latt_mcarr l))
 360        →exc_carr (excess_base_OF_semi_lattice (latt_mcarr l))
 361      )
 362    ]);
 363    generalize in ⊢ (?→?→? ? (match % return ? with [_⇒?] ? ?) ?);
 364    unfold excess_base_OF_lattice_ in ⊢ (? ? ? %→?);
 365    cases (latt_with1 l);
 366   change in ⊢ (?→?→?→? ? (match ? return ? with [_⇒(?:%→%->%)] ? ?) ?)
 367   with ((λx.ap_carr x) (latt_mcarr l));
 368   simplify in ⊢ (?→?→?→? ? (match ? return ? with [_⇒(?:%→%->%)] ? ?) ?);
 369   cases (latt_with3 l);
 370
 371    change in ⊢ (? ? % ?→?) with ((λx.ap_carr x) l);
 372    simplify in ⊢ (% → ?);
 373    change in ⊢ (?→?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
 374      with ((λx.ap_carr x) (apartness_OF_lattice_ l));
 375    unfold apartness_OF_lattice_;
 376    cases (latt_with3 l); simplify;
 377    change in ⊢ (? ? ? %→%→%→?) with ((λx.exc_carr x) l);
 378    unfold excess_base_OF_lattice_;
 379    cases (latt_with1 l); simplify;
 380    change in \vdash (? -> % -> % -> ?) with (exc_carr (excess_base_OF_semi_lattice (latt_jcarr_ l)));
 381    change in ⊢ ((? ? % ?)→%→%→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
 382      with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)));
 383    simplify;
 384    intro H;
 385    unfold excess_base_OF_semi_lattice1;
 386    unfold excess_base_OF_excess1;
 387    unfold excess_base_OF_excess_1;
 388    change
 389 *)
 390
 391 change in ⊢ (?→?→? ? (% ? ?) ?) with
 392   (match refl_eq ? (Type_OF_lattice_ l) in eq
 393    return (λR.λE:eq ? (Type_OF_lattice_ l) R.R → R → R)
 394    with [refl_eq⇒
 395      match latt_with3 l in eq
 396      return
 397        (λright:apartness
 398         .(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right
 399           .ap_carr right→ap_carr right→ap_carr right))
 400      with [refl_eq⇒ sl_meet (latt_jcarr_ l)]
 401    ]);
 402    generalize in ⊢ (?→?→? ? (match % return ? with [_⇒?] ? ?) ?);
 403    change in ⊢ (? ? % ?→?) with ((λx.ap_carr x) l);
 404    simplify in ⊢ (% → ?);
 405    change in ⊢ (?→?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
 406      with ((λx.ap_carr x) (apartness_OF_lattice_ l));
 407    unfold apartness_OF_lattice_;
 408    cases (latt_with3 l); simplify;
 409    change in ⊢ (? ? ? %→%→%→?) with ((λx.exc_carr x) l);
 410    unfold excess_base_OF_lattice_;
 411    cases (latt_with1 l); simplify;
 412    change in \vdash (? -> % -> % -> ?) with (exc_carr (excess_base_OF_semi_lattice (latt_jcarr_ l)));
 413    change in ⊢ ((? ? % ?)→%→%→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
 414      with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)));
 415    simplify;
 416    intro H;
 417    change in ⊢ (?→?→%) with (le (mk_excess_base
 418           ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
 419           ((λx.exc_excess x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
 420           ((λx.exc_coreflexive x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
 421           ((λx.exc_cotransitive x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
 422         ) (match H
 423  in eq
 424  return
 425 λR:Type
 426 .(λE:eq Type (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) R
 427   .R→R→R)
 428  with
 429 [refl_eq⇒sl_meet (latt_jcarr_ l)] x y) y);
 430  simplify in ⊢ (?→?→? (? % ???) ? ?);
 431  change in ⊢ (?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
 432  with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)));
 433  simplify in  ⊢ (?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?);
 434  lapply (match H in eq return
 435         λright.λe:eq ? (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) right.
 436
 437 ∀x:right
 438 .∀y:right
 439  .le
 440   (mk_excess_base right ???)
 441   (match e
 442     in eq
 443     return
 444    λR:Type.(λE:eq Type (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) R.R→R→R)
 445     with
 446    [refl_eq⇒sl_meet (latt_jcarr_ l)] x y) y
 447         with [refl_eq ⇒ ?]) as XX;
 448   [cases e; apply (exc_excess (latt_jcarr_ l));
 449   |unfold;cases e;simplify;apply (exc_coreflexive (latt_jcarr_ l));
 450   |unfold;cases e;simplify;apply (exc_cotransitive (latt_jcarr_ l));
 451   ||apply XX|
 452   |apply XX;
 453
 454          simplify; apply (sl_lem);
 455 |elim FALSE]
 456 qed.
 457
 458
 459
 460
 461 coercion cic:/matita/lattice/latt_jcarr.con.
 462
 463 interpretation "Lattice meet" 'and a b =
 464  (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _) a b).
 465
 466 interpretation "Lattice join" 'or a b =
 467  (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _) a b).
 468
 469 record lattice : Type ≝ {
 470   latt_carr:> lattice_;
 471   absorbjm: ∀f,g:latt_carr. (f ∨ (f ∧ g)) ≈ f;
 472   absorbmj: ∀f,g:latt_carr. (f ∧ (f ∨ g)) ≈ f
 473 }.
 474
 475 notation "'meet'"        non associative with precedence 50 for @{'meet}.
 476 notation "'meet_refl'"   non associative with precedence 50 for @{'meet_refl}.
 477 notation "'meet_comm'"   non associative with precedence 50 for @{'meet_comm}.
 478 notation "'meet_assoc'"  non associative with precedence 50 for @{'meet_assoc}.
 479 notation "'strong_extm'" non associative with precedence 50 for @{'strong_extm}.
 480 notation "'le_to_eqm'"   non associative with precedence 50 for @{'le_to_eqm}.
 481 notation "'lem'"         non associative with precedence 50 for @{'lem}.
 482 notation "'join'"        non associative with precedence 50 for @{'join}.
 483 notation "'join_refl'"   non associative with precedence 50 for @{'join_refl}.
 484 notation "'join_comm'"   non associative with precedence 50 for @{'join_comm}.
 485 notation "'join_assoc'"  non associative with precedence 50 for @{'join_assoc}.
 486 notation "'strong_extj'" non associative with precedence 50 for @{'strong_extj}.
 487 notation "'le_to_eqj'"   non associative with precedence 50 for @{'le_to_eqj}.
 488 notation "'lej'"         non associative with precedence 50 for @{'lej}.
 489
 490 interpretation "Lattice meet"        'meet        = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _)).
 491 interpretation "Lattice meet_refl"   'meet_refl   = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_mcarr.con _)).
 492 interpretation "Lattice meet_comm"   'meet_comm   = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_mcarr.con _)).
 493 interpretation "Lattice meet_assoc"  'meet_assoc  = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_mcarr.con _)).
 494 interpretation "Lattice strong_extm" 'strong_extm = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_mcarr.con _)).
 495 interpretation "Lattice le_to_eqm"   'le_to_eqm   = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_mcarr.con _)).
 496 interpretation "Lattice lem"         'lem         = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_mcarr.con _)).
 497 interpretation "Lattice join"        'join        = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _)).
 498 interpretation "Lattice join_refl"   'join_refl   = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_jcarr.con _)).
 499 interpretation "Lattice join_comm"   'join_comm   = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_jcarr.con _)).
 500 interpretation "Lattice join_assoc"  'join_assoc  = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_jcarr.con _)).
 501 interpretation "Lattice strong_extm" 'strong_extj = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_jcarr.con _)).
 502 interpretation "Lattice le_to_eqj"   'le_to_eqj   = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_jcarr.con _)).
 503 interpretation "Lattice lej"         'lej         = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_jcarr.con _)).
 504
 505 notation "'feq_jl'" non associative with precedence 50 for @{'feq_jl}.
 506 notation "'feq_jr'" non associative with precedence 50 for @{'feq_jr}.
 507 notation "'feq_ml'" non associative with precedence 50 for @{'feq_ml}.
 508 notation "'feq_mr'" non associative with precedence 50 for @{'feq_mr}.
 509 interpretation "Lattice feq_jl" 'feq_jl = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_jcarr.con _)).
 510 interpretation "Lattice feq_jr" 'feq_jr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_jcarr.con _)).
 511 interpretation "Lattice feq_ml" 'feq_ml = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_mcarr.con _)).
 512 interpretation "Lattice feq_mr" 'feq_mr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_mcarr.con _)).
 513
 514
 515 interpretation "Lattive meet le" 'leq a b =
 516  (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice1.con _) a b).
 517
 518 interpretation "Lattive join le (aka ge)" 'geq a b =
 519  (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice.con _) a b).
 520
 521 (* these coercions help unification, handmaking a bit of conversion
 522    over an open term
 523 *)
 524 lemma le_to_ge: ∀l:lattice.∀a,b:l.a ≤ b → b ≥ a.
 525 intros(l a b H); apply H;
 526 qed.
 527
 528 lemma ge_to_le: ∀l:lattice.∀a,b:l.b ≥ a → a ≤ b.
 529 intros(l a b H); apply H;
 530 qed.
 531
 532 coercion cic:/matita/lattice/le_to_ge.con nocomposites.
 533 coercion cic:/matita/lattice/ge_to_le.con nocomposites.