1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
17 record semi_lattice_base : Type ≝ {
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)
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).
29 lemma excess_of_semi_lattice_base: semi_lattice_base → excess.
33 [1: apply mk_excess_dual_smart;
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);]
51 apply apartness_of_excess_base;
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);]
69 |2,3: intros (x y H); assumption;]
72 record semi_lattice : Type ≝ {
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
83 interpretation "semi lattice meet" 'and a b = (cic:/matita/lattice/sl_meet.con _ a b).
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);
90 lemma sl_feq_mr: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (a ∧ c) ≈ (b ∧ c).
92 apply (Eq≈ ? (sl_meet_comm ???)); apply (Eq≈ ?? (sl_meet_comm ???));
93 apply sl_feq_ml; assumption;
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));
104 unfold excess_of_semi_lattice_base; simplify;
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));
114 whd in H; elim H; clear H;
115 [ apply (ap_coreflexive (excess_of_semi_lattice_base slb) (x ✗ x) t);
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]
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);
164 (* ED(≰,≱) → EB(≰') → ED(≰',≱') *)
165 lemma subst_excess_base: excess_dual → excess_base → excess_dual.
166 intros; apply (mk_excess_dual_smart e1);
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;
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) →
180 intros (e e1 H1 H2); apply (mk_excess e1 H1 H2);
183 (* SL(E,M,H2-5(#),H67(≰)) → E' → c E = c E' → H67'(≰') → SL(E,M,p2-5,H67') *)
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) →
192 change with ((λx.ap_carr x) e -> (λx.ap_carr x) e -> (λx.ap_carr x) e);
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;]]
206 lemma excess_of_excess_base: excess_base → excess.
209 [apply (mk_excess_ (mk_excess_dual_smart eb));
210 [apply (apartness_of_excess_base eb);
212 |2,3: intros; assumption]
215 lemma subst_excess_preserves_aprtness:
219 exc_ap l = exc_ap (subst_excess l e p H1 H2).
222 simplify; assumption;
226 lemma subst_excess__preserves_aprtness:
230 exc_ap l = apartness_OF_excess (subst_excess_ l (subst_dual_excess l (subst_excess_base l e) p) H1 H2).
231 intros 3; (unfold subst_excess_; unfold subst_dual_excess; unfold subst_excess_base; unfold exc_ap; unfold mk_excess_dual_smart; simplify);
232 (unfold subst_excess_base in p; unfold mk_excess_dual_smart in p; simplify in p);
237 lemma subst_excess_base_in_excess_:
240 ∀p:exc_carr d = exc_carr eb.
243 apply (subst_dual_excess e_);
244 [apply (subst_excess_base e_ eb);
248 definition hole ≝ λT:Type.λx:T.x.
250 notation < "\ldots" non associative with precedence 50 for @{'hole}.
251 interpretation "hole" 'hole = (cic:/matita/lattice/hole.con _ _).
253 lemma subst_excess_base_in_excess:
256 ∀p:exc_carr d = exc_carr eb.
257 (∀y1,x1:eb. (?(ap_apart d)) y1 x1 → y1 ≰ x1 ∨ x1 ≰ y1) →
258 (∀y2,x2:eb.y2 ≰ x2 ∨ x2 ≰ y2 → (?(ap_apart d)) y2 x2) →
260 [1,3,4:apply Type|2,5:intro f; cases p; apply f]
261 intros (d eb p H1 H2);
262 apply (subst_excess_ d);
263 [apply (subst_excess_base_in_excess_ d eb p);
264 |apply hole; clear H2;
265 change in ⊢ (%→%→?) with (exc_carr eb);
266 change in ⊢ (?→?→?→? (? % ? ?) (? % ? ?)) with eb; intros (y x H3);
267 apply H1; generalize in match H3;
268 unfold ap_apart; unfold subst_excess_base_in_excess_;
269 unfold subst_dual_excess; simplify;
270 generalize in match x;
271 generalize in match y;
272 cases p; simplify; intros; assumption;
273 |apply hole; clear H1;
274 change in ⊢ (%→%→?) with (exc_carr eb);
275 change in ⊢ (?→?→? (? % ? ?) (? % ? ?)→?) with eb; intros (y x H3);
276 unfold ap_apart; unfold subst_excess_base_in_excess_;
277 unfold subst_dual_excess; simplify; generalize in match (H2 ?? H3);
278 generalize in match x; generalize in match y; cases p;
282 lemma tech1: ∀e:excess.
285 exc_ap e = exc_ap_ (subst_excess_base_in_excess e eb p H1 H2).
286 intros (e eb p H1 H2);
287 unfold subst_excess_base_in_excess;
288 unfold subst_excess_; simplify;
289 unfold subst_excess_base_in_excess_;
290 unfold subst_dual_excess; simplify; reflexivity;
295 exc_ap e = exc_ap (mk_excess_ (subst_excess_base e eb) (exc_ap e) p).
296 intros (e eb p);unfold exc_ap; simplify; cases p; simplify; reflexivity;
301 ∀a1,b1,a2,b2,a3,b3,a4,b4,a5,b5.
302 a1=b1 → a2=b2 → a3=b3 → a4=b4 → a5=b5 → mk_apartness a1 a2 a3 a4 a5 = mk_apartness b1 b2 b3 b4 b5.
303 intros; cases H; cases H1; cases H2; cases H3; cases H4; reflexivity;
307 lemma subst_excess_base_in_excess_preserves_apartness:
311 apartness_OF_excess e =
312 apartness_OF_excess (subst_excess_base_in_excess e eb H H1 H2).
313 intros (e eb p H1 H2);
314 unfold subst_excess_base_in_excess;
315 unfold subst_excess_; unfold subst_excess_base_in_excess_;
316 unfold subst_dual_excess; unfold apartness_OF_excess;
317 simplify in ⊢ (? ? ? (? %));
318 rewrite < (tech2 e eb);
322 alias symbol "nleq" = "Excess base excess".
323 lemma subst_excess_base_in_semi_lattice:
326 ∀p:exc_carr sl = exc_carr eb.
327 (∀y1,x1:eb. (?(ap_apart sl)) y1 x1 → y1 ≰ x1 ∨ x1 ≰ y1) →
328 (∀y2,x2:eb.y2 ≰ x2 ∨ x2 ≰ y2 → (?(ap_apart sl)) y2 x2) →
329 (∀x3,y3:eb.(le eb) x3 y3 → (?(eq sl)) x3 ((?(sl_meet sl)) x3 y3)) →
330 (∀x4,y4:eb.(le eb) ((?(sl_meet sl)) x4 y4) y4) →
332 [2:apply Prop|3,7,9,10:apply Type|4:apply (exc_carr eb)|1,5,6,8,11:intro f; cases p; apply f;]
333 intros (sl eb H H1 H2 H3 H4);
334 apply (subst_excess sl);
335 [apply (subst_excess_base_in_excess sl eb H H1 H2);
336 |rewrite > (subst_excess_preserves_aprtness sl);
339 clear H3 H4; unfold apartness_OF_semi_lattice;
340 generalize in match (sl_exc sl);
341 intro; whd in \vdash (? ? ? %); unfold in ⊢ (? ? ? (? ? match ? (? %) return ? with [_⇒?] ? ? ?));
345 apply (subst_excess__preserves_aprtness (sl_exc sl) eb H H1 H2);
346 | (clear H4;change in ⊢ (%→%→?) with (exc_carr eb);change in ⊢ (?→?→? % ? ?→?) with eb; simplify);
348 (generalize in ⊢ (? (? (? ? ? % ?)) ? ?); intro P1);
349 (generalize in ⊢ (? (? (? ? ? ? %)) ? ?); intro P2);
350 generalize in match (H3 x y LE);
351 generalize in match x as x;
352 generalize in match y as y;
353 generalize in ⊢ (?→?→?→? (? (? ? ? % ?)) ? ?); intro P1;
354 generalize in ⊢ (?→?→?→? (? (? ? ? ? %)) ? ?); intro P2;
355 change (%->?) with (ap_carr ());
359 lapply (pippo sl eb H P1 P2);
361 intros (x y H5); generalize in match (H3 x y H5); clear H4;
362 generalize in ⊢ (?→? (? (? ? ? % ?)) ? ?); intro P;
363 generalize in ⊢ (?→? (? (? ? ? ? %)) ? ?); intro Q;
366 change in ⊢ (?→? (? (? ? (? % ? ?) ? ?)) ? ?) with ((λx.excess_carr x) sl); simplify;
367 change in ⊢ (?→? (? (? ? (? ? (? % ?) ?) ? ?)) ? ?) with ((λx.excess_dual_OF_excess x) sl);simplify;
369 rewrite < (subst_excess__preserves_aprtness (sl_exc sl) eb H P Q);
370 generalize in ⊢ (?→?→?→? ? ? (match ? ? ? ? % ? return ? with [_⇒?] ? ?)); intro A;
371 generalize in ⊢ (?→?→?→? ? ? (match ? ? ? ? ? % return ? with [_⇒?] ? ?)); intro B;
378 record lattice_ : Type ≝ {
379 latt_mcarr:> semi_lattice;
380 latt_jcarr_: semi_lattice;
381 (*latt_with1: latt_jcarr_ = subst latt_jcarr (exc_dual_dual latt_mcarr)*)
382 (* latt_with1: (subst_excess_
385 (excess_dual_OF_excess (sl_exc latt_jcarr_))
386 (excess_base_OF_excess (sl_exc latt_mcarr))))) =
390 latt_with1: excess_base_OF_excess1 (sl_exc latt_jcarr_) = excess_base_OF_excess (sl_exc latt_mcarr);
391 latt_with2: excess_base_OF_excess (sl_exc latt_jcarr_) = excess_base_OF_excess1 (sl_exc latt_mcarr);
392 latt_with3: apartness_OF_excess (sl_exc latt_jcarr_) = apartness_OF_excess (sl_exc latt_mcarr)
397 lemma latt_jcarr : lattice_ → semi_lattice.
399 apply mk_semi_lattice;
402 [apply (mk_excess_dual_smart l);
405 |unfold mk_excess_dual_smart; simplify;
406 intros (x y H); cases (ap2exc ??? H); [right|left] assumption;
407 |unfold mk_excess_dual_smart; simplify;
408 intros (x y H);cases H; apply exc2ap;[right|left] assumption;]]
409 unfold mk_excess_dual_smart; simplify;
410 [1: change with ((λx.ap_carr x) l → (λx.ap_carr x) l → (λx.ap_carr x) l);
411 simplify; unfold apartness_OF_lattice_;
412 cases (latt_with3 l); apply (sl_meet (latt_jcarr_ l));
413 |2: change in ⊢ (%→?) with ((λx.ap_carr x) l); simplify;
414 unfold apartness_OF_lattice_;
415 cases (latt_with3 l); apply (sl_meet_refl (latt_jcarr_ l));
416 |3: change in ⊢ (%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_;
417 cases (latt_with3 l); apply (sl_meet_comm (latt_jcarr_ l));
418 |4: change in ⊢ (%→%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_;
419 cases (latt_with3 l); apply (sl_meet_assoc (latt_jcarr_ l));
420 |5: change in ⊢ (%→%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_;
421 cases (latt_with3 l); apply (sl_strong_extm (latt_jcarr_ l));
424 unfold excess_base_OF_lattice_;
425 change in ⊢ (?→?→? ? (% ? ?) ?)
426 with (match latt_with3 l
430 .(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right_1
431 .ap_carr right_1→ap_carr right_1→ap_carr right_1)
433 [refl_eq⇒sl_meet (latt_jcarr_ l)]
436 change in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?)
437 with ((λx.exc_carr x) (excess_base_OF_semi_lattice (latt_mcarr l)));
438 unfold excess_base_OF_lattice_ in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?);
439 simplify in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?);
440 change in ⊢ (?→?→? ? (% ? ?) ?) with
441 (match refl_eq ? (excess__OF_semi_lattice (latt_mcarr l)) in eq
442 return (λR.λE:eq ? (excess_base_OF_semi_lattice (latt_mcarr l)) R.R → R → R)
444 (match latt_with3 l in eq
447 .(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right
448 .ap_carr right→ap_carr right→ap_carr right))
449 with [refl_eq⇒ sl_meet (latt_jcarr_ l)]
451 exc_carr (excess_base_OF_semi_lattice (latt_mcarr l))
452 →exc_carr (excess_base_OF_semi_lattice (latt_mcarr l))
453 →exc_carr (excess_base_OF_semi_lattice (latt_mcarr l))
456 generalize in ⊢ (?→?→? ? (match % return ? with [_⇒?] ? ?) ?);
457 unfold excess_base_OF_lattice_ in ⊢ (? ? ? %→?);
458 cases (latt_with1 l);
459 change in ⊢ (?→?→?→? ? (match ? return ? with [_⇒(?:%→%->%)] ? ?) ?)
460 with ((λx.ap_carr x) (latt_mcarr l));
461 simplify in ⊢ (?→?→?→? ? (match ? return ? with [_⇒(?:%→%->%)] ? ?) ?);
462 cases (latt_with3 l);
464 change in ⊢ (? ? % ?→?) with ((λx.ap_carr x) l);
465 simplify in ⊢ (% → ?);
466 change in ⊢ (?→?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
467 with ((λx.ap_carr x) (apartness_OF_lattice_ l));
468 unfold apartness_OF_lattice_;
469 cases (latt_with3 l); simplify;
470 change in ⊢ (? ? ? %→%→%→?) with ((λx.exc_carr x) l);
471 unfold excess_base_OF_lattice_;
472 cases (latt_with1 l); simplify;
473 change in \vdash (? -> % -> % -> ?) with (exc_carr (excess_base_OF_semi_lattice (latt_jcarr_ l)));
474 change in ⊢ ((? ? % ?)→%→%→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
475 with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)));
478 unfold excess_base_OF_semi_lattice1;
479 unfold excess_base_OF_excess1;
480 unfold excess_base_OF_excess_1;
484 change in ⊢ (?→?→? ? (% ? ?) ?) with
485 (match refl_eq ? (Type_OF_lattice_ l) in eq
486 return (λR.λE:eq ? (Type_OF_lattice_ l) R.R → R → R)
488 match latt_with3 l in eq
491 .(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right
492 .ap_carr right→ap_carr right→ap_carr right))
493 with [refl_eq⇒ sl_meet (latt_jcarr_ l)]
495 generalize in ⊢ (?→?→? ? (match % return ? with [_⇒?] ? ?) ?);
496 change in ⊢ (? ? % ?→?) with ((λx.ap_carr x) l);
497 simplify in ⊢ (% → ?);
498 change in ⊢ (?→?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
499 with ((λx.ap_carr x) (apartness_OF_lattice_ l));
500 unfold apartness_OF_lattice_;
501 cases (latt_with3 l); simplify;
502 change in ⊢ (? ? ? %→%→%→?) with ((λx.exc_carr x) l);
503 unfold excess_base_OF_lattice_;
504 cases (latt_with1 l); simplify;
505 change in \vdash (? -> % -> % -> ?) with (exc_carr (excess_base_OF_semi_lattice (latt_jcarr_ l)));
506 change in ⊢ ((? ? % ?)→%→%→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
507 with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)));
510 change in ⊢ (?→?→%) with (le (mk_excess_base
511 ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
512 ((λx.exc_excess x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
513 ((λx.exc_coreflexive x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
514 ((λx.exc_cotransitive x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
519 .(λE:eq Type (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) R
522 [refl_eq⇒sl_meet (latt_jcarr_ l)] x y) y);
523 simplify in ⊢ (?→?→? (? % ???) ? ?);
524 change in ⊢ (?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
525 with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)));
526 simplify in ⊢ (?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?);
527 lapply (match H in eq return
528 λright.λe:eq ? (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) right.
533 (mk_excess_base right ???)
537 λR:Type.(λE:eq Type (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) R.R→R→R)
539 [refl_eq⇒sl_meet (latt_jcarr_ l)] x y) y
540 with [refl_eq ⇒ ?]) as XX;
541 [cases e; apply (exc_excess (latt_jcarr_ l));
542 |unfold;cases e;simplify;apply (exc_coreflexive (latt_jcarr_ l));
543 |unfold;cases e;simplify;apply (exc_cotransitive (latt_jcarr_ l));
547 simplify; apply (sl_lem);
554 coercion cic:/matita/lattice/latt_jcarr.con.
556 interpretation "Lattice meet" 'and a b =
557 (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _) a b).
559 interpretation "Lattice join" 'or a b =
560 (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _) a b).
562 record lattice : Type ≝ {
563 latt_carr:> lattice_;
564 absorbjm: ∀f,g:latt_carr. (f ∨ (f ∧ g)) ≈ f;
565 absorbmj: ∀f,g:latt_carr. (f ∧ (f ∨ g)) ≈ f
568 notation "'meet'" non associative with precedence 50 for @{'meet}.
569 notation "'meet_refl'" non associative with precedence 50 for @{'meet_refl}.
570 notation "'meet_comm'" non associative with precedence 50 for @{'meet_comm}.
571 notation "'meet_assoc'" non associative with precedence 50 for @{'meet_assoc}.
572 notation "'strong_extm'" non associative with precedence 50 for @{'strong_extm}.
573 notation "'le_to_eqm'" non associative with precedence 50 for @{'le_to_eqm}.
574 notation "'lem'" non associative with precedence 50 for @{'lem}.
575 notation "'join'" non associative with precedence 50 for @{'join}.
576 notation "'join_refl'" non associative with precedence 50 for @{'join_refl}.
577 notation "'join_comm'" non associative with precedence 50 for @{'join_comm}.
578 notation "'join_assoc'" non associative with precedence 50 for @{'join_assoc}.
579 notation "'strong_extj'" non associative with precedence 50 for @{'strong_extj}.
580 notation "'le_to_eqj'" non associative with precedence 50 for @{'le_to_eqj}.
581 notation "'lej'" non associative with precedence 50 for @{'lej}.
583 interpretation "Lattice meet" 'meet = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _)).
584 interpretation "Lattice meet_refl" 'meet_refl = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_mcarr.con _)).
585 interpretation "Lattice meet_comm" 'meet_comm = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_mcarr.con _)).
586 interpretation "Lattice meet_assoc" 'meet_assoc = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_mcarr.con _)).
587 interpretation "Lattice strong_extm" 'strong_extm = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_mcarr.con _)).
588 interpretation "Lattice le_to_eqm" 'le_to_eqm = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_mcarr.con _)).
589 interpretation "Lattice lem" 'lem = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_mcarr.con _)).
590 interpretation "Lattice join" 'join = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _)).
591 interpretation "Lattice join_refl" 'join_refl = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_jcarr.con _)).
592 interpretation "Lattice join_comm" 'join_comm = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_jcarr.con _)).
593 interpretation "Lattice join_assoc" 'join_assoc = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_jcarr.con _)).
594 interpretation "Lattice strong_extm" 'strong_extj = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_jcarr.con _)).
595 interpretation "Lattice le_to_eqj" 'le_to_eqj = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_jcarr.con _)).
596 interpretation "Lattice lej" 'lej = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_jcarr.con _)).
598 notation "'feq_jl'" non associative with precedence 50 for @{'feq_jl}.
599 notation "'feq_jr'" non associative with precedence 50 for @{'feq_jr}.
600 notation "'feq_ml'" non associative with precedence 50 for @{'feq_ml}.
601 notation "'feq_mr'" non associative with precedence 50 for @{'feq_mr}.
602 interpretation "Lattice feq_jl" 'feq_jl = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_jcarr.con _)).
603 interpretation "Lattice feq_jr" 'feq_jr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_jcarr.con _)).
604 interpretation "Lattice feq_ml" 'feq_ml = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_mcarr.con _)).
605 interpretation "Lattice feq_mr" 'feq_mr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_mcarr.con _)).
608 interpretation "Lattive meet le" 'leq a b =
609 (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice1.con _) a b).
611 interpretation "Lattive join le (aka ge)" 'geq a b =
612 (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice.con _) a b).
614 (* these coercions help unification, handmaking a bit of conversion
617 lemma le_to_ge: ∀l:lattice.∀a,b:l.a ≤ b → b ≥ a.
618 intros(l a b H); apply H;
621 lemma ge_to_le: ∀l:lattice.∀a,b:l.b ≥ a → a ≤ b.
622 intros(l a b H); apply H;
625 coercion cic:/matita/lattice/le_to_ge.con nocomposites.
626 coercion cic:/matita/lattice/ge_to_le.con nocomposites.