When will this terminate?

Question

I actually want to prove one theorem but i think if I prove on the other side that is fine also.

I have defined a stream of positive rationals like this:

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 

Here pair is a record with ℤ and ℕ fields:

 --records of rational number
record pair : Set where
  field
    x : ℤ
    y : ℕ

mkPair : ℤ → ℕ → pair
mkPair a b = record { x = a; y = b}

Now I want to prove that every rational which is in positiveRat will be positive.

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))) = {!!}

I am writing the proof by splitting on pf. But it is unstoppable.

Answer 1

This is very easy to solve on this mock example because stream is periodic:

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

However, I imagine in your real example, stream is not periodic. There is no generic answer; the correct proof of lemma depends on how your real stream is defined, so you will have to post that.