-(*
-<<<<<<< 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 ********************************)
projects / helm.git / blobdiff