Я экспериментирую с определением 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
.Я предполагаю, что в доказательстве у меня должно быть (по крайней мере) предложение 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
Как я могу сделать это доказательство?