From b3dd479a0a36aeea948dcea09336fe8dfec1462d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 16 Jan 2008 12:04:06 +0000 Subject: [PATCH] yes! the lattice_(#) -> prelattice(<) -> lattice(< -> #) works! --- helm/software/matita/dama/excess.ma | 4 +- helm/software/matita/dama/infsup.ma | 53 ++++++- helm/software/matita/dama/lattice.ma | 148 ++++++++++++------ helm/software/matita/dama/metric_lattice.ma | 18 +-- helm/software/matita/dama/metric_space.ma | 2 +- .../matita/dama/sandwich_corollary.ma | 6 +- 6 files changed, 159 insertions(+), 72 deletions(-) diff --git a/helm/software/matita/dama/excess.ma b/helm/software/matita/dama/excess.ma index c7d31c229..55f531a9b 100644 --- a/helm/software/matita/dama/excess.ma +++ b/helm/software/matita/dama/excess.ma @@ -51,7 +51,7 @@ record apartness : Type ≝ { ap_cotransitive: cotransitive ? ap_apart }. -notation "a break # b" non associative with precedence 50 for @{ 'apart $a $b}. +notation "hvbox(a break # b)" non associative with precedence 50 for @{ 'apart $a $b}. interpretation "apartness" 'apart x y = (cic:/matita/excess/ap_apart.con _ x y). @@ -73,7 +73,7 @@ coercion cic:/matita/excess/apart_of_excess.con. definition eq ≝ λA:apartness.λa,b:A. ¬ (a # b). -notation "a break ≈ b" non associative with precedence 50 for @{ 'napart $a $b}. +notation "hvbox(a break ≈ b)" non associative with precedence 50 for @{ 'napart $a $b}. interpretation "alikeness" 'napart a b = (cic:/matita/excess/eq.con _ a b). diff --git a/helm/software/matita/dama/infsup.ma b/helm/software/matita/dama/infsup.ma index 05b497cc5..7ba29dd1b 100644 --- a/helm/software/matita/dama/infsup.ma +++ b/helm/software/matita/dama/infsup.ma @@ -25,8 +25,8 @@ definition infimum ≝ (* 3.20 *) lemma supremum_uniq: - ∀R.∀ml:mlattice R.∀xn:sequence ml.increasing ? xn → (* BUG again the wrong coercion is chosen *) - ∀x,y:apart_of_metric_space ? ml.supremum ?? xn x → supremum ?? xn y → x ≈ y. + ∀R.∀ml:mlattice R.∀xn:sequence ml.increasing ? xn → + ∀x,y:ml.supremum ?? xn x → supremum ?? xn y → δ x y ≈ 0. intros (R ml xn Hxn x y Sx Sy); elim (Sx Hxn) (_ Hx); elim (Sy Hxn) (_ Hy); apply (tends_uniq ?? xn ?? Hx Hy); @@ -42,6 +42,18 @@ definition ank ≝ [ O ⇒ (shift ?? xn k) O | S n1 ⇒ (shift ?? xn k) (S n1) ∧ ank_aux n1] in ank_aux. + +notation < "'a'\sup k" non associative with precedence 50 for + @{ 'ank $x $k }. + +interpretation "ank" 'ank x k = + (cic:/matita/infsup/ank.con _ _ x k). + +notation < "'a'(k \atop n)" non associative with precedence 50 for + @{ 'ank2 $x $k $n }. + +interpretation "ank2" 'ank2 x k n = + (cic:/matita/infsup/ank.con _ _ x k n). definition bnk ≝ λR.λml:mlattice R.λxn:sequence ml.λk:nat. @@ -52,14 +64,14 @@ definition bnk ≝ in bnk_aux. lemma ank_decreasing: - ∀R.∀ml:mlattice R.∀xn:sequence ml.∀m.decreasing ? (ank ?? xn m). -intros (R ml xn m); unfold; intro n; simplify; apply lem; + ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k.decreasing ? (ank ?? xn k). +intros (R ml xn k); unfold; intro n; simplify; apply lem; qed. (* 3.26 *) lemma ankS: ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat. - ((ank ?? xn k) (S n)) ≈ (xn k ∧ ank ?? xn (S k) n). + ((ank ?? xn k) (S n)) ≈ (xn k ∧ ank ?? xn (S k) n). intros (R ml xn k n); elim n; simplify; [apply meet_comm] simplify in H; apply (Eq≈ ? (feq_ml ???? (H))); clear H; apply (Eq≈ ? (meet_assoc ????)); @@ -68,6 +80,37 @@ apply feq_mr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %)))); simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %)))); apply meet_comm; qed. + +(* 3.27 *) +lemma foo: + ∀R.∀ml:mlattice R.∀xn:sequence ml. + ∀alpha:sequence ml. (∀k.strong_inf ml (ank ?? xn k) (alpha k)) → + increasing ml alpha. +intros (R ml xn alpha H); unfold strong_inf in H; unfold lower_bound in H; unfold; +intro n; +letin H2 ≝ (λk.ankS ?? xn k n); clearbody H2; +cut (∀k.((xn k) ∧ (ank ?? xn (S k) n)) ≤ (ank ?? xn (S k) n)) as H3; [2:intro k; apply lem;] +cut (∀k.(ank ?? xn k (S n)) ≤ (ank ?? xn (S k) n)) as H4; [2: + intro k; apply (le_transitive ml ???? (H3 ?)); + apply (Le≪ ? (H2 k)); + +elim (H (S n)) (H4 H5); intro H6; elim (H5 ? H6) (m Hm); +lapply (H4 m) as H7; + + clear H5 H6; + + + +lapply (H n) as H1; clear H; elim H1 (LB H); clear H1; +lapply (LB (S n)) as H1; clear LB; +lapply (ankS ?? xn n n) as H2; + +lapply (Le≪ (xn n∧ank R ml xn (S n) n) H2); + +cases H (LB H1); clear H; + + + \ No newline at end of file diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma index 66f14b942..9b163378e 100644 --- a/helm/software/matita/dama/lattice.ma +++ b/helm/software/matita/dama/lattice.ma @@ -12,74 +12,127 @@ (* *) (**************************************************************************) - - include "excess.ma". -record lattice : Type ≝ { - l_carr:> apartness; - join: l_carr → l_carr → l_carr; - meet: l_carr → l_carr → l_carr; - join_refl: ∀x.join x x ≈ x; - meet_refl: ∀x.meet x x ≈ x; - 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 x y) z; - meet_assoc: ∀x,y,z:l_carr. meet x (meet y z) ≈ meet (meet x y) z; - absorbjm: ∀f,g:l_carr. join f (meet f g) ≈ f; - absorbmj: ∀f,g:l_carr. meet f (join f g) ≈ f; - strong_extj: ∀x.strong_ext ? (join x); - strong_extm: ∀x.strong_ext ? (meet x) +record lattice_ : Type ≝ { + l_carr: apartness; + l_meet: l_carr → l_carr → l_carr; + l_meet_refl: ∀x.l_meet x x ≈ x; + l_meet_comm: ∀x,y:l_carr. l_meet x y ≈ l_meet y x; + l_meet_assoc: ∀x,y,z:l_carr. l_meet x (l_meet y z) ≈ l_meet (l_meet x y) z; + l_strong_extm: ∀x.strong_ext ? (l_meet x) }. -interpretation "Lattice meet" 'and a b = - (cic:/matita/lattice/meet.con _ a b). +definition excl ≝ λl:lattice_.λa,b:l_carr l.ap_apart (l_carr l) a (l_meet l a b). -interpretation "Lattice join" 'or a b = - (cic:/matita/lattice/join.con _ a b). - -definition excl ≝ λl:lattice.λa,b:l.a # (a ∧ b). - -lemma excess_of_lattice: lattice → excess. -intro l; apply (mk_excess l (excl l)); -[ intro x; unfold; intro H; unfold in H; apply (ap_coreflexive l x); - apply (ap_rewr ??? (x∧x) (meet_refl l x)); assumption; +lemma excess_of_lattice_: lattice_ → excess. +intro l; apply (mk_excess (l_carr l) (excl l)); +[ intro x; unfold; intro H; unfold in H; apply (ap_coreflexive (l_carr l) x); + apply (ap_rewr ??? (l_meet l x x) (l_meet_refl ? x)); assumption; | intros 3 (x y z); unfold excl; intro H; - cases (ap_cotransitive ??? (x∧z∧y) H) (H1 H2); [2: - left; apply ap_symmetric; apply (strong_extm ? y); - apply (ap_rewl ???? (meet_comm ???)); - apply (ap_rewr ???? (meet_comm ???)); + cases (ap_cotransitive ??? (l_meet l (l_meet l x z) y) H) (H1 H2); [2: + left; apply ap_symmetric; apply (l_strong_extm ? y); + apply (ap_rewl ???? (l_meet_comm ???)); + apply (ap_rewr ???? (l_meet_comm ???)); assumption] - cases (ap_cotransitive ??? (x∧z) H1) (H2 H3); [left; assumption] - right; apply (strong_extm ? x); apply (ap_rewr ???? (meet_assoc ????)); + cases (ap_cotransitive ??? (l_meet l x z) H1) (H2 H3); [left; assumption] + right; apply (l_strong_extm ? x); apply (ap_rewr ???? (l_meet_assoc ????)); assumption] qed. -coercion cic:/matita/lattice/excess_of_lattice.con. +(* coercion cic:/matita/lattice/excess_of_lattice_.con. *) + +record prelattice : Type ≝ { + pl_carr:> excess; + meet: pl_carr → pl_carr → pl_carr; + 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; + 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 "Lattice meet" 'and a b = + (cic:/matita/lattice/meet.con _ a b). -lemma feq_ml: ∀ml:lattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b). +lemma feq_ml: ∀ml:prelattice.∀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:lattice.∀a,b,c:ml. a ≈ b → (a ∧ c) ≈ (b ∧ c). +lemma feq_mr: ∀ml:prelattice.∀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_lattice_: lattice_ → prelattice. +intro l_; apply (mk_prelattice (excess_of_lattice_ l_)); [apply (l_meet l_);] +unfold excess_of_lattice_; try unfold apart_of_excess; simplify; +unfold excl; simplify; +[intro x; intro H; elim H; clear H; + [apply (l_meet_refl l_ x); + lapply (Ap≫ ? (l_meet_comm ???) t) as H; clear t; + lapply (l_strong_extm l_ ??? H); apply ap_symmetric; assumption + | lapply (Ap≪ ? (l_meet_refl ?x) t) as H; clear t; + lapply (l_strong_extm l_ ??? H); apply (l_meet_refl l_ x); + apply ap_symmetric; assumption] +|intros 3 (x y H); cases H (H1 H2); clear H; + [lapply (Ap≪ ? (l_meet_refl ? (l_meet l_ x y)) H1) as H; clear H1; + lapply (l_strong_extm l_ ??? H) as H1; clear H; + lapply (Ap≪ ? (l_meet_comm ???) H1); apply (ap_coreflexive ?? Hletin); + |lapply (Ap≪ ? (l_meet_refl ? (l_meet l_ y x)) H2) as H; clear H2; + lapply (l_strong_extm l_ ??? H) as H1; clear H; + lapply (Ap≪ ? (l_meet_comm ???) H1);apply (ap_coreflexive ?? Hletin);] +|intros 4 (x y z H); cases H (H1 H2); clear H; + [lapply (Ap≪ ? (l_meet_refl ? (l_meet l_ x (l_meet l_ y z))) H1) as H; clear H1; + lapply (l_strong_extm l_ ??? H) as H1; clear H; + lapply (Ap≪ ? (eq_sym ??? (l_meet_assoc ?x y z)) H1) as H; clear H1; + apply (ap_coreflexive ?? H); + |lapply (Ap≪ ? (l_meet_refl ? (l_meet l_ (l_meet l_ x y) z)) H2) as H; clear H2; + lapply (l_strong_extm l_ ??? H) as H1; clear H; + lapply (Ap≪ ? (l_meet_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≪ ? (l_meet_refl ??) H1) as H; clear H1; + lapply (l_strong_extm l_ ??? H) as H1; clear H; + lapply (l_strong_extm l_ ??? H1) as H; clear H1; + cases (ap_cotransitive ??? (l_meet l_ y z) H);[left|right|right|left] try assumption; + [apply ap_symmetric;apply (Ap≪ ? (l_meet_comm ???)); + |apply (Ap≫ ? (l_meet_comm ???)); + |apply ap_symmetric;] assumption; +|intros 4 (x y H H1); apply H; clear H; elim H1 (H H); + lapply (Ap≪ ? (l_meet_refl ??) H) as H1; clear H; + lapply (l_strong_extm l_ ??? H1) as H; clear H1;[2: apply ap_symmetric] + assumption +|intros 3 (x y H); + cut (l_meet l_ x y ≈ l_meet l_ x (l_meet l_ y y)) as H1;[2: + intro; lapply (l_strong_extm ???? a); apply (l_meet_refl l_ y); + apply ap_symmetric; assumption;] + lapply (Ap≪ ? (eq_sym ??? H1) H); apply (l_meet_assoc l_ x y y); + assumption; ] +qed. + +record lattice : Type ≝ { + lat_carr:> prelattice; + join: lat_carr → lat_carr → lat_carr; + join_refl: ∀x.join x x ≈ x; + join_comm: ∀x,y:lat_carr. join x y ≈ join y x; + join_assoc: ∀x,y,z:lat_carr. join x (join y z) ≈ join (join x y) z; + absorbjm: ∀f,g:lat_carr. join f (meet ? f g) ≈ f; + absorbmj: ∀f,g:lat_carr. meet ? f (join f g) ≈ f; + strong_extj: ∀x.strong_ext ? (join x) +}. + +interpretation "Lattice join" 'or a b = + (cic:/matita/lattice/join.con _ a b). lemma feq_jl: ∀ml: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_extj ???? H1); qed. -lemma le_to_eqm: ∀ml:lattice.∀a,b:ml. a ≤ b → a ≈ (a ∧ b). -intros (l a b H); - unfold le in H; unfold excess_of_lattice in H; - unfold excl in H; simplify in H; -unfold eq; assumption; -qed. - lemma le_to_eqj: ∀ml:lattice.∀a,b:ml. a ≤ b → b ≈ (a ∨ b). intros (l a b H); lapply (le_to_eqm ??? H) as H1; lapply (feq_jl ??? b H1) as H2; @@ -88,12 +141,3 @@ apply (Eq≈ (b∨a∧b) ? H2); clear H1 H2 H; apply (Eq≈ (b∨(b∧a)) ? (feq_jl ???? (meet_comm ???))); apply eq_sym; apply absorbjm; qed. - -lemma lem: ∀ml:lattice.∀a,b:ml.(a ∧ b) ≤ b. -intros; unfold le; unfold excess_of_lattice; unfold excl; simplify; -intro H; apply (ap_coreflexive ? (a∧b)); -apply (Ap≫ (a∧(b∧b)) (feq_ml ???? (meet_refl ? b))); -apply (Ap≫ ? (meet_assoc ????)); assumption; -qed. - - diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma index 40f3d41eb..a2d257342 100644 --- a/helm/software/matita/dama/metric_lattice.ma +++ b/helm/software/matita/dama/metric_lattice.ma @@ -12,18 +12,16 @@ (* *) (**************************************************************************) - - include "metric_space.ma". include "lattice.ma". record mlattice_ (R : todgroup) : Type ≝ { ml_mspace_: metric_space R; - ml_lattice_: lattice; - ml_with_: ms_carr ? ml_mspace_ = l_carr ml_lattice_; - ml_with2_: l_carr ml_lattice_ = apart_of_metric_space ? ml_mspace_ + ml_lattice:> lattice; + ml_with_: ms_carr ? ml_mspace_ = apart_of_excess (pl_carr ml_lattice) }. +(* lemma ml_lattice: ∀R.mlattice_ R → lattice. intros (R ml); apply (mk_lattice (apart_of_metric_space ? (ml_mspace_ ? ml))); try unfold eq; cases (ml_with2_ ? ml); @@ -36,13 +34,15 @@ cases (ml_with2_ ? ml); qed. coercion cic:/matita/metric_lattice/ml_lattice.con. +*) lemma ml_mspace: ∀R.mlattice_ R → metric_space R. -intros (R ml); apply (mk_metric_space R ml); +intros (R ml); apply (mk_metric_space R (apart_of_excess ml)); +unfold apartness_OF_mlattice_; +[rewrite < (ml_with_ ? ml); apply (metric ? (ml_mspace_ ? ml))] cases (ml_with_ ? ml); simplify; -[apply (metric ? (ml_mspace_ ? ml));|apply (mpositive ? (ml_mspace_ ? ml)); -|apply (mreflexive ? (ml_mspace_ ? ml));|apply (msymmetric ? (ml_mspace_ ? ml)); -|apply (mtineq ? (ml_mspace_ ? ml))] +[apply (mpositive ? (ml_mspace_ ? ml));|apply (mreflexive ? (ml_mspace_ ? ml)); +|apply (msymmetric ? (ml_mspace_ ? ml));|apply (mtineq ? (ml_mspace_ ? ml))] qed. coercion cic:/matita/metric_lattice/ml_mspace.con. diff --git a/helm/software/matita/dama/metric_space.ma b/helm/software/matita/dama/metric_space.ma index 595407de8..bd16b2bd6 100644 --- a/helm/software/matita/dama/metric_space.ma +++ b/helm/software/matita/dama/metric_space.ma @@ -47,7 +47,7 @@ intros (R ms); apply (mk_apartness ? (apart_metric ? ms)); unfold apart_metric; apply (lt0plus_orlt ????? LT0); apply mpositive;] qed. -coercion cic:/matita/metric_space/apart_of_metric_space.con. +(* coercion cic:/matita/metric_space/apart_of_metric_space.con. *) lemma ap2delta: ∀R.∀m:metric_space R.∀x,y:m.x#y → 0 < δ x y. intros 2 (R m); cases m 0; simplify; intros; assumption; qed. diff --git a/helm/software/matita/dama/sandwich_corollary.ma b/helm/software/matita/dama/sandwich_corollary.ma index 8dafe1f63..72da08236 100644 --- a/helm/software/matita/dama/sandwich_corollary.ma +++ b/helm/software/matita/dama/sandwich_corollary.ma @@ -19,13 +19,13 @@ include "metric_lattice.ma". (* 3.17 *) lemma tends_uniq: ∀R.∀ml:mlattice R.∀xn:sequence ml. - ∀x,y:apart_of_metric_space ? ml. + ∀x,y:ml. (* BUG: it inserts a compesoed coercion instead of an hand made one, what to do? prefer the human made one or allow to kill a coercion? *) - xn ⇝ x → xn ⇝ y → x ≈ y. + xn ⇝ x → xn ⇝ y → δ x y ≈ 0. intros (R ml xn x y H1 H2); unfold tends0 in H1 H2; unfold d2s in H1 H2; -intro Axy; lapply (ap2delta R ml x y Axy) as ge0; +intro Axy; lapply (ap_le_to_lt ??? (ap_symmetric ??? Axy) (mpositive ? ml ??)) as ge0; cases (H1 (δ x y/1) (divide_preserves_lt ??? ge0)) (n1 Hn1); clear H1; cases (H2 (δ x y/1) (divide_preserves_lt ??? ge0)) (n2 Hn2); clear H2; letin N ≝ (S (n2 + n1)); -- 2.39.2