Skip to content

Instantly share code, notes, and snippets.

@krtx
Created February 5, 2017 16:43
Show Gist options
  • Save krtx/e6afab9c87fdea32d33ebe5835464296 to your computer and use it in GitHub Desktop.
Save krtx/e6afab9c87fdea32d33ebe5835464296 to your computer and use it in GitHub Desktop.
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₂)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment