导电证明的问题

Question

我正在尝试使用 Agda 理解协同归纳法（我正在阅读 Sangiorgi 的书）。我已经设法证明了流之间的一些简单等式，但我仍然试图证明所有自然数（ℕ 类型的值）都在流 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 = ?

Answer 1

只是分享完整的解决方案...

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))

导电证明的问题

Problems with a conductive proof

agda