From b56efd5aa8eb322443ae5880e8833f1a302bf171 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Sat, 27 Apr 2013 14:59:25 +0000 Subject: [PATCH] commit by user andrea --- weblib/arithmetics/bigO.ma | 60 +++++++++++++++++++++ weblib/basics/sets.ma | 108 +++++++++++++++++++++++++++++++++++++ 2 files changed, 168 insertions(+) create mode 100644 weblib/arithmetics/bigO.ma create mode 100644 weblib/basics/sets.ma diff --git a/weblib/arithmetics/bigO.ma b/weblib/arithmetics/bigO.ma new file mode 100644 index 000000000..95ccd1f43 --- /dev/null +++ b/weblib/arithmetics/bigO.ma @@ -0,0 +1,60 @@ +include "arithmetics/nat.ma". +include "basics/sets.ma". + +(* O f g means g ∈ O(f) *) +definition O: relation (nat→nat) ≝ + λf,g. ∃c.∃n0.∀n. n0 ≤ n → g n ≤ c* (f n). + +lemma O_refl: ∀s. O s s. +#s %{1} %{0} #n #_ >commutative_times associative_times @le_times [//|@H2 @(le_maxr … Hmax)] +qed. + +lemma sub_O_to_O: ∀s1,s2. O s1 ⊆ O s2 → O s2 s1. +#s1 #s2 #H @H // qed. + +lemma O_to_sub_O: ∀s1,s2. O s2 s1 → O s1 ⊆ O s2. +#s1 #s2 #H #g #Hg @(O_trans … H) // qed. + +definition sum_f ≝ λf,g:nat→nat.λn.f n + g n. +interpretation "function sum" 'plus f g = (sum_f f g). + +lemma O_plus: ∀f,g,s. O s f → O s g → O s (f+g). +#f #g #s * #cf * #nf #Hf * #cg * #ng #Hg +%{(cf+cg)} %{(max nf ng)} #n #Hmax normalize +>distributive_times_plus_r @le_plus + [@Hf @(le_maxl … Hmax) |@Hg @(le_maxr … Hmax) ] +qed. + +lemma O_plus_l: ∀f,s1,s2. O s1 f → O (s1+s2) f. +#f #s1 #s2 * #c * #a #Os1f %{c} %{a} #n #lean +@(transitive_le … (Os1f n lean)) @le_times // +qed. + +lemma O_absorbl: ∀f,g,s. O s f → O f g → O s (g+f). +#f #g #s #Osf #Ofg @(O_plus … Osf) @(O_trans … Osf) // +qed. + +lemma O_absorbr: ∀f,g,s. O s f → O f g → O s (f+g). +#f #g #s #Osf #Ofg @(O_plus … Osf) @(O_trans … Osf) // +qed. + +(* +lemma O_ff: ∀f,s. O s f → O s (f+f). +#f #s #Osf /2/ +qed. *) + +lemma O_ext2: ∀f,g,s. O s f → (∀x.f x = g x) → O s g. +#f #g #s * #c * #a #Osf #eqfg %{c} %{a} #n #lean