这将于何时终止

Question

我实际上想证明一个定理，但我认为如果我在另一边证明，那也没问题。

我定义了一系列积极的理由，比如：

one : ℤ
one = + 1
next : pair → pair
next q = if (n eq one) then (mkPair (+ m Data.Integer.+ one) 1)
         else (mkPair (n Data.Integer.- one) (m Nat.+ 1))
  where
     n = getX q
     m = getY q
-- eq is defined correctly for equivalence of two integer. 
rational : Stream pair
rational = iterate next (mkPair one 1) 
RQ : pair → Stream pair → Stream pair
RQ q (x ∷ xs) = (x add q) ∷ ♯ (RQ q (♭ xs))    
positiveRat : Stream pair
positiveRat = RQ (mkPair (+ 0) (1)) rational 

这里pair是一个记录ℤ和ℕ字段：

 --records of rational number
record pair : Set where
  field
    x : ℤ
    y : ℕ
mkPair : ℤ → ℕ → pair
mkPair a b = record { x = a; y = b}

现在我想证明positiveRat中的每个有理数都是正的。

open import Data.Stream
open import Data.Nat
open import Data.Rational
open import Data.Integer
open import Coinduction
open import Data.Unit
lemma : (x : pair) → (x ∈ positiveRat) → (+ 0 Data.Integer.≤ pair.x x)
lemma .(record { x = + 1 ; y = 1 }) here = +≤+ z≤n
lemma .(record { x = + 2 ; y = 1 }) (there here) = +≤+ z≤n
lemma .(record { x = + 1 ; y = 2 }) (there (there here)) = {!!}
lemma q (there (there (there pf))) = {!!}

我在pf上分格写证明。但它势不可挡。

Answer 1

这在这个模拟示例中很容易解决，因为stream是周期性的：

lemma : (x : ℚ) → (x ∈ stream) → (+ 0 Data.Integer.≤ ℚ.numerator x)
lemma .(record { numerator = + 1}) here = +≤+ z≤n
lemma .(record { numerator = + 2}) (there here) = +≤+ z≤n
lemma .(record { numerator = + 3}) (there (there here)) = +≤+ z≤n
lemma q (there (there (there pf))) = lemma q pf

然而，我想在您的真实示例中，stream不是周期性的。没有通用的答案；lemma的正确证明取决于你真正的stream是如何定义的，所以你必须发布它。