--- /dev/null
+
+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. *)
+
+
+
+
+
+
+
+
+
+
+
+
projects / helm.git / blobdiff