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.
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);
165 record lattice_ : Type ≝ {
166 latt_mcarr:> semi_lattice;
167 latt_jcarr_: semi_lattice;
168 latt_with: sl_exc latt_jcarr_ = dual_exc (sl_exc latt_mcarr)
171 lemma latt_jcarr : lattice_ → semi_lattice.
173 apply (mk_semi_lattice (dual_exc l));
174 unfold excess_OF_lattice_;
175 cases (latt_with l); simplify;
176 [apply sl_meet|apply sl_meet_refl|apply sl_meet_comm|apply sl_meet_assoc|
177 apply sl_strong_extm| apply sl_le_to_eqm|apply sl_lem]
180 coercion cic:/matita/lattice/latt_jcarr.con.
182 interpretation "Lattice meet" 'and a b =
183 (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _) a b).
185 interpretation "Lattice join" 'or a b =
186 (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _) a b).
188 record lattice : Type ≝ {
189 latt_carr:> lattice_;
190 absorbjm: ∀f,g:latt_carr. (f ∨ (f ∧ g)) ≈ f;
191 absorbmj: ∀f,g:latt_carr. (f ∧ (f ∨ g)) ≈ f
194 notation "'meet'" non associative with precedence 50 for @{'meet}.
195 notation "'meet_refl'" non associative with precedence 50 for @{'meet_refl}.
196 notation "'meet_comm'" non associative with precedence 50 for @{'meet_comm}.
197 notation "'meet_assoc'" non associative with precedence 50 for @{'meet_assoc}.
198 notation "'strong_extm'" non associative with precedence 50 for @{'strong_extm}.
199 notation "'le_to_eqm'" non associative with precedence 50 for @{'le_to_eqm}.
200 notation "'lem'" non associative with precedence 50 for @{'lem}.
201 notation "'join'" non associative with precedence 50 for @{'join}.
202 notation "'join_refl'" non associative with precedence 50 for @{'join_refl}.
203 notation "'join_comm'" non associative with precedence 50 for @{'join_comm}.
204 notation "'join_assoc'" non associative with precedence 50 for @{'join_assoc}.
205 notation "'strong_extj'" non associative with precedence 50 for @{'strong_extj}.
206 notation "'le_to_eqj'" non associative with precedence 50 for @{'le_to_eqj}.
207 notation "'lej'" non associative with precedence 50 for @{'lej}.
209 interpretation "Lattice meet" 'meet = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _)).
210 interpretation "Lattice meet_refl" 'meet_refl = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_mcarr.con _)).
211 interpretation "Lattice meet_comm" 'meet_comm = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_mcarr.con _)).
212 interpretation "Lattice meet_assoc" 'meet_assoc = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_mcarr.con _)).
213 interpretation "Lattice strong_extm" 'strong_extm = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_mcarr.con _)).
214 interpretation "Lattice le_to_eqm" 'le_to_eqm = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_mcarr.con _)).
215 interpretation "Lattice lem" 'lem = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_mcarr.con _)).
216 interpretation "Lattice join" 'join = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _)).
217 interpretation "Lattice join_refl" 'join_refl = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_jcarr.con _)).
218 interpretation "Lattice join_comm" 'join_comm = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_jcarr.con _)).
219 interpretation "Lattice join_assoc" 'join_assoc = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_jcarr.con _)).
220 interpretation "Lattice strong_extm" 'strong_extj = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_jcarr.con _)).
221 interpretation "Lattice le_to_eqj" 'le_to_eqj = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_jcarr.con _)).
222 interpretation "Lattice lej" 'lej = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_jcarr.con _)).
224 notation "'feq_jl'" non associative with precedence 50 for @{'feq_jl}.
225 notation "'feq_jr'" non associative with precedence 50 for @{'feq_jr}.
226 notation "'feq_ml'" non associative with precedence 50 for @{'feq_ml}.
227 notation "'feq_mr'" non associative with precedence 50 for @{'feq_mr}.
228 interpretation "Lattice feq_jl" 'feq_jl = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_jcarr.con _)).
229 interpretation "Lattice feq_jr" 'feq_jr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_jcarr.con _)).
230 interpretation "Lattice feq_ml" 'feq_ml = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_mcarr.con _)).
231 interpretation "Lattice feq_mr" 'feq_mr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_mcarr.con _)).
234 interpretation "Lattive meet le" 'leq a b =
235 (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice1.con _) a b).
237 interpretation "Lattive join le (aka ge)" 'geq a b =
238 (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice.con _) a b).
240 (* these coercions help unification, handmaking a bit of conversion
243 lemma le_to_ge: ∀l:lattice.∀a,b:l.a ≤ b → b ≥ a.
244 intros(l a b H); apply H;
247 lemma ge_to_le: ∀l:lattice.∀a,b:l.b ≥ a → a ≤ b.
248 intros(l a b H); apply H;
251 coercion cic:/matita/lattice/le_to_ge.con nocomposites.
252 coercion cic:/matita/lattice/ge_to_le.con nocomposites.