Проблемы с проводящим доказательством

Я пытаюсь понять коиндукцию (читаю книгу Санджорджи), используя Агду. Мне уже удалось доказать некоторые простые равенства между потоками, но я застрял, пытаясь доказать, что все натуральные числа (значения типа ℕ) находятся в потоке allℕ --- функция allℕisℕ. Любой совет о том, как мне поступить с этим?

open import Coinduction
open import Data.Nat

module Simple where

   data Stream (A : Set) : Set where
     _∷_ : A → ∞ (Stream A) → Stream A

   infix 4 _∈_

   data _∈_ {A : Set} : A → Stream A → Set where
     here  : ∀ {x xs} → x ∈ x ∷ xs
     there : ∀ {x y xs} → (x ∈ ♭ xs) → x ∈ y ∷ xs

   enum : ℕ → Stream ℕ
   enum n = n ∷ (♯ enum (suc n))

   allℕ : Stream ℕ
   allℕ = enum 0

   allℕisℕ : ∀ (n : ℕ) → n ∈ allℕ
   allℕisℕ n = ?

agda
person Rodrigo Ribeiro    schedule 20.02.2015    source источник
comment
Попробуйте сначала доказать эту лемму: cong : ∀ {m n} → n ∈ enum m → suc n ∈ enum (suc m). Я добавлю более подробный ответ, когда у меня будет свободная минутка.   -  person Vitus    schedule 21.02.2015
comment
Спасибо за совет. Я довольно легко доказал эту лемму, но я не понимаю, как эта лемма может помочь мне доказать, что все числа находятся в потоке. Основная трудность для меня состоит в том, как мне ухитриться доказать, что n ∈ enum m использовать cong лемму.   -  person Rodrigo Ribeiro    schedule 21.02.2015
comment
Совпадение с шаблоном на n и обработка обоих случаев. cong очень полезен для случая suc.   -  person Vitus    schedule 22.02.2015
comment
Оу... Вы абсолютно правы! Как я могу не видеть это раньше? rs... В любом случае, спасибо за ваше время!   -  person Rodrigo Ribeiro    schedule 22.02.2015

Ответы (1)


arrow_upward
0
arrow_downward

Просто поделился полным решением...

open import Coinduction
open import Data.Nat

module Simple where

  data Stream (A : Set) : Set where
    _∷_ : A → ∞ (Stream A) → Stream A

  infix 4 _∈_

  data _∈_ {A : Set} : A → Stream A → Set where
    here  : ∀ {x xs} → x ∈ x ∷ xs
    there : ∀ {x y xs} → (x ∈ ♭ xs) → x ∈ y ∷ xs

  enum : ℕ → Stream ℕ
  enum n = n ∷ (♯ enum (suc n))

  allℕ : Stream ℕ
  allℕ = enum 0

  ∈-suc : ∀ {n m : ℕ} → n ∈ enum m → suc n ∈ enum (suc m)
  ∈-suc here = here
  ∈-suc (there p) = there (∈-suc p)

  allℕisℕ : ∀ (n : ℕ) → n ∈ allℕ
  allℕisℕ zero = here
  allℕisℕ (suc n) = there (∈-suc (allℕisℕ n))
person Rodrigo Ribeiro    schedule 25.02.2015