include "excess.ma".
-record directed : Type ≝ {
- dir_carr: apartness;
- dir_op: dir_carr → dir_carr → dir_carr;
- dir_op_refl: ∀x.dir_op x x ≈ x;
- dir_op_comm: ∀x,y:dir_carr. dir_op x y ≈ dir_op y x;
- dir_op_assoc: ∀x,y,z:dir_carr. dir_op x (dir_op y z) ≈ dir_op (dir_op x y) z;
- dir_strong_extop: ∀x.strong_ext ? (dir_op x)
+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)
}.
-definition excl ≝
- λl:directed.λa,b:dir_carr l.ap_apart (dir_carr l) a (dir_op l a b).
-
-lemma excess_of_directed: directed → excess.
-intro l; apply (mk_excess (dir_carr l) (excl l));
-[ intro x; unfold; intro H; unfold in H; apply (ap_coreflexive (dir_carr l) x);
- apply (ap_rewr ??? (dir_op l x x) (dir_op_refl ? x)); assumption;
-| intros 3 (x y z); unfold excl; intro H;
- cases (ap_cotransitive ??? (dir_op l (dir_op l x z) y) H) (H1 H2); [2:
- left; apply ap_symmetric; apply (dir_strong_extop ? y);
- apply (ap_rewl ???? (dir_op_comm ???));
- apply (ap_rewr ???? (dir_op_comm ???));
- assumption]
- cases (ap_cotransitive ??? (dir_op l x z) H1) (H2 H3); [left; assumption]
- right; apply (dir_strong_extop ? x); apply (ap_rewr ???? (dir_op_assoc ????));
- assumption]
+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_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 prelattice : Type ≝ {
- pl_carr:> excess;
- meet: pl_carr → pl_carr → pl_carr;
+record semi_lattice : Type ≝ {
+ sl_exc:> excess;
+ meet: sl_exc → sl_exc → sl_exc;
meet_refl: ∀x.meet x x ≈ x;
- meet_comm: ∀x,y:pl_carr. meet x y ≈ meet y x;
- meet_assoc: ∀x,y,z:pl_carr. meet x (meet y z) ≈ meet (meet x y) z;
+ meet_comm: ∀x,y. meet x y ≈ meet y x;
+ meet_assoc: ∀x,y,z. meet x (meet y z) ≈ meet (meet x y) z;
strong_extm: ∀x.strong_ext ? (meet x);
le_to_eqm: ∀x,y.x ≤ y → x ≈ meet x y;
lem: ∀x,y.(meet x y) ≤ y
}.
-interpretation "prelattice meet" 'and a b =
- (cic:/matita/lattice/meet.con _ a b).
+interpretation "semi lattice meet" 'and a b = (cic:/matita/lattice/meet.con _ a b).
-lemma feq_ml: ∀ml:prelattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
+lemma 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 (strong_extm ???? H1);
qed.
-lemma feq_mr: ∀ml:prelattice.∀a,b,c:ml. a ≈ b → (a ∧ c) ≈ (b ∧ c).
+lemma feq_mr: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (a ∧ c) ≈ (b ∧ c).
intros (l a b c H);
apply (Eq≈ ? (meet_comm ???)); apply (Eq≈ ?? (meet_comm ???));
apply feq_ml; assumption;
qed.
-lemma prelattice_of_directed: directed → prelattice.
-intro l_; apply (mk_prelattice (excess_of_directed l_)); [apply (dir_op l_);]
+
+(*
+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 (dir_op_refl l_ x);
- lapply (Ap≫ ? (dir_op_comm ???) t) as H; clear t;
- lapply (dir_strong_extop l_ ??? H); apply ap_symmetric; assumption
- | lapply (Ap≪ ? (dir_op_refl ?x) t) as H; clear t;
- lapply (dir_strong_extop l_ ??? H); apply (dir_op_refl l_ x);
+ [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≪ ? (dir_op_refl ? (dir_op l_ x y)) H1) as H; clear H1;
- lapply (dir_strong_extop l_ ??? H) as H1; clear H;
- lapply (Ap≪ ? (dir_op_comm ???) H1); apply (ap_coreflexive ?? Hletin);
- |lapply (Ap≪ ? (dir_op_refl ? (dir_op l_ y x)) H2) as H; clear H2;
- lapply (dir_strong_extop l_ ??? H) as H1; clear H;
- lapply (Ap≪ ? (dir_op_comm ???) H1);apply (ap_coreflexive ?? Hletin);]
+ [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≪ ? (dir_op_refl ? (dir_op l_ x (dir_op l_ y z))) H1) as H; clear H1;
- lapply (dir_strong_extop l_ ??? H) as H1; clear H;
- lapply (Ap≪ ? (eq_sym ??? (dir_op_assoc ?x y z)) H1) as H; clear H1;
+ [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≪ ? (dir_op_refl ? (dir_op l_ (dir_op l_ x y) z)) H2) as H; clear H2;
- lapply (dir_strong_extop l_ ??? H) as H1; clear H;
- lapply (Ap≪ ? (dir_op_assoc ?x y z) H1) as H; clear H1;
+ |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≪ ? (dir_op_refl ??) H1) as H; clear H1;
- lapply (dir_strong_extop l_ ??? H) as H1; clear H;
- lapply (dir_strong_extop l_ ??? H1) as H; clear H1;
- cases (ap_cotransitive ??? (dir_op l_ y z) H);[left|right|right|left] try assumption;
- [apply ap_symmetric;apply (Ap≪ ? (dir_op_comm ???));
- |apply (Ap≫ ? (dir_op_comm ???));
+ 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≪ ? (dir_op_refl ??) H) as H1; clear H;
- lapply (dir_strong_extop l_ ??? H1) as H; clear H1;[2: apply ap_symmetric]
+ 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 (dir_op l_ x y ≈ dir_op l_ x (dir_op l_ y y)) as H1;[2:
- intro; lapply (dir_strong_extop ???? a); apply (dir_op_refl l_ y);
+ 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 (dir_op_assoc l_ x y y);
+ lapply (Ap≪ ? (eq_sym ??? H1) H); apply (sl_op_assoc l_ x y y);
assumption; ]
qed.
+*)
+
record lattice_ : Type ≝ {
- latt_mcarr:> prelattice;
- latt_jcarr_: prelattice;
- latt_with: pl_carr latt_jcarr_ = dual_exc (pl_carr latt_mcarr)
+ latt_mcarr:> semi_lattice;
+ latt_jcarr_: semi_lattice;
+ latt_with: sl_exc latt_jcarr_ = dual_exc (sl_exc latt_mcarr)
}.
-lemma latt_jcarr : lattice_ → prelattice.
+lemma latt_jcarr : lattice_ → semi_lattice.
intro l;
-apply (mk_prelattice (dual_exc l)); unfold excess_OF_lattice_;
+apply (mk_semi_lattice (dual_exc l));
+unfold excess_OF_lattice_;
cases (latt_with l); simplify;
[apply meet|apply meet_refl|apply meet_comm|apply meet_assoc|
apply strong_extm| apply le_to_eqm|apply lem]
projects / helm.git / blobdiff