(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/lattices/".
+include "excess.ma".
-include "excedence.ma".
+record semi_lattice_base : Type ≝ {
+ sl_carr:> apartness;
+ sl_op: sl_carr → sl_carr → sl_carr;
+ sl_op_refl: ∀x.sl_op x x ≈ x;
+ sl_op_comm: ∀x,y:sl_carr. sl_op x y ≈ sl_op y x;
+ sl_op_assoc: ∀x,y,z:sl_carr. sl_op x (sl_op y z) ≈ sl_op (sl_op x y) z;
+ sl_strong_extop: ∀x.strong_ext ? (sl_op x)
+}.
-record lattice : Type ≝ {
- l_carr:> apartness;
- join: l_carr → l_carr → l_carr;
- meet: l_carr → l_carr → l_carr;
- join_comm: ∀x,y:l_carr. join x y ≈ join y x;
- meet_comm: ∀x,y:l_carr. meet x y ≈ meet y x;
- join_assoc: ∀x,y,z:l_carr. join x (join y z) ≈ join (join y x) z;
- meet_assoc: ∀x,y,z:l_carr. meet x (meet y z) ≈ meet (meet y x) z;
- absorbjm: ∀f,g:l_carr. join f (meet f g) ≈ f;
- absorbmj: ∀f,g:l_carr. meet f (join f g) ≈ f
+notation "a \cross b" left associative with precedence 50 for @{ 'op $a $b }.
+interpretation "semi lattice base operation" 'op a b = (cic:/matita/lattice/sl_op.con _ a b).
+
+lemma excess_of_semi_lattice_base: semi_lattice_base → excess.
+intro l;
+apply mk_excess;
+[1: apply mk_excess_;
+ [1: apply mk_excess_dual_smart;
+
+ apply (mk_excess_base (sl_carr l));
+ [1: apply (λa,b:sl_carr l.a # (a ✗ b));
+ |2: unfold; intros 2 (x H); simplify in H;
+ lapply (Ap≪ ? (sl_op_refl ??) H) as H1; clear H;
+ apply (ap_coreflexive ?? H1);
+ |3: unfold; simplify; intros (x y z H1);
+ cases (ap_cotransitive ??? ((x ✗ z) ✗ y) H1) (H2 H2);[2:
+ lapply (Ap≪ ? (sl_op_comm ???) H2) as H21;
+ lapply (Ap≫ ? (sl_op_comm ???) H21) as H22; clear H21 H2;
+ lapply (sl_strong_extop ???? H22); clear H22;
+ left; apply ap_symmetric; assumption;]
+ cases (ap_cotransitive ??? (x ✗ z) H2) (H3 H3);[left;assumption]
+ right; lapply (Ap≫ ? (sl_op_assoc ????) H3) as H31;
+ apply (sl_strong_extop ???? H31);]
+
+ |2:
+ apply apartness_of_excess_base;
+
+ apply (mk_excess_base (sl_carr l));
+ [1: apply (λa,b:sl_carr l.a # (a ✗ b));
+ |2: unfold; intros 2 (x H); simplify in H;
+ lapply (Ap≪ ? (sl_op_refl ??) H) as H1; clear H;
+ apply (ap_coreflexive ?? H1);
+ |3: unfold; simplify; intros (x y z H1);
+ cases (ap_cotransitive ??? ((x ✗ z) ✗ y) H1) (H2 H2);[2:
+ lapply (Ap≪ ? (sl_op_comm ???) H2) as H21;
+ lapply (Ap≫ ? (sl_op_comm ???) H21) as H22; clear H21 H2;
+ lapply (sl_strong_extop ???? H22); clear H22;
+ left; apply ap_symmetric; assumption;]
+ cases (ap_cotransitive ??? (x ✗ z) H2) (H3 H3);[left;assumption]
+ right; lapply (Ap≫ ? (sl_op_assoc ????) H3) as H31;
+ apply (sl_strong_extop ???? H31);]
+
+ |3: apply refl_eq;]
+|2,3: intros (x y H); assumption;]
+qed.
+
+record semi_lattice : Type ≝ {
+ sl_exc:> excess;
+ sl_meet: sl_exc → sl_exc → sl_exc;
+ sl_meet_refl: ∀x.sl_meet x x ≈ x;
+ sl_meet_comm: ∀x,y. sl_meet x y ≈ sl_meet y x;
+ sl_meet_assoc: ∀x,y,z. sl_meet x (sl_meet y z) ≈ sl_meet (sl_meet x y) z;
+ sl_strong_extm: ∀x.strong_ext ? (sl_meet x);
+ sl_le_to_eqm: ∀x,y.x ≤ y → x ≈ sl_meet x y;
+ sl_lem: ∀x,y.(sl_meet x y) ≤ y
+}.
+
+interpretation "semi lattice meet" 'and a b = (cic:/matita/lattice/sl_meet.con _ a b).
+
+lemma sl_feq_ml: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
+intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
+intro H1; apply H; clear H; apply (sl_strong_extm ???? H1);
+qed.
+
+lemma sl_feq_mr: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (a ∧ c) ≈ (b ∧ c).
+intros (l a b c H);
+apply (Eq≈ ? (sl_meet_comm ???)); apply (Eq≈ ?? (sl_meet_comm ???));
+apply sl_feq_ml; assumption;
+qed.
+
+
+(*
+lemma semi_lattice_of_semi_lattice_base: semi_lattice_base → semi_lattice.
+intro slb; apply (mk_semi_lattice (excess_of_semi_lattice_base slb));
+[1: apply (sl_op slb);
+|2: intro x; apply (eq_trans (excess_of_semi_lattice_base slb)); [2:
+ apply (sl_op_refl slb);|1:skip] (sl_op slb x x)); ? (sl_op_refl slb x));
+
+ unfold excess_of_semi_lattice_base; simplify;
+ intro H; elim H;
+ [
+
+
+ lapply (ap_rewl (excess_of_semi_lattice_base slb) x ? (sl_op slb x x)
+ (eq_sym (excess_of_semi_lattice_base slb) ?? (sl_op_refl slb x)) t);
+ change in x with (sl_carr slb);
+ apply (Ap≪ (x ✗ x)); (sl_op_refl slb x));
+
+whd in H; elim H; clear H;
+ [ apply (ap_coreflexive (excess_of_semi_lattice_base slb) (x ✗ x) t);
+
+prelattice (excess_of_directed l_)); [apply (sl_op l_);]
+unfold excess_of_directed; try unfold apart_of_excess; simplify;
+unfold excl; simplify;
+[intro x; intro H; elim H; clear H;
+ [apply (sl_op_refl l_ x);
+ lapply (Ap≫ ? (sl_op_comm ???) t) as H; clear t;
+ lapply (sl_strong_extop l_ ??? H); apply ap_symmetric; assumption
+ | lapply (Ap≪ ? (sl_op_refl ?x) t) as H; clear t;
+ lapply (sl_strong_extop l_ ??? H); apply (sl_op_refl l_ x);
+ apply ap_symmetric; assumption]
+|intros 3 (x y H); cases H (H1 H2); clear H;
+ [lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ x y)) H1) as H; clear H1;
+ lapply (sl_strong_extop l_ ??? H) as H1; clear H;
+ lapply (Ap≪ ? (sl_op_comm ???) H1); apply (ap_coreflexive ?? Hletin);
+ |lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ y x)) H2) as H; clear H2;
+ lapply (sl_strong_extop l_ ??? H) as H1; clear H;
+ lapply (Ap≪ ? (sl_op_comm ???) H1);apply (ap_coreflexive ?? Hletin);]
+|intros 4 (x y z H); cases H (H1 H2); clear H;
+ [lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ x (sl_op l_ y z))) H1) as H; clear H1;
+ lapply (sl_strong_extop l_ ??? H) as H1; clear H;
+ lapply (Ap≪ ? (eq_sym ??? (sl_op_assoc ?x y z)) H1) as H; clear H1;
+ apply (ap_coreflexive ?? H);
+ |lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ (sl_op l_ x y) z)) H2) as H; clear H2;
+ lapply (sl_strong_extop l_ ??? H) as H1; clear H;
+ lapply (Ap≪ ? (sl_op_assoc ?x y z) H1) as H; clear H1;
+ apply (ap_coreflexive ?? H);]
+|intros (x y z H); elim H (H1 H1); clear H;
+ lapply (Ap≪ ? (sl_op_refl ??) H1) as H; clear H1;
+ lapply (sl_strong_extop l_ ??? H) as H1; clear H;
+ lapply (sl_strong_extop l_ ??? H1) as H; clear H1;
+ cases (ap_cotransitive ??? (sl_op l_ y z) H);[left|right|right|left] try assumption;
+ [apply ap_symmetric;apply (Ap≪ ? (sl_op_comm ???));
+ |apply (Ap≫ ? (sl_op_comm ???));
+ |apply ap_symmetric;] assumption;
+|intros 4 (x y H H1); apply H; clear H; elim H1 (H H);
+ lapply (Ap≪ ? (sl_op_refl ??) H) as H1; clear H;
+ lapply (sl_strong_extop l_ ??? H1) as H; clear H1;[2: apply ap_symmetric]
+ assumption
+|intros 3 (x y H);
+ cut (sl_op l_ x y ≈ sl_op l_ x (sl_op l_ y y)) as H1;[2:
+ intro; lapply (sl_strong_extop ???? a); apply (sl_op_refl l_ y);
+ apply ap_symmetric; assumption;]
+ lapply (Ap≪ ? (eq_sym ??? H1) H); apply (sl_op_assoc l_ x y y);
+ assumption; ]
+qed.
+*)
+
+(* ED(≰,≱) → EB(≰') → ED(≰',≱') *)
+lemma subst_excess_base: excess_dual → excess_base → excess_dual.
+intros; apply (mk_excess_dual_smart e1);
+qed.
+
+(* E_(ED(≰,≱),AP(#),c ED = c AP) → ED' → c DE' = c E_ → E_(ED',#,p) *)
+lemma subst_dual_excess: ∀e:excess_.∀e1:excess_dual.exc_carr e = exc_carr e1 → excess_.
+intros (e e1 p); apply (mk_excess_ e1 e); cases p; reflexivity;
+qed.
+
+(* E(E_,H1,H2) → E_' → H1' → H2' → E(E_',H1',H2') *)
+alias symbol "nleq" = "Excess excess_".
+lemma subst_excess_: ∀e:excess. ∀e1:excess_.
+ (∀y,x:e1. y # x → y ≰ x ∨ x ≰ y) →
+ (∀y,x:e1.y ≰ x ∨ x ≰ y → y # x) →
+ excess.
+intros (e e1 H1 H2); apply (mk_excess e1 H1 H2);
+qed.
+
+(* SL(E,M,H2-5(#),H67(≰)) → E' → c E = c E' → H67'(≰') → SL(E,M,p2-5,H67') *)
+lemma subst_excess:
+ ∀l:semi_lattice.
+ ∀e:excess.
+ ∀p:exc_ap l = exc_ap e.
+ (∀x,y:e.(le (exc_dual_base e)) x y → x ≈ (?(sl_meet l)) x y) →
+ (∀x,y:e.(le (exc_dual_base e)) ((?(sl_meet l)) x y) y) →
+ semi_lattice.
+[1,2:intro M;
+ change with ((λx.ap_carr x) e -> (λx.ap_carr x) e -> (λx.ap_carr x) e);
+ cases p; apply M;
+|intros (l e p H1 H2);
+ apply (mk_semi_lattice e);
+ [ change with ((λx.ap_carr x) e -> (λx.ap_carr x) e -> (λx.ap_carr x) e);
+ cases p; simplify; apply (sl_meet l);
+ |2: change in ⊢ (% → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_refl;
+ |3: change in ⊢ (% → % → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_comm;
+ |4: change in ⊢ (% → % → % → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_assoc;
+ |5: change in ⊢ (% → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_strong_extm;
+ |6: clear H2; apply H1;
+ |7: clear H1; apply H2;]]
+qed.
+
+lemma excess_of_excess_base: excess_base → excess.
+intro eb;
+apply mk_excess;
+ [apply (mk_excess_ (mk_excess_dual_smart eb));
+ [apply (apartness_of_excess_base eb);
+ |reflexivity]
+ |2,3: intros; assumption]
+qed.
+
+lemma subst_excess_base_in_semi_lattice:
+ ∀sl:semi_lattice.
+ ∀eb:excess_base.
+ ∀p:exc_carr sl = exc_carr eb.
+
+ mancano le 4 proprietà riscritte con p
+
+ semi_lattice.
+intros (l eb H); apply (subst_excess l);
+ [apply (subst_excess_ l);
+ [apply (subst_dual_excess l);
+ [apply (subst_excess_base l eb);
+ |apply H;]
+ | change in \vdash (% -> % -> ?) with (exc_carr eb);
+ letin xxx \def (ap2exc l); clearbody xxx;
+ change in xxx:(%→%→?) with (Type_OF_semi_lattice l);
+ whd in ⊢ (?→?→? (? %) ? ?→?);
+ unfold exc_ap;
+ simplify in ⊢ (?→?→%→?);
+
+intros 2;
+generalize in ⊢ (% -> ?); intro P;
+generalize in match x in ⊢ % as x;
+generalize in match y in ⊢ % as y; clear x y;
+
+
+cases H; simplify;
+
+
+cut (Πy:exc_carr eb
+.Πx:exc_carr eb
+ .match
+ (match H
+ in eq
+ return
+ λright_1:Type
+ .(λmatched:eq Type (Type_OF_excess_ (excess__OF_semi_lattice l)) right_1
+ .eq Type (Type_OF_excess_ (excess__OF_semi_lattice l)) right_1)
+ with
+ [refl_eq⇒refl_eq Type (Type_OF_excess_ (excess__OF_semi_lattice l))])
+ in eq
+ return
+ λright_1:Type
+ .(λmatched:eq Type (ap_carr (exc_ap (excess__OF_semi_lattice l))) right_1
+ .right_1→right_1→Type)
+ with
+ [refl_eq⇒ap_apart (exc_ap (excess__OF_semi_lattice l))] y x);[2:
+
+
+ change in ⊢ (?→?→? % ? ?→?) with (exc_ap_ (excess__OF_semi_lattice l));
+ generalize in match H in \vdash (? -> %); cases H;
+ cases H;
+
+
+normalize in ⊢ (?→?→?→? (? (? (? ? (% ? ?) ?)) ? ?) ?);
+whd in ⊢ (?→?→? % ? ?→?); change in ⊢ (?→?→? (? % ? ? ? ?) ? ?→?) with (exc_carr eb);
+cases H;
+ change in ⊢ (?→?→? % ? ?→?) with (exc_ap l);
+(subst_dual_excess (excess__OF_semi_lattice l)
+ (subst_excess_base (excess_dual_OF_semi_lattice l) eb) H)
+
+
+ unfold subst_excess_base;
+ unfold mk_excess_dual_smart;
+ unfold excess__OF_semi_lattice;
+ unfold excess_dual_OF_semi_lattice;
+ unfold excess_dual_OF_semi_lattice;
+
+ reflexivity]
+*)
+
+record lattice_ : Type ≝ {
+ latt_mcarr:> semi_lattice;
+ latt_jcarr_: semi_lattice;
+(* latt_with1: (subst_excess_
+ (subst_dual_excess
+ (subst_excess_base
+ (excess_dual_OF_excess (sl_exc latt_jcarr_))
+ (excess_base_OF_excess (sl_exc latt_mcarr))))) =
+ sl_exc latt_jcarr_;
+
+*)
+ latt_with1: excess_base_OF_excess1 (sl_exc latt_jcarr_) = excess_base_OF_excess (sl_exc latt_mcarr);
+ latt_with2: excess_base_OF_excess (sl_exc latt_jcarr_) = excess_base_OF_excess1 (sl_exc latt_mcarr);
+ latt_with3: apartness_OF_excess (sl_exc latt_jcarr_) = apartness_OF_excess (sl_exc latt_mcarr)
}.
+axiom FALSE: False.
+lemma latt_jcarr : lattice_ → semi_lattice.
+intro l;
+apply mk_semi_lattice;
+ [apply mk_excess;
+ [apply mk_excess_;
+ [apply (mk_excess_dual_smart l);
+ |apply (exc_ap l);
+ |reflexivity]
+ |unfold mk_excess_dual_smart; simplify;
+ intros (x y H); cases (ap2exc ??? H); [right|left] assumption;
+ |unfold mk_excess_dual_smart; simplify;
+ intros (x y H);cases H; apply exc2ap;[right|left] assumption;]]
+unfold mk_excess_dual_smart; simplify;
+[1: change with ((λx.ap_carr x) l → (λx.ap_carr x) l → (λx.ap_carr x) l);
+ simplify; unfold apartness_OF_lattice_;
+ cases (latt_with3 l); apply (sl_meet (latt_jcarr_ l));
+|2: change in ⊢ (%→?) with ((λx.ap_carr x) l); simplify;
+ unfold apartness_OF_lattice_;
+ cases (latt_with3 l); apply (sl_meet_refl (latt_jcarr_ l));
+|3: change in ⊢ (%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_;
+ cases (latt_with3 l); apply (sl_meet_comm (latt_jcarr_ l));
+|4: change in ⊢ (%→%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_;
+ cases (latt_with3 l); apply (sl_meet_assoc (latt_jcarr_ l));
+|5: change in ⊢ (%→%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_;
+ cases (latt_with3 l); apply (sl_strong_extm (latt_jcarr_ l));
+|7:
(*
-include "ordered_sets.ma".
-
-record lattice (C:Type) (join,meet:C→C→C) : Prop \def
- { (* abelian semigroup properties *)
- l_comm_j: symmetric ? join;
- l_associative_j: associative ? join;
- l_comm_m: symmetric ? meet;
- l_associative_m: associative ? meet;
- (* other properties *)
- l_adsorb_j_m: ∀f,g:C. join f (meet f g) = f;
- l_adsorb_m_j: ∀f,g:C. meet f (join f g) = f
- }.
-
-record lattice : Type \def
- { l_carrier:> Type;
- l_join: l_carrier→l_carrier→l_carrier;
- l_meet: l_carrier→l_carrier→l_carrier;
- l_lattice_properties:> is_lattice ? l_join l_meet
- }.
+unfold excess_base_OF_lattice_;
+ change in ⊢ (?→?→? ? (% ? ?) ?)
+ with (match latt_with3 l
+ in eq
+ return
+λright_1:apartness
+.(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right_1
+ .ap_carr right_1→ap_carr right_1→ap_carr right_1)
+ with
+[refl_eq⇒sl_meet (latt_jcarr_ l)]
+ : ?
+);
+ change in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?)
+ with ((λx.exc_carr x) (excess_base_OF_semi_lattice (latt_mcarr l)));
+ unfold excess_base_OF_lattice_ in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?);
+ simplify in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?);
+change in ⊢ (?→?→? ? (% ? ?) ?) with
+ (match refl_eq ? (excess__OF_semi_lattice (latt_mcarr l)) in eq
+ return (λR.λE:eq ? (excess_base_OF_semi_lattice (latt_mcarr l)) R.R → R → R)
+ with [refl_eq⇒
+ (match latt_with3 l in eq
+ return
+ (λright:apartness
+ .(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right
+ .ap_carr right→ap_carr right→ap_carr right))
+ with [refl_eq⇒ sl_meet (latt_jcarr_ l)]
+ :
+ exc_carr (excess_base_OF_semi_lattice (latt_mcarr l))
+ →exc_carr (excess_base_OF_semi_lattice (latt_mcarr l))
+ →exc_carr (excess_base_OF_semi_lattice (latt_mcarr l))
+ )
+ ]);
+ generalize in ⊢ (?→?→? ? (match % return ? with [_⇒?] ? ?) ?);
+ unfold excess_base_OF_lattice_ in ⊢ (? ? ? %→?);
+ cases (latt_with1 l);
+ change in ⊢ (?→?→?→? ? (match ? return ? with [_⇒(?:%→%->%)] ? ?) ?)
+ with ((λx.ap_carr x) (latt_mcarr l));
+ simplify in ⊢ (?→?→?→? ? (match ? return ? with [_⇒(?:%→%->%)] ? ?) ?);
+ cases (latt_with3 l);
+
+ change in ⊢ (? ? % ?→?) with ((λx.ap_carr x) l);
+ simplify in ⊢ (% → ?);
+ change in ⊢ (?→?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
+ with ((λx.ap_carr x) (apartness_OF_lattice_ l));
+ unfold apartness_OF_lattice_;
+ cases (latt_with3 l); simplify;
+ change in ⊢ (? ? ? %→%→%→?) with ((λx.exc_carr x) l);
+ unfold excess_base_OF_lattice_;
+ cases (latt_with1 l); simplify;
+ change in \vdash (? -> % -> % -> ?) with (exc_carr (excess_base_OF_semi_lattice (latt_jcarr_ l)));
+ change in ⊢ ((? ? % ?)→%→%→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
+ with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)));
+ simplify;
+ intro H;
+ unfold excess_base_OF_semi_lattice1;
+ unfold excess_base_OF_excess1;
+ unfold excess_base_OF_excess_1;
+ change
+*)
+
+change in ⊢ (?→?→? ? (% ? ?) ?) with
+ (match refl_eq ? (Type_OF_lattice_ l) in eq
+ return (λR.λE:eq ? (Type_OF_lattice_ l) R.R → R → R)
+ with [refl_eq⇒
+ match latt_with3 l in eq
+ return
+ (λright:apartness
+ .(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right
+ .ap_carr right→ap_carr right→ap_carr right))
+ with [refl_eq⇒ sl_meet (latt_jcarr_ l)]
+ ]);
+ generalize in ⊢ (?→?→? ? (match % return ? with [_⇒?] ? ?) ?);
+ change in ⊢ (? ? % ?→?) with ((λx.ap_carr x) l);
+ simplify in ⊢ (% → ?);
+ change in ⊢ (?→?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
+ with ((λx.ap_carr x) (apartness_OF_lattice_ l));
+ unfold apartness_OF_lattice_;
+ cases (latt_with3 l); simplify;
+ change in ⊢ (? ? ? %→%→%→?) with ((λx.exc_carr x) l);
+ unfold excess_base_OF_lattice_;
+ cases (latt_with1 l); simplify;
+ change in \vdash (? -> % -> % -> ?) with (exc_carr (excess_base_OF_semi_lattice (latt_jcarr_ l)));
+ change in ⊢ ((? ? % ?)→%→%→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
+ with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)));
+ simplify;
+ intro H;
+ change in ⊢ (?→?→%) with (le (mk_excess_base
+ ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
+ ((λx.exc_excess x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
+ ((λx.exc_coreflexive x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
+ ((λx.exc_cotransitive x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
+ ) (match H
+ in eq
+ return
+λR:Type
+.(λE:eq Type (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) R
+ .R→R→R)
+ with
+[refl_eq⇒sl_meet (latt_jcarr_ l)] x y) y);
+ simplify in ⊢ (?→?→? (? % ???) ? ?);
+ change in ⊢ (?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
+ with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)));
+ simplify in ⊢ (?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?);
+ lapply (match H in eq return
+ λright.λe:eq ? (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) right.
+
+∀x:right
+.∀y:right
+ .le
+ (mk_excess_base right ???)
+ (match e
+ in eq
+ return
+ λR:Type.(λE:eq Type (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) R.R→R→R)
+ with
+ [refl_eq⇒sl_meet (latt_jcarr_ l)] x y) y
+ with [refl_eq ⇒ ?]) as XX;
+ [cases e; apply (exc_excess (latt_jcarr_ l));
+ |unfold;cases e;simplify;apply (exc_coreflexive (latt_jcarr_ l));
+ |unfold;cases e;simplify;apply (exc_cotransitive (latt_jcarr_ l));
+ ||apply XX|
+ |apply XX;
+
+ simplify; apply (sl_lem);
+|elim FALSE]
+qed.
+
+
+
+
+coercion cic:/matita/lattice/latt_jcarr.con.
interpretation "Lattice meet" 'and a b =
- (cic:/matita/lattices/l_meet.con _ a b).
+ (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _) a b).
interpretation "Lattice join" 'or a b =
- (cic:/matita/lattices/l_join.con _ a b).
-
-definition le \def λL:lattice.λf,g:L. (f ∧ g) = f.
-
-definition ordered_set_of_lattice: lattice → ordered_set.
- intros (L);
- apply mk_ordered_set;
- [2: apply (le L)
- | skip
- | apply mk_is_order_relation;
- [ unfold reflexive;
- intros;
- unfold;
- rewrite < (l_adsorb_j_m ? ? ? L ? x) in ⊢ (? ? (? ? ? %) ?);
- rewrite > l_adsorb_m_j;
- [ reflexivity
- | apply (l_lattice_properties L)
- ]
- | intros;
- unfold transitive;
- unfold le;
- intros;
- rewrite < H;
- rewrite > (l_associative_m ? ? ? L);
- rewrite > H1;
- reflexivity
- | unfold antisimmetric;
- unfold le;
- intros;
- rewrite < H;
- rewrite > (l_comm_m ? ? ? L);
- assumption
- ]
- ]
+ (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _) a b).
+
+record lattice : Type ≝ {
+ latt_carr:> lattice_;
+ absorbjm: ∀f,g:latt_carr. (f ∨ (f ∧ g)) ≈ f;
+ absorbmj: ∀f,g:latt_carr. (f ∧ (f ∨ g)) ≈ f
+}.
+
+notation "'meet'" non associative with precedence 50 for @{'meet}.
+notation "'meet_refl'" non associative with precedence 50 for @{'meet_refl}.
+notation "'meet_comm'" non associative with precedence 50 for @{'meet_comm}.
+notation "'meet_assoc'" non associative with precedence 50 for @{'meet_assoc}.
+notation "'strong_extm'" non associative with precedence 50 for @{'strong_extm}.
+notation "'le_to_eqm'" non associative with precedence 50 for @{'le_to_eqm}.
+notation "'lem'" non associative with precedence 50 for @{'lem}.
+notation "'join'" non associative with precedence 50 for @{'join}.
+notation "'join_refl'" non associative with precedence 50 for @{'join_refl}.
+notation "'join_comm'" non associative with precedence 50 for @{'join_comm}.
+notation "'join_assoc'" non associative with precedence 50 for @{'join_assoc}.
+notation "'strong_extj'" non associative with precedence 50 for @{'strong_extj}.
+notation "'le_to_eqj'" non associative with precedence 50 for @{'le_to_eqj}.
+notation "'lej'" non associative with precedence 50 for @{'lej}.
+
+interpretation "Lattice meet" 'meet = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice meet_refl" 'meet_refl = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice meet_comm" 'meet_comm = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice meet_assoc" 'meet_assoc = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice strong_extm" 'strong_extm = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice le_to_eqm" 'le_to_eqm = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice lem" 'lem = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice join" 'join = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice join_refl" 'join_refl = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice join_comm" 'join_comm = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice join_assoc" 'join_assoc = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice strong_extm" 'strong_extj = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice le_to_eqj" 'le_to_eqj = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice lej" 'lej = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_jcarr.con _)).
+
+notation "'feq_jl'" non associative with precedence 50 for @{'feq_jl}.
+notation "'feq_jr'" non associative with precedence 50 for @{'feq_jr}.
+notation "'feq_ml'" non associative with precedence 50 for @{'feq_ml}.
+notation "'feq_mr'" non associative with precedence 50 for @{'feq_mr}.
+interpretation "Lattice feq_jl" 'feq_jl = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice feq_jr" 'feq_jr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice feq_ml" 'feq_ml = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice feq_mr" 'feq_mr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_mcarr.con _)).
+
+
+interpretation "Lattive meet le" 'leq a b =
+ (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice1.con _) a b).
+
+interpretation "Lattive join le (aka ge)" 'geq a b =
+ (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice.con _) a b).
+
+(* these coercions help unification, handmaking a bit of conversion
+ over an open term
+*)
+lemma le_to_ge: ∀l:lattice.∀a,b:l.a ≤ b → b ≥ a.
+intros(l a b H); apply H;
+qed.
+
+lemma ge_to_le: ∀l:lattice.∀a,b:l.b ≥ a → a ≤ b.
+intros(l a b H); apply H;
qed.
-coercion cic:/matita/lattices/ordered_set_of_lattice.con.
-*)
\ No newline at end of file
+coercion cic:/matita/lattice/le_to_ge.con nocomposites.
+coercion cic:/matita/lattice/ge_to_le.con nocomposites.
\ No newline at end of file