--- /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 *)
+(* *)
+(**************************************************************************)
+
+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<R1∨R1<x) (x=R1) (trichotomy_Rlt x R1))
+ [simplify;cases (decide (x<R1) (R1<x) H1)
+ [elim (asym_Rlt ?? H H2)
+ |simplify;
+ apply (\snd (choose ℝ (lub (expcut x y)) (Rexp_lemma x y H2)))]
+ |simplify;rewrite > H1 in H;elim (irrefl_Rlt ? H)]]
+qed.*)
+
+interpretation "real numbers exponent" 'exp a b = (Rexp a b _).
--- /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 *)
+(* *)
+(**************************************************************************)
+
+include "R/Rexp.ma".
+
+(* ... definition logcut : ∀b,y,x:R.Prop ≝
+ λb,y,x.y < b \sup x. *)
\ No newline at end of file
--- /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 *)
+(* *)
+(**************************************************************************)
+
+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
--- /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 *)
+(* *)
+(**************************************************************************)
+
+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<y → y^n<x → y≤a
+ case 0 < x ≤ 1 : take y = x/2
+ 0 < (x/2)^n < x ⇒ 0 < x/2 ≤ a
+ case 1 < x : take y = 1
+ 0 < 1^n = 1 < x ⇒ 0 < 1 ≤ a
+ unfold in H1;elim H1;unfold in H2;lapply (H1 R1)
+ [elim Hletin
+ [autobatch
+ |rewrite < H3;autobatch]
+ |unfold;split
+ [autobatch
+ |rewrite > 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
-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
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
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
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
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
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
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.
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
projects / helm.git / commitdiff