]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/dama/dama_duality/lattice.ma
notational update in ground_2 and basic_2
[helm.git] / matita / matita / contribs / dama / dama_duality / 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 55 for @{ 'op $a $b }.
27 interpretation "semi lattice base operation" 'op a b = (sl_op ? 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 = (sl_meet ? 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 definition hole ≝ λT:Type.λx:T.x.
184
185 notation < "\ldots" non associative with precedence 55 for @{'hole}.
186 interpretation "hole" 'hole = (hole ? ?).
187
188 (* SL(E,M,H2-5(#),H67(≰)) → E' → c E = c E' → H67'(≰') → SL(E,M,p2-5,H67') *)
189 lemma subst_excess: 
190   ∀l:semi_lattice.
191   ∀e:excess. 
192   ∀p:exc_ap l = exc_ap e.
193   (∀x,y:e.(le (exc_dual_base e)) x y → x ≈ (?(sl_meet l)) x y) →
194   (∀x,y:e.(le (exc_dual_base e)) ((?(sl_meet l)) x y) y) → 
195   semi_lattice.
196 [1,2:intro M;
197  change with ((λx.ap_carr x) e -> (λx.ap_carr x) e -> (λx.ap_carr x) e);
198  cases p; apply M;
199 |intros (l e p H1 H2);
200  apply (mk_semi_lattice e);
201    [ change with ((λx.ap_carr x) e -> (λx.ap_carr x) e -> (λx.ap_carr x) e);
202      cases p; simplify; apply (sl_meet l);
203    |2: change in ⊢ (% → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_refl;
204    |3: change in ⊢ (% → % → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_comm;
205    |4: change in ⊢ (% → % → % → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_assoc;  
206    |5: change in ⊢ (% → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_strong_extm;
207    |6: clear H2; apply hole; apply H1;
208    |7: clear H1; apply hole; apply H2;]]
209 qed.
210
211 lemma excess_of_excess_base: excess_base → excess.
212 intro eb;
213 apply mk_excess;
214   [apply (mk_excess_ (mk_excess_dual_smart eb));
215     [apply (apartness_of_excess_base eb);
216     |reflexivity]
217   |2,3: intros; assumption]
218 qed. 
219
220 lemma subst_excess_preserves_aprtness:
221   ∀l:semi_lattice.
222   ∀e:excess.
223   ∀p,H1,H2. 
224   exc_ap l = exc_ap (subst_excess l e p H1 H2).
225 intros; 
226 unfold subst_excess;
227 simplify; assumption;
228 qed.
229
230
231 lemma subst_excess__preserves_aprtness:
232   ∀l:excess.
233   ∀e:excess_base.
234   ∀p,H1,H2. 
235   exc_ap l = apartness_OF_excess (subst_excess_ l (subst_dual_excess l (subst_excess_base l e) p) H1 H2).
236 intros 3; (unfold subst_excess_; unfold subst_dual_excess; unfold subst_excess_base; unfold exc_ap; unfold mk_excess_dual_smart; simplify);
237 (unfold subst_excess_base in p; unfold mk_excess_dual_smart in p; simplify in p);
238 intros; cases p;
239 reflexivity;
240 qed.
241
242 lemma subst_excess_base_in_excess_:
243   ∀d:excess_.
244   ∀eb:excess_base.
245   ∀p:exc_carr d = exc_carr eb.
246   excess_.
247 intros (e_ eb);
248 apply (subst_dual_excess e_);
249   [apply (subst_excess_base e_ eb);
250   |assumption]
251 qed.
252
253 lemma subst_excess_base_in_excess:
254   ∀d:excess.
255   ∀eb:excess_base.
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) →
259   excess.
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;
279    intros; assumption;]
280 qed.    
281
282 lemma tech1: ∀e:excess.
283  ∀eb:excess_base.
284  ∀p,H1,H2.
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;
291 qed.
292
293 lemma tech2: 
294  ∀e:excess_.∀eb.∀p.
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;
297 qed.
298   
299 (*
300 lemma eq_fap:
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;
304 qed.
305 *)
306
307 lemma subst_excess_base_in_excess_preserves_apartness:
308  ∀e:excess.
309  ∀eb:excess_base.
310  ∀H,H1,H2.
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 );
319 reflexivity;
320 qed.
321  
322  
323  
324 alias symbol "nleq" = "Excess base excess".
325 lemma subst_excess_base_in_semi_lattice: 
326   ∀sl:semi_lattice.
327   ∀eb:excess_base.
328   ∀p:exc_carr sl = exc_carr eb.
329   (∀y1,x1:eb. (?(ap_apart sl)) y1  x1 → y1 ≰ x1 ∨ x1 ≰ y1) →
330   (∀y2,x2:eb.y2 ≰ x2 ∨ x2 ≰ y2 →  (?(ap_apart sl)) y2 x2) →
331   (∀x3,y3:eb.(le eb) x3 y3 → (?(eq sl)) x3 ((?(sl_meet sl)) x3 y3)) →
332   (∀x4,y4:eb.(le eb) ((?(sl_meet sl)) x4 y4) y4) → 
333   semi_lattice.
334 [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;]
335 intros (sl eb H H1 H2 H3 H4); 
336 apply (subst_excess sl);
337   [apply (subst_excess_base_in_excess sl eb H H1 H2);
338   |apply subst_excess_base_in_excess_preserves_apartness;
339   |change in ⊢ (%→%→?) with ((λx.ap_carr x) (subst_excess_base_in_excess (sl_exc sl) eb H H1 H2)); simplify;
340    intros 3 (x y LE); clear H3 LE;
341    generalize in match x as x; generalize in match y as y;
342    generalize in match H1 as H1;generalize in match H2 as H2;
343    clear x y H1 H2 H4; STOP
344  
345    apply (match H return λr:Type.λm:Type_OF_semi_lattice sl=r.
346    ∀H2:(Πy2:exc_carr eb
347                .Πx2:exc_carr eb
348                 .Or (exc_excess eb y2 x2) (exc_excess eb x2 y2)
349                  →match H
350                      in eq
351                      return 
352                     λright_1:Type
353                     .(λmatched:eq Type (Type_OF_semi_lattice sl) right_1
354                       .right_1→right_1→Type)
355                      with 
356                     [refl_eq⇒ap_apart (apartness_OF_semi_lattice sl)] y2 x2)
357 .∀H1:Πy1:exc_carr eb
358                .Πx1:exc_carr eb
359                 .match H
360                   in eq
361                   return 
362                  λright_1:Type
363                  .(λmatched:eq Type (Type_OF_semi_lattice sl) right_1
364                    .right_1→right_1→Type)
365                   with 
366                  [refl_eq⇒ap_apart (apartness_OF_semi_lattice sl)] y1 x1
367                  →Or (exc_excess eb y1 x1) (exc_excess eb x1 y1)
368  .∀y:ap_carr
369               (apartness_OF_excess (subst_excess_base_in_excess (sl_exc sl) eb H H1 H2))
370   .∀x:ap_carr
371                (apartness_OF_excess
372                 (subst_excess_base_in_excess (sl_exc sl) eb H H1 H2))
373    .eq
374     (apartness_OF_excess (subst_excess_base_in_excess (sl_exc sl) eb H H1 H2)) x
375     (match 
376      subst_excess_base_in_excess_preserves_apartness (sl_exc sl) eb H H1 H2
377       in eq
378       return 
379      λright_1:apartness
380      .(λmatched:eq apartness (apartness_OF_semi_lattice sl) right_1
381        .ap_carr right_1→ap_carr right_1→ap_carr right_1)
382       with 
383      [refl_eq⇒sl_meet sl] x y)
384    
385    with [ refl_eq ⇒ ?]);
386    
387    
388    cases (subst_excess_base_in_excess_preserves_apartness sl eb H H1 H2);
389    cases H;
390    cases (subst_excess_base_in_excess_preserves_apartness (sl_exc sl) eb H H1 H2); simplify;
391    change in x:(%) with (exc_carr eb);
392    change in y:(%) with (exc_carr eb);
393    generalize in match OK; generalize in match x as x; generalize in match y as y;
394    cases H; simplify; (* funge, ma devo fare 2 rewrite in un colpo solo *)
395    *) 
396   |cases FALSE;
397   ] 
398 qed.
399
400 record lattice_ : Type ≝ {
401   latt_mcarr:> semi_lattice;
402   latt_jcarr_: semi_lattice;
403   W1:?; W2:?; W3:?; W4:?; W5:?;
404   latt_with1: latt_jcarr_ = subst_excess_base_in_semi_lattice latt_jcarr_
405     (excess_base_OF_semi_lattice latt_mcarr) W1 W2 W3 W4 W5   
406 }.
407
408 lemma latt_jcarr : lattice_ → semi_lattice.
409 intro l; apply (subst_excess_base_in_semi_lattice (latt_jcarr_ l) (excess_base_OF_semi_lattice (latt_mcarr l)) (W1 l) (W2 l) (W3 l) (W4 l) (W5 l));
410 qed.
411     
412 coercion cic:/matita/lattice/latt_jcarr.con.
413
414 interpretation "Lattice meet" 'and a b =
415  (sl_meet (latt_mcarr _) a b).  
416
417 interpretation "Lattice join" 'or a b =
418  (sl_meet (latt_jcarr _) a b).  
419
420 record lattice : Type ≝ {
421   latt_carr:> lattice_;
422   absorbjm: ∀f,g:latt_carr. (f ∨ (f ∧ g)) ≈ f;
423   absorbmj: ∀f,g:latt_carr. (f ∧ (f ∨ g)) ≈ f
424 }.
425
426 notation "'meet'"        non associative with precedence 55 for @{'meet}.
427 notation "'meet_refl'"   non associative with precedence 55 for @{'meet_refl}.
428 notation "'meet_comm'"   non associative with precedence 55 for @{'meet_comm}.
429 notation "'meet_assoc'"  non associative with precedence 55 for @{'meet_assoc}.
430 notation "'strong_extm'" non associative with precedence 55 for @{'strong_extm}.
431 notation "'le_to_eqm'"   non associative with precedence 55 for @{'le_to_eqm}.
432 notation "'lem'"         non associative with precedence 55 for @{'lem}.
433 notation "'join'"        non associative with precedence 55 for @{'join}.
434 notation "'join_refl'"   non associative with precedence 55 for @{'join_refl}.
435 notation "'join_comm'"   non associative with precedence 55 for @{'join_comm}.
436 notation "'join_assoc'"  non associative with precedence 55 for @{'join_assoc}.
437 notation "'strong_extj'" non associative with precedence 55 for @{'strong_extj}.
438 notation "'le_to_eqj'"   non associative with precedence 55 for @{'le_to_eqj}.
439 notation "'lej'"         non associative with precedence 55 for @{'lej}.
440
441 interpretation "Lattice meet"        'meet        = (sl_meet (latt_mcarr ?)).
442 interpretation "Lattice meet_refl"   'meet_refl   = (sl_meet_refl (latt_mcarr ?)).
443 interpretation "Lattice meet_comm"   'meet_comm   = (sl_meet_comm (latt_mcarr ?)).
444 interpretation "Lattice meet_assoc"  'meet_assoc  = (sl_meet_assoc (latt_mcarr ?)).
445 interpretation "Lattice strong_extm" 'strong_extm = (sl_strong_extm (latt_mcarr ?)).
446 interpretation "Lattice le_to_eqm"   'le_to_eqm   = (sl_le_to_eqm (latt_mcarr ?)).
447 interpretation "Lattice lem"         'lem         = (sl_lem (latt_mcarr ?)).
448 interpretation "Lattice join"        'join        = (sl_meet (latt_jcarr ?)).
449 interpretation "Lattice join_refl"   'join_refl   = (sl_meet_refl (latt_jcarr ?)).
450 interpretation "Lattice join_comm"   'join_comm   = (sl_meet_comm (latt_jcarr ?)).
451 interpretation "Lattice join_assoc"  'join_assoc  = (sl_meet_assoc (latt_jcarr ?)).
452 interpretation "Lattice strong_extm" 'strong_extj = (sl_strong_extm (latt_jcarr ?)).
453 interpretation "Lattice le_to_eqj"   'le_to_eqj   = (sl_le_to_eqm (latt_jcarr ?)).
454 interpretation "Lattice lej"         'lej         = (sl_lem (latt_jcarr ?)).
455
456 notation "'feq_jl'" non associative with precedence 55 for @{'feq_jl}.
457 notation "'feq_jr'" non associative with precedence 55 for @{'feq_jr}.
458 notation "'feq_ml'" non associative with precedence 55 for @{'feq_ml}.
459 notation "'feq_mr'" non associative with precedence 55 for @{'feq_mr}.
460 interpretation "Lattice feq_jl" 'feq_jl = (sl_feq_ml (latt_jcarr ?)).
461 interpretation "Lattice feq_jr" 'feq_jr = (sl_feq_mr (latt_jcarr ?)).
462 interpretation "Lattice feq_ml" 'feq_ml = (sl_feq_ml (latt_mcarr ?)).
463 interpretation "Lattice feq_mr" 'feq_mr = (sl_feq_mr (latt_mcarr ?)).
464
465
466 interpretation "Lattive meet le" 'leq a b = (le (excess_OF_lattice1 ?) a b).
467
468 interpretation "Lattive join le (aka ge)" 'geq a b =
469  (le (excess_OF_lattice _) a b).
470
471 (* these coercions help unification, handmaking a bit of conversion 
472    over an open term 
473 *)
474 lemma le_to_ge: ∀l:lattice.∀a,b:l.a ≤ b → b ≥ a.
475 intros(l a b H); apply H;
476 qed.
477
478 lemma ge_to_le: ∀l:lattice.∀a,b:l.b ≥ a → a ≤ b.
479 intros(l a b H); apply H;
480 qed.
481
482 coercion cic:/matita/lattice/le_to_ge.con nocomposites.
483 coercion cic:/matita/lattice/ge_to_le.con nocomposites.