proof - CoNat : 证明 0 在左边是中性的
问题描述
我正在试验Jesper Cockx 和 Andreas AbelCoNat
的这篇论文中的定义:
open import Data.Bool
open import Relation.Binary.PropositionalEquality
record CoNat : Set where
coinductive
field iszero : Bool
pred : .(iszero ≡ false) -> CoNat
open CoNat public
我定义zero
和plus
:
zero : CoNat
iszero zero = true
pred zero ()
plus : CoNat -> CoNat -> CoNat
iszero (plus m n) = iszero m ∧ iszero n
pred (plus m n) _ with iszero m | inspect iszero m | iszero n | inspect iszero n
... | false | [ p ] | _ | _ = plus (pred m p) n
... | true | _ | false | [ p ] = plus m (pred n p)
pred (plus _ _) () | true | _ | true | _
我定义了双相似性:
record _≈_ (m n : CoNat) : Set where
coinductive
field
iszero-≈ : iszero m ≡ iszero n
pred-≈ : ∀ p q -> pred m p ≈ pred n q
open _≈_ public
但我坚持plus zero n
与n
. 我的猜测是,在证明中我应该(至少)有一个 with 子句iszero n
:
plus-zero-l : ∀ n -> plus zero n ≈ n
iszero-≈ (plus-zero-l _) = refl
pred-≈ (plus-zero-l n) p q with iszero n
... | _ = ?
但是 Agda 抱怨以下错误消息:
iszero n != w of type Bool
when checking that the type
(n : CoNat) (w : Bool) (p q : w ≡ false) →
(pred (plus zero n) _ | true | [ refl ] | w | [ refl ]) ≈ pred n _
of the generated with function is well-formed
我怎样才能做出这个证明?
解决方案
推荐阅读
- maven - Surefire 不会触发集成测试
- c# - 如何处理 IEqualityComparer 中的空值?
- android - 来自 exoplayer 的 TimelineQueueNavigator 给出了错误的索引
- vba - 将自定义模具用作 Visio 形状的 VBA 填充图案
- jira - 根据状态过滤故事,但包括其所有子任务
- python - 打印到打印机 python turtle 图形图像
- azure-logic-apps - 本地 SQL Server 到 Azure
- magento - Magento 1 上的 SagePay
- mysql - Spark MariaDB jdbc SQL 查询返回列名而不是列值
- angular - 如何循环通过角度获取请求响应