Когда это закончится?

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, поэтому вам придется опубликовать его.