matita/matita/lib/reverse_complexity/complexity.ma

   1 include "reverse_complexity/basics.ma".
   2 include "reverse_complexity/big_O.ma".
   3
   4 (********************************* complexity *********************************)
   5
   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. *)
  10
  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.
  15
  16 axiom monotonic_MSC: monotonic ? le MSC.
  17 axiom MSC_pair_eq: ∀a,b. MSC 〈a,b〉 = MSC a + MSC b.
  18
  19
  20 lemma MSC_pair: ∀a,b. MSC 〈a,b〉 ≤ MSC a + MSC b. // qed.
  21
  22 (* C s i means i is running in O(s) *)
  23
  24 definition C ≝ λs,i.∃c.∃a.∀x.a ≤ x → ∃y.
  25   U i x (c*(s x)) = Some ? y.
  26
  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.
  29
  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.
  32
  33
  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 | //]
  37 qed.
  38
  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 | //]
  42 qed.
  43
  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 //
  48 qed.
  49
  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) //
  56 qed.
  57
  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
  60 qed.
  61
  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).
  65
  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) //]
  70 qed.
  71
  72 (************************************* smn ************************************)
  73 axiom smn: ∀f,s. CF s f → ∀x. CF (λy.s 〈x,y〉) (λy.f 〈x,y〉).
  74
  75 (****************************** constructibility ******************************)
  76
  77 definition constructible ≝ λs. CF s s.
  78
  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 | //]
  82 qed.
  83
  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 //
  87 qed.
  88
  89
  90 (***************************** primitive recursion ****************************)
  91
  92 (* no arguments *)
  93
  94 let rec prim_rec0 (k:nat) (h:nat →nat) n on n ≝
  95   match n with
  96   [ O ⇒ k
  97   | S a ⇒ h 〈a, prim_rec0 k h a〉].
  98
  99 lemma prim_rec0_S: ∀k,h,n.
 100   prim_rec0 k h (S n) = h 〈n, prim_rec0 k h n〉.
 101 // qed.
 102
 103 let rec prim_rec0_compl (k,sk:nat) (h,sh:nat →nat) n on n ≝
 104   match n with
 105   [ O ⇒ sk
 106   | S a ⇒ prim_rec0_compl k sk h sh a + sh (prim_rec0 k h a)].
 107
 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).
 112
 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
 117 qed.
 118
 119 (* with arguments. m is a vector of arguments *)
 120 let rec prim_rec (k,h:nat →nat) n m on n ≝
 121   match n with
 122   [ O ⇒ k m
 123   | S a ⇒ h 〈a,〈prim_rec k h a m, m〉〉].
 124
 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〉〉.
 127 // qed.
 128
 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 //
 134 qed.
 135
 136 definition unary_pr ≝ λk,h,x. prim_rec k h (fst x) (snd x).
 137
 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 //
 141 qed.
 142
 143 let rec prim_rec_compl (k,h,sk,sh:nat →nat) n m on n ≝
 144   match n with
 145   [ O ⇒ sk m
 146   | S a ⇒ prim_rec_compl k h sk sh a m + sh 〈a,〈prim_rec k h a m,m〉〉].
 147
 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).
 152
 153 lemma CF_prim_rec: ∀k,h,sk,sh,sf. CF sk k → CF sh h →
 154   O sf (unary_pr sk
 155         (λx. fst (snd x) +
 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)
 159 @O_refl
 160 qed.
 161
 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 ???);
 166 >fst_pair >snd_pair
 167 whd in match (unary_pr ???); >fst_pair >snd_pair elim a
 168   [normalize //
 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 //
 173   ]
 174 qed.
 175
 176 (**************************** primitive operations*****************************)
 177
 178 definition id ≝ λx:nat.x.
 179
 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〉).
 185
 186 lemma CF_fst: CF MSC fst.
 187 @(ext_CF (fst ∘ id)) [#n //] @(CF_comp_fst … CF_id)
 188 qed.
 189
 190 lemma CF_snd: CF MSC snd.
 191 @(ext_CF (snd ∘ id)) [#n //] @(CF_comp_snd … CF_id)
 192 qed.
 193
 194 (**************************** arithmetic operations ***************************)
 195
 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).
 202
 203 (******************************** if then else ********************************)
 204
 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 //
 208 qed.
 209
 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
 214   |@(CF_comp ??? s)
 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
 219       |@O_plus
 220         [@O_plus_l @O_refl
 221         |@O_plus
 222           [@O_plus_l @le_to_O #x @monotonic_MSC //
 223           |@O_plus_r @O_refl
 224           ]
 225         ]
 226       ]
 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
 236         ]
 237       |@le_plus //
 238       ]
 239     ]
 240   ]
 241 qed.
 242
 243 (********************************* simulation *********************************)
 244
 245 definition pU_unary ≝ λp. pU (fst p) (fst (snd p)) (snd (snd p)).
 246
 247 axiom sU : nat → nat.
 248 axiom CF_U : CF sU pU_unary.
 249
 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〉〉.
 252
 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
 260 qed.
 261
 262 axiom sU_pos: ∀x. 0 < sU x.
 263
 264 axiom sU_le: ∀i,x,s. s ≤ sU 〈i,〈x,s〉〉.
 265
 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 //
 268 qed.
 269
 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〉) //
 273 qed.
 274
 275
 276
 277
 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)).
 280
 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 %
 284 qed.
 285
 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 %
 289 qed.
 290