如何证明正有理数上的减半函数总是存在性的？

Question

open import Data.Nat using (ℕ;suc;zero)
open import Data.Rational
open import Data.Product
open import Relation.Nullary
open import Data.Bool using (Bool;false;true)

halve : ℕ → ℚ
halve zero = 1ℚ
halve (suc p) = ½ * halve p

∃-halve : ∀ {a b} → 0ℚ < a → a < b → ∃[ p ] (halve p * b < a)
∃-halve {a} {b} 0<a a<b = h 1 where
  h : ℕ → ∃[ p ] (halve p * b < a)
  h p with halve p * b <? a
  h p | .true because ofʸ b'<a = p , b'<a
  h p | .false because ofⁿ ¬b'<a = h (suc p)

终止检查器在最后一种情况下失败了，这并不奇怪，因为递归显然既没有资金充足也没有结构。尽管如此，我很确定这应该是有效的，但不知道如何证明 ∃-halve 的终止。关于如何做到这一点有什么建议吗？

Answer 1

当你卡在这样的引理上时，一个好的通用原则是暂时忘记 Agda 及其技术细节。您将如何以尽可能基本的方式在人类可读的普通数学散文中证明它？

您的“迭代减半”函数正在计算 b/(2^p)。所以你试图证明：对于任何正有理数 a、b，都有一些自然的 p 这样 b/(2^p) < a。这个不等式等价于 2^p > b/a。您可以将其分解为两个步骤：找到一些自然 n ≥ b/a，然后找到一些 p 使得 2^p > n.

如评论中所述，找到此类数字的自然方法是实现上限函数和 log_2 函数。但是正如您所说，这些工作量很大，您在这里不需要它们；你只需要 existence 这样的数字。所以你可以分三步完成上面的证明，每一步都足够基本，可以作为一个独立的 Agda 证明，只需要非常基本的代数事实作为背景：

引理 1：对于任何有理数 q，有一些自然的 n > q。（证明：使用有理数排序的定义，以及一点代数。）
引理 2：对于任何自然 n，存在一些自然 p 使得 2^p > n。（证明：例如 p := (n+1); 通过对 n 的归纳证明2^(n+1) > n.)
引理 3：这些共同暗示了你想要的关于减半的定理。（证明：一些带有理数的代数，表明 b/(2^p) < a 等同于 2^p > b/a，并表明您的迭代减半函数给出 b/2^p.)

如何证明正有理数上的减半函数总是存在性的？

How to prove that the halving function over positive rationals always has an existential?

rational-number

agda