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

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。

如评论中所述，找到此类数字的自然方法是实现 ceiling 函数和 log_2 函数。但是正如您所说，这些工作量很大，您在这里不需要它们；你只需要这样的数字存在。所以你可以分三步完成上面的证明，每一步都足够基本，可以作为独立的 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.)