update in ground

[helm.git] / matita / matita / lib / reverse_complexity / speed_clean.ma

diff --git a/matita/matita/lib/reverse_complexity/speed_clean.ma b/matita/matita/lib/reverse_complexity/speed_clean.ma
index 7c04bfd761c54dfd4436c8fd308b6f617d082966..bfd3d34b150a1e6cdc0a7dce299d1989def3239b 100644 (file)
--- a/matita/matita/lib/reverse_complexity/speed_clean.ma
+++ b/matita/matita/lib/reverse_complexity/speed_clean.ma
@@ -4,6 +4,7 @@ include "arithmetics/bigops.ma".
 include "arithmetics/sigma_pi.ma".
 include "arithmetics/bounded_quantifiers.ma".
 include "reverse_complexity/big_O.ma".
 include "arithmetics/sigma_pi.ma".
 include "arithmetics/bounded_quantifiers.ma".
 include "reverse_complexity/big_O.ma".

+include "basics/core_notation/napart_2.ma".

 
 (************************* notation for minimization *****************************)
 notation "μ_{ ident i < n } p" 
 
 (************************* notation for minimization *****************************)
 notation "μ_{ ident i < n } p" 


@@ -490,6 +491,16 @@ axiom CF_mu: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
  
 definition constructible ≝ λs. CF s s.
 
  
 definition constructible ≝ λs. CF s s.
 

+lemma constr_comp : ∀s1,s2. constructible s1 → constructible s2 →
+  (∀x. x ≤ s2 x) → constructible (s2 ∘ s1).
+#s1 #s2 #Hs1 #Hs2 #Hle @(CF_comp … Hs1 Hs2) @O_plus @le_to_O #x [@Hle | //] 
+qed.
+
+lemma ext_constr: ∀s1,s2. (∀x.s1 x = s2 x) → 
+  constructible s1 → constructible s2.
+#s1 #s2 #Hext #Hs1 @(ext_CF … Hext) @(monotonic_CF … Hs1)  #x >Hext //
+qed. 
+

 (********************************* simulation *********************************)
 
 axiom sU : nat → nat. 
 (********************************* simulation *********************************)
 
 axiom sU : nat → nat. 


@@ -676,13 +687,12 @@ axiom compl_g6: ∀h.
 *)
 
 lemma compl_g6: ∀h.
 *)
 
 lemma compl_g6: ∀h.

-  (∀x.MSC x≤h (S (fst (snd x))) (fst x)) →

   constructible (λx. h (fst x) (snd x)) →
   constructible (λx. h (fst x) (snd x)) →

-  (CF (λx. sU 〈fst (snd x),〈fst x,h (S (fst (snd x))) (fst x)〉〉) 
+  (CF (λx. sU 〈max (fst (snd x)) (snd (snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉) 

     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))).
     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))).

-#h #hle #hconstr @(ext_CF (termb_aux h))
+#h #hconstr @(ext_CF (termb_aux h))

   [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
   [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]

-@(CF_comp … (λx.h (S (fst (snd x))) (fst x)) … CF_termb) 
+@(CF_comp … (λx.MSC x + h (S (fst (snd x))) (fst x)) … CF_termb) 

   [@CF_comp_pair
     [@CF_comp_fst @(monotonic_CF … CF_snd) #x //
     |@CF_comp_pair
   [@CF_comp_pair
     [@CF_comp_fst @(monotonic_CF … CF_snd) #x //
     |@CF_comp_pair


@@ -695,12 +705,27 @@ lemma compl_g6: ∀h.
         ]
       ]
     ]
         ]
       ]
     ]

-  |@O_plus [@le_to_O #n @sU_le | // ]
+  |@O_plus
+    [@O_plus
+      [@(O_trans … (λx.MSC (fst x) + MSC (max (fst (snd x)) (snd (snd x))))) 
+        [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
+         >fst_pair >snd_pair @(transitive_le … (MSC_pair …)) 
+         >distributive_times_plus @le_plus [//]
+         cases (surj_pair b) #c * #d #eqb >eqb
+         >fst_pair >snd_pair @(transitive_le … (MSC_pair …)) 
+         whd in ⊢ (??%); @le_plus 
+          [@monotonic_MSC @(le_maxl … (le_n …)) 
+          |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))  
+          ]
+        |@O_plus [@le_to_O #x @sU_le_x |@le_to_O #x @sU_le_i]
+        ]     
+      |@le_to_O #n @sU_le
+      ] 
+    |@le_to_O #x @monotonic_sU // @(le_maxl … (le_n …)) ]

   ]
 qed.
   ]
 qed.

-          
-        
-definition faux1 ≝ λh.
+             
+(* definition faux1 ≝ λh.

   (λx.MSC x + (snd (snd x)-fst x)*(λx.sU 〈fst (snd x),〈fst x,h (S (fst (snd x))) (fst x)〉〉) 〈snd (snd x),x〉).
   
 (* complexity of min_input *)
   (λx.MSC x + (snd (snd x)-fst x)*(λx.sU 〈fst (snd x),〈fst x,h (S (fst (snd x))) (fst x)〉〉) 〈snd (snd x),x〉).
   
 (* complexity of min_input *)


@@ -712,9 +737,9 @@ lemma compl_g7: ∀h.
     (λp:ℕ.min_input h (fst p) (snd (snd p))).
 #h #hle #hcostr #hmono @(monotonic_CF … (faux1 h))
   [#n normalize >fst_pair >snd_pair //]
     (λp:ℕ.min_input h (fst p) (snd (snd p))).
 #h #hle #hcostr #hmono @(monotonic_CF … (faux1 h))
   [#n normalize >fst_pair >snd_pair //]

-@compl_g5 [2:@(compl_g6 h hle hcostr)] #n #x #y #lexy >fst_pair >snd_pair 
+@compl_g5 [2:@(compl_g6 h hcostr)] #n #x #y #lexy >fst_pair >snd_pair 

 >fst_pair >snd_pair @monotonic_sU // @hmono @lexy
 >fst_pair >snd_pair @monotonic_sU // @hmono @lexy

-qed.
+qed.*)

 
 definition big : nat →nat ≝ λx. 
   let m ≝ max (fst x) (snd x) in 〈m,m〉.
 
 definition big : nat →nat ≝ λx. 
   let m ≝ max (fst x) (snd x) in 〈m,m〉.


@@ -727,17 +752,32 @@ lemma le_big : ∀x. x ≤ big x.
 [@(le_maxl … (le_n …)) | @(le_maxr … (le_n …))]
 qed.
 
 [@(le_maxl … (le_n …)) | @(le_maxr … (le_n …))]
 qed.
 

+definition faux2 ≝ λh.
+  (λx.MSC x + (snd (snd x)-fst x)*
+    (λx.sU 〈max (fst(snd x)) (snd(snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉) 〈snd (snd x),x〉).
+ 
+(* proviamo con x *)
+lemma compl_g7: ∀h. 
+  constructible (λx. h (fst x) (snd x)) →
+  (∀n. monotonic ? le (h n)) → 
+  CF (λx.MSC x + (snd (snd x)-fst x)*sU 〈max (fst x) (snd x),〈snd (snd x),h (S (fst x)) (snd (snd x))〉〉)
+    (λp:ℕ.min_input h (fst p) (snd (snd p))).
+#h #hcostr #hmono @(monotonic_CF … (faux2 h))
+  [#n normalize >fst_pair >snd_pair //]
+@compl_g5 [2:@(compl_g6 h hcostr)] #n #x #y #lexy >fst_pair >snd_pair 
+>fst_pair >snd_pair @monotonic_sU // @hmono @lexy
+qed.
+

 (* proviamo con x *)
 lemma compl_g71: ∀h. 
 (* proviamo con x *)
 lemma compl_g71: ∀h. 

-  (∀x.MSC x≤h (S (fst (snd x))) (fst x)) →

   constructible (λx. h (fst x) (snd x)) →
   (∀n. monotonic ? le (h n)) → 
   CF (λx.MSC (big x) + (snd (snd x)-fst x)*sU 〈max (fst x) (snd x),〈snd (snd x),h (S (fst x)) (snd (snd x))〉〉)
     (λp:ℕ.min_input h (fst p) (snd (snd p))).
   constructible (λx. h (fst x) (snd x)) →
   (∀n. monotonic ? le (h n)) → 
   CF (λx.MSC (big x) + (snd (snd x)-fst x)*sU 〈max (fst x) (snd x),〈snd (snd x),h (S (fst x)) (snd (snd x))〉〉)
     (λp:ℕ.min_input h (fst p) (snd (snd p))).

-#h #hle #hcostr #hmono @(monotonic_CF … (compl_g7 h hle hcostr hmono)) #x
+#h #hcostr #hmono @(monotonic_CF … (compl_g7 h hcostr hmono)) #x

 @le_plus [@monotonic_MSC //]
 cases (decidable_le (fst x) (snd(snd x))) 
 @le_plus [@monotonic_MSC //]
 cases (decidable_le (fst x) (snd(snd x))) 

-  [#Hle @le_times // @monotonic_sU // @(le_maxl … (le_n … )) 
+  [#Hle @le_times // @monotonic_sU  

   |#Hlt >(minus_to_0 … (lt_to_le … )) [// | @not_le_to_lt @Hlt]
   ]
 qed.
   |#Hlt >(minus_to_0 … (lt_to_le … )) [// | @not_le_to_lt @Hlt]
   ]
 qed.


@@ -798,16 +838,14 @@ qed. *)
 (* axiom daemon : False. *)
 
 lemma compl_g9 : ∀h. 
 (* axiom daemon : False. *)
 
 lemma compl_g9 : ∀h. 

-  (∀x.MSC x≤h (S (fst (snd x))) (fst x)) →
-  (∀x.MSC x≤h (S (fst x)) (snd(snd x))) →

   constructible (λx. h (fst x) (snd x)) →
   (∀n. monotonic ? le (h n)) → 
   (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
   CF (λx. (S (snd x-fst x))*MSC 〈x,x〉 + 
       (snd x-fst x)*(S(snd x-fst x))*sU 〈x,〈snd x,h (S (fst x)) (snd x)〉〉)
    (auxg h).
   constructible (λx. h (fst x) (snd x)) →
   (∀n. monotonic ? le (h n)) → 
   (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
   CF (λx. (S (snd x-fst x))*MSC 〈x,x〉 + 
       (snd x-fst x)*(S(snd x-fst x))*sU 〈x,〈snd x,h (S (fst x)) (snd x)〉〉)
    (auxg h).

-#h #hle #hle1 #hconstr #hmono #hantimono 
-@(compl_g2 h ??? (compl_g3 … (compl_g71 h hle hconstr hmono)) (compl_g81 h hle1 hconstr))
+#h #hconstr #hmono #hantimono 
+@(compl_g2 h ??? (compl_g3 … (compl_g71 h hconstr hmono)) (compl_g8 h hconstr))

 @O_plus 
   [@O_plus_l @le_to_O #x >(times_n_1 (MSC x)) >commutative_times @le_times
     [// | @monotonic_MSC // ]]
 @O_plus 
   [@O_plus_l @le_to_O #x >(times_n_1 (MSC x)) >commutative_times @le_times
     [// | @monotonic_MSC // ]]


@@ -842,13 +880,11 @@ lemma sg_def : ∀h,a,b.
 qed. 
 
 lemma compl_g11 : ∀h.
 qed. 
 
 lemma compl_g11 : ∀h.

-  (∀x.MSC x≤h (S (fst (snd x))) (fst x)) →
-  (∀x.MSC x≤h (S (fst x)) (snd(snd x))) →

   constructible (λx. h (fst x) (snd x)) →
   (∀n. monotonic ? le (h n)) → 
   (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
   CF (sg h) (unary_g h).
   constructible (λx. h (fst x) (snd x)) →
   (∀n. monotonic ? le (h n)) → 
   (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
   CF (sg h) (unary_g h).

-#h #hle #hle1 #hconstr #Hm #Ham @compl_g1 @(compl_g9 h hle hle1 hconstr Hm Ham)
+#h #hconstr #Hm #Ham @compl_g1 @(compl_g9 h hconstr Hm Ham)

 qed. 
 
 (**************************** closing the argument ****************************)
 qed. 
 
 (**************************** closing the argument ****************************)


@@ -860,7 +896,7 @@ let rec h_of_aux (r:nat →nat) (c,d,b:nat) on d : nat ≝
      d*(S d)*sU 〈〈b-d,b〉,〈b,r (h_of_aux r c d1 b)〉〉].
 
 lemma h_of_aux_O: ∀r,c,b.
      d*(S d)*sU 〈〈b-d,b〉,〈b,r (h_of_aux r c d1 b)〉〉].
 
 lemma h_of_aux_O: ∀r,c,b.

-  h_of_aux r c O b  = c (* MSC 〈〈b,b〉,〈b,b〉〉*) .
+  h_of_aux r c O b  = c.

 // qed.
 
 lemma h_of_aux_S : ∀r,c,d,b. 
 // qed.
 
 lemma h_of_aux_S : ∀r,c,d,b. 


@@ -883,13 +919,6 @@ lemma h_of_def: ∀r,a,b.h_of r 〈a,b〉 =
   h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (b - a) b.
 #r #a #b normalize >fst_pair >snd_pair //
 qed.
   h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (b - a) b.
 #r #a #b normalize >fst_pair >snd_pair //
 qed.

-
-lemma h_le1 : ∀r.(∀x. x ≤ r x) → monotonic ? le r →
-(∀x:ℕ.MSC x≤r (h_of r 〈S (fst x),snd (snd x)〉)).
-#r #Hr #Hmono #x @(transitive_le ???? (Hr …))
->h_of_def
-   
-(*  (∀x.MSC x≤h (S (fst x)) (snd(snd x))) → *)

   
 lemma mono_h_of_aux: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
   ∀d,d1,c,c1,b,b1.c ≤ c1 → d ≤ d1 → b ≤ b1 → 
   
 lemma mono_h_of_aux: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
   ∀d,d1,c,c1,b,b1.c ≤ c1 → d ≤ d1 → b ≤ b1 → 


@@ -923,10 +952,14 @@ cut (max i a ≤ max i b)
   [@monotonic_MSC @le_pair @le_pair @Hmax |/2 by monotonic_le_minus_l/ |@leab]
 qed.
 
   [@monotonic_MSC @le_pair @le_pair @Hmax |/2 by monotonic_le_minus_l/ |@leab]
 qed.
 

+axiom h_of_constr : ∀r:nat →nat. 
+  (∀x. x ≤ r x) → monotonic ? le r → constructible r →
+  constructible (h_of r).
+

 lemma speed_compl: ∀r:nat →nat. 
 lemma speed_compl: ∀r:nat →nat. 

-  (∀x. x ≤ r x) → monotonic ? le r →
+  (∀x. x ≤ r x) → monotonic ? le r → constructible r →

   CF (h_of r) (unary_g (λi,x. r(h_of r 〈i,x〉))).
   CF (h_of r) (unary_g (λi,x. r(h_of r 〈i,x〉))).

-#r #Hr #Hmono @(monotonic_CF … (compl_g11 …)) 
+#r #Hr #Hmono #Hconstr @(monotonic_CF … (compl_g11 …)) 

   [#x cases (surj_pair x) #a * #b #eqx >eqx 
    >sg_def cases (decidable_le b a)
     [#leba >(minus_to_0 … leba) normalize in ⊢ (?%?);
   [#x cases (surj_pair x) #a * #b #eqx >eqx 
    >sg_def cases (decidable_le b a)
     [#leba >(minus_to_0 … leba) normalize in ⊢ (?%?);


@@ -959,7 +992,10 @@ lemma speed_compl: ∀r:nat →nat.
    cut (max b n = n) 
     [normalize >(le_to_leb_true … lebn) %] #Hmaxb 
    >Hmaxa >Hmaxb @Hmono @(mono_h_of_aux r … Hr Hmono) // /2 by monotonic_le_minus_r/
    cut (max b n = n) 
     [normalize >(le_to_leb_true … lebn) %] #Hmaxb 
    >Hmaxa >Hmaxb @Hmono @(mono_h_of_aux r … Hr Hmono) // /2 by monotonic_le_minus_r/

-  |#n #a #b #leab @Hmono @(mono_h_of2 … Hr Hmono … leab) 
+  |#n #a #b #leab @Hmono @(mono_h_of2 … Hr Hmono … leab)
+  |@(constr_comp … Hconstr Hr) @(ext_constr (h_of r))
+    [#x cases (surj_pair x) #a * #b #eqx >eqx >fst_pair >snd_pair //]  
+   @(h_of_constr r Hr Hmono Hconstr)

   ]
 qed.
 
   ]
 qed.
 


@@ -972,19 +1008,19 @@ qed.  *)
 axiom smn: ∀f,s. CF s f → ∀x. CF (λy.s 〈x,y〉) (λy.f 〈x,y〉).
 
 lemma speed_compl_i: ∀r:nat →nat. 
 axiom smn: ∀f,s. CF s f → ∀x. CF (λy.s 〈x,y〉) (λy.f 〈x,y〉).
 
 lemma speed_compl_i: ∀r:nat →nat. 

-  (∀x. x ≤ r x) → monotonic ? le r →
+  (∀x. x ≤ r x) → monotonic ? le r → constructible r →

   ∀i. CF (λx.h_of r 〈i,x〉) (λx.g (λi,x. r(h_of r 〈i,x〉)) i x).
   ∀i. CF (λx.h_of r 〈i,x〉) (λx.g (λi,x. r(h_of r 〈i,x〉)) i x).

-#r #Hr #Hmono #i 
+#r #Hr #Hmono #Hconstr #i 

 @(ext_CF (λx.unary_g (λi,x. r(h_of r 〈i,x〉)) 〈i,x〉))
   [#n whd in ⊢ (??%%); @eq_f @sym_eq >fst_pair >snd_pair %]
 @(ext_CF (λx.unary_g (λi,x. r(h_of r 〈i,x〉)) 〈i,x〉))
   [#n whd in ⊢ (??%%); @eq_f @sym_eq >fst_pair >snd_pair %]

-@smn @(ext_CF … (speed_compl r Hr Hmono)) #n //
+@smn @(ext_CF … (speed_compl r Hr Hmono Hconstr)) #n //

 qed.
 
 theorem pseudo_speedup: 
 qed.
 
 theorem pseudo_speedup: 

-  ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r →
+  ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →

   ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧ O sf (r ∘ sg).
 (* ∃m,a.∀n. a≤n → r(sg a) < m * sf n. *)
   ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧ O sf (r ∘ sg).
 (* ∃m,a.∀n. a≤n → r(sg a) < m * sf n. *)

-#r #Hr #Hmono
+#r #Hr #Hmono #Hconstr

 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *) 
 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
 #Hcodei #HCi 
 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *) 
 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
 #Hcodei #HCi 


@@ -992,7 +1028,7 @@ theorem pseudo_speedup:
 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
 (* sg is (λx.h_of r 〈i,x〉) *)
 %{(λx. h_of r 〈S i,x〉)}
 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
 (* sg is (λx.h_of r 〈i,x〉) *)
 %{(λx. h_of r 〈S i,x〉)}

-lapply (speed_compl_i … Hr Hmono (S i)) #Hg
+lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg

 %[%[@condition_1 |@Hg]
  |cases Hg #H1 * #j * #Hcodej #HCj
   lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
 %[%[@condition_1 |@Hg]
  |cases Hg #H1 * #j * #Hcodej #HCj
   lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)


@@ -1005,11 +1041,11 @@ lapply (speed_compl_i … Hr Hmono (S i)) #Hg
 qed.
 
 theorem pseudo_speedup': 
 qed.
 
 theorem pseudo_speedup': 

-  ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r →
+  ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →

   ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧ 
   (* ¬ O (r ∘ sg) sf. *)
   ∃m,a.∀n. a≤n → r(sg a) < m * sf n. 
   ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧ 
   (* ¬ O (r ∘ sg) sf. *)
   ∃m,a.∀n. a≤n → r(sg a) < m * sf n. 

-#r #Hr #Hmono
+#r #Hr #Hmono #Hconstr 

 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *) 
 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
 #Hcodei #HCi 
 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *) 
 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
 #Hcodei #HCi 


@@ -1017,7 +1053,7 @@ theorem pseudo_speedup':
 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
 (* sg is (λx.h_of r 〈i,x〉) *)
 %{(λx. h_of r 〈S i,x〉)}
 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
 (* sg is (λx.h_of r 〈i,x〉) *)
 %{(λx. h_of r 〈S i,x〉)}

-lapply (speed_compl_i … Hr Hmono (S i)) #Hg
+lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg

 %[%[@condition_1 |@Hg]
  |cases Hg #H1 * #j * #Hcodej #HCj
   lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
 %[%[@condition_1 |@Hg]
  |cases Hg #H1 * #j * #Hcodej #HCj
   lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)


@@ -1029,4 +1065,4 @@ lapply (speed_compl_i … Hr Hmono (S i)) #Hg
   @Hmono @(mono_h_of2 … Hr Hmono … ltin)
  ]
 qed.
   @Hmono @(mono_h_of2 … Hr Hmono … ltin)
  ]
 qed.

-  
\ No newline at end of file
+