From: Wilmer Ricciotti Date: Fri, 13 Feb 2009 15:16:55 +0000 (+0000) Subject: Axiomatization of real numbers (work in progress) X-Git-Tag: make_still_working~4202 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=10dbebadd2931de5b93871a6b4989e07f668e166;p=helm.git Axiomatization of real numbers (work in progress) --- diff --git a/helm/software/matita/library/R/Rexp.ma b/helm/software/matita/library/R/Rexp.ma new file mode 100644 index 000000000..7cea39259 --- /dev/null +++ b/helm/software/matita/library/R/Rexp.ma @@ -0,0 +1,288 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "R/root.ma". +include "nat/orders.ma". +include "Z/times.ma". + +definition Rexp_Z ≝ +λx:R.λy:Z.match y with +[ pos z ⇒ Rexp_nat x (S z) +| neg z ⇒ Rinv (Rexp_nat x (S z)) +| OZ ⇒ R1 ]. + +lemma eq_Rexp_nat_Rexp_Z : ∀x.∀n:nat.Rexp_nat x n = Rexp_Z x n. +intros;cases n;simplify;reflexivity; +qed. + +definition expcut : ∀x,y,z:R.Prop ≝ + λx,y,z:R.∃p:Z.∃q:nat.∃H1,H2. + z = root q (Rexp_Z x p) H1 H2 ∧ p ≤ (y*q). + +axiom Zopp_to_Ropp : ∀z. R_of_Z (Zopp z) = Ropp (R_of_Z z). +axiom distr_Rinv_Rtimes : ∀x,y.x ≠ R0 → y ≠ R0 → Rinv (x*y) = Rinv x * Rinv y. +axiom Rinv_Rexp_nat : ∀n,z. z ≠ R0 → Rinv (Rexp_nat z n) = Rexp_nat (Rinv z) n. + +lemma Rexp_nat_R0 : ∀x,n.Rexp_nat x n = R0 → x = R0. +intros 2;elim n +[simplify in H;elim not_eq_R0_R1;symmetry;assumption +|simplify in H1; + cases (trichotomy_Rlt x R0) + [apply H;simplify in H1;cases H2;lapply (Rlt_to_neq ? ? H3); + rewrite < (Rtimes_x_R0 (Rinv x)); + rewrite > sym_Rtimes in ⊢ (???%);apply eq_Rtimes_l_to_r + [assumption + |2,4:rewrite > sym_Rtimes;assumption + |intro;apply Hletin;symmetry;assumption] + |assumption]] +qed. + +lemma Rexp_Z_Rexp_Z_Rtimes : + ∀x,y,z.x ≠ R0 → Rexp_Z (Rexp_Z x y) z = Rexp_Z x (y*z). +intros;cases y +[simplify;cases z + [reflexivity + |simplify;rewrite > sym_Rtimes;rewrite > Rtimes_x_R1; + elim n + [reflexivity + |simplify;rewrite > sym_Rtimes;rewrite > Rtimes_x_R1;assumption] + |simplify;rewrite > sym_Rtimes;rewrite > Rtimes_x_R1; + elim n;simplify + [rewrite < Rtimes_x_R1;rewrite < sym_Rtimes; + apply Rinv_Rtimes_l;intro;autobatch + |rewrite > sym_Rtimes;rewrite > Rtimes_x_R1;assumption]] +|cases z + [reflexivity + |simplify;change in ⊢ (? ? (? ? (? % ?)) ?) with (Rexp_nat x (S n)); + rewrite > Rexp_nat_Rexp_nat_Rtimes; + rewrite > assoc_Rtimes;rewrite < Rexp_nat_plus_Rtimes;do 2 apply eq_f; + rewrite > sym_times in ⊢ (???%); simplify; + do 2 rewrite < assoc_plus;rewrite < sym_plus in ⊢ (? ? (? % ?) ?); + rewrite < sym_times;reflexivity + |simplify;apply eq_f;change in ⊢ (? ? (? ? (? % ?)) ?) with (Rexp_nat x (S n)); + rewrite > Rexp_nat_Rexp_nat_Rtimes; + rewrite > assoc_Rtimes;rewrite < Rexp_nat_plus_Rtimes; + do 2 apply eq_f;rewrite > sym_times in ⊢ (???%); simplify; + do 2 rewrite < assoc_plus;rewrite < sym_plus in ⊢ (? ? (? % ?) ?); + rewrite < sym_times;reflexivity] +|cases z + [reflexivity + |simplify;change in ⊢ (? ? (? (? %) (? (? %) ?)) ?) with (Rexp_nat x (S n)); + rewrite < Rinv_Rexp_nat + [rewrite < distr_Rinv_Rtimes + [apply eq_f;rewrite > Rexp_nat_Rexp_nat_Rtimes; + rewrite < Rexp_nat_plus_Rtimes; + change in ⊢ (? ? ? %) with (Rexp_nat x (S (n1+n*S n1))); + apply eq_f;autobatch paramodulation + |intro;apply H;apply (Rexp_nat_R0 ?? H1) + |intro;apply H;lapply (Rexp_nat_R0 ?? H1);apply (Rexp_nat_R0 ?? Hletin)] + |intro;apply H;apply (Rexp_nat_R0 ?? H1)] + |simplify;rewrite < Rinv_Rexp_nat + [rewrite < distr_Rinv_Rtimes + [rewrite < Rinv_inv + [change in ⊢ (? ? (? ? (? % ?)) ?) with (Rexp_nat x (S n)); + rewrite > Rexp_nat_Rexp_nat_Rtimes; + rewrite > assoc_Rtimes;rewrite < Rexp_nat_plus_Rtimes; + apply eq_f;apply eq_f;rewrite > sym_times in ⊢ (???%); simplify; + do 2 rewrite < assoc_plus;rewrite < sym_plus in ⊢ (? ? (? % ?) ?); + rewrite < sym_times;reflexivity + |intro;apply H; + change in H1:(??%?) with (Rexp_nat (x*Rexp_nat x n) (S n1)); + lapply (Rexp_nat_R0 ?? H1); + change in Hletin:(??%?) with (Rexp_nat x (S n)); + apply (Rexp_nat_R0 ?? Hletin)] + |intro;apply H;change in H1:(??%?) with (Rexp_nat x (S n)); + apply (Rexp_nat_R0 ?? H1) + |intro;apply H; + lapply (Rexp_nat_R0 ?? H1); + change in Hletin:(??%?) with (Rexp_nat x (S n)); + apply (Rexp_nat_R0 ?? Hletin)] + |intro;apply H;change in H1:(??%?) with (Rexp_nat x (S n)); + apply (Rexp_nat_R0 ?? H1)]]] +qed. + +lemma pos_Rexp_nat : ∀x,n.R0 < x → R0 < Rexp_nat x n. +intros;elim n;simplify +[autobatch +|rewrite < (Rtimes_x_R0 x);apply Rlt_times_l;assumption] +qed. + +lemma Rexp_nat_R0_Sn : ∀n.Rexp_nat R0 (S n) = R0. +intro;simplify;rewrite > sym_Rtimes;rewrite > Rtimes_x_R0;reflexivity; +qed. + +lemma lt_to_lt_Rexp_nat : ∀x,y,n.R0 ≤ x → R0 ≤ y → O < n → x < y → + Rexp_nat x n < Rexp_nat y n. +intros;cases H +[cases H1 + [elim H2;simplify + [do 2 rewrite > Rtimes_x_R1;assumption + |apply (trans_Rlt ? (y*Rexp_nat x n1)) + [rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%); + apply Rlt_times_l + [assumption + |apply pos_Rexp_nat;assumption] + |apply Rlt_times_l;autobatch]] + |rewrite < H5 in H3;elim (irrefl_Rlt R0);apply (trans_Rlt ? x);assumption] +|cases H1 + [rewrite < H4;cases H2;rewrite > Rexp_nat_R0_Sn + [simplify;rewrite > Rtimes_x_R1;assumption + |apply pos_Rexp_nat;assumption] + |elim (irrefl_Rlt x);rewrite < H4 in ⊢ (??%);rewrite > H5;assumption]] +qed. + +lemma le_to_le_Rexp_nat : ∀x,y,n.R0 ≤ x → R0 ≤ y → x ≤ y → + Rexp_nat x n ≤ Rexp_nat y n. +intros;elim n +[right;reflexivity +|cases H + [cases H1 + [cases H2 + [left;apply lt_to_lt_Rexp_nat;autobatch + |rewrite > H6;right;reflexivity] + |rewrite < H5 in H2;elim (irrefl_Rlt R0);cases H2 + [apply (trans_Rlt ? x);assumption + |rewrite < H6 in ⊢ (??%);assumption]] + |rewrite < H4;rewrite > Rexp_nat_R0_Sn;cases H1 + [left;apply pos_Rexp_nat;assumption + |rewrite < H5;rewrite > Rexp_nat_R0_Sn;right;reflexivity]]] +qed. + +lemma inj_Rexp_nat : ∀x,y,n.R0 ≤ x → R0 ≤ y → O < n → + Rexp_nat x n = Rexp_nat y n → x = y. +intros;cases (trichotomy_Rlt x y) +[cases H4 + [lapply (lt_to_lt_Rexp_nat ??? H H1 H2 H5);rewrite > H3 in Hletin; + elim (irrefl_Rlt ? Hletin) + |lapply (lt_to_lt_Rexp_nat ??? H1 H H2 H5);rewrite > H3 in Hletin; + elim (irrefl_Rlt ? Hletin)] +|assumption] +qed. + +axiom eq_Rinv_Ropp_Ropp_Rinv : ∀x. x ≠ R0 → Rinv (Ropp x) = Ropp (Rinv x). +lemma Rlt_times_r : ∀x,y,z:R.x < y → R0 < z → x*z < y*z. +intros;rewrite < sym_Rtimes;rewrite < sym_Rtimes in ⊢ (??%); +autobatch; +qed. + +lemma Rexp_nat_R1 : ∀x.Rexp_nat x 1 = x. +intros;simplify;rewrite > Rtimes_x_R1;reflexivity; +qed. + +alias symbol "lt" = "real numbers less than". +lemma Rexp_lemma : ∀x,y:R. R1 < x → ∃z.lub (expcut x y) z. +intros;apply R_dedekind +[unfold expcut;cases (trichotomy_Rlt y R0) + [cases H1 + [cases (R_archimedean R1 (Ropp y)) + [apply ex_intro[apply (Rexp_Z x (Zopp x1))] + apply ex_intro[apply (Zopp x1)] + apply ex_intro[apply 1] + apply ex_intro[apply le_n] + apply ex_intro + [left;cases x1;simplify + [autobatch + |apply lt_R0_Rinv;change in ⊢(??%) with (Rexp_nat x (S n)); + apply pos_Rexp_nat;autobatch] + |split + [cases (root_sound 1 (Rexp_Z x (-x1))) + [rewrite > Rexp_nat_R1 in H5;apply H5 + |*:skip] + |simplify;left;rewrite > Rtimes_x_R1;rewrite > Ropp_inv in ⊢ (??%); + lapply (Rlt_to_Rlt_Ropp_Ropp ?? H3);rewrite > Rtimes_x_R1 in Hletin; + rewrite > Zopp_to_Ropp;apply Hletin]] + |autobatch] + |cases (R_archimedean y R1) + [cut (O < x1) [|elim daemon] + cut (R0 ≤ x) [|left;apply (trans_Rlt ???? H);autobatch] + apply ex_intro[apply (root x1 x Hcut Hcut1);assumption] + apply ex_intro[apply (Z_of_nat 1)] + apply ex_intro[apply x1] + apply ex_intro[assumption] + apply ex_intro + [simplify;rewrite > Rtimes_x_R1;assumption + |simplify in ⊢ (? (? ? ? (? ? % ? ?)) ?); + split + [symmetry;cases (root_sound x1 (x*R1) Hcut) + [apply root_unique + [apply H4 + |rewrite > Rtimes_x_R1 in H5:(??%?); + symmetry;assumption] + |skip] + |simplify;rewrite > sym_Rtimes;left;assumption]] + |assumption]] + |rewrite > H1; + apply ex_intro + [apply (root 1 (Rexp_Z x OZ)) + [autobatch + |simplify;left;autobatch] + |apply ex_intro[apply OZ] + apply ex_intro[apply 1] + apply ex_intro[autobatch] + apply ex_intro[simplify;left;autobatch] + split + [reflexivity + |simplify;rewrite > Rtimes_x_R1;right;reflexivity]]] +|cases (R_archimedean R1 y) + [apply ex_intro[apply (Rexp_Z x x1)] + unfold;intros;unfold in H2; + cases H2;cases H3;cases H4;cases H5;cases H6; + clear H2 H3 H4 H5 H6; + rewrite > Rtimes_x_R1 in H1; + cut (x2 < x1*x3) + [apply (trans_Rle ? (root x3 (Rexp_Z x (x1*x3)) ??)) + [assumption + |apply (trans_Rle ??? x5);(*monotonia potenza*)elim daemon + |rewrite > H7;left; + (* monotonia della root *) + elim daemon + |right;elim (root_sound x3 (Rexp_Z (Rexp_Z x x1) x3)) + [rewrite < Rexp_Z_Rexp_Z_Rtimes + [apply (inj_Rexp_nat ?? x3) + [apply H2 + |left;rewrite < eq_Rexp_nat_Rexp_Z;apply pos_Rexp_nat; + autobatch + |assumption + |symmetry;rewrite > eq_Rexp_nat_Rexp_Z;apply H3] + |intro;rewrite > H4 in H;apply (asym_Rlt ?? H);apply lt_R0_R1] + |*:skip]] + |(*apply Rlt_div_l_to_r manca *) elim daemon] + |autobatch]] +qed. + +definition Rexp : ∀x,y:R.R0 < x → R. +intros;cases (decide ? ? (trichotomy_Rlt x R1)) +[cases (decide ? ? H1) + [apply (\fst (choose ?? (Rexp_lemma (Rinv x) r ?))); + rewrite < Rtimes_x_R1 in ⊢(??%);rewrite < sym_Rtimes; + apply Rlt_times_l_to_r + [assumption + |rewrite < sym_Rtimes;rewrite > Rtimes_x_R1;assumption] + |apply (\fst (choose ?? (Rexp_lemma x r H2)))] +|apply R1] +qed. + +(* testing "decide" axiom +lemma aaa : ∀x,y:R.R1 < x → lub (expcut x y) (Rexp x y ?). +[autobatch +|intros;unfold Rexp; + cases (decide (x H1 in H;elim (irrefl_Rlt ? H)]] +qed.*) + +interpretation "real numbers exponent" 'exp a b = (Rexp a b _). diff --git a/helm/software/matita/library/R/Rlog.ma b/helm/software/matita/library/R/Rlog.ma new file mode 100644 index 000000000..f8303ff8f --- /dev/null +++ b/helm/software/matita/library/R/Rlog.ma @@ -0,0 +1,18 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "R/Rexp.ma". + +(* ... definition logcut : ∀b,y,x:R.Prop ≝ + λb,y,x.y < b \sup x. *) \ No newline at end of file diff --git a/helm/software/matita/library/R/r.ma b/helm/software/matita/library/R/r.ma new file mode 100644 index 000000000..46a4e416b --- /dev/null +++ b/helm/software/matita/library/R/r.ma @@ -0,0 +1,431 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "logic/equality.ma". +include "logic/coimplication.ma". +include "logic/cprop_connectives.ma". +include "datatypes/constructors.ma". +include "nat/orders.ma". +include "Z/z.ma". + +axiom choose : ∀A:Type.∀P:A → Prop.(∃x.P x) → exP ? P. +alias symbol "plus" = "Disjoint union". +axiom decide : ∀A,B.A ∨ B → A + B. + +axiom R : Type. + +axiom R0 : R. +axiom R1 : R. + +axiom Rplus : R → R → R. +axiom Rtimes : R → R → R. +axiom Ropp : R → R. +axiom Rinv : R → R. +axiom Rlt : R → R → Prop. +definition Rle : R → R → Prop ≝ λx,y:R.Rlt x y ∨ x = y. + +interpretation "real numbers" 'R = R. + +interpretation "real numbers plus" 'plus x y = (Rplus x y). +interpretation "real numbers times" 'times x y = (Rtimes x y). +interpretation "real numbers opposite" 'uminus x = (Ropp x). +interpretation "real numbers reciprocal" 'invert x = (Rinv x). +interpretation "real numbers less than" 'lt x y = (Rlt x y). +interpretation "real numbers less eq" 'leq x y = (Rle x y). + +axiom not_eq_R0_R1 : ¬ R0 = R1. + +(* commutative ring with unity *) + +axiom sym_Rplus : ∀x,y:R. x + y = y + x. +axiom assoc_Rplus : ∀x,y,z:R.(x+y)+z = x+(y+z). +axiom Rplus_x_R0 : ∀x.x + R0 = x. +axiom Rplus_Ropp : ∀x.x + (-x) = R0. + +axiom sym_Rtimes : ∀x,y:R. x * y = y * x. +axiom assoc_Rtimes : ∀x,y,z:R.(x*y)*z = x*(y*z). +axiom Rtimes_x_R1 : ∀x.x * R1 = x. +axiom distr_Rtimes_Rplus_l : ∀x,y,z:R.x*(y+z) = x*y + x*z. + +lemma distr_Rtimes_Rplus_r : ∀x,y,z:R.(x+y)*z = x*z + y*z. +intros;autobatch paramodulation; +qed. + +(* commutative field *) + +axiom Rinv_Rtimes_l : ∀x. ¬ x = R0 → x * (Rinv x) = R1. + +(* ordered commutative field *) + +axiom irrefl_Rlt : ∀x:R.¬ x < x. +axiom asym_Rlt : ∀x,y:R. x < y → ¬ y < x. +axiom trans_Rlt : ∀x,y,z:R.x < y → y < z → x < z. +axiom trichotomy_Rlt : ∀x,y.x < y ∨ y < x ∨ x = y. + +lemma trans_Rle : ∀x,y,z:R.x ≤ y → y ≤ z → x ≤ z. +intros;cases H +[cases H1 + [left;autobatch + |rewrite < H3;assumption] +|rewrite > H2;assumption] +qed. + +axiom Rlt_plus_l : ∀x,y,z:R.x < y → z + x < z + y. +axiom Rlt_times_l : ∀x,y,z:R.x < y → R0 < z → z*x < z*y. + +(* FIXME: these should be lemmata *) +axiom Rle_plus_l : ∀x,y,z:R.x ≤ y → z + x ≤ z + y. +axiom Rle_times_l : ∀x,y,z:R.x ≤ y → R0 < z → z*x ≤ z*y. + +lemma Rle_plus_r : ∀x,y,z:R.x ≤ y → x + z ≤ y + z. +intros; +rewrite > sym_Rplus;rewrite > sym_Rplus in ⊢ (??%); +autobatch; +qed. + +lemma Rle_times_r : ∀x,y,z:R.x ≤ y → R0 < z → x*z ≤ y*z. +intros; +rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%); +autobatch; +qed. + +(* Dedekind-completeness *) + +definition ub ≝ λS: R → Prop.λx:R.∀y.S y → y ≤ x. +definition lub ≝ λS: R → Prop.λx:R.ub S x ∧ ∀y. ub S y → x ≤ y. + +axiom R_dedekind : ∀S:R → Prop.(∃x.S x) → (∃x.ub S x) → ∃x.lub S x. + +(* coercions *) + +definition R_of_nat : nat → R ≝ + λn.match n with + [ O ⇒ R0 + | S p ⇒ let rec aux m ≝ + match m with + [ O ⇒ R1 + | S q ⇒ (aux q) + R1] in aux p]. + +definition R_of_Z ≝ +λz.match z with +[ pos n ⇒ R_of_nat (S n) +| neg n ⇒ Ropp (R_of_nat (S n)) +| OZ ⇒ R0 ]. + +(* FIXME!!! coercion clash! *) +coercion R_of_Z. + +(*coercion R_of_nat.*) + +(* archimedean property *) + +axiom R_archimedean : ∀x,y:R.R0 < x → ∃n:nat.y < n*x. + +(*definition Rminus : R → R → R ≝ + λx,y.x + (-y).*) + +interpretation "real numbers minus" 'minus x y = (Rplus x (Ropp y)). +interpretation "real numbers divide" 'divide x y = (Rtimes x (Rinv y)). + +(* basic properties *) + +(* equality *) + +(* +lemma Rplus_eq_l : ∀x,y,z.x = y → z + x= z + y. +intros;autobatch; +qed. + +lemma Rplus_eq_r Rtimes_eq_l Rtimes_eq_r analogamente *) + +lemma eq_Rplus_l_to_r : ∀a,b,c:R.a+b=c → a = c-b. +intros;lapply (eq_f ? ? (λx:R.x-b) ? ? H); +rewrite > assoc_Rplus in Hletin;rewrite > Rplus_Ropp in Hletin; +rewrite > Rplus_x_R0 in Hletin;assumption; +qed. + +lemma eq_Rplus_r_to_l : ∀a,b,c:R.a=b+c → a-c = b. +intros;symmetry;apply eq_Rplus_l_to_r;symmetry;assumption; +qed. + +lemma eq_Rminus_l_to_r : ∀a,b,c:R.a-b=c → a = c+b. +intros;lapply (eq_f ? ? (λx:R.x+b) ? ? H); +rewrite > assoc_Rplus in Hletin;rewrite > sym_Rplus in Hletin:(??(??%)?); +rewrite > Rplus_Ropp in Hletin;rewrite > Rplus_x_R0 in Hletin;assumption; +qed. + +lemma eq_Rminus_r_to_l : ∀a,b,c:R.a=b-c → a+c = b. +intros;symmetry;apply eq_Rminus_l_to_r;autobatch paramodulation; +qed. + +lemma eq_Rtimes_l_to_r : ∀a,b,c:R.b ≠ R0 → a*b=c → a = c/b. +intros;lapply (eq_f ? ? (λx:R.x/b) ? ? H1); +rewrite > assoc_Rtimes in Hletin;rewrite > Rinv_Rtimes_l in Hletin +[rewrite > Rtimes_x_R1 in Hletin;assumption +|assumption] +qed. + +lemma eq_Rtimes_r_to_l : ∀a,b,c:R.c ≠ R0 → a=b*c → a/c = b. +intros;symmetry;apply eq_Rtimes_l_to_r +[assumption +|symmetry;assumption] +qed. + +lemma eq_Rdiv_l_to_r : ∀a,b,c:R.b ≠ R0 → a/b=c → a = c*b. +intros;lapply (eq_f ? ? (λx:R.x*b) ? ? H1); +rewrite > assoc_Rtimes in Hletin;rewrite > sym_Rtimes in Hletin:(??(??%)?); +rewrite > Rinv_Rtimes_l in Hletin +[rewrite > Rtimes_x_R1 in Hletin;assumption +|assumption] +qed. + +lemma eq_Rdiv_r_to_l : ∀a,b,c:R.c ≠ R0 → a=b/c → a*c = b. +intros;symmetry;apply eq_Rdiv_l_to_r +[assumption +|symmetry;assumption] +qed. + +(* lemma unique_Ropp : ∀x,y.x + y = R0 → y = -x. +intros;autobatch paramodulation; +qed. *) + +lemma Rtimes_x_R0 : ∀x.x * R0 = R0. +intro; +rewrite < Rplus_x_R0 in ⊢ (? ? % ?); +rewrite < (Rplus_Ropp (x*R0)) in ⊢ (? ? (? ? %) %); +rewrite < assoc_Rplus; +apply eq_f2;autobatch paramodulation; +qed. + +lemma eq_Rtimes_Ropp_R1_Ropp : ∀x.x*(-R1) = -x. +intro. +rewrite < Rplus_x_R0 in ⊢ (? ? % ?); +rewrite < Rplus_x_R0 in ⊢ (? ? ? %); +rewrite < (Rplus_Ropp x) in ⊢ (? ? % ?); +rewrite < assoc_Rplus; +rewrite < sym_Rplus in ⊢ (? ? % ?); +rewrite < sym_Rplus in ⊢ (? ? (? ? %) ?); +apply eq_f2 [reflexivity] +rewrite < Rtimes_x_R1 in ⊢ (? ? (? % ?) ?); +rewrite < distr_Rtimes_Rplus_l;autobatch paramodulation; +qed. + +lemma Ropp_inv : ∀x.x = Ropp (Ropp x). +intro;autobatch; +qed. + +lemma Rinv_inv : ∀x.x ≠ R0 → x = Rinv (Rinv x). +intros;rewrite < Rtimes_x_R1 in ⊢ (???%);rewrite > sym_Rtimes; +apply eq_Rtimes_l_to_r +[intro;lapply (eq_f ? ? (λy:R.x*y) ? ? H1); + rewrite > Rinv_Rtimes_l in Hletin + [rewrite > Rtimes_x_R0 in Hletin;apply not_eq_R0_R1;symmetry;assumption + |assumption] +|apply Rinv_Rtimes_l;assumption] +qed. + +lemma Ropp_R0 : R0 = - R0. +rewrite < eq_Rtimes_Ropp_R1_Ropp;autobatch paramodulation; +qed. + +lemma distr_Ropp_Rplus : ∀x,y:R.-(x + y) = -x -y. +intros;rewrite < eq_Rtimes_Ropp_R1_Ropp; +rewrite > sym_Rtimes;rewrite > distr_Rtimes_Rplus_l; +autobatch paramodulation; +qed. + +lemma Ropp_Rtimes_l : ∀x,y:R.-(x*y) = -x*y. +intros;rewrite < eq_Rtimes_Ropp_R1_Ropp; +rewrite > sym_Rtimes;rewrite < assoc_Rtimes;autobatch paramodulation; +qed. + +lemma Ropp_Rtimes_r : ∀x,y:R.-(x*y) = x*-y. +intros;rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (???%); +autobatch; +qed. + +(* less than *) + +lemma Rlt_to_Rlt_Ropp_Ropp : ∀x,y.x < y → -y < -x. +intros;rewrite < Rplus_x_R0 in ⊢ (??%); +rewrite < (Rplus_Ropp y);rewrite < Rplus_x_R0 in ⊢ (?%?); +rewrite < assoc_Rplus;rewrite < sym_Rplus in ⊢ (??%); +apply Rlt_plus_l; +rewrite < (Rplus_Ropp x);rewrite < sym_Rplus in ⊢ (?%?);autobatch; +qed. + +lemma lt_R0_R1 : R0 < R1. +elim (trichotomy_Rlt R0 R1) [|elim (not_eq_R0_R1 H)] +elim H [assumption] +rewrite > Ropp_inv in ⊢ (??%);rewrite < eq_Rtimes_Ropp_R1_Ropp; +rewrite < (Rtimes_x_R0 (-R1)); +apply Rlt_times_l;rewrite < (Rtimes_x_R0 (-R1)); +rewrite > sym_Rtimes;rewrite > eq_Rtimes_Ropp_R1_Ropp;autobatch; +qed. + +lemma pos_z_to_lt_Rtimes_Rtimes_to_lt : ∀x,y,z.R0 < z → z*x < z*y → x < y. +intros;elim (trichotomy_Rlt x y) +[elim H2 [assumption] + elim (asym_Rlt (z*y) (z*x));autobatch +|rewrite > H2 in H1;elim (irrefl_Rlt ? H1)] +qed. + +lemma pos_z_to_le_Rtimes_Rtimes_to_lt : ∀x,y,z.R0 < z → z*x ≤ z*y → x ≤ y. +intros;cases H1 +[left;autobatch +|right;rewrite < Rtimes_x_R1;rewrite < Rtimes_x_R1 in ⊢ (???%); + rewrite < sym_Rtimes;rewrite < sym_Rtimes in ⊢ (???%); + rewrite < (Rinv_Rtimes_l z) + [rewrite < sym_Rtimes in ⊢ (??(?%?)?);rewrite < sym_Rtimes in ⊢ (???(?%?)); + autobatch paramodulation + |intro;rewrite > H3 in H;apply (irrefl_Rlt R0);assumption]] +qed. + +lemma neg_z_to_lt_Rtimes_Rtimes_to_lt : ∀x,y,z.z < R0 → z*x < z*y → y < x. +intros;rewrite > Ropp_inv in ⊢ (?%?); +rewrite > Ropp_inv in ⊢ (??%); +apply Rlt_to_Rlt_Ropp_Ropp;apply (pos_z_to_lt_Rtimes_Rtimes_to_lt ?? (-z)) +[rewrite > Ropp_R0;autobatch +|rewrite < (eq_Rtimes_Ropp_R1_Ropp) in ⊢ (?(??%)?); + rewrite < (eq_Rtimes_Ropp_R1_Ropp) in ⊢ (??(??%)); + do 2 rewrite < assoc_Rtimes; + rewrite > eq_Rtimes_Ropp_R1_Ropp; + rewrite > eq_Rtimes_Ropp_R1_Ropp in ⊢ (??%); + rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%); + rewrite < (eq_Rtimes_Ropp_R1_Ropp) in ⊢ (?%?); + rewrite < (eq_Rtimes_Ropp_R1_Ropp) in ⊢ (??%); + do 2 rewrite > assoc_Rtimes; + rewrite > eq_Rtimes_Ropp_R1_Ropp; + rewrite < Ropp_inv; + rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%); + assumption] +qed. + +lemma lt_R0_Rinv : ∀x.R0 < x → R0 < Rinv x. +intros;apply (pos_z_to_lt_Rtimes_Rtimes_to_lt ?? x H);rewrite > Rinv_Rtimes_l; +[rewrite > Rtimes_x_R0;autobatch +|intro;apply (irrefl_Rlt x);rewrite < H1 in H;assumption] +qed. + +lemma pos_times_pos_pos : ∀x,y.R0 < x → R0 < y → R0 < x*y. +intros;rewrite < (Rtimes_x_R0 x);autobatch; +qed. + +lemma pos_plus_pos_pos : ∀x,y.R0 < x → R0 < y → R0 < x+y. +intros;rewrite < (Rplus_Ropp x);apply Rlt_plus_l; +apply (trans_Rlt ???? H1);rewrite > Ropp_R0; +apply Rlt_to_Rlt_Ropp_Ropp;assumption; +qed. + +lemma Rlt_to_neq : ∀x,y:R.x < y → x ≠ y. +intros;intro;rewrite > H1 in H;apply (irrefl_Rlt ? H); +qed. + +lemma lt_Rinv : ∀x,y.R0 < x → x < y → Rinv y < Rinv x. +intros; +lapply (Rlt_times_l ? ? (Rinv x * Rinv y) H1) +[rewrite > sym_Rtimes in Hletin;rewrite < assoc_Rtimes in Hletin; + rewrite > assoc_Rtimes in Hletin:(??%); + rewrite > sym_Rtimes in Hletin:(??(??%)); + rewrite > Rinv_Rtimes_l in Hletin + [rewrite > Rinv_Rtimes_l in Hletin + [rewrite > Rtimes_x_R1 in Hletin;rewrite > sym_Rtimes in Hletin; + rewrite > Rtimes_x_R1 in Hletin;assumption + |intro;rewrite > H2 in H1;apply (asym_Rlt ? ? H H1)] + |intro;rewrite > H2 in H;apply (irrefl_Rlt ? H)] +|apply pos_times_pos_pos;apply lt_R0_Rinv;autobatch] +qed. + +lemma Rlt_plus_l_to_r : ∀a,b,c.a + b < c → a < c - b. +intros;rewrite < Rplus_x_R0;rewrite < (Rplus_Ropp b); +rewrite < assoc_Rplus; +rewrite < sym_Rplus;rewrite < sym_Rplus in ⊢ (??%); +apply Rlt_plus_l;assumption; +qed. + +lemma Rlt_plus_r_to_l : ∀a,b,c.a < b + c → a - c < b. +intros;rewrite > Ropp_inv;rewrite > Ropp_inv in ⊢ (??%); +apply Rlt_to_Rlt_Ropp_Ropp;rewrite > distr_Ropp_Rplus; +apply Rlt_plus_l_to_r;rewrite < distr_Ropp_Rplus;apply Rlt_to_Rlt_Ropp_Ropp; +assumption; +qed. + +lemma Rlt_minus_l_to_r : ∀a,b,c.a - b < c → a < c + b. +intros;rewrite > (Ropp_inv b);apply Rlt_plus_l_to_r;assumption; +qed. + +lemma Rlt_minus_r_to_l : ∀a,b,c.a < b - c → a + c < b. +intros;rewrite > (Ropp_inv c);apply Rlt_plus_r_to_l;assumption; +qed. + +lemma Rlt_div_r_to_l : ∀a,b,c.R0 < c → a < b/c → a*c < b. +intros;rewrite < sym_Rtimes; +rewrite < Rtimes_x_R1 in ⊢ (??%);rewrite < sym_Rtimes in ⊢ (??%); +rewrite < (Rinv_Rtimes_l c) +[rewrite > assoc_Rtimes;apply Rlt_times_l + [rewrite > sym_Rtimes;assumption + |autobatch] +|intro;elim (Rlt_to_neq ?? H);symmetry;assumption] +qed. + +lemma Rlt_times_l_to_r : ∀a,b,c.R0 < b → a*b < c → a < c/b. +intros;rewrite < sym_Rtimes; +rewrite < Rtimes_x_R1;rewrite < sym_Rtimes; +rewrite < (Rinv_Rtimes_l b) +[rewrite < sym_Rtimes in ⊢ (? (? % ?) ?); + rewrite > assoc_Rtimes;apply Rlt_times_l + [rewrite > sym_Rtimes;assumption + |autobatch] +|intro;elim (Rlt_to_neq ?? H);symmetry;assumption] +qed. + +lemma Rle_plus_l_to_r : ∀a,b,c.a + b ≤ c → a ≤ c - b. +intros;cases H +[left;autobatch +|right;autobatch] +qed. + +lemma Rle_plus_r_to_l : ∀a,b,c.a ≤ b + c → a - c ≤ b. +intros;cases H +[left;autobatch +|right;autobatch] +qed. + +lemma Rle_minus_l_to_r : ∀a,b,c.a - b ≤ c → a ≤ c + b. +intros;cases H +[left;autobatch +|right;autobatch] +qed. + +lemma Rle_minus_r_to_l : ∀a,b,c.a ≤ b - c → a + c ≤ b. +intros;cases H +[left;autobatch +|right;autobatch] +qed. + +lemma R_OF_nat_S : ∀n.R_OF_nat (S n) = R_OF_nat n + R1. +intros;elim n;simplify +[autobatch paramodulation +|reflexivity] +qed. + +lemma nat_lt_to_R_lt : ∀m,n:nat.m < n → R_OF_nat m < R_OF_nat n. +intros;elim H +[cases m;simplify + [autobatch + |rewrite < Rplus_x_R0 in ⊢ (?%?);apply Rlt_plus_l;autobatch] +|apply (trans_Rlt ??? H2);cases n1;simplify + [autobatch + |rewrite < Rplus_x_R0 in ⊢ (?%?);apply Rlt_plus_l;autobatch]] +qed. \ No newline at end of file diff --git a/helm/software/matita/library/R/root.ma b/helm/software/matita/library/R/root.ma new file mode 100644 index 000000000..574483be7 --- /dev/null +++ b/helm/software/matita/library/R/root.ma @@ -0,0 +1,380 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "Q/q/q.ma". +include "R/r.ma". + +let rec Rexp_nat x n on n ≝ + match n with + [ O ⇒ R1 + | S p ⇒ x * (Rexp_nat x p) ]. + +axiom daemon : False. + +lemma Rexp_nat_tech : ∀a,b,n.O < n → R0 < b → b < a → + Rexp_nat a n - Rexp_nat b n ≤ n*(a - b)*Rexp_nat a (n-1). +intros;elim H +[simplify;right;autobatch paramodulation +|simplify in ⊢ (? ? (? ? %));rewrite < minus_n_O; + rewrite > distr_Rtimes_Rplus_l; + rewrite > sym_Rtimes; + rewrite > distr_Rtimes_Rplus_l; + rewrite > sym_Rtimes in ⊢ (? ? (? (? ? %) ?));rewrite < assoc_Rtimes; + rewrite > R_OF_nat_S;rewrite > sym_Rtimes in ⊢ (? ? (? ? (? ? %))); + rewrite > distr_Rtimes_Rplus_l;rewrite > Rtimes_x_R1; + rewrite > sym_Rplus in ⊢ (? ? (? % ?)); + rewrite > assoc_Rplus;simplify;rewrite > sym_Rtimes; + apply Rle_plus_l; + do 2 rewrite > distr_Rtimes_Rplus_l;rewrite > Rtimes_x_R1; + rewrite < Rplus_x_R0;rewrite > sym_Rplus; + apply Rle_plus_r_to_l;rewrite < assoc_Rplus; + apply Rle_minus_l_to_r;rewrite > sym_Rplus;rewrite > Rplus_x_R0; + apply Rle_minus_l_to_r;rewrite < Ropp_Rtimes_r; + rewrite < Ropp_inv;rewrite < sym_Rplus;rewrite < sym_Rtimes; + rewrite > Ropp_Rtimes_r;rewrite < distr_Rtimes_Rplus_l; + apply (trans_Rle ? (b*n1*(a-b)*Rexp_nat a (n1-1))) + [do 2 rewrite > assoc_Rtimes;apply Rle_times_l + [rewrite < assoc_Rtimes;assumption|autobatch] + |rewrite > assoc_Rtimes in ⊢ (??%);rewrite < distr_Rtimes_Rplus_l; + rewrite < distr_Rtimes_Rplus_r; + rewrite > sym_Rtimes in ⊢ (? ? (? ? %));rewrite < assoc_Rtimes; + rewrite > sym_Rtimes;do 2 rewrite < assoc_Rtimes; + rewrite > (?:(Rexp_nat a n1 = Rexp_nat a (n1-1)*a)) + [do 2 rewrite > assoc_Rtimes;do 2 rewrite > assoc_Rtimes in ⊢ (??%); + apply Rle_times_l + [apply Rle_times_r + [left;assumption + |elim daemon] (* trivial *) + |elim daemon] (* trivial: auxiliary lemma *) + |rewrite > sym_Rtimes;elim H3;simplify + [reflexivity + |rewrite < minus_n_O;reflexivity]]]] +qed. + +(* FIXME: se uso la notazione, la disambiguazione fa un casino... *) +(*lemma roots_lemma : ∀x:R.∀n:nat.R0 ≤ x → 1 ≤ n → ∃y.R0 ≤ y ∧ x = Rexp_nat y n.*) + +lemma roots_lemma : ∀x:R.∀n:nat.R0 ≤ x → 1 ≤ n → ex ? (λy.R0 ≤ y ∧ x = Rexp_nat y n). +intros;cases H +[alias symbol "lt" = "real numbers less than". +letin bound ≝ (λy:R.R0 < y ∧ Rexp_nat y n < x); + elim (R_dedekind bound) + [cut (R0 < a) + [| + (* Hp: ∀y.0 Rtimes_x_R1;rewrite < Rplus_x_R0 in ⊢ (? % ?); + autobatch]] *) + elim daemon] + apply ex_intro[apply a] + split [left;assumption] + elim H3;unfold in H4;unfold bound in H4; + cases (trichotomy_Rlt x (Rexp_nat a n)) [|assumption] + cases H6 + [letin k ≝ ((Rexp_nat a n - x)*Rinv (n*Rexp_nat a (n-1))); + cut (R0 < k) [|elim daemon] + cut (k < a) [|elim daemon] + cut (ub bound (a-k)) + [lapply (H5 ? Hcut3);rewrite < Rplus_x_R0 in Hletin:(?%?); + rewrite > sym_Rplus in Hletin:(? % ?);lapply (Rle_plus_l_to_r ? ? ? Hletin); + rewrite > assoc_Rplus in Hletin1; + rewrite > sym_Rplus in Hletin1:(? ? (? ? %)); + rewrite < assoc_Rplus in Hletin1; + lapply (Rle_minus_r_to_l ??? Hletin1); + rewrite > sym_Rplus in Hletin2;rewrite > Rplus_x_R0 in Hletin2; + rewrite > Rplus_Ropp in Hletin2;cases Hletin2 + [elim (asym_Rlt ?? Hcut1 H8) + |rewrite > H8 in Hcut1;elim (irrefl_Rlt ? Hcut1)] + |unfold;intros;elim H8;unfold k;rewrite < Rplus_x_R0; + rewrite < sym_Rplus;apply Rle_minus_r_to_l; + apply (pos_z_to_le_Rtimes_Rtimes_to_lt ? ? (n*Rexp_nat a (n-1))) + [apply pos_times_pos_pos + [lapply (nat_lt_to_R_lt ?? H1);autobatch + |elim daemon] + |rewrite > Rtimes_x_R0;do 2 rewrite > distr_Rtimes_Rplus_l; + rewrite > sym_Rtimes in ⊢ (? ? (? (? ? (? ? (? %))) ?)); + rewrite > Ropp_Rtimes_r; + rewrite < assoc_Rtimes in ⊢ (? ? (? (? ? %) ?)); + rewrite > Rinv_Rtimes_l + [rewrite > sym_Rtimes in ⊢ (? ? (? (? ? %) ?)); + rewrite > Rtimes_x_R1;rewrite > distr_Ropp_Rplus; + rewrite < Ropp_inv;rewrite < assoc_Rplus; + rewrite > assoc_Rplus in ⊢ (? ? (? % ?)); + rewrite > sym_Rplus in ⊢ (? ? (? % ?)); + rewrite > assoc_Rplus;rewrite > sym_Rplus; + apply Rle_minus_l_to_r;rewrite > distr_Ropp_Rplus; + rewrite < Ropp_inv;rewrite < sym_Rplus;rewrite > Rplus_x_R0; + rewrite < distr_Rtimes_Rplus_l; + apply (trans_Rle ? (Rexp_nat a n - Rexp_nat y n)) + [apply Rle_plus_l;left;autobatch + |rewrite > assoc_Rtimes;rewrite > sym_Rtimes in ⊢ (??(??%)); + rewrite < assoc_Rtimes;apply Rexp_nat_tech + [autobatch + |assumption + |(* by transitivity y^n < x < a^n and injectivity *) elim daemon]] + |intro;apply (irrefl_Rlt (n*Rexp_nat a (n-1))); + rewrite > H11 in ⊢ (?%?);apply pos_times_pos_pos + [lapply (nat_lt_to_R_lt ?? H1);autobatch + |elim daemon]]]] +|elim (R_archimedean R1 ((x-Rexp_nat a n)/(n*Rexp_nat (a+1) (n-1)))) + [|autobatch] + rewrite > Rtimes_x_R1 in H8; + letin h ≝ ((x-Rexp_nat a n)/(n*Rexp_nat (a+1) (n-1)*a1)); + lapply (H4 (a+h)) + [rewrite < Rplus_x_R0 in Hletin:(??%);rewrite < sym_Rplus in Hletin:(??%); + lapply (Rle_plus_r_to_l ? ? ? Hletin); + rewrite > sym_Rplus in Hletin1:(?(?%?)?);rewrite > assoc_Rplus in Hletin1; + rewrite > Rplus_Ropp in Hletin1;rewrite > Rplus_x_R0 in Hletin1; + unfold h in Hletin1; + cut (R0 < (x-Rexp_nat a n)/(n*Rexp_nat (a+1) (n-1)*a1)) + [cases Hletin1 + [elim (asym_Rlt ? ? Hcut1 H9) + |rewrite > H9 in Hcut1;elim (irrefl_Rlt ? Hcut1)] + |apply pos_times_pos_pos + [apply Rlt_plus_l_to_r;rewrite > sym_Rplus;rewrite > Rplus_x_R0; + assumption + |apply lt_R0_Rinv;apply pos_times_pos_pos + [apply pos_times_pos_pos + [lapply (nat_lt_to_R_lt ?? H1);autobatch + |elim daemon] + |apply (trans_Rlt ???? H8);apply pos_times_pos_pos + [apply Rlt_plus_l_to_r;rewrite > sym_Rplus;rewrite > Rplus_x_R0; + assumption + |apply lt_R0_Rinv;apply pos_times_pos_pos + [lapply (nat_lt_to_R_lt ?? H1);autobatch + |elim daemon]]]]] + |split + [(* show that h > R0, also useful in previous parts of the proof *) + elim daemon + |(* by monotonicity ov Rexp_nat *) elim daemon]]] +|apply ex_intro[apply (x/(x+R1))] + unfold bound;simplify;split + [apply pos_times_pos_pos + [assumption + |apply lt_R0_Rinv;apply pos_plus_pos_pos + [assumption + |autobatch]] + |apply (trans_Rlt ? (x/(x+R1))) + [(* antimonotone exponential with base in [0,1] *) elim daemon + |rewrite < Rtimes_x_R1 in ⊢ (??%); + apply Rlt_times_l + [rewrite < (Rinv_Rtimes_l R1) + [rewrite > sym_Rtimes in ⊢ (??%);rewrite > Rtimes_x_R1; + apply lt_Rinv + [autobatch + |rewrite > Rinv_Rtimes_l + [apply Rlt_minus_l_to_r;rewrite > Rplus_Ropp;assumption + |intro;elim not_eq_R0_R1;symmetry;assumption]] + |intro;elim not_eq_R0_R1;symmetry;assumption] + |assumption]]] +|apply ex_intro[apply (x+R1)] + unfold ub;intros;unfold in H3;elim H3;cases (trichotomy_Rlt y (x+R1)) + [cases H6 + [left;assumption + |elim (asym_Rlt (Rexp_nat y n) x) + [assumption + |apply (trans_Rlt ? y) + [apply (trans_Rlt ???? H7);rewrite > sym_Rplus; + apply Rlt_minus_l_to_r;rewrite > Rplus_Ropp;autobatch + |(* monotonia; il caso n=1 andra` facilmente gestito a parte *) + elim daemon]]] + |right;assumption]] +|apply ex_intro[apply R0] + split + [right;reflexivity + |rewrite < H2;elim H1; + simplify;rewrite > sym_Rtimes;rewrite > Rtimes_x_R0;reflexivity]] +qed. + +definition root : ∀n:nat.∀x:R.O < n → R0 ≤ x → R. +intros;apply (\fst (choose ?? (roots_lemma x n ??)));assumption; +qed. + +notation < "hvbox(maction (\root mstyle scriptlevel 1(term 19 n) + \of (term 19 x)) ((\root n \of x)\sub(h,k)))" + with precedence 90 for @{ 'aroot $n $x $h $k}. + +interpretation "real numbers root" 'aroot n x h k = (root n x h k). + +(* FIXME: qui non c'e` modo di far andare la notazione...*) +(*lemma root_sound : ∀n:nat.∀x:R.1 ≤ n → R0 ≤ x → + R0 ≤ (root n x ??) ∧ x = Rexp_nat (root n x ??) n.*) +alias id "PAnd" = "cic:/matita/logic/connectives/And.ind#xpointer(1/1)". + +lemma root_sound : ∀n:nat.∀x:R.1 ≤ n → R0 ≤ x → + PAnd (R0 ≤ (root n x ??)) (x = Rexp_nat (root n x ??) n). +try assumption; +intros;unfold root;apply (\snd (choose ?? (roots_lemma x n ??))); +qed. + +lemma defactorize_O_nfa_zero : ∀x.defactorize x = 0 → x = nfa_zero. +intro;elim x +[reflexivity +|simplify in H;destruct H +|simplify in H;cut (∀m.defactorize_aux n m ≠ O) + [elim (Hcut ? H) + |intro;intro;autobatch]] +qed. + +lemma lt_O_defactorize_numerator : ∀f.0 < defactorize (numerator f). +intro;elim f;simplify +[rewrite < plus_n_O;rewrite > plus_n_O in ⊢ (?%?);apply lt_plus; + apply lt_O_exp;autobatch +|autobatch +|generalize in match H;generalize in match (not_eq_numerator_nfa_zero f1); + cases (numerator f1);intros + [elim H1;reflexivity + |simplify;cases z;simplify + [1,3:autobatch + |rewrite < plus_n_O;rewrite > plus_n_O in ⊢ (?%?); + apply lt_plus;autobatch] + |simplify;cases z;simplify; + [1,3:autobatch + |rewrite < plus_n_O;rewrite > (times_n_O O) in ⊢ (?%?); + apply lt_times + [rewrite > plus_n_O in ⊢ (?%?); apply lt_plus;autobatch + |autobatch]]]] +qed. + +lemma lt_O_defactorize_denominator : ∀f.O < defactorize (denominator f). +intros;unfold denominator;apply lt_O_defactorize_numerator; +qed. + +lemma Rexp_nat_pos : ∀x,n.R0 ≤ x → R0 ≤ Rexp_nat x n. +intros;elim n;simplify +[left;autobatch +|cases H + [cases H1 + [left;autobatch + |right;rewrite < H3;rewrite > Rtimes_x_R0;reflexivity] + |right;rewrite < H2;rewrite > sym_Rtimes;rewrite > Rtimes_x_R0;reflexivity]] +qed. + +definition Rexp_Q : ∀x:R.Q → R0 ≤ x → R. +apply (λx,q,p.match q with + [ OQ ⇒ R1 + | Qpos r ⇒ match r with + [ one ⇒ x + | frac f ⇒ root (defactorize (denominator f)) + (Rexp_nat x (defactorize (numerator f))) + (lt_O_defactorize_denominator ?) ? ] + | Qneg r ⇒ match r with + [ one ⇒ Rinv x + | frac f ⇒ Rinv (root (defactorize (denominator f)) + (Rexp_nat x (defactorize (numerator f))) + (lt_O_defactorize_denominator ?) ?) ]]); +autobatch; +qed. + +lemma Rexp_nat_plus_Rtimes : + ∀x,p,q.Rexp_nat x (p+q) = Rexp_nat x p * Rexp_nat x q. +intros;elim q +[simplify;autobatch paramodulation +|rewrite < sym_plus;simplify;autobatch paramodulation] +qed. + +lemma monotonic_Rexp_nat : ∀x,y,n.O < n → R0 ≤ x → x < y → + Rexp_nat x n < Rexp_nat y n. +intros;elim H;simplify +[do 2 rewrite > Rtimes_x_R1;assumption +|apply (trans_Rlt ? (y*Rexp_nat x n1)) + [rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%); + apply Rlt_times_l + [assumption + |(* already proved, but for ≤: shit! *)elim daemon] + |apply Rlt_times_l + [assumption + |cases H1 + [autobatch + |rewrite > H5;assumption]]]] +qed. + +lemma inj_Rexp_nat_l : ∀x,y,n.O < n → R0 ≤ x → R0 ≤ y → + Rexp_nat x n = Rexp_nat y n → x = y. +intros;cases (trichotomy_Rlt x y) +[cases H4 + [lapply (monotonic_Rexp_nat ?? n H H1 H5); + elim (Rlt_to_neq ?? Hletin H3) + |lapply (monotonic_Rexp_nat ?? n H H2 H5); + elim (Rlt_to_neq ?? Hletin);symmetry;assumption] +|assumption] +qed. + +lemma root_unique : ∀x,y,n.R0 ≤ x → R0 ≤ y → O < n → + Rexp_nat y n = x → y = root n x ? ?. +[1,2:assumption +|intros;cases (root_sound n x) + [2,3:assumption + |rewrite > H5 in H3;lapply (inj_Rexp_nat_l ?????? H3);assumption]] +qed. + +lemma Rtimes_Rexp_nat : ∀x,y:R.∀p.Rexp_nat x p*Rexp_nat y p = Rexp_nat (x*y) p. +intros;elim p;simplify +[autobatch paramodulation +|rewrite > assoc_Rtimes;rewrite < assoc_Rtimes in ⊢ (? ? (? ? %) ?); + rewrite < sym_Rtimes in ⊢ (? ? (? ? (? % ?)) ?); + rewrite < H;do 3 rewrite < assoc_Rtimes;reflexivity] +qed. + +lemma times_root : ∀x,y,n,H,H1,H2,H3. + root n x H H2 * root n y H H3 = root n (x*y) H H1. +intros;lapply (Rtimes_Rexp_nat (root n x H H2) (root n y H H3) n); +lapply (sym_eq ??? Hletin); +cases (root_sound n x) +[2,3:assumption +|cases (root_sound n y) + [2,3:assumption + |rewrite < H5 in Hletin1;rewrite < H7 in Hletin1; + lapply (root_unique ?????? Hletin1) + [assumption + |cases H4 + [cases H6 + [left;autobatch + |right;autobatch paramodulation] + |right;autobatch paramodulation] + |*:assumption]]] +qed. + +lemma Rexp_nat_Rexp_nat_Rtimes : + ∀x,p,q.Rexp_nat (Rexp_nat x p) q = Rexp_nat x (p*q). +intros;elim q +[rewrite < times_n_O;simplify;reflexivity +|rewrite < times_n_Sm;rewrite > Rexp_nat_plus_Rtimes;simplify; + rewrite < H;reflexivity] +qed. + +lemma root_root_times : ∀x,n,m,H,H1,H2.root m (root n x H H1) H2 ? = + root (m*n) x ? H1. +[cases (root_sound n x H H1);assumption +|autobatch +|intros;lapply (Rexp_nat_Rexp_nat_Rtimes (root m (root n x H H1) H2 ?) m n) + [cases (root_sound n x H H1);assumption + |cases (root_sound m (root n x H H1)) + [2:assumption + |3:cases (root_sound n x H H1);assumption + |rewrite < H4 in Hletin:(??%?);lapply (root_sound n x H H1); + cases Hletin1;rewrite < H6 in Hletin:(??%?); + apply root_unique + [apply H3 + |symmetry;apply Hletin]]]] +qed. \ No newline at end of file diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index aaf7d6869..64edcc026 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -1,5 +1,5 @@ -demo/formal_topology.ma logic/cprop_connectives.ma logic/equality.ma dama/sandwich.ma dama/ordered_uniform.ma +demo/formal_topology.ma logic/cprop_connectives.ma logic/equality.ma Q/ratio/rtimes.ma Q/fraction/ftimes.ma Q/ratio/rinv.ma demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma @@ -18,43 +18,46 @@ algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/ nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma -datatypes/compare.ma list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma +datatypes/compare.ma dama/models/nat_uniform.ma dama/models/discrete_uniformity.ma dama/nat_ordered_set.ma -didactic/exercises/substitution.ma nat/minus.ma didactic/exercises/natural_deduction_fst_order.ma didactic/support/natural_deduction.ma +didactic/exercises/substitution.ma nat/minus.ma nat/factorization2.ma list/list.ma nat/factorization.ma nat/sieve.ma dama/models/increasing_supremum_stabilizes.ma dama/models/nat_uniform.ma dama/russell_support.ma dama/supremum.ma nat/le_arith.ma logic/connectives.ma Q/nat_fact/times.ma nat/factorization.ma decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma +Fsub/defn.ma Fsub/util.ma didactic/exercises/duality.ma nat/minus.ma nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma dama/supremum.ma dama/nat_ordered_set.ma dama/sequence.ma datatypes/constructors.ma nat/plus.ma nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma +R/Rexp.ma R/root.ma Z/times.ma nat/orders.ma didactic/exercises/natural_deduction1.ma didactic/support/natural_deduction.ma nat/times.ma nat/plus.ma nat/chebyshev_thm.ma nat/neper.ma Z/z.ma datatypes/bool.ma nat/nat.ma demo/cantor.ma datatypes/constructors.ma demo/formal_topology.ma +dama/models/nat_ordered_uniform.ma dama/bishop_set_rewrite.ma dama/models/nat_uniform.ma dama/ordered_uniform.ma nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma nat/le_arith.ma nat/orders.ma nat/times.ma decidable_kit/fgraph.ma decidable_kit/fintype.ma -dama/models/nat_ordered_uniform.ma dama/bishop_set_rewrite.ma dama/models/nat_uniform.ma dama/ordered_uniform.ma dama/bishop_set.ma dama/ordered_set.ma nat/euler_theorem.ma nat/map_iter_p.ma nat/nat.ma nat/totient.ma Q/fraction/ftimes.ma Q/fraction/finv.ma Q/nat_fact/times.ma Q/ratio/ratio.ma Z/times.ma nat/factorial.ma nat/le_arith.ma Z/plus.ma Z/z.ma nat/minus.ma Q/ratio/rinv.ma Q/fraction/finv.ma Q/ratio/ratio.ma -decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma dama/ordered_set.ma datatypes/constructors.ma logic/cprop_connectives.ma +decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma Q/q/qplus.ma nat/factorization.ma decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma -Z/orders.ma Z/z.ma nat/orders.ma +R/r.ma Z/z.ma datatypes/constructors.ma logic/coimplication.ma logic/cprop_connectives.ma logic/equality.ma nat/orders.ma nat/map_iter_p.ma nat/count.ma nat/permutation.ma Q/q.ma Q/fraction/fraction.ma Z/compare.ma Z/plus.ma nat/factorization.ma +Z/orders.ma Z/z.ma nat/orders.ma nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma demo/realisability.ma datatypes/constructors.ma logic/connectives.ma list/list.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma nat/orders.ma nat/plus.ma @@ -63,6 +66,7 @@ didactic/support/natural_deduction.ma nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma Q/frac.ma Q/q/q.ma Q/q/qinv.ma nat/factorization.ma nat/nat.ma +.unnamed.ma logic/connectives.ma nat/nat.ma didactic/exercises/shannon.ma nat/minus.ma Q/q/qtimes.ma Q/q/qinv.ma Q/ratio/rtimes.ma nat/minus.ma nat/compare.ma nat/le_arith.ma @@ -72,8 +76,9 @@ algebra/finite_groups.ma algebra/groups.ma nat/relevant_equations.ma decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma algebra/semigroups.ma higher_order_defs/functions.ma -dama/models/discrete_uniformity.ma dama/bishop_set_rewrite.ma dama/uniform.ma dama/lebesgue.ma dama/ordered_set.ma dama/property_exhaustivity.ma dama/sandwich.ma +dama/models/discrete_uniformity.ma dama/bishop_set_rewrite.ma dama/uniform.ma +Fsub/part1a.ma Fsub/defn.ma higher_order_defs/relations.ma logic/connectives.ma nat/factorization.ma nat/ord.ma nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma @@ -97,27 +102,30 @@ higher_order_defs/ordering.ma logic/equality.ma nat/congruence.ma nat/primes.ma nat/relevant_equations.ma logic/equality.ma logic/connectives.ma higher_order_defs/relations.ma dama/property_exhaustivity.ma dama/ordered_uniform.ma dama/property_sigma.ma -Z/compare.ma Z/orders.ma nat/compare.ma -datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma nat/gcd.ma nat/lt_arith.ma nat/primes.ma -Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma +datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma +Z/compare.ma Z/orders.ma nat/compare.ma algebra/monoids.ma algebra/semigroups.ma nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma +Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma datatypes/categories.ma logic/cprop_connectives.ma nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma dama/nat_ordered_set.ma nat/orders.ma dama/bishop_set.ma nat/compare.ma -Q/fraction/finv.ma Q/fraction/fraction.ma Z/plus.ma dama/russell_support.ma logic/cprop_connectives.ma nat/nat.ma +Q/fraction/finv.ma Q/fraction/fraction.ma Z/plus.ma +Fsub/util.ma list/in.ma list/list.ma logic/equality.ma nat/compare.ma nat/binomial.ma nat/factorial2.ma nat/iteration2.ma +R/root.ma logic/connectives.ma Q/q/q.ma R/r.ma nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma higher_order_defs/functions.ma logic/equality.ma Q/fraction/numerator_denominator.ma Q/fraction/finv.ma -datatypes/constructors.ma logic/equality.ma +Fsub/part1a_inversion.ma Fsub/defn.ma nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma +datatypes/constructors.ma logic/equality.ma didactic/exercises/natural_deduction_theories.ma didactic/support/natural_deduction.ma nat/plus.ma -nat/plus.ma nat/nat.ma Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma +nat/plus.ma nat/nat.ma dama/sequence.ma nat/nat.ma nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma nat/gcd_properties1.ma nat/gcd.ma @@ -125,6 +133,7 @@ list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma didactic/exercises/natural_deduction.ma didactic/support/natural_deduction.ma dama/bishop_set_rewrite.ma dama/bishop_set.ma Z/times.ma Z/plus.ma nat/lt_arith.ma +R/Rlog.ma R/Rexp.ma Z/sigma_p.ma Z/plus.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma nat/o.ma nat/binomial.ma nat/sqrt.ma dama/property_sigma.ma dama/ordered_uniform.ma dama/russell_support.ma diff --git a/helm/software/matita/library/logic/cprop_connectives.ma b/helm/software/matita/library/logic/cprop_connectives.ma index facda2848..266bb11a4 100644 --- a/helm/software/matita/library/logic/cprop_connectives.ma +++ b/helm/software/matita/library/logic/cprop_connectives.ma @@ -100,6 +100,26 @@ interpretation "exT \snd" 'pi2 = (pi2exT _ _). interpretation "exT \snd" 'pi2a x = (pi2exT _ _ x). interpretation "exT \snd" 'pi2b x y = (pi2exT _ _ x y). +inductive exP (A:Type) (P:A→Prop) : CProp ≝ + ex_introP: ∀w:A. P w → exP A P. + +interpretation "dependent pair for Prop" 'dependent_pair a b = + (ex_introP _ _ a b). + +interpretation "CProp exists for Prop" 'exists \eta.x = (exP _ x). + +definition pi1exP ≝ λA,P.λx:exP A P.match x with [ex_introP x _ ⇒ x]. +definition pi2exP ≝ + λA,P.λx:exP A P.match x return λx.P (pi1exP ?? x) with [ex_introP _ p ⇒ p]. + +interpretation "exT \fst" 'pi1 = (pi1exP _ _). +interpretation "exT \fst" 'pi1a x = (pi1exP _ _ x). +interpretation "exT \fst" 'pi1b x y = (pi1exP _ _ x y). +interpretation "exT \snd" 'pi2 = (pi2exP _ _). +interpretation "exT \snd" 'pi2a x = (pi2exP _ _ x). +interpretation "exT \snd" 'pi2b x y = (pi2exP _ _ x y). + + inductive exT23 (A:Type) (P:A→CProp) (Q:A→CProp) (R:A→A→CProp) : CProp ≝ ex_introT23: ∀w,p:A. P w → Q p → R w p → exT23 A P Q R. diff --git a/helm/software/matita/library/nat/bertrand.ma b/helm/software/matita/library/nat/bertrand.ma index 17f4c72e0..ce92ee4ed 100644 --- a/helm/software/matita/library/nat/bertrand.ma +++ b/helm/software/matita/library/nat/bertrand.ma @@ -610,7 +610,7 @@ qed. theorem le_B_split1_teta:\forall n.18 \le n \to not_bertrand n \to B_split1 (2*n) \le teta (2 * n / 3). -intros.unfold B_split1.unfold teta. +intros. unfold B_split1.unfold teta. apply (trans_le ? (pi_p (S (2*n)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1))))) [apply le_pi_p.intros. apply le_exp