weblib/Reverse_complexity/reverse.ma

   1
   2 include "arithmetics/nat.ma".
   3 include "basics/types.ma".
   4 include "arithmetics/min_max.ma".
   5 include "arithmetics/bigO.ma".
   6
   7 (*********************************** pairing **********************************)
   8
   9 axiom pair: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
  10 axiom fst : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
  11 axiom snd : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
  12 axiom fst_pair: ∀a,b. \ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/pair.dec"\ 6pair\ 5/a\ 6 a b) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a.
  13 axiom snd_pair: ∀a,b. \ 5a href="cic:/matita/Reverse_complexity/reverse/snd.dec"\ 6snd\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/pair.dec"\ 6pair\ 5/a\ 6 a b) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b.
  14
  15 interpretation "abstract pair" 'pair f g = (pair f g).
  16
  17 (************************ basic complexity notions ****************************)
  18
  19 (* u is the deterministic configuration relation of the universal machine (one
  20    step) *)
  21
  22 axiom u: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/basics/types/option.ind(1,0,1)"\ 6option\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
  23
  24 let rec U c n on n ≝
  25   match n with
  26   [ O ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
  27   | S m ⇒ match \ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 c with
  28     [ None ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? c (* halting case *)
  29     | Some c1 ⇒ U c1 m
  30     ]
  31   ].
  32
  33 lemma halt_U: ∀i,n,y. \ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ? → \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y → y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 i.
  34 #i #n #y #H cases n
  35   [normalize #H1 destruct |#m normalize >H normalize #H1 destruct //]
  36 qed.
  37
  38 lemma Some_to_halt: ∀n,i,y. \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y → \ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ? .
  39 #n elim n
  40   [#i #y normalize #H destruct (H)
  41   |#m #Hind #i #y normalize
  42    cut (\ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ? \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6c. \ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? c)
  43     [cases (\ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 i) [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | #c %2 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ ]]
  44    *[#H >H normalize #H1 destruct (H1) // |* #c #H >H normalize @Hind ]
  45   ]
  46 qed.
  47
  48 lemma monotonici_U: ∀y,n,m,i.
  49   \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y → \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i (n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y.
  50 #y #n #m elim m
  51   [#i normalize #H destruct
  52   |#p #Hind #i <\ 5a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"\ 6plus_n_Sm\ 5/a\ 6 normalize
  53     cut (\ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ? \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6c. \ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? c)
  54     [cases (\ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 i) [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | #c %2 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ ]]
  55    *[#H1 >H1 normalize // |* #c #H >H normalize #H1 @Hind //]
  56   ]
  57 qed.
  58
  59 lemma monotonic_U: ∀i,n,m,y.n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6m →
  60   \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y → \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y.
  61 #i #n #m #y #lenm #H >(\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 m n) // @\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonici_U.def(5)"\ 6monotonici_U\ 5/a\ 6 //
  62 qed.
  63
  64 (* axiom U: nat → nat → option nat. *)
  65 (* axiom monotonic_U: ∀i,n,m,y.n ≤m →
  66    U i n = Some ? y → U i m = Some ? y. *)
  67
  68 lemma unique_U: ∀i,n,m,yn,ym.
  69   \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? yn → \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? ym → yn \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 ym.
  70 #i #n #m #yn #ym #Hn #Hm cases (\ 5a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"\ 6decidable_le\ 5/a\ 6 n m)
  71   [#lenm lapply (\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"\ 6monotonic_U\ 5/a\ 6 … lenm Hn) >Hm #HS destruct (HS) //
  72   |#ltmn lapply (\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"\ 6monotonic_U\ 5/a\ 6 … n … Hm) [@\ 5a href="cic:/matita/arithmetics/nat/lt_to_le.def(6)"\ 6lt_to_le\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"\ 6not_le_to_lt\ 5/a\ 6 //]
  73    >Hn #HS destruct (HS) //
  74   ]
  75 qed.
  76
  77 definition code_for ≝ λf,i.∀x.
  78   \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6n.∀m. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 〈i,x\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x.
  79
  80 definition terminate ≝ λc,r. \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6y. \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 c r \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y.
  81
  82 interpretation "termination" 'fintersects c r = (terminate c r).
  83
  84 definition lang ≝ λi,x.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6r,y\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6 \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 〈i,x\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 r \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6  \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 y.
  85
  86 lemma lang_cf :∀f,i,x. \ 5a href="cic:/matita/Reverse_complexity/reverse/code_for.def(2)"\ 6code_for\ 5/a\ 6 f i →
  87   \ 5a href="cic:/matita/Reverse_complexity/reverse/lang.def(2)"\ 6lang\ 5/a\ 6 i x \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6y.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 y.
  88 #f #i #x normalize #H %
  89   [* #n * #y * #H1 #posy %{y} % //
  90    cases (H x) -H #m #H <(H (\ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 n m)) [2:@(\ 5a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"\ 6le_maxr\ 5/a\ 6 … n) //]
  91    @(\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"\ 6monotonic_U\ 5/a\ 6 … H1) @(\ 5a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"\ 6le_maxl\ 5/a\ 6 … m) //
  92   |cases (H x) -H #m #Hm * #y #Hy %{m} %{y} >Hm //
  93   ]
  94 qed.
  95
  96 (******************************* complexity classes ***************************)
  97
  98 axiom size: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
  99 axiom of_size: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
 100
 101 interpretation "size" 'card n = (size n).
 102
 103 axiom size_of_size: ∀n. |\ 5a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"\ 6of_size\ 5/a\ 6 n\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n.
 104 axiom of_size_max: ∀i,n. |i\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n → i \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"\ 6of_size\ 5/a\ 6 n.
 105
 106 axiom size_fst : ∀n. |\ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 n\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 |n\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
 107
 108 axiom a : Max0.
 109
 110 definition size_f ≝ λf,n.Max_{i\ 5font class="Apple-style-span" color="#FF0000"\ 6 < \ 5/font\ 6S (of_size n) | eqb (|i|) n }|(f i)|.
 111
 112 lemma size_f_def: ∀f,n. size_f f n =
 113   Max_{i < S (of_size n) | eqb (|i|) n}|(f i)|.
 114 // qed.
 115
 116 lemma size_f_size : ∀f,n. size_f (f ∘ size) n = |(f n)|.
 117 #f #n @le_to_le_to_eq
 118   [@Max_le #a #lta #Ha normalize >(eqb_true_to_eq  … Ha) //
 119   |<(size_of_size n) in ⊢ (?%?); >size_f_def
 120    @(le_Max (λi.|f (|i|)|) ? (S (of_size n)) (of_size n) ??)
 121     [@le_S_S // | @eq_to_eqb_true //]
 122   ]
 123 qed.
 124
 125 lemma size_f_id : ∀n. size_f (λx.x) n = n.
 126 #n @le_to_le_to_eq
 127   [@Max_le #a #lta #Ha >(eqb_true_to_eq  … Ha) //
 128   |<(size_of_size n) in ⊢ (?%?); >size_f_def
 129    @(le_Max (λi.|i|) ? (S (of_size n)) (of_size n) ??)
 130     [@le_S_S // | @eq_to_eqb_true //]
 131   ]
 132 qed.
 133
 134 lemma size_f_fst : ∀n. size_f fst n ≤ n.
 135 #n @Max_le #a #lta #Ha <(eqb_true_to_eq  … Ha) //
 136 qed.
 137
 138 (* definition def ≝ λf:nat → option nat.λx.∃y. f x = Some ? y.*)
 139
 140 (* C s i means that the complexity of i is O(s) *)
 141
 142 definition C ≝ λs,i.∃c.∃a.∀x.a ≤ |x| → ∃y.
 143   U 〈i,x〉 (c*(s(|x|))) = Some ? y.
 144
 145 definition CF ≝ λs,f.∃i.code_for f i ∧ C s i.
 146
 147 lemma ext_CF : ∀f,g,s. (∀n. f n = g n) → CF s f → CF s g.
 148 #f #g #s #Hext * #i * #Hcode #HC %{i} %
 149   [#x cases (Hcode x) #a #H %{a} <Hext @H | //]
 150 qed.
 151
 152 lemma monotonic_CF: ∀s1,s2,f. O s2 s1 → CF s1 f → CF s2 f.
 153 #s1 #s2 #f * #c1 * #a #H * #i * #Hcodef #HCs1 %{i} % //
 154 cases HCs1 #c2 * #b #H2 %{(c2*c1)} %{(max a b)}
 155 #x #Hmax cases (H2 x ?) [2:@(le_maxr … Hmax)] #y #Hy
 156 %{y} @(monotonic_U …Hy) >associative_times @le_times // @H @(le_maxl … Hmax)
 157 qed.
 158
 159 (************************** The diagonal language *****************************)
 160
 161 (* the diagonal language used for the hierarchy theorem *)
 162
 163 definition diag ≝ λs,i.
 164   U 〈fst i,i〉 (s (|i|)) = Some ? 0.
 165
 166 lemma equiv_diag: ∀s,i.
 167   diag s i ↔ 〈fst i, i〉 ↓ s (|i|) ∧ ¬lang (fst i) i.
 168 #s #i %
 169   [whd in ⊢ (%→?); #H % [%{0} //] % * #x * #y *
 170    #H1 #Hy cut (0 = y) [@(unique_U … H H1)] #eqy /2/
 171   |* * #y cases y //
 172    #y0 #H * #H1 @False_ind @H1 -H1 whd %{(s (|i|))} %{(S y0)} % //
 173   ]
 174 qed.
 175
 176 (* Let us define the characteristic function diag_cf for diag, and prove
 177 it correctness *)
 178
 179 definition diag_cf ≝ λs,i.
 180   match U 〈fst i,i〉 (s (|i|)) with
 181   [ None ⇒ None ?
 182   | Some y ⇒ if (eqb y 0) then (Some ? 1) else (Some ? 0)].
 183
 184 lemma diag_cf_OK: ∀s,x. diag s x ↔ ∃y.diag_cf s x = Some ? y ∧ 0 < y.
 185 #s #x %
 186   [whd in ⊢ (%→?); #H %{1} % // whd in ⊢ (??%?); >H //
 187   |* #y * whd in ⊢ (??%?→?→%);
 188    cases (U 〈fst x,x〉 (s (|x|))) normalize
 189     [#H destruct
 190     |#x cases (true_or_false (eqb x 0)) #Hx >Hx
 191       [>(eqb_true_to_eq … Hx) //
 192       |normalize #H destruct #H @False_ind @(absurd ? H) @lt_to_not_le //
 193       ]
 194     ]
 195   ]
 196 qed.
 197
 198 lemma diag_spec: ∀s,i. code_for (diag_cf s) i → ∀x. lang i x ↔ diag s x.
 199 #s #i #Hcode #x @(iff_trans  … (lang_cf … Hcode)) @iff_sym @diag_cf_OK
 200 qed.
 201
 202 (******************************************************************************)
 203
 204 lemma absurd1: ∀P. iff P (¬ P) →False.
 205 #P * #H1 #H2 cut (¬P) [% #H2 @(absurd … H2) @H1 //]
 206 #H3 @(absurd ?? H3) @H2 @H3
 207 qed.
 208
 209 (* axiom weak_pad : ∀a,∃a0.∀n. a0 < n → ∃b. |〈a,b〉| = n. *)
 210 axiom pad : ∀a,n. |a| < n → ∃b. |〈a,b〉| = n.
 211
 212 lemma not_included_ex: ∀s1,s2. not_O s2 s1 → ∀i. C s2 i →
 213   ∃b.〈i, 〈i,b〉〉 ↓ s1 (|〈i,b〉|).
 214 #s1 #s2  #H #i * #c * #x0 #H1
 215 cases (H c (max (S(|i|)) x0)) #x1 * #H2 #H3 cases (pad i x1 ?)
 216   [#b #H4 %{b}
 217    cases (H1 〈i,b〉 ?)
 218     [#z >H4 #H5 %{z} @(monotonic_U … H5) @lt_to_le //
 219     |>H4 @(le_maxr … H2)
 220     ]
 221   |@(le_maxl … H2)
 222   ]
 223 qed.
 224
 225 lemma diag1_not_s1: ∀s1,s2. not_O s2 s1 → ¬ CF s2 (diag_cf s1).
 226 #s1 #s2 #H1 % * #i * #Hcode_i #Hs2_i
 227 cases (not_included_ex  … H1 ? Hs2_i) #b #H2
 228 lapply (diag_spec … Hcode_i) #H3
 229 @(absurd1 (lang i 〈i,b〉))
 230 @(iff_trans … (H3 〈i,b〉))
 231 @(iff_trans … (equiv_diag …)) >fst_pair
 232 %[* #_ // |#H6 % // ]
 233 qed.
 234
 235 (******************************************************************************)
 236 (* definition sumF ≝ λf,g:nat→nat.λn.f n + g n. *)
 237
 238 definition to_Some ≝ λf.λx:nat. Some nat (f x).
 239
 240 definition deopt ≝ λn. match n with
 241   [ None ⇒ 1
 242   | Some n ⇒ n].
 243
 244 definition opt_comp ≝ λf,g:nat → option nat. λx.
 245   match g x with
 246   [ None ⇒ None ?
 247   | Some y ⇒ f y ].
 248
 249 (* axiom CFU: ∀h,g,s. CF s (to_Some h)  → CF s (to_Some (of_size ∘ g)) →
 250   CF (Slow s) (λx.U (h x) (g x)). *)
 251
 252 axiom sU2: nat → nat → nat.
 253 axiom sU: nat → nat → nat → nat.
 254
 255 (* axiom CFU: CF sU (λx.U (fst x) (snd x)). *)
 256
 257 axiom CFU: ∀h,g,f,s1,s2,s3.
 258   CF s1 (to_Some h)  → CF s2 (to_Some g) → CF s3 (to_Some f) →
 259   CF (λx. s1 x + s2 x + s3 x + sU (size_f h x) (size_f g x) (size_f f x))
 260     (λx.U 〈h x,g x〉 (|f x|)).
 261
 262 axiom monotonic_sU: ∀a1,a2,b1,b2,c1,c2. a1 ≤ a2 → b1 ≤ b2 → c1 ≤c2 →
 263   sU a1 b1 c1 ≤ sU a2 b2 c2.
 264
 265 definition sU_space ≝ λi,x,r.i+x+r.
 266 definition sU_time ≝ λi,x,r.i+x+(i^2)*r*(log 2 r).
 267
 268 (*
 269 axiom CF_comp: ∀f,g,s1, s2. CF s1 f → CF s2 g →
 270   CF (λx.s2 x + s1 (size (deopt (g x)))) (opt_comp f g).
 271
 272 (* axiom CF_comp: ∀f,g,s1, s2. CF s1 f → CF s2 g →
 273   CF (s1 ∘ (λx. size (deopt (g x)))) (opt_comp f g). *)
 274
 275 axiom CF_comp_strong: ∀f,g,s1,s2. CF s1 f → CF s2 g →
 276   CF (s1 ∘ s2) (opt_comp f g). *)
 277
 278 definition IF ≝ λb,f,g:nat →option nat. λx.
 279   match b x with
 280   [None ⇒ None ?
 281   |Some n ⇒ if (eqb n 0) then f x else g x].
 282
 283 axiom IF_CF: ∀b,f,g,sb,sf,sg. CF sb b → CF sf f → CF sg g →
 284   CF (λn. sb n + sf n + sg n) (IF b f g).
 285
 286 lemma diag_cf_def : ∀s.∀i.
 287   diag_cf s i =
 288     IF (λi.U (pair (fst i) i) (|of_size (s (|i|))|)) (λi.Some ? 1) (λi.Some ? 0) i.
 289 #s #i normalize >size_of_size // qed.
 290
 291 (* and now ... *)
 292 axiom CF_pair: ∀f,g,s. CF s (λx.Some ? (f x)) → CF s (λx.Some ? (g x)) →
 293   CF s (λx.Some ? (pair (f x) (g x))).
 294
 295 axiom CF_fst: ∀f,s. CF s (λx.Some ? (f x)) → CF s (λx.Some ? (fst (f x))).
 296
 297 definition minimal ≝ λs. CF s (λn. Some ? n) ∧ ∀c. CF s (λn. Some ? c).
 298
 299
 300 (*
 301 axiom le_snd: ∀n. |snd n| ≤ |n|.
 302 axiom daemon: ∀P:Prop.P. *)
 303
 304 definition constructible ≝ λs. CF s (λx.Some ? (of_size (s (|x|)))).
 305
 306 (*
 307 lemma compl1: ∀s.
 308   CF s (to_Some fst)  → CF s (to_Some (λx.x)) → CF s (to_Some (λx.(s (|x|)))) →
 309   CF (λx. s x + s x + s x + sU (size_f fst x) (size_f (λx.x) x) (size_f (λx.(s (|x|))) x))
 310     (λx.U 〈fst x,x〉 (|s (|x|)|)).
 311 #s #H1 #H2 #H3 @CFU //
 312 qed.
 313
 314 lemma compl1: ∀s.
 315   CF s (to_Some fst)  → CF s (to_Some (λx.x)) → CF s (to_Some (λx.(s (|x|)))) →
 316   CF (λx. s x + s x + s x + sU (size_f fst x) (size_f (λx.x) x) (|(s x)| ))
 317     (λx.U 〈fst x,x〉 (|s (|x|)|)).
 318 #s #H1 #H2 #H3 @monotonic_CF [3: @(CFU ??? s s s) @CFU //
 319 qed.  *)
 320
 321 lemma diag_s: ∀s. minimal s → constructible s →
 322   CF (λx.s x + sU x x (s x)) (diag_cf s).
 323 #s * #Hs_id #Hs_c #Hs_constr
 324 @ext_CF [2: #n @sym_eq @diag_cf_def | skip]
 325 @(monotonic_CF ???? (IF_CF (λi:ℕ.U (pair (fst i) i) (|of_size (s (|i|))|))
 326    … (λi.s i + s i + s i + (sU (size_f fst i) (size_f (λi.i) i) (size_f (λi.of_size (s (|i|))) i))) … (Hs_c 1) (Hs_c 0) … ))
 327   [2: @CFU [@CF_fst // | // |@Hs_constr]
 328   |@(O_ext2 (λn:ℕ.s n+sU (size_f fst n) n (s n) + (s n+s n+s n+s n)))
 329     [2: #i >size_f_size >size_of_size >size_f_id //]
 330    @O_absorbr
 331     [%{1} %{0} #n #_ >commutative_times <times_n_1 @le_plus //
 332      @monotonic_sU //
 333     |@O_plus_l @(O_plus … (O_refl s)) @(O_plus … (O_refl s))
 334      @(O_plus … (O_refl s)) //
 335   ]
 336 qed.
 337
 338
 339 (*************************** The hierachy theorem *****************************)
 340
 341 (*
 342 theorem hierarchy_theorem_right: ∀s1,s2:nat→nat.
 343   O s1 idN → constructible s1 →
 344     not_O s2 s1 → ¬ CF s1 ⊆ CF s2.
 345 #s1 #s2 #Hs1 #monos1 #H % #H1
 346 @(absurd … (CF s2 (diag_cf s1)))
 347   [@H1 @diag_s // |@(diag1_not_s1 … H)]
 348 qed.
 349 *)
 350
 351 theorem hierarchy_theorem_left: ∀s1,s2:nat→nat.
 352    O(s1) ⊆ O(s2) → CF s1 ⊆ CF s2.
 353 #s1 #s2 #HO #f * #i * #Hcode * #c * #a #Hs1_i %{i} % //
 354 cases (sub_O_to_O … HO) -HO #c1 * #b #Hs1s2
 355 %{(c*c1)} %{(max a b)} #x #lemax
 356 cases (Hs1_i x ?) [2: @(le_maxl …lemax)]
 357 #y #Hy %{y} @(monotonic_U … Hy) >associative_times
 358 @le_times // @Hs1s2 @(le_maxr … lemax)
 359 qed.