CoNat：证明 0 向左是中性的

Question

我正在试验 Jesper Cockx 和 Andreas Abel 摘自 this paper 的 CoNat 定义：

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:

的 with 子句

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，但可能有类似的目的。

CoNat：证明 0 向左是中性的

CoNat : proving that 0 is neutral to the left

proof

agda

curry-howard

coinduction

codata