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.
(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.
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.
+
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;
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
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<x+(x)\sup(n1));[2:
- apply (lt_rewl ??? 0 (zero_neutral ??)); assumption].
-cases (ltplus_orlt ????? Hcut); [assumption]
-apply f; assumption;
-qed.
-
-lemma gt_pow2: ∀G:dgroup.∀x,y:G.∀n.pow ? x n + pow ? y n ≈ pow ? (x+y) n.
-intros (G x y n); elim n; [apply (Eq≈ 0 (zero_neutral ??)); apply eq_reflexive]
-simplify; apply (Eq≈ (x+y+((x)\sup(n1)+(y)\sup(n1)))); [
- apply (Eq≈ (x+((x)\sup(n1)+(y+(y)\sup(n1))))); [
- apply eq_sym; apply plus_assoc;]
- apply (Eq≈ (x+((x)\sup(n1)+y+(y)\sup(n1)))); [
- apply feq_plusl; apply plus_assoc;]
- apply (Eq≈ (x+(y+(x)\sup(n1)+(y)\sup(n1)))); [
- apply feq_plusl; apply feq_plusr; apply plus_comm;]
- apply (Eq≈ (x+(y+((x)\sup(n1)+(y)\sup(n1))))); [
- apply feq_plusl; apply eq_sym; apply plus_assoc;]
- apply plus_assoc;]
-apply feq_plusl; assumption;
-qed.
-
-lemma xxxx: ∀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 pow_gt0: ∀G:todgroup.∀y:G.∀n.0 < y → 0 < pow ? y (S n).
-intros (G y n H); elim n; [apply (lt_rewr ??? (0+y) (plus_comm ???)); apply (lt_rewr ??? y (zero_neutral ??)); apply H]
-simplify; apply (lt_rewl ? 0 ? (0+0) (zero_neutral ? 0));
-apply ltplus; assumption;
-qed.
-
-lemma divide_preserves_lt: ∀G:todgroup.∀e:G.∀n.0<e → 0 < e/n.
-intros; elim n; [apply (lt_rewr ???? (div1 ??));assumption]
-unfold divide; elim (dg_prop G e (S n1)); simplify; simplify in f;
-apply (gt_pow ?? (S (S n1))); apply (lt_rewr ???? f); assumption;
-qed.
-
-
-lemma bar1: ∀G:togroup.∀x,y:G.∀n.pow ? x (S n) # pow ? y (S n) → x # y.
-intros 4 (G x y n); elim n; [2:
- simplify in a;
- cases (xxxx ????? a); [assumption]
- apply f; assumption;]
-apply (plus_cancr_ap ??? 0); assumption;
-qed.
-
-
-lemma lt_suplt: ∀G:todgroup.∀x,y:G.∀n.
-x < y → x\sup (S n) < y\sup (S n).
+lemma lt_ltpow: ∀G:todgroup.∀x,y:G.∀n. x < y → S n * x < S n * y.
intros; elim n; [simplify; apply flt_plusr; assumption]
simplify; apply (ltplus); [assumption] assumption;
qed.
-lemma suplt_lt: ∀G:todgroup.∀x,y:G.∀n. x\sup (S n) < y\sup (S n) → x < y.
+lemma ltpow_lt: ∀G:todgroup.∀x,y:G.∀n. S n * x < S n * y → x < y.
intros 4; elim n; [apply (plus_cancr_lt ??? 0); assumption]
simplify in l; cases (ltplus_orlt ????? l); [assumption]
apply f; assumption;
qed.
-lemma supeqplus_lt: ∀G:todgroup.∀x,y:G.∀n,m.
- 0<x → 0<y → x\sup (S n) ≈ y\sup (S (n+S m)) → y < x.
-intros (G x y n m H1 H2 H3); apply (suplt_lt ??? n); apply (lt_rewr ???? H3);
+lemma divide_preserves_lt: ∀G:todgroup.∀e:G.∀n.0<e → 0 < e/n.
+intros; elim n; [apply (lt_rewr ???? (div1 ??));assumption]
+unfold divide; elim (dg_prop G e (S n1)); simplify; simplify in f;
+apply (ltpow_lt ??? (S n1)); simplify; apply (lt_rewr ???? f);
+apply (lt_rewl ???? (zero_neutral ??));
+apply (lt_rewl ???? (zero_neutral ??));
+apply (lt_rewl ???? (powzero ?n1));
+assumption;
+qed.
+
+lemma poweqplus_lt: ∀G:todgroup.∀x,y:G.∀n,m.
+ 0<x → 0<y → S n * x ≈ S (n + S m) * y → y < x.
+intros (G x y n m H1 H2 H3); apply (ltpow_lt ??? n); apply (lt_rewr ???? H3);
clear H3; elim m; [
- rewrite > 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<e → e/3 + e/2 + e/2 < e.
-intro G; cases G; unfold divide; intro e;
-cases (dg_prop (mk_todgroup todg_order todg_division_ H) e 3) 0;
-cases (dg_prop (mk_todgroup todg_order todg_division_ H) e 2) 0; simplify;
-intro H3;
-cut (0<w1\sup 3); [2: apply (lt_rewr ???? H2); assumption]
-cut (0<w\sup 4); [2: apply (lt_rewr ???? H1); assumption]
-lapply (gt_pow ??? Hcut) as H4;
-lapply (gt_pow ??? Hcut1) as H5;
-cut (w<w1);[2: apply (supeqplus_lt ??? 2 O); try assumption; apply (Eq≈ ? H2 H1);]
-apply (plus_cancr_lt ??? w1);
-apply (lt_rewl ??? (w+e)); [
- apply (Eq≈ (w+w1\sup 3) ? H2);
- apply (Eq≈ (w+w1+(w1+w1)) (plus_assoc ??w1 w1));
- apply (Eq≈ (w+(w1+(w1+w1))) (plus_assoc ?w w1 ?));
- simplify; repeat apply feq_plusl; apply eq_sym;
- apply (Eq≈ ? (plus_comm ???)); apply zero_neutral;]
-apply (lt_rewl ???? (plus_comm ???));
-apply flt_plusl; assumption;
-qed.
-
-
-
include "metric_space.ma".
-record premetric_lattice_ (R : ogroup) : Type ≝ {
+record premetric_lattice_ (R : todgroup) : Type ≝ {
pml_carr:> metric_space R;
meet: pml_carr → pml_carr → pml_carr;
join: pml_carr → pml_carr → pml_carr
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;
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);]
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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<e → e/3 + e/2 + e/2 < e.
+intro G; cases G; unfold divide; intro e;
+alias num (instance 0) = "natural number".
+cases (dg_prop (mk_todgroup todg_order todg_division_ H) e 3) 0;
+cases (dg_prop (mk_todgroup todg_order todg_division_ H) e 2) 0; simplify;
+intro H3;
+cut (0<w1) as H4; [2:
+ apply (ltpow_lt ??? 2); apply (lt_rewr ???? H2);
+ apply (lt_rewl ???? (powzero ? 3)); assumption]
+cut (0<w) as H5; [2:
+ apply (ltpow_lt ??? 3); apply (lt_rewr ???? H1);
+ apply (lt_rewl ???? (powzero ? 4)); assumption]
+cut (w<w1) as H6; [2:
+ apply (poweqplus_lt ??? 2 O); try assumption; apply (Eq≈ ? H2 H1);]
+apply (plus_cancr_lt ??? w1);
+apply (lt_rewl ??? (w+e)); [
+ apply (Eq≈ (w+3*w1) ? H2);
+ apply (Eq≈ (w+w1+(w1+w1)) (plus_assoc ??w1 w1));
+ apply (Eq≈ (w+(w1+(w1+w1))) (plus_assoc ?w w1 ?));
+ simplify; repeat apply feq_plusl; apply eq_sym;
+ apply (Eq≈ ? (plus_comm ???)); apply zero_neutral;]
+apply (lt_rewl ???? (plus_comm ???));
+apply flt_plusl; assumption;
+qed.
+
+definition d2s ≝
+ λR.λml:mlattice R.λs:sequence ml.λk.λn. δ (s n) k.
+
+notation "s ⇝ x" non associative with precedence 50 for @{'tends $s $x}.
+
+interpretation "tends to" 'tends s x =
+ (cic:/matita/sequence/tends0.con _ (cic:/matita/sandwich/d2s.con _ _ s x)).
+
+alias symbol "and" = "constructive and".
+theorem sandwich:
+ ∀R.∀ml:mlattice R.∀an,bn,xn:sequence ml.∀x:ml.
+ (∀n. (an n ≤ xn n) ∧ (xn n ≤ bn n)) →
+ an ⇝ x →
+ bn ⇝ x →
+ xn ⇝ x.
+intros (R ml an bn xn x H Ha Hb); unfold tends0 in Ha Hb ⊢ %. unfold d2s in Ha Hb ⊢ %.
+intros (e He);
+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 ???? ? (sandwich_ineq ?? 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.
projects / helm.git / commitdiff