X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flibrary%2FR%2Froot.ma;fp=matita%2Fmatita%2Flibrary%2FR%2Froot.ma;h=50f98d9a9732ebe9673bb7f2729afe61f64898cc;hb=2c01ff6094173915e7023076ea48b5804dca7778;hp=0000000000000000000000000000000000000000;hpb=a050e3f80d7ea084ce0184279af98e8251c7d2a6;p=helm.git

diff --git a/matita/matita/library/R/root.ma b/matita/matita/library/R/root.ma
new file mode 100644
index 000000000..50f98d9a9
--- /dev/null
+++ b/matita/matita/library/R/root.ma
@@ -0,0 +1,383 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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
+    [apply (nat_lt_to_R_lt ?? H1);
+    |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
+     | cut (∀x,y.(S x ≤ y) = (x < y));[2: intros; reflexivity]
+       (* applyS Rexp_nat_tech by sym_Rtimes, assoc_Rtimes;*)
+      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
+     [apply (nat_lt_to_R_lt ?? H1);
+     |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
+      [apply (nat_lt_to_R_lt ?? H1);
+      |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
+       [apply (nat_lt_to_R_lt ?? H1);
+       |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 depth=2]
+ |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
+| change in match O with (O*O); apply lt_times; assumption; 
+  (* autobatch paramodulation; non fa narrowing, non fa deep subsumption... *) 
+|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