proof - CoNat : proving that 0 is neutral to the left

Question

我正在试验 CoNat 的定义取自 this paper作者: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类似于 n .我的猜测是，在证明中我应该(至少)有一个用于 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 的定义的引理，但这里有一个替代定义，可以让证明通过:

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 : CoNat
zero .iszero = true
zero .pred ()

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′ : (n m : CoNat) → CoNat
plus′ n m .iszero = n .iszero ∧ m .iszero
plus′ n m .pred eq with n .iszero | m .iszero | n .pred | m .pred
plus′ n m .pred eq | false | _      | pn | pm = plus′ (pn refl) m
plus′ n m .pred eq | true  | false  | pn | pm = plus′ n (pm refl)
plus′ n m .pred () | true  | true   | pn | pm

plus′-zero-l : ∀ n → plus′ zero n ≈ n
plus′-zero-l n .iszero-≈ = refl
plus′-zero-l n .pred-≈ p q with n .iszero | n .pred
plus′-zero-l n .pred-≈ () _ | true  | pn
plus′-zero-l n .pred-≈ p q  | false | pn = plus′-zero-l (pn _)

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

两种相互定义的数据类型，一种是归纳的，一种是共归纳的，如 Normalization by Evaluation in the Delay Monad .

标准库的 variation of the previous approach ，它使用 Thunk数据类型。

CoNat′ = ℕ ⊎ ⊤ ，这不完全是一个 conat，但可能用于类似的目的。