From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 31 May 2013 09:39:54 +0000 (+0000)
Subject: gap.ma
X-Git-Tag: make_still_working~1145
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=26cb762e7dcd0ffde5a94c402ed9bb0717be14ba;p=helm.git

gap.ma
---

diff --git a/matita/matita/lib/reverse_complexity/gap.ma b/matita/matita/lib/reverse_complexity/gap.ma
new file mode 100644
index 000000000..2c8b6e938
--- /dev/null
+++ b/matita/matita/lib/reverse_complexity/gap.ma
@@ -0,0 +1,251 @@
+
+include "arithmetics/minimization.ma".
+include "arithmetics/bigops.ma".
+include "arithmetics/pidgeon_hole.ma".
+include "arithmetics/iteration.ma".
+
+(************************** notation for miminimization ***********************)
+
+(* an alternative defintion of minimization 
+definition Min ≝ λa,f. 
+  \big[min,a]_{i < a | f i} i. *)
+
+notation "μ_{ ident i < n } p" 
+  with precedence 80 for @{min $n 0 (λ${ident i}.$p)}.
+
+notation "μ_{ ident i ≤ n } p" 
+  with precedence 80 for @{min (S $n) 0 (λ${ident i}.$p)}.
+  
+notation "μ_{ ident i ∈ [a,b] } p"
+  with precedence 80 for @{min (S $b-$a) $a (λ${ident i}.$p)}.
+  
+lemma f_min_true: ∀f,a,b.
+  (∃i. a ≤ i ∧ i ≤ b ∧ f i = true) → f (μ_{i ∈[a,b]} (f i)) = true.
+#f #a #b * #i * * #Hil #Hir #Hfi @(f_min_true … (λx. f x)) <plus_minus_m_m 
+  [%{i} % // % [@Hil |@le_S_S @Hir]|@le_S @(transitive_le … Hil Hir)]
+qed.
+
+lemma min_up: ∀f,a,b.
+  (∃i. a ≤ i ∧ i ≤ b ∧ f i = true) → μ_{i ∈[a,b]}(f i) ≤ b. 
+#f #a #b * #i * * #Hil #Hir #Hfi @le_S_S_to_le
+cut ((S b) = S b - a + a) [@plus_minus_m_m @le_S @(transitive_le … Hil Hir)]
+#Hcut >Hcut in ⊢ (??%); @lt_min %{i} % // % [@Hil |<Hcut @le_S_S @Hir]
+qed.
+
+(*************************** Kleene's predicate *******************************)
+
+axiom U: nat → nat →nat → option nat.
+
+axiom monotonic_U: ∀i,x,n,m,y.n ≤m →
+  U i x n = Some ? y → U i x m = Some ? y.
+  
+lemma unique_U: ∀i,x,n,m,yn,ym.
+  U i x n = Some ? yn → U i x m = Some ? ym → yn = ym.
+#i #x #n #m #yn #ym #Hn #Hm cases (decidable_le n m)
+  [#lenm lapply (monotonic_U … lenm Hn) >Hm #HS destruct (HS) //
+  |#ltmn lapply (monotonic_U … n … Hm) [@lt_to_le @not_le_to_lt //]
+   >Hn #HS destruct (HS) //
+  ]
+qed.
+
+definition terminate ≝ λi,x,r. ∃y. U i x r = Some ? y.
+
+notation "〈i,x〉 ↓ r" with precedence 60 for @{terminate $i $x $r}.
+
+lemma terminate_dec: ∀i,x,n. 〈i,x〉 ↓ n ∨ ¬ 〈i,x〉 ↓ n.
+#i #x #n normalize cases (U i x n)
+  [%2 % * #y #H destruct|#y %1 %{y} //]
+qed. 
+
+definition termb ≝ λi,x,t. 
+  match U i x t with [None ⇒ false |Some y ⇒ true].
+
+lemma termb_true_to_term: ∀i,x,t. termb i x t = true → 〈i,x〉 ↓ t.
+#i #x #t normalize cases (U i x t) normalize [#H destruct | #y #_ %{y} //]
+qed.    
+
+lemma term_to_termb_true: ∀i,x,t. 〈i,x〉 ↓ t → termb i x t = true.
+#i #x #t * #y #H normalize >H // 
+qed.    
+
+lemma decidable_test : ∀n,x,r,r1.
+       (∀i. i < n → 〈i,x〉 ↓ r ∨ ¬ 〈i,x〉 ↓ r1) ∨ 
+       (∃i. i < n ∧ (¬ 〈i,x〉 ↓ r ∧ 〈i,x〉 ↓ r1)).
+#n #x #r1 #r2
+  cut (∀i0.decidable ((〈i0,x〉↓r1) ∨ ¬ 〈i0,x〉 ↓ r2)) 
+    [#j @decidable_or [@terminate_dec |@decidable_not @terminate_dec ]] #Hdec
+ cases(decidable_forall ? Hdec n) 
+  [#H %1 @H  
+  |#H %2 cases (not_forall_to_exists … Hdec H) #j * #leji #Hj
+   %{j} % // % 
+    [@(not_to_not … Hj) #H %1 @H 
+    |cases (terminate_dec j x r2) // #H @False_ind cases Hj -Hj #Hj
+     @Hj %2 @H
+  ]
+qed.
+
+(**************************** the gap theorem *********************************)
+definition gapP ≝ λn,x,g,r. ∀i. i < n → 〈i,x〉 ↓ r ∨ ¬ 〈i,x〉 ↓ g r.
+
+lemma gapP_def : ∀n,x,g,r. 
+  gapP n x g r = ∀i. i < n → 〈i,x〉 ↓ r ∨ ¬ 〈i,x〉 ↓ g r.
+// qed.
+
+lemma upper_bound_aux: ∀g,b,n,x. (∀x. x ≤ g x) → ∀k.
+  (∃j.j < k ∧
+    (∀i. i < n → 〈i,x〉 ↓ g^j b ∨ ¬ 〈i,x〉 ↓ g^(S j) b)) ∨
+  ∃l. |l| = k ∧ unique ? l ∧ ∀i. i ∈ l → i < n ∧ 〈i,x〉 ↓ g^k b .
+#g#b #n #x #Hg #k elim k 
+  [%2 %{([])} normalize % [% //|#x @False_ind]
+  |#k0 * 
+    [* #j * #lej #H %1 %{j} % [@le_S // | @H ]
+    |* #l * * #Hlen #Hunique #Hterm
+     cases (decidable_test n x (g^k0 b) (g^(S k0) b))
+      [#Hcase %1 %{k0} % [@le_n | @Hcase]
+      |* #j * #ltjn * #H1 #H2 %2 
+       %{(j::l)} % 
+        [ % [normalize @eq_f @Hlen] whd % // % #H3
+         @(absurd ?? H1) @(proj2 … (Hterm …)) @H3
+        |#x *
+          [#eqxj >eqxj % // 
+          |#Hmemx cases(Hterm … Hmemx) #lexn * #y #HU
+           % [@lexn] %{y} @(monotonic_U ?????? HU) @Hg
+          ]
+        ]
+      ]
+    ]
+  ]
+qed.
+       
+lemma upper_bound: ∀g,b,n,x. (∀x. x ≤ g x) → ∃r. 
+  (* b ≤ r ∧ r ≤ g^n b ∧ ∀i. i < n → 〈i,x〉 ↓ r ∨ ¬ 〈i,x〉 ↓ g r. *)
+  b ≤ r ∧ r ≤ g^n b ∧ gapP n x g r. 
+#g #b #n #x #Hg 
+cases (upper_bound_aux g b n x Hg n)
+  [* #j * #Hj #H %{(g^j b)} % [2: @H] % [@le_iter //]
+   @monotonic_iter2 // @lt_to_le //
+  |* #l * * #Hlen #Hunique #Hterm %{(g^n b)} % 
+    [% [@le_iter // |@le_n]] 
+   #i #lein %1 @(proj2 … (Hterm ??)) 
+   @(eq_length_to_mem_all … Hlen Hunique … lein)
+   #x #memx @(proj1  … (Hterm ??)) //
+  ]
+qed. 
+
+definition gapb ≝ λn,x,g,r.
+  \big[andb,true]_{i < n} ((termb i x r) ∨ ¬(termb i x (g r))). 
+  
+lemma gapb_def : ∀n,x,g,r. gapb n x g r =
+  \big[andb,true]_{i < n} ((termb i x r) ∨ ¬(termb i x (g r))). 
+// qed.
+
+lemma gapb_true_to_gapP : ∀n,x,g,r. 
+  gapb n x g r = true → ∀i. i < n → 〈i,x〉 ↓ r ∨ ¬(〈i,x〉 ↓ (g r)).
+#n #x #g #r elim n 
+  [>gapb_def >bigop_Strue //
+   #H #i #lti0 @False_ind @(absurd … lti0) @le_to_not_lt //
+  |#m #Hind >gapb_def >bigop_Strue //
+   #H #i #leSm cases (le_to_or_lt_eq … leSm)
+    [#lem @Hind [@(andb_true_r … H)|@le_S_S_to_le @lem]
+    |#eqi >(injective_S … eqi) lapply (andb_true_l … H) -H #H cases (orb_true_l … H) -H
+      [#H %1 @termb_true_to_term //
+      |#H %2 % #H1 >(term_to_termb_true …  H1) in H; normalize #H destruct
+      ]
+    ]
+  ]
+qed.
+
+lemma gapP_to_gapb_true : ∀n,x,g,r. 
+  (∀i. i < n → 〈i,x〉 ↓ r ∨ ¬(〈i,x〉 ↓ (g r))) → gapb n x g r = true. 
+#n #x #g #r elim n //
+#m #Hind #H >gapb_def >bigop_Strue // @true_to_andb_true
+  [cases (H m (le_n …)) 
+    [#H2 @orb_true_r1 @term_to_termb_true //
+    |#H2 @orb_true_r2 @sym_eq @noteq_to_eqnot @sym_not_eq 
+     @(not_to_not … H2) @termb_true_to_term 
+    ]
+  |@Hind #i0 #lei0 @H @le_S //
+  ]
+qed.
+
+
+(* the gap function *)
+let rec gap g n on n ≝
+  match n with 
+  [ O ⇒ 1
+  | S m ⇒ let b ≝ gap g m in μ_{i ∈ [b,g^n b]} (gapb n n g i)
+  ].
+  
+lemma gapS: ∀g,m. 
+  gap g (S m) = 
+    (let b ≝ gap g m in 
+      μ_{i ∈ [b,g^(S m) b]} (gapb (S m) (S m) g i)).
+// qed.
+
+lemma upper_bound_gapb: ∀g,m. (∀x. x ≤ g x) → 
+  ∃r:ℕ.gap g m ≤ r ∧ r ≤ g^(S m) (gap g m) ∧ gapb (S m) (S m) g r = true.
+#g #m #leg 
+lapply (upper_bound g (gap g m) (S m) (S m) leg) * #r * *
+#H1 #H2 #H3 %{r} % 
+  [% // |@gapP_to_gapb_true @H3]
+qed.
+   
+lemma gapS_true: ∀g,m. (∀x. x ≤g x) → gapb (S m) (S m) g (gap g (S m)) = true.
+#g #m #leg @(f_min_true (gapb (S m) (S m) g)) @upper_bound_gapb //
+qed.
+  
+theorem gap_theorem: ∀g,i.(∀x. x ≤ g x)→∃k.∀n.k < n → 
+   〈i,n〉 ↓ (gap g n) ∨ ¬ 〈i,n〉 ↓ (g (gap g n)).
+#g #i #leg %{i} * 
+  [#lti0 @False_ind @(absurd ?? (not_le_Sn_O i) ) //
+  |#m #leim lapply (gapS_true g m leg) #H
+   @(gapb_true_to_gapP … H) //
+  ]
+qed.
+
+(* an upper bound *)
+
+let rec sigma n ≝ 
+  match n with 
+  [ O ⇒ 0 | S m ⇒ n + sigma m ].
+  
+lemma gap_bound: ∀g. (∀x. x ≤ g x) → (monotonic ? le g) → 
+  ∀n.gap g n ≤ g^(sigma n) 1.
+#g #leg #gmono #n elim n 
+  [normalize //
+  |#m #Hind >gapS @(transitive_le ? (g^(S m) (gap g m)))
+    [@min_up @upper_bound_gapb // 
+    |@(transitive_le ? (g^(S m) (g^(sigma m) 1)))
+      [@monotonic_iter // |>iter_iter >commutative_plus @le_n
+    ]
+  ]
+qed.
+
+lemma gap_bound2: ∀g. (∀x. x ≤ g x) → (monotonic ? le g) → 
+  ∀n.gap g n ≤ g^(n*n) 1.
+#g #leg #gmono #n elim n 
+  [normalize //
+  |#m #Hind >gapS @(transitive_le ? (g^(S m) (gap g m)))
+    [@min_up @upper_bound_gapb // 
+    |@(transitive_le ? (g^(S m) (g^(m*m) 1)))
+      [@monotonic_iter //
+      |>iter_iter @monotonic_iter2 [@leg | normalize <plus_n_Sm @le_S_S //
+    ]
+  ]
+qed.
+
+(*
+axiom universal: ∃u.∀i,x,y. 
+  ∃n. U u 〈i,x〉 n = Some y ↔ ∃m.U i x m = Some y. *)
+
+   
+
+
+
+
+
+
+
+
+
+