From 11f667afbb87725dd5e243d4b3717d19f584a481 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 4 Dec 2007 09:55:44 +0000 Subject: [PATCH] sandwitch theorem done --- helm/software/matita/dama/divisible_group.ma | 48 +++++-- helm/software/matita/dama/group.ma | 6 + helm/software/matita/dama/metric_lattice.ma | 96 +------------- .../matita/dama/ordered_divisible_group.ma | 117 +++-------------- .../software/matita/dama/premetric_lattice.ma | 8 +- helm/software/matita/dama/sandwich.ma | 123 ++++++++++++++++++ 6 files changed, 197 insertions(+), 201 deletions(-) create mode 100644 helm/software/matita/dama/sandwich.ma diff --git a/helm/software/matita/dama/divisible_group.ma b/helm/software/matita/dama/divisible_group.ma index 5c7025a9c..7d2eeed45 100644 --- a/helm/software/matita/dama/divisible_group.ma +++ b/helm/software/matita/dama/divisible_group.ma @@ -17,15 +17,15 @@ set "baseuri" "cic:/matita/divisible_group/". include "nat/orders.ma". include "group.ma". -let rec pow (G : abelian_group) (x : G) (n : nat) on n : G ≝ - match n with [ O ⇒ 0 | S m ⇒ x + pow ? x m]. +let rec gpow (G : abelian_group) (x : G) (n : nat) on n : G ≝ + match n with [ O ⇒ 0 | S m ⇒ x + gpow ? x m]. -interpretation "abelian group pow" 'exp x n = - (cic:/matita/divisible_group/pow.con _ x n). +interpretation "additive abelian group pow" 'times n x = + (cic:/matita/divisible_group/gpow.con _ x n). record dgroup : Type ≝ { dg_carr:> abelian_group; - dg_prop: ∀x:dg_carr.∀n:nat.∃y.pow ? y (S n) ≈ x + dg_prop: ∀x:dg_carr.∀n:nat.∃y.S n * y ≈ x }. lemma divide: ∀G:dgroup.G → nat → G. @@ -36,15 +36,15 @@ interpretation "divisible group divide" 'divide x n = (cic:/matita/divisible_group/divide.con _ x n). lemma divide_divides: - ∀G:dgroup.∀x:G.∀n. pow ? (x / n) (S n) ≈ x. + ∀G:dgroup.∀x:G.∀n. S n * (x / n) ≈ x. intro G; cases G; unfold divide; intros (x n); simplify; cases (f x n); simplify; exact H; qed. -lemma feq_pow: ∀G:dgroup.∀x,y:G.∀n.x≈y → pow ? x n ≈ pow ? y n. +lemma feq_pow: ∀G:dgroup.∀x,y:G.∀n.x≈y → n * x ≈ n * y. intros (G x y n H); elim n; [apply eq_reflexive] -simplify; apply (Eq≈ (x + (pow ? y n1)) H1); -apply (Eq≈ (y+pow ? y n1) H (eq_reflexive ??)); +simplify; apply (Eq≈ (x + (n1 * y)) H1); +apply (Eq≈ (y+n1*y) H (eq_reflexive ??)); qed. lemma div1: ∀G:dgroup.∀x:G.x/O ≈ x. @@ -53,3 +53,33 @@ cases (f x O); simplify; simplify in H; intro; apply H; apply (ap_rewl ???? (plus_comm ???)); apply (ap_rewl ???w (zero_neutral ??)); assumption; qed. + +lemma appow_ap: ∀G:dgroup.∀x,y:G.∀n.S n * x # S n * y → x # y. +intros 4 (G x y n); elim n; [2: + simplify in a; + cases (applus ????? a); [assumption] + apply f; assumption;] +apply (plus_cancr_ap ??? 0); assumption; +qed. + +lemma pluspow: ∀G:dgroup.∀x,y:G.∀n.n * (x+y) ≈ n * x + n * y. +intros (G x y n); elim n; [ + simplify; apply (Eq≈ 0 ? (zero_neutral ? 0)); apply eq_reflexive] +simplify; apply eq_sym; apply (Eq≈ (x+y+(n1*x+n1*y))); [ + apply (Eq≈ (x+(n1*x+(y+(n1*y))))); [ + apply eq_sym; apply plus_assoc;] + apply (Eq≈ (x+((n1*x+y+(n1*y))))); [ + apply feq_plusl; apply plus_assoc;] + apply (Eq≈ (x+(y+n1*x+n1*y))); [ + apply feq_plusl; apply feq_plusr; apply plus_comm;] + apply (Eq≈ (x+(y+(n1*x+n1*y)))); [ + apply feq_plusl; apply eq_sym; apply plus_assoc;] + apply plus_assoc;] +apply feq_plusl; apply eq_sym; assumption; +qed. + +lemma powzero: ∀G:dgroup.∀n.n*0 ≈ 0. [2: apply dg_carr; apply G] +intros; elim n; [simplify; apply eq_reflexive] +simplify; apply (Eq≈ ? (zero_neutral ??)); assumption; +qed. + diff --git a/helm/software/matita/dama/group.ma b/helm/software/matita/dama/group.ma index a04cd3bcc..b298e82e0 100644 --- a/helm/software/matita/dama/group.ma +++ b/helm/software/matita/dama/group.ma @@ -138,6 +138,12 @@ apply (ap_rewl ??? (y + (x + -x))); apply (ap_rewr ??? z (zero_neutral ??)); assumption]] qed. + +lemma applus: ∀E:abelian_group.∀x,a,y,b:E.x + a # y + b → x # y ∨ a # b. +intros; cases (ap_cotransitive ??? (y+a) a1); [left|right] +[apply (plus_cancr_ap ??? a)|apply (plus_cancl_ap ??? y)] +assumption; +qed. lemma plus_cancl: ∀G:abelian_group.∀y,z,x:G. x+y ≈ x+z → y ≈ z. intros 6 (G y z x E Ayz); apply E; apply fap_plusl; assumption; diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma index be9412087..cca643098 100644 --- a/helm/software/matita/dama/metric_lattice.ma +++ b/helm/software/matita/dama/metric_lattice.ma @@ -89,102 +89,18 @@ cut ( δx y+ δy z ≈ δ(y∨x) (y∨z)+ δ(y∧x) (y∧z)); [ apply (le_rewr ??? (δx y+ δy z)); [assumption] apply le_reflexive] lapply (le_to_eqm ??? Lxy) as Dxm; lapply (le_to_eqm ??? Lyz) as Dym; lapply (le_to_eqj ??? Lxy) as Dxj; lapply (le_to_eqj ??? Lyz) as Dyj; clear Lxy Lyz; -apply (Eq≈ (δ(x∧y) y + δy z)); [apply feq_plusr; apply (meq_l ????? Dxm);] -apply (Eq≈ (δ(x∧y) (y∧z) + δy z)); [apply feq_plusr; apply (meq_r ????? Dym);] -apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) z)); [apply feq_plusl; apply (meq_l ????? Dxj);] -apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) (y∨z))); [apply feq_plusl; apply (meq_r ????? Dyj);] +apply (Eq≈ (δ(x∧y) y + δy z) (meq_l ????? Dxm)); +apply (Eq≈ (δ(x∧y) (y∧z) + δy z) (meq_r ????? Dym)); +apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) z) (meq_l ????? Dxj)); +apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) (y∨z)) (meq_r ????? Dyj)); apply (Eq≈ ? (plus_comm ???)); -apply (Eq≈ (δ(y∨x) (y∨z)+ δ(x∧y) (y∧z))); [apply feq_plusr; apply (meq_l ????? (join_comm ???));] +apply (Eq≈ (δ(y∨x) (y∨z)+ δ(x∧y) (y∧z)) (meq_l ????? (join_comm ?x y))); apply feq_plusl; -apply (Eq≈ (δ(y∧x) (y∧z))); [apply (meq_l ????? (meet_comm ???));] +apply (Eq≈ (δ(y∧x) (y∧z)) (meq_l ????? (meet_comm ?x y))); apply eq_reflexive; qed. -include "sequence.ma". -include "nat/plus.ma". -lemma ltwl: ∀a,b,c:nat. b + a < c → a < c. -intros 3 (x y z); elim y (H z IH H); [apply H] -apply IH; apply lt_S_to_lt; apply H; -qed. - -lemma ltwr: ∀a,b,c:nat. a + b < c → a < c. -intros 3 (x y z); rewrite > sym_plus; apply ltwl; -qed. - - -definition d2s ≝ - λR.λml:mlattice R.λs:sequence ml.λk.λn. δ (s n) k. -(* -notation "s ⇝ 'Zero'" non associative with precedence 50 for @{'tends0 $s }. - -interpretation "tends to" 'tends s x = - (cic:/matita/sequence/tends0.con _ s). -*) - -alias symbol "leq" = "ordered sets less or equal than". -alias symbol "and" = "constructive and". -alias symbol "exists" = "constructive exists (Type)". -theorem carabinieri: - ∀R.∀ml:mlattice R.∀an,bn,xn:sequence ml. - (∀n. (an n ≤ xn n) ∧ (xn n ≤ bn n)) → - ∀x:ml. tends0 ? (d2s ? ml an x) → tends0 ? (d2s ? ml bn x) → - tends0 ? (d2s ? ml xn x). -intros (R ml an bn xn H x Ha Hb); unfold tends0 in Ha Hb ⊢ %. unfold d2s in Ha Hb ⊢ %. -intros (e He); -alias num (instance 0) = "natural number". -elim (Ha (e/2) (divide_preserves_lt ??? He)) (n1 H1); clear Ha; -elim (Hb (e/3) (divide_preserves_lt ??? He)) (n2 H2); clear Hb; -constructor 1; [apply (n1 + n2);] intros (n3 Hn3); -lapply (ltwr ??? Hn3) as Hn1n3; lapply (ltwl ??? Hn3) as Hn2n3; -elim (H1 ? Hn1n3) (H3 H4); elim (H2 ? Hn2n3) (H5 H6); clear Hn1n3 Hn2n3; -elim (H n3) (H7 H8); clear H H1 H2; -lapply (le_to_eqm ??? H7) as Dxm; lapply (le_to_eqj ??? H7) as Dym; -(* the main step *) -cut (δ (xn n3) x ≤ δ (bn n3) x + δ (an n3) x + δ (an n3) x); [2: - apply (le_transitive ???? (mtineq ???? (an n3))); - lapply (le_mtri ????? H7 H8); - lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? Hletin); - cut ( δ(an n3) (bn n3)+- δ(xn n3) (bn n3)≈( δ(an n3) (xn n3))); [2: - apply (Eq≈  (0 + δ(an n3) (xn n3)) ? (zero_neutral ??)); - apply (Eq≈  (δ(an n3) (xn n3) + 0) ? (plus_comm ???)); - apply (Eq≈  (δ(an n3) (xn n3) +  (-δ(xn n3) (bn n3) +  δ(xn n3) (bn n3))) ? (opp_inverse ??)); - apply (Eq≈  (δ(an n3) (xn n3) +  (δ(xn n3) (bn n3) + -δ(xn n3) (bn n3))) ? (plus_comm ?? (δ(xn n3) (bn n3)))); - apply (Eq≈  ? ? (eq_sym ??? (plus_assoc ????))); assumption;] clear Hletin1; - apply (le_rewl ???  ( δ(an n3) (xn n3)+ δ(an n3) x));[ - apply feq_plusr; apply msymmetric;] - apply (le_rewl ???  (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x));[ - apply feq_plusr; assumption;] - clear Hcut Hletin Dym Dxm H8 H7 H6 H5 H4 H3; - apply (le_rewl ??? (- δ(xn n3) (bn n3)+ δ(an n3) (bn n3)+δ(an n3) x));[ - apply feq_plusr; apply plus_comm;] - apply (le_rewl ??? (- δ(xn n3) (bn n3)+ (δ(an n3) (bn n3)+δ(an n3) x)) (plus_assoc ????)); - apply (le_rewl ??? ((δ(an n3) (bn n3)+δ(an n3) x)+- δ(xn n3) (bn n3)) (plus_comm ???)); - apply lew_opp; [apply mpositive] apply fle_plusr; - apply (le_rewr ???? (plus_comm ???)); - apply (le_rewr ??? ( δ(an n3) x+ δx (bn n3)) (msymmetric ????)); - apply mtineq;] -split; [ - apply (lt_le_transitive ????? (mpositive ????)); - split; elim He; [apply le_zero_x_to_le_opp_x_zero; assumption;] - cases t1; [ - left; apply exc_zero_opp_x_to_exc_x_zero; - apply (Ex≫ ? (eq_opp_opp_x_x ??));assumption;] - right; apply exc_opp_x_zero_to_exc_zero_x; - apply (Ex≪ ? (eq_opp_opp_x_x ??)); assumption;] -clear Dxm Dym H7 H8 Hn3 H5 H3 n1 n2; -apply (le_lt_transitive ???? ? (core1 ?? He)); -apply (le_transitive ???? Hcut); -apply (le_transitive ??  (e/3+ δ(an n3) x+ δ(an n3) x)); [ - repeat apply fle_plusr; cases H6; assumption;] -apply (le_transitive ??  (e/3+ e/2 + δ(an n3) x)); [ - apply fle_plusr; apply fle_plusl; cases H4; assumption;] -apply (le_transitive ??  (e/3+ e/2 + e/2)); [ - apply fle_plusl; cases H4; assumption;] -apply le_reflexive; -qed. - - (* 3.17 conclusione: δ x y ≈ 0 *) (* 3.20 conclusione: δ x y ≈ 0 *) (* 3.21 sup forte diff --git a/helm/software/matita/dama/ordered_divisible_group.ma b/helm/software/matita/dama/ordered_divisible_group.ma index 805cce956..cae552114 100644 --- a/helm/software/matita/dama/ordered_divisible_group.ma +++ b/helm/software/matita/dama/ordered_divisible_group.ma @@ -32,123 +32,44 @@ qed. coercion cic:/matita/ordered_divisible_group/todg_division.con. -lemma pow_lt: ∀G:todgroup.∀x:G.∀n.0 < x → 0 < x + pow ? x n. -intros (G x n H); elim n; [ - simplify; apply (lt_rewr ???? (plus_comm ???)); - apply (lt_rewr ???x (zero_neutral ??)); assumption] -simplify; apply (lt_transitive ?? (x+(x)\sup(n1))); [assumption] -apply flt_plusl; apply (lt_rewr ???? (plus_comm ???)); -apply (lt_rewl ??? (0 + (x \sup n1)) (eq_sym ??? (zero_neutral ??))); -apply (lt_rewl ???? (plus_comm ???)); -apply flt_plusl; assumption; -qed. - -lemma pow_ge: ∀G:todgroup.∀x:G.∀n.0 ≤ x → 0 ≤ pow ? x n. +lemma pow_ge: ∀G:todgroup.∀x:G.∀n.0 ≤ x → 0 ≤ n * x. intros (G x n); elim n; simplify; [apply le_reflexive] apply (le_transitive ???? H1); -apply (le_rewl ??? (0+(x\sup n1)) (zero_neutral ??)); +apply (le_rewl ??? (0+(n1*x)) (zero_neutral ??)); apply fle_plusr; assumption; qed. -lemma gt_pow: ∀G:todgroup.∀x:G.∀n.0 < pow ? x n → 0 < x. -intros 3; elim n; [ - simplify in l; cases (lt_coreflexive ?? l);] -simplify in l; -cut (0+0 sym_plus; simplify; apply (lt_rewl ??? (0+(y+y\sup n))); [ + rewrite > sym_plus; simplify; apply (lt_rewl ??? (0+(y+n*y))); [ apply eq_sym; apply zero_neutral] apply flt_plusr; assumption;] apply (lt_transitive ???? l); rewrite > sym_plus; simplify; rewrite > (sym_plus n); simplify; repeat apply flt_plusl; -apply (lt_rewl ???(0+y\sup(n1+n))); [apply eq_sym; apply zero_neutral] +apply (lt_rewl ???(0+(n1+n)*y)); [apply eq_sym; apply zero_neutral] apply flt_plusr; assumption; qed. -alias num (instance 0) = "natural number". -lemma core1: ∀G:todgroup.∀e:G.0 metric_space R; meet: pml_carr → pml_carr → pml_carr; join: pml_carr → pml_carr → pml_carr @@ -28,7 +28,7 @@ interpretation "valued lattice meet" 'and a b = interpretation "valued lattice join" 'or a b = (cic:/matita/premetric_lattice/join.con _ _ a b). -record premetric_lattice_props (R : ogroup) (ml : premetric_lattice_ R) : Prop ≝ { +record premetric_lattice_props (R : todgroup) (ml : premetric_lattice_ R) : Prop ≝ { prop1a: ∀a : ml.δ (a ∧ a) a ≈ 0; prop1b: ∀a : ml.δ (a ∨ a) a ≈ 0; prop2a: ∀a,b: ml. δ (a ∨ b) (b ∨ a) ≈ 0; @@ -40,14 +40,14 @@ record premetric_lattice_props (R : ogroup) (ml : premetric_lattice_ R) : Prop prop5: ∀a,b,c: ml. δ (a ∨ b) (a ∨ c) + δ (a ∧ b) (a ∧ c) ≤ δ b c }. -record pmlattice (R : ogroup) : Type ≝ { +record pmlattice (R : todgroup) : Type ≝ { carr :> premetric_lattice_ R; ispremetriclattice:> premetric_lattice_props R carr }. include "lattice.ma". -lemma lattice_of_pmlattice: ∀R: ogroup. pmlattice R → lattice. +lemma lattice_of_pmlattice: ∀R: todgroup. pmlattice R → lattice. intros (R pml); apply (mk_lattice (apart_of_metric_space ? pml)); [apply (join ? pml)|apply (meet ? pml) |3,4,5,6,7,8,9,10: intros (x y z); whd; intro H; whd in H; cases H (LE AP);] diff --git a/helm/software/matita/dama/sandwich.ma b/helm/software/matita/dama/sandwich.ma new file mode 100644 index 000000000..c83136c77 --- /dev/null +++ b/helm/software/matita/dama/sandwich.ma @@ -0,0 +1,123 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/sandwich/". + +include "nat/plus.ma". +include "nat/orders.ma". + +lemma ltwl: ∀a,b,c:nat. b + a < c → a < c. +intros 3 (x y z); elim y (H z IH H); [apply H] +apply IH; apply lt_S_to_lt; apply H; +qed. + +lemma ltwr: ∀a,b,c:nat. a + b < c → a < c. +intros 3 (x y z); rewrite > sym_plus; apply ltwl; +qed. + +include "sequence.ma". +include "metric_lattice.ma". + +lemma sandwich_ineq: ∀G:todgroup.∀e:G.0