http://adam.chlipala.net/cpdt/html/GeneralRec.html#noBadChains in Agda

InfiniteChain.agda

module InfiniteChain where

-- http://adam.chlipala.net/cpdt/html/GeneralRec.html#noBadChains in Agda

open import Induction.WellFounded
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

record Stream (A : Set) : Set where
  coinductive
  field
    hd : A
    tl : Stream A

open Stream

record infinite-chain {A : Set} (R : A → A → Set) (xs : Stream A) : Set where
  coinductive
  field
    hd-∞ : R (hd (tl xs)) (hd xs)
    tl-∞ : infinite-chain R (tl xs)

open infinite-chain

cons : ∀ {A} → A → Stream A → Stream A
cons x xs = record { hd = x ; tl = xs }

no-infinite-chains′ : ∀ {A} {R : A → A → Set} {x}
                     → Acc R x
                     → ∀ s → ¬ (infinite-chain R (cons x s))
no-infinite-chains′ (acc rs) s ic
  with no-infinite-chains′ (rs (hd s) (hd-∞ ic))
                           (tl s)
                           (record { hd-∞ = hd-∞ (tl-∞ ic)
                                   ; tl-∞ = tl-∞ (tl-∞ ic) })
... | ()

no-infinite-chains : ∀ {A} {R : A → A → Set}
                     → Well-founded R
                     → ∀ s → ¬ (infinite-chain R s)
no-infinite-chains wf s ic =
  no-infinite-chains′ (wf (hd s))
                      (tl s)
                      (record { hd-∞ = hd-∞ ic ; tl-∞ = tl-∞ ic })

-- せっかく書いたので残す
record _≈_ {A : Set} (xs : Stream A) (ys : Stream A) : Set where
  coinductive
  field
    hd-≈ : hd xs ≡ hd ys
    tl-≈ : tl xs ≈ tl ys

open _≈_

≈-refl : ∀ {A} {xs : Stream A} → xs ≈ xs
hd-≈ ≈-refl = refl
tl-≈ ≈-refl = ≈-refl

≈-sym : ∀ {A} {xs ys : Stream A} → xs ≈ ys → ys ≈ xs
hd-≈ (≈-sym eq) = sym (hd-≈ eq)
tl-≈ (≈-sym eq) = ≈-sym (tl-≈ eq)

≈-trans : ∀ {A} {xs ys zs : Stream A} → xs ≈ ys → ys ≈ zs → xs ≈ zs
hd-≈ (≈-trans eq₁ eq₂) = trans (hd-≈ eq₁) (hd-≈ eq₂)
tl-≈ (≈-trans eq₁ eq₂) = ≈-trans (tl-≈ eq₁) (tl-≈ eq₂)