3 
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. 关于如何做到这一点的任何建议？

4

1 回答 1

6

当你被困在这样的引理上时，一个好的一般原则是暂时忘记 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。）

于 2019-12-12T12:07:26.043 回答