导电证明的问题
导电证明的问题
提问于 2015-02-20 23:56:15
我试着用Agda来理解共感应(我在读Sangiorgi的书)。我已经证明了流之间的一些简单等式，但是我不得不证明所有自然数(ℕ类型的值)都在流中--ℕ--函数--所有ℕ都是ℕ。有什么关于我该怎么做的建议吗？
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 = ?回答 1
Stack Overflow用户
回答已采纳
发布于 2015-02-25 19:46:21
分享完整的解决方案..。
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))页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/28640248
复制相关文章
相似问题
腾讯云开发者
