如何证明对正有理数的减半函数始终具有存在性？

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 函数。但是正如您所说，这些工作量相当大，而您在这里不需要它们；你只需要存在这样的数字。因此，您可以分三个步骤完成上述证明，每个步骤对于独立的 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。）