X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Freverse_complexity%2Fspeedup.ma;h=52b7db0ddc9e9ab800eae0a09bf40bd8ab3dbfc7;hb=84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a;hp=12605c9e4cf1d1d510363edbec147071f2000af5;hpb=b8e8c61042dd7d4d8bc00971e1ebcd6858064682;p=helm.git

diff --git a/matita/matita/lib/reverse_complexity/speedup.ma b/matita/matita/lib/reverse_complexity/speedup.ma
index 12605c9e4..52b7db0dd 100644
--- a/matita/matita/lib/reverse_complexity/speedup.ma
+++ b/matita/matita/lib/reverse_complexity/speedup.ma
@@ -1,192 +1,5 @@
-(*
-<<<<<<< HEAD:matita/matita/broken_lib/reverse_complexity/toolkit.ma
-include "basics/types.ma".
-include "arithmetics/minimization.ma".
-include "arithmetics/bigops.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" 
-  with precedence 80 for @{min $n 0 (λ${ident i}.$p)}.
-
-notation "μ_{ ident i ≤ n } p" 
-  with precedence 80 for @{min (S $n) 0 (λ${ident i}.$p)}.
-  
-notation "μ_{ ident i ∈ [a,b[ } p"
-  with precedence 80 for @{min ($b-$a) $a (λ${ident i}.$p)}.
-  
-notation "μ_{ ident i ∈ [a,b] } p"
-  with precedence 80 for @{min (S $b-$a) $a (λ${ident i}.$p)}.
-  
-(************************************ MAX *************************************)
-notation "Max_{ ident i < n | p } f"
-  with precedence 80
-for @{'bigop $n max 0 (λ${ident i}. $p) (λ${ident i}. $f)}.
-
-notation "Max_{ ident i < n } f"
-  with precedence 80
-for @{'bigop $n max 0 (λ${ident i}.true) (λ${ident i}. $f)}.
-
-notation "Max_{ ident j ∈ [a,b[ } f"
-  with precedence 80
-for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
-  (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
-  
-notation "Max_{ ident j ∈ [a,b[ | p } f"
-  with precedence 80
-for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
-  (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
-
-lemma Max_assoc: ∀a,b,c. max (max a b) c = max a (max b c).
-#a #b #c normalize cases (true_or_false (leb a b)) #leab >leab normalize
-  [cases (true_or_false (leb b c )) #lebc >lebc normalize
-    [>(le_to_leb_true a c) // @(transitive_le ? b) @leb_true_to_le //
-    |>leab //
-    ]
-  |cases (true_or_false (leb b c )) #lebc >lebc normalize //
-   >leab normalize >(not_le_to_leb_false a c) // @lt_to_not_le 
-   @(transitive_lt ? b) @not_le_to_lt @leb_false_to_not_le //
-  ]
-qed.
-
-lemma Max0 : ∀n. max 0 n = n.
-// qed.
-
-lemma Max0r : ∀n. max n 0 = n.
-#n >commutative_max //
-qed.
-
-definition MaxA ≝ 
-  mk_Aop nat 0 max Max0 Max0r (λa,b,c.sym_eq … (Max_assoc a b c)). 
-
-definition MaxAC ≝ mk_ACop nat 0 MaxA commutative_max.
-
-lemma le_Max: ∀f,p,n,a. a < n → p a = true →
-  f a ≤  Max_{i < n | p i}(f i).
-#f #p #n #a #ltan #pa 
->(bigop_diff p ? 0 MaxAC f a n) // @(le_maxl … (le_n ?))
-qed.
-
-lemma le_MaxI: ∀f,p,n,m,a. m ≤ a → a < n → p a = true →
-  f a ≤  Max_{i ∈ [m,n[ | p i}(f i).
-#f #p #n #m #a #lema #ltan #pa 
->(bigop_diff ? ? 0 MaxAC (λi.f (i+m)) (a-m) (n-m)) 
-  [<plus_minus_m_m // @(le_maxl … (le_n ?))
-  |<plus_minus_m_m //
-  |/2 by monotonic_lt_minus_l/
-  ]
-qed.
-
-lemma Max_le: ∀f,p,n,b. 
-  (∀a.a < n → p a = true → f a ≤ b) → Max_{i < n | p i}(f i) ≤ b.
-#f #p #n elim n #b #H // 
-#b0 #H1 cases (true_or_false (p b)) #Hb
-  [>bigop_Strue [2:@Hb] @to_max [@H1 // | @H #a #ltab #pa @H1 // @le_S //]
-  |>bigop_Sfalse [2:@Hb] @H #a #ltab #pa @H1 // @le_S //
-  ]
-qed.
-
-(********************************** pairing ***********************************)
-axiom pair: nat → nat → nat.
-axiom fst : nat → nat.
-axiom snd : nat → nat.
-
-interpretation "abstract pair" 'pair f g = (pair f g). 
-
-axiom fst_pair: ∀a,b. fst 〈a,b〉 = a.
-axiom snd_pair: ∀a,b. snd 〈a,b〉 = b.
-axiom surj_pair: ∀x. ∃a,b. x = 〈a,b〉. 
-
-axiom le_fst : ∀p. fst p ≤ p.
-axiom le_snd : ∀p. snd p ≤ p.
-axiom le_pair: ∀a,a1,b,b1. a ≤ a1 → b ≤ b1 → 〈a,b〉 ≤ 〈a1,b1〉.
-
-(************************************* U **************************************)
-axiom U: nat → nat →nat → option nat. 
-
-axiom monotonic_U: ∀i,x,n,m,y.n ≤m →
-  U i x n = Some ? y → U i x m = Some ? y.
-  
-lemma unique_U: ∀i,x,n,m,yn,ym.
-  U i x n = Some ? yn → U i x m = Some ? ym → yn = ym.
-#i #x #n #m #yn #ym #Hn #Hm cases (decidable_le n m)
-  [#lenm lapply (monotonic_U … lenm Hn) >Hm #HS destruct (HS) //
-  |#ltmn lapply (monotonic_U … n … Hm) [@lt_to_le @not_le_to_lt //]
-   >Hn #HS destruct (HS) //
-  ]
-qed.
-
-definition code_for ≝ λf,i.∀x.
-  ∃n.∀m. n ≤ m → U i x m = f x.
-
-definition terminate ≝ λi,x,r. ∃y. U i x r = Some ? y. 
-
-notation "{i ⊙ x} ↓ r" with precedence 60 for @{terminate $i $x $r}. 
-
-lemma terminate_dec: ∀i,x,n. {i ⊙ x} ↓ n ∨ ¬ {i ⊙ x} ↓ n.
-#i #x #n normalize cases (U i x n)
-  [%2 % * #y #H destruct|#y %1 %{y} //]
-qed.
-  
-lemma monotonic_terminate: ∀i,x,n,m.
-  n ≤ m → {i ⊙ x} ↓ n → {i ⊙ x} ↓ m.
-#i #x #n #m #lenm * #z #H %{z} @(monotonic_U … H) //
-qed.
-
-definition termb ≝ λi,x,t. 
-  match U i x t with [None ⇒ false |Some y ⇒ true].
-
-lemma termb_true_to_term: ∀i,x,t. termb i x t = true → {i ⊙ x} ↓ t.
-#i #x #t normalize cases (U i x t) normalize [#H destruct | #y #_ %{y} //]
-qed.    
-
-lemma term_to_termb_true: ∀i,x,t. {i ⊙ x} ↓ t → termb i x t = true.
-#i #x #t * #y #H normalize >H // 
-qed.    
-
-definition out ≝ λi,x,r. 
-  match U i x r with [ None ⇒ 0 | Some z ⇒ z]. 
-
-definition bool_to_nat: bool → nat ≝ 
-  λb. match b with [true ⇒ 1 | false ⇒ 0]. 
-
-coercion bool_to_nat. 
-
-definition pU : nat → nat → nat → nat ≝ λi,x,r.〈termb i x r,out i x r〉.
-
-lemma pU_vs_U_Some : ∀i,x,r,y. pU i x r = 〈1,y〉 ↔ U i x r = Some ? y.
-#i #x #r #y % normalize
-  [cases (U i x r) normalize 
-    [#H cut (0=1) [lapply (eq_f … fst … H) >fst_pair >fst_pair #H @H] 
-     #H1 destruct
-    |#a #H cut (a=y) [lapply (eq_f … snd … H) >snd_pair >snd_pair #H1 @H1] 
-     #H1 //
-    ]
-  |#H >H //]
-qed.
-  
-lemma pU_vs_U_None : ∀i,x,r. pU i x r = 〈0,0〉 ↔ U i x r = None ?.
-#i #x #r % normalize
-  [cases (U i x r) normalize //
-   #a #H cut (1=0) [lapply (eq_f … fst … H) >fst_pair >fst_pair #H1 @H1] 
-   #H1 destruct
-  |#H >H //]
-qed.
-
-lemma fst_pU: ∀i,x,r. fst (pU i x r) = termb i x r.
-#i #x #r normalize cases (U i x r) normalize >fst_pair //
-qed.
-
-lemma snd_pU: ∀i,x,r. snd (pU i x r) = out i x r.
-#i #x #r normalize cases (U i x r) normalize >snd_pair //
-qed.
-=======
 include "reverse_complexity/bigops_compl.ma".
->>>>>>> reverse_complexity lib restored:matita/matita/lib/reverse_complexity/speedup.ma
-*)
+include "basics/core_notation/napart_2.ma".
 
 (********************************* the speedup ********************************)