CoNat ：证明 0 在左边是中性的

Question

我正在尝试CoNat从Jesper Cockx 和 Andreas Abel 的这篇论文中得到的定义：

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是bisimilar来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

我怎样才能做这个证明？

Answer 1

我无法立即用您的定义来证明引理plus，但这里有一个替代定义，可以使证明通过：

\n\n

open import Data.Bool\nopen import Relation.Binary.PropositionalEquality\n\nrecord CoNat : Set where\n  coinductive\n  field iszero : Bool\n        pred : .(iszero \xe2\x89\xa1 false) -> CoNat\n\nopen CoNat public\n\nzero : CoNat\nzero .iszero = true\nzero .pred ()\n\nrecord _\xe2\x89\x88_ (m n : CoNat) : Set where\n  coinductive\n  field\n    iszero-\xe2\x89\x88 : iszero m \xe2\x89\xa1 iszero n\n    pred-\xe2\x89\x88 : \xe2\x88\x80 p q \xe2\x86\x92 pred m p \xe2\x89\x88 pred n q\n\nopen _\xe2\x89\x88_ public\n\nplus\xe2\x80\xb2 : (n m : CoNat) \xe2\x86\x92 CoNat\nplus\xe2\x80\xb2 n m .iszero = n .iszero \xe2\x88\xa7 m .iszero\nplus\xe2\x80\xb2 n m .pred eq with n .iszero | m .iszero | n .pred | m .pred\nplus\xe2\x80\xb2 n m .pred eq | false | _      | pn | pm = plus\xe2\x80\xb2 (pn refl) m\nplus\xe2\x80\xb2 n m .pred eq | true  | false  | pn | pm = plus\xe2\x80\xb2 n (pm refl)\nplus\xe2\x80\xb2 n m .pred () | true  | true   | pn | pm\n\nplus\xe2\x80\xb2-zero-l : \xe2\x88\x80 n \xe2\x86\x92 plus\xe2\x80\xb2 zero n \xe2\x89\x88 n\nplus\xe2\x80\xb2-zero-l n .iszero-\xe2\x89\x88 = refl\nplus\xe2\x80\xb2-zero-l n .pred-\xe2\x89\x88 p q with n .iszero | n .pred\nplus\xe2\x80\xb2-zero-l n .pred-\xe2\x89\x88 () _ | true  | pn\nplus\xe2\x80\xb2-zero-l n .pred-\xe2\x89\x88 p q  | false | pn = plus\xe2\x80\xb2-zero-l (pn _)\n

\n\n\n\n

FWIW，考虑到 plus 需要这样的努力，我不认为 conats 的这种表示特别好用。您可能需要考虑以下替代方案：

\n\n

\n
• 两种相互定义的数据类型，一种是归纳型，一种是共归纳型，如《延迟单子中的求值标准化》中所示。
\n
• 标准库是先前方法的变体，它使用Thunk数据类型。
\n
• CoNat\xe2\x80\xb2 = \xe2\x84\x95 \xe2\x8a\x8e \xe2\x8a\xa4，这并不完全是一个conat，但可以用于类似的目的。
\n

\n