1 include "reverse_complexity/basics.ma".
2 include "reverse_complexity/big_O.ma".
4 (********************************* complexity *********************************)
6 (* We assume operations have a minimal structural complexity MSC.
7 For instance, for time complexity, MSC is equal to the size of input.
8 For space complexity, MSC is typically 0, since we only measure the space
9 required in addition to dimension of the input. *)
11 axiom MSC : nat → nat.
12 axiom MSC_sublinear : ∀n. MSC (S n) ≤ S (MSC n).
13 (* axiom MSC_S: O MSC (λx.MSC (S x)) . *)
14 axiom MSC_le: ∀n. MSC n ≤ n.
16 axiom monotonic_MSC: monotonic ? le MSC.
17 axiom MSC_pair_eq: ∀a,b. MSC 〈a,b〉 = MSC a + MSC b.
20 lemma MSC_pair: ∀a,b. MSC 〈a,b〉 ≤ MSC a + MSC b. // qed.
22 (* C s i means i is running in O(s) *)
24 definition C ≝ λs,i.∃c.∃a.∀x.a ≤ x → ∃y.
25 U i x (c*(s x)) = Some ? y.
27 (* C f s means f ∈ O(s) where MSC ∈O(s) *)
28 definition CF ≝ λs,f.∃i.code_for (total f) i ∧ C s i.
30 axiom MSC_in: ∀f,h. CF h f → ∀x. MSC x ≤ h x.
31 axiom MSC_out: ∀f,h. CF h f → ∀x. MSC (f x) ≤ h x.
34 lemma ext_CF : ∀f,g,s. (∀n. f n = g n) → CF s f → CF s g.
35 #f #g #s #Hext * #i * #Hcode #HC %{i} %
36 [#x cases (Hcode x) #a #H %{a} whd in match (total ??); <Hext @H | //]
39 lemma ext_CF1 : ∀f,g,s. (∀n. f n = g n) → CF s g → CF s f.
40 #f #g #s #Hext * #i * #Hcode #HC %{i} %
41 [#x cases (Hcode x) #a #H %{a} whd in match (total ??); >Hext @H | //]
44 lemma monotonic_CF: ∀s1,s2,f.(∀x. s1 x ≤ s2 x) → CF s1 f → CF s2 f.
45 #s1 #s2 #f #H * #i * #Hcode #Hs1
46 %{i} % [//] cases Hs1 #c * #a -Hs1 #Hs1 %{c} %{a} #n #lean
47 cases(Hs1 n lean) #y #Hy %{y} @(monotonic_U …Hy) @le_times //
50 lemma O_to_CF: ∀s1,s2,f.O s2 s1 → CF s1 f → CF s2 f.
51 #s1 #s2 #f #H * #i * #Hcode #Hs1
52 %{i} % [//] cases Hs1 #c * #a -Hs1 #Hs1
53 cases H #c1 * #a1 #Ha1 %{(c*c1)} %{(a+a1)} #n #lean
54 cases(Hs1 n ?) [2:@(transitive_le … lean) //] #y #Hy %{y} @(monotonic_U …Hy)
55 >associative_times @le_times // @Ha1 @(transitive_le … lean) //
58 lemma timesc_CF: ∀s,f,c.CF (λx.c*s x) f → CF s f.
59 #s #f #c @O_to_CF @O_times_c
62 (********************************* composition ********************************)
63 axiom CF_comp: ∀f,g,sf,sg,sh. CF sg g → CF sf f →
64 O sh (λx. sg x + sf (g x)) → CF sh (f ∘ g).
66 lemma CF_comp_ext: ∀f,g,h,sh,sf,sg. CF sg g → CF sf f →
67 (∀x.f(g x) = h x) → O sh (λx. sg x + sf (g x)) → CF sh h.
68 #f #g #h #sh #sf #sg #Hg #Hf #Heq #H @(ext_CF (f ∘ g))
69 [#n normalize @Heq | @(CF_comp … H) //]
72 (************************************* smn ************************************)
73 axiom smn: ∀f,s. CF s f → ∀x. CF (λy.s 〈x,y〉) (λy.f 〈x,y〉).
75 (****************************** constructibility ******************************)
77 definition constructible ≝ λs. CF s s.
79 lemma constr_comp : ∀s1,s2. constructible s1 → constructible s2 →
80 (∀x. x ≤ s2 x) → constructible (s2 ∘ s1).
81 #s1 #s2 #Hs1 #Hs2 #Hle @(CF_comp … Hs1 Hs2) @O_plus @le_to_O #x [@Hle | //]
84 lemma ext_constr: ∀s1,s2. (∀x.s1 x = s2 x) →
85 constructible s1 → constructible s2.
86 #s1 #s2 #Hext #Hs1 @(ext_CF … Hext) @(monotonic_CF … Hs1) #x >Hext //
90 (***************************** primitive recursion ****************************)
94 let rec prim_rec0 (k:nat) (h:nat →nat) n on n ≝
97 | S a ⇒ h 〈a, prim_rec0 k h a〉].
99 lemma prim_rec0_S: ∀k,h,n.
100 prim_rec0 k h (S n) = h 〈n, prim_rec0 k h n〉.
103 let rec prim_rec0_compl (k,sk:nat) (h,sh:nat →nat) n on n ≝
106 | S a ⇒ prim_rec0_compl k sk h sh a + sh (prim_rec0 k h a)].
108 axiom CF_prim_rec0_gen: ∀k,h,sk,sh,sh1,sf. CF sh h →
109 O sh1 (λx.snd x + sh 〈fst x,prim_rec0 k h (fst x)〉) →
110 O sf (prim_rec0 sk sh1) →
111 CF sf (prim_rec0 k h).
113 lemma CF_prim_rec0: ∀k,h,sk,sh,sf. CF sh h →
114 O sf (prim_rec0 sk (λx. snd x + sh 〈fst x,prim_rec0 k h (fst x)〉))
115 → CF sf (prim_rec0 k h).
116 #k #h #sk #sh #sf #Hh #HO @(CF_prim_rec0_gen … Hh … HO) @O_refl
119 (* with arguments. m is a vector of arguments *)
120 let rec prim_rec (k,h:nat →nat) n m on n ≝
123 | S a ⇒ h 〈a,〈prim_rec k h a m, m〉〉].
125 lemma prim_rec_S: ∀k,h,n,m.
126 prim_rec k h (S n) m = h 〈n,〈prim_rec k h n m, m〉〉.
129 lemma prim_rec_le: ∀k1,k2,h1,h2. (∀x.k1 x ≤ k2 x) →
130 (∀x,y.x ≤y → h1 x ≤ h2 y) →
131 ∀x,m. prim_rec k1 h1 x m ≤ prim_rec k2 h2 x m.
132 #k1 #k2 #h1 #h2 #lek #leh #x #m elim x //
133 #n #Hind normalize @leh @le_pair // @le_pair //
136 definition unary_pr ≝ λk,h,x. prim_rec k h (fst x) (snd x).
138 lemma prim_rec_unary: ∀k,h,a,b.
139 prim_rec k h a b = unary_pr k h 〈a,b〉.
140 #k #h #a #b normalize >fst_pair >snd_pair //
143 let rec prim_rec_compl (k,h,sk,sh:nat →nat) n m on n ≝
146 | S a ⇒ prim_rec_compl k h sk sh a m + sh 〈a,〈prim_rec k h a m,m〉〉].
148 axiom CF_prim_rec_gen: ∀k,h,sk,sh,sh1. CF sk k → CF sh h →
149 O sh1 (λx. fst (snd x) +
150 sh 〈fst x,〈unary_pr k h 〈fst x,snd (snd x)〉,snd (snd x)〉〉) →
151 CF (unary_pr sk sh1) (unary_pr k h).
153 lemma CF_prim_rec: ∀k,h,sk,sh,sf. CF sk k → CF sh h →
156 sh 〈fst x,〈unary_pr k h 〈fst x,snd (snd x)〉,snd (snd x)〉〉))
157 → CF sf (unary_pr k h).
158 #k #h #sk #sh #sf #Hk #Hh #Osf @(O_to_CF … Osf) @(CF_prim_rec_gen … Hk Hh)
162 lemma constr_prim_rec: ∀s1,s2. constructible s1 → constructible s2 →
163 (∀n,r,m. 2 * r ≤ s2 〈n,〈r,m〉〉) → constructible (unary_pr s1 s2).
164 #s1 #s2 #Hs1 #Hs2 #Hincr @(CF_prim_rec … Hs1 Hs2) whd %{2} %{0}
165 #x #_ lapply (surj_pair x) * #a * #b #eqx >eqx whd in match (unary_pr ???);
167 whd in match (unary_pr ???); >fst_pair >snd_pair elim a
169 |#n #Hind >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair
170 >prim_rec_S @transitive_le [| @(monotonic_le_plus_l … Hind)]
171 @transitive_le [| @(monotonic_le_plus_l … (Hincr n ? b))]
172 whd in match (unary_pr ???); >fst_pair >snd_pair //
176 (**************************** primitive operations*****************************)
178 definition id ≝ λx:nat.x.
180 axiom CF_id: CF MSC id.
181 axiom CF_const: ∀k.CF MSC (λx.k).
182 axiom CF_comp_fst: ∀h,f. CF h f → CF h (fst ∘ f).
183 axiom CF_comp_snd: ∀h,f. CF h f → CF h (snd ∘ f).
184 axiom CF_comp_pair: ∀h,f,g. CF h f → CF h g → CF h (λx. 〈f x,g x〉).
186 lemma CF_fst: CF MSC fst.
187 @(ext_CF (fst ∘ id)) [#n //] @(CF_comp_fst … CF_id)
190 lemma CF_snd: CF MSC snd.
191 @(ext_CF (snd ∘ id)) [#n //] @(CF_comp_snd … CF_id)
194 (**************************** arithmetic operations ***************************)
196 axiom CF_compS: ∀h,f. CF h f → CF h (S ∘ f).
197 axiom CF_le: ∀h,f,g. CF h f → CF h g → CF h (λx. leb (f x) (g x)).
198 axiom CF_eqb: ∀h,f,g. CF h f → CF h g → CF h (λx.eqb (f x) (g x)).
199 axiom CF_max1: ∀h,f,g. CF h f → CF h g → CF h (λx. max (f x) (g x)).
200 axiom CF_plus: ∀h,f,g. CF h f → CF h g → CF h (λx. f x + g x).
201 axiom CF_minus: ∀h,f,g. CF h f → CF h g → CF h (λx. f x - g x).
203 (******************************** if then else ********************************)
205 lemma if_prim_rec: ∀b:nat → bool. ∀f,g:nat → nat.∀x:nat.
206 if b x then f x else g x = prim_rec g (f ∘ snd ∘ snd) (b x) x.
207 #b #f #g #x cases (b x) normalize //
210 lemma CF_if: ∀b:nat → bool. ∀f,g,s. CF s b → CF s f → CF s g →
211 CF s (λx. if b x then f x else g x).
212 #b #f #g #s #CFb #CFf #CFg @(ext_CF (λx.unary_pr g (f ∘ snd ∘ snd) 〈b x,x〉))
213 [#n @sym_eq normalize >fst_pair >snd_pair @if_prim_rec
215 [|@CF_comp_pair // @(O_to_CF … CF_id) @le_to_O @MSC_in //
216 |@(CF_prim_rec_gen ??? (λx.MSC x + s(snd (snd x))) … CFg) [3:@O_refl|]
217 @(CF_comp … (λx.MSC x + s(snd x)) … CF_snd)
218 [@(CF_comp … s … CF_snd CFf) @O_refl
222 [@O_plus_l @le_to_O #x @monotonic_MSC //
227 |%{6} %{0} #n #_ normalize in ⊢ (??%); <plus_n_O cases (b n) normalize
228 >snd_pair >fst_pair normalize
229 [@le_plus [//] >fst_pair >fst_pair >snd_pair >fst_pair
230 @le_plus [//] >snd_pair >snd_pair >snd_pair >snd_pair
231 <associative_plus <associative_plus @le_plus [|//]
232 @(transitive_le … (MSC_pair …)) >associative_plus @le_plus
233 [@(transitive_le ???? (MSC_in … CFf n)) @monotonic_MSC //
234 |@(transitive_le … (MSC_pair …)) @le_plus [|@(MSC_in … CFf)]
235 normalize @MSC_out @CFg
243 (********************************* simulation *********************************)
245 definition pU_unary ≝ λp. pU (fst p) (fst (snd p)) (snd (snd p)).
247 axiom sU : nat → nat.
248 axiom CF_U : CF sU pU_unary.
250 axiom monotonic_sU: ∀i1,i2,x1,x2,s1,s2. i1 ≤ i2 → x1 ≤ x2 → s1 ≤ s2 →
251 sU 〈i1,〈x1,s1〉〉 ≤ sU 〈i2,〈x2,s2〉〉.
253 lemma monotonic_sU_aux : ∀x1,x2. fst x1 ≤ fst x2 → fst (snd x1) ≤ fst (snd x2) →
254 snd (snd x1) ≤ snd (snd x2) → sU x1 ≤ sU x2.
255 #x1 #x2 cases (surj_pair x1) #a1 * #y #eqx1 >eqx1 -eqx1 cases (surj_pair y)
256 #b1 * #c1 #eqy >eqy -eqy
257 cases (surj_pair x2) #a2 * #y2 #eqx2 >eqx2 -eqx2 cases (surj_pair y2)
258 #b2 * #c2 #eqy2 >eqy2 -eqy2 >fst_pair >snd_pair >fst_pair >snd_pair
259 >fst_pair >snd_pair >fst_pair >snd_pair @monotonic_sU
262 axiom sU_pos: ∀x. 0 < sU x.
264 axiom sU_le: ∀i,x,s. s ≤ sU 〈i,〈x,s〉〉.
266 lemma sU_le_i: ∀i,x,s. MSC i ≤ sU 〈i,〈x,s〉〉.
267 #i #x #s @(transitive_le ???? (MSC_in … CF_U 〈i,〈x,s〉〉)) @monotonic_MSC //
270 lemma sU_le_x: ∀i,x,s. MSC x ≤ sU 〈i,〈x,s〉〉.
271 #i #x #s @(transitive_le ???? (MSC_in … CF_U 〈i,〈x,s〉〉)) @monotonic_MSC
272 @(transitive_le … 〈x,s〉) //
278 definition termb_unary ≝ λx:ℕ.termb (fst x) (fst (snd x)) (snd (snd x)).
279 definition out_unary ≝ λx:ℕ.out (fst x) (fst (snd x)) (snd (snd x)).
281 lemma CF_termb: CF sU termb_unary.
282 @(ext_CF (fst ∘ pU_unary)) [2: @CF_comp_fst @CF_U]
283 #n whd in ⊢ (??%?); whd in ⊢ (??(?%)?); >fst_pair %
286 lemma CF_out: CF sU out_unary.
287 @(ext_CF (snd ∘ pU_unary)) [2: @CF_comp_snd @CF_U]
288 #n whd in ⊢ (??%?); whd in ⊢ (??(?%)?); >snd_pair %