matita/matita/lib/reverse_complexity/gap.ma

   1
   2 include "arithmetics/minimization.ma".
   3 include "arithmetics/bigops.ma".
   4 include "arithmetics/pidgeon_hole.ma".
   5 include "arithmetics/iteration.ma".
   6
   7 (************************** notation for miminimization ***********************)
   8
   9 (* an alternative defintion of minimization
  10 definition Min ≝ λa,f.
  11   \big[min,a]_{i < a | f i} i. *)
  12
  13 notation "μ_{ ident i < n } p"
  14   with precedence 80 for @{min $n 0 (λ${ident i}.$p)}.
  15
  16 notation "μ_{ ident i ≤ n } p"
  17   with precedence 80 for @{min (S $n) 0 (λ${ident i}.$p)}.
  18
  19 notation "μ_{ ident i ∈ [a,b] } p"
  20   with precedence 80 for @{min (S $b-$a) $a (λ${ident i}.$p)}.
  21
  22 lemma f_min_true: ∀f,a,b.
  23   (∃i. a ≤ i ∧ i ≤ b ∧ f i = true) → f (μ_{i ∈[a,b]} (f i)) = true.
  24 #f #a #b * #i * * #Hil #Hir #Hfi @(f_min_true … (λx. f x)) <plus_minus_m_m
  25   [%{i} % // % [@Hil |@le_S_S @Hir]|@le_S @(transitive_le … Hil Hir)]
  26 qed.
  27
  28 lemma min_up: ∀f,a,b.
  29   (∃i. a ≤ i ∧ i ≤ b ∧ f i = true) → μ_{i ∈[a,b]}(f i) ≤ b.
  30 #f #a #b * #i * * #Hil #Hir #Hfi @le_S_S_to_le
  31 cut ((S b) = S b - a + a) [@plus_minus_m_m @le_S @(transitive_le … Hil Hir)]
  32 #Hcut >Hcut in ⊢ (??%); @lt_min %{i} % // % [@Hil |<Hcut @le_S_S @Hir]
  33 qed.
  34
  35 (*************************** Kleene's predicate *******************************)
  36
  37 axiom U: nat → nat →nat → option nat.
  38
  39 axiom monotonic_U: ∀i,x,n,m,y.n ≤m →
  40   U i x n = Some ? y → U i x m = Some ? y.
  41
  42 lemma unique_U: ∀i,x,n,m,yn,ym.
  43   U i x n = Some ? yn → U i x m = Some ? ym → yn = ym.
  44 #i #x #n #m #yn #ym #Hn #Hm cases (decidable_le n m)
  45   [#lenm lapply (monotonic_U … lenm Hn) >Hm #HS destruct (HS) //
  46   |#ltmn lapply (monotonic_U … n … Hm) [@lt_to_le @not_le_to_lt //]
  47    >Hn #HS destruct (HS) //
  48   ]
  49 qed.
  50
  51 definition terminate ≝ λi,x,r. ∃y. U i x r = Some ? y.
  52
  53 notation "〈i,x〉 ↓ r" with precedence 60 for @{terminate $i $x $r}.
  54
  55 lemma terminate_dec: ∀i,x,n. 〈i,x〉 ↓ n ∨ ¬ 〈i,x〉 ↓ n.
  56 #i #x #n normalize cases (U i x n)
  57   [%2 % * #y #H destruct|#y %1 %{y} //]
  58 qed.
  59
  60 definition termb ≝ λi,x,t.
  61   match U i x t with [None ⇒ false |Some y ⇒ true].
  62
  63 lemma termb_true_to_term: ∀i,x,t. termb i x t = true → 〈i,x〉 ↓ t.
  64 #i #x #t normalize cases (U i x t) normalize [#H destruct | #y #_ %{y} //]
  65 qed.
  66
  67 lemma term_to_termb_true: ∀i,x,t. 〈i,x〉 ↓ t → termb i x t = true.
  68 #i #x #t * #y #H normalize >H //
  69 qed.
  70
  71 lemma decidable_test : ∀n,x,r,r1.
  72        (∀i. i < n → 〈i,x〉 ↓ r ∨ ¬ 〈i,x〉 ↓ r1) ∨
  73        (∃i. i < n ∧ (¬ 〈i,x〉 ↓ r ∧ 〈i,x〉 ↓ r1)).
  74 #n #x #r1 #r2
  75   cut (∀i0.decidable ((〈i0,x〉↓r1) ∨ ¬ 〈i0,x〉 ↓ r2))
  76     [#j @decidable_or [@terminate_dec |@decidable_not @terminate_dec ]] #Hdec
  77  cases(decidable_forall ? Hdec n)
  78   [#H %1 @H
  79   |#H %2 cases (not_forall_to_exists … Hdec H) #j * #leji #Hj
  80    %{j} % // %
  81     [@(not_to_not … Hj) #H %1 @H
  82     |cases (terminate_dec j x r2) // #H @False_ind cases Hj -Hj #Hj
  83      @Hj %2 @H
  84   ]
  85 qed.
  86
  87 (**************************** the gap theorem *********************************)
  88 definition gapP ≝ λn,x,g,r. ∀i. i < n → 〈i,x〉 ↓ r ∨ ¬ 〈i,x〉 ↓ g r.
  89
  90 lemma gapP_def : ∀n,x,g,r.
  91   gapP n x g r = ∀i. i < n → 〈i,x〉 ↓ r ∨ ¬ 〈i,x〉 ↓ g r.
  92 // qed.
  93
  94 lemma upper_bound_aux: ∀g,b,n,x. (∀x. x ≤ g x) → ∀k.
  95   (∃j.j < k ∧
  96     (∀i. i < n → 〈i,x〉 ↓ g^j b ∨ ¬ 〈i,x〉 ↓ g^(S j) b)) ∨
  97   ∃l. |l| = k ∧ unique ? l ∧ ∀i. i ∈ l → i < n ∧ 〈i,x〉 ↓ g^k b .
  98 #g#b #n #x #Hg #k elim k
  99   [%2 %{([])} normalize % [% //|#x @False_ind]
 100   |#k0 *
 101     [* #j * #lej #H %1 %{j} % [@le_S // | @H ]
 102     |* #l * * #Hlen #Hunique #Hterm
 103      cases (decidable_test n x (g^k0 b) (g^(S k0) b))
 104       [#Hcase %1 %{k0} % [@le_n | @Hcase]
 105       |* #j * #ltjn * #H1 #H2 %2
 106        %{(j::l)} %
 107         [ % [normalize @eq_f @Hlen] whd % // % #H3
 108          @(absurd ?? H1) @(proj2 … (Hterm …)) @H3
 109         |#x *
 110           [#eqxj >eqxj % //
 111           |#Hmemx cases(Hterm … Hmemx) #lexn * #y #HU
 112            % [@lexn] %{y} @(monotonic_U ?????? HU) @Hg
 113           ]
 114         ]
 115       ]
 116     ]
 117   ]
 118 qed.
 119
 120 lemma upper_bound: ∀g,b,n,x. (∀x. x ≤ g x) → ∃r.
 121   (* b ≤ r ∧ r ≤ g^n b ∧ ∀i. i < n → 〈i,x〉 ↓ r ∨ ¬ 〈i,x〉 ↓ g r. *)
 122   b ≤ r ∧ r ≤ g^n b ∧ gapP n x g r.
 123 #g #b #n #x #Hg
 124 cases (upper_bound_aux g b n x Hg n)
 125   [* #j * #Hj #H %{(g^j b)} % [2: @H] % [@le_iter //]
 126    @monotonic_iter2 // @lt_to_le //
 127   |* #l * * #Hlen #Hunique #Hterm %{(g^n b)} %
 128     [% [@le_iter // |@le_n]]
 129    #i #lein %1 @(proj2 … (Hterm ??))
 130    @(eq_length_to_mem_all … Hlen Hunique … lein)
 131    #x #memx @(proj1  … (Hterm ??)) //
 132   ]
 133 qed.
 134
 135 definition gapb ≝ λn,x,g,r.
 136   \big[andb,true]_{i < n} ((termb i x r) ∨ ¬(termb i x (g r))).
 137
 138 lemma gapb_def : ∀n,x,g,r. gapb n x g r =
 139   \big[andb,true]_{i < n} ((termb i x r) ∨ ¬(termb i x (g r))).
 140 // qed.
 141
 142 lemma gapb_true_to_gapP : ∀n,x,g,r.
 143   gapb n x g r = true → ∀i. i < n → 〈i,x〉 ↓ r ∨ ¬(〈i,x〉 ↓ (g r)).
 144 #n #x #g #r elim n
 145   [>gapb_def >bigop_Strue //
 146    #H #i #lti0 @False_ind @(absurd … lti0) @le_to_not_lt //
 147   |#m #Hind >gapb_def >bigop_Strue //
 148    #H #i #leSm cases (le_to_or_lt_eq … leSm)
 149     [#lem @Hind [@(andb_true_r … H)|@le_S_S_to_le @lem]
 150     |#eqi >(injective_S … eqi) lapply (andb_true_l … H) -H #H cases (orb_true_l … H) -H
 151       [#H %1 @termb_true_to_term //
 152       |#H %2 % #H1 >(term_to_termb_true …  H1) in H; normalize #H destruct
 153       ]
 154     ]
 155   ]
 156 qed.
 157
 158 lemma gapP_to_gapb_true : ∀n,x,g,r.
 159   (∀i. i < n → 〈i,x〉 ↓ r ∨ ¬(〈i,x〉 ↓ (g r))) → gapb n x g r = true.
 160 #n #x #g #r elim n //
 161 #m #Hind #H >gapb_def >bigop_Strue // @true_to_andb_true
 162   [cases (H m (le_n …))
 163     [#H2 @orb_true_r1 @term_to_termb_true //
 164     |#H2 @orb_true_r2 @sym_eq @noteq_to_eqnot @sym_not_eq
 165      @(not_to_not … H2) @termb_true_to_term
 166     ]
 167   |@Hind #i0 #lei0 @H @le_S //
 168   ]
 169 qed.
 170
 171
 172 (* the gap function *)
 173 let rec gap g n on n ≝
 174   match n with
 175   [ O ⇒ 1
 176   | S m ⇒ let b ≝ gap g m in μ_{i ∈ [b,g^n b]} (gapb n n g i)
 177   ].
 178
 179 lemma gapS: ∀g,m.
 180   gap g (S m) =
 181     (let b ≝ gap g m in
 182       μ_{i ∈ [b,g^(S m) b]} (gapb (S m) (S m) g i)).
 183 // qed.
 184
 185 lemma upper_bound_gapb: ∀g,m. (∀x. x ≤ g x) →
 186   ∃r:ℕ.gap g m ≤ r ∧ r ≤ g^(S m) (gap g m) ∧ gapb (S m) (S m) g r = true.
 187 #g #m #leg
 188 lapply (upper_bound g (gap g m) (S m) (S m) leg) * #r * *
 189 #H1 #H2 #H3 %{r} %
 190   [% // |@gapP_to_gapb_true @H3]
 191 qed.
 192
 193 lemma gapS_true: ∀g,m. (∀x. x ≤g x) → gapb (S m) (S m) g (gap g (S m)) = true.
 194 #g #m #leg @(f_min_true (gapb (S m) (S m) g)) @upper_bound_gapb //
 195 qed.
 196
 197 theorem gap_theorem: ∀g,i.(∀x. x ≤ g x)→∃k.∀n.k < n →
 198    〈i,n〉 ↓ (gap g n) ∨ ¬ 〈i,n〉 ↓ (g (gap g n)).
 199 #g #i #leg %{i} *
 200   [#lti0 @False_ind @(absurd ?? (not_le_Sn_O i) ) //
 201   |#m #leim lapply (gapS_true g m leg) #H
 202    @(gapb_true_to_gapP … H) //
 203   ]
 204 qed.
 205
 206 (* an upper bound *)
 207
 208 let rec sigma n ≝
 209   match n with
 210   [ O ⇒ 0 | S m ⇒ n + sigma m ].
 211
 212 lemma gap_bound: ∀g. (∀x. x ≤ g x) → (monotonic ? le g) →
 213   ∀n.gap g n ≤ g^(sigma n) 1.
 214 #g #leg #gmono #n elim n
 215   [normalize //
 216   |#m #Hind >gapS @(transitive_le ? (g^(S m) (gap g m)))
 217     [@min_up @upper_bound_gapb //
 218     |@(transitive_le ? (g^(S m) (g^(sigma m) 1)))
 219       [@monotonic_iter // |>iter_iter >commutative_plus @le_n
 220     ]
 221   ]
 222 qed.
 223
 224 lemma gap_bound2: ∀g. (∀x. x ≤ g x) → (monotonic ? le g) →
 225   ∀n.gap g n ≤ g^(n*n) 1.
 226 #g #leg #gmono #n elim n
 227   [normalize //
 228   |#m #Hind >gapS @(transitive_le ? (g^(S m) (gap g m)))
 229     [@min_up @upper_bound_gapb //
 230     |@(transitive_le ? (g^(S m) (g^(m*m) 1)))
 231       [@monotonic_iter //
 232       |>iter_iter @monotonic_iter2 [@leg | normalize <plus_n_Sm @le_S_S //
 233     ]
 234   ]
 235 qed.
 236
 237 (*
 238 axiom universal: ∃u.∀i,x,y.
 239   ∃n. U u 〈i,x〉 n = Some y ↔ ∃m.U i x m = Some y. *)
 240
 241
 242
 243
 244
 245
 246
 247
 248
 249
 250
 251