CoNat : proving that 0 is neutral to the left

Question

I am experimenting with the definition of CoNat taken from this paper by Jesper Cockx and 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

I define zero and 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  | _

And I define bisimilarity:

record _≈_ (m n : CoNat) : Set where
  coinductive
  field
    iszero-≈ : iszero m ≡ iszero n
    pred-≈ : ∀ p q -> pred m p ≈ pred n q

open _≈_ public

But I am stuck with the proof that plus zero n is bisimilar to n. My guess is that in the proof I should have (at least) a with-clause for 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
... | _ = ?

But Agda complains with to the following error message:

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

How can I make this proof?

Answer 1

I wasn't immediately able to prove the lemma with your definition of plus, but here's an alternative definition that makes the proof go through:

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, given that plus requires such an effort, I can't see this representation of conats being particularly nice to work with. You might want to consider these alternatives:

• Two mutually defined datatypes, one inductive and one coinductive, as in Normalization by Evaluation in the Delay Monad.
• The standard library's variation of the previous approach, which uses the Thunk datatype.
• CoNat′ = ℕ ⊎ ⊤, which is not exactly a conat but may serve similar purposes.