An answer to my previous question noted that given an inductive type in Cubical Agda (v2.6.1, Cubical repo version acabbd9), one should proceed to define a relation on the datatype by recursion and then prove that this relation is equivalent to path equality; this allows "encode/decode" or "NoConfusion" proofs which let you prove equalities more easily.
So I have the following definition of the binary naturals as a higher inductive type: essentially, a binary natural is "a list of bits, little-endian, but adding most-significant zeros doesn't change the number". (I thought this seemed the most natural definition, but I can't actually find a similar definition anywhere already.)
{-# OPTIONS --safe --warning=error --cubical --without-K #-}
open import Agda.Primitive
open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
module BinNat where
data False : Set where
record True : Set where
data List {a : _} (A : Set a) : Set a where
[] : List A
_::_ : A → List A → List A
_++_ : {a : _} {A : Set a} → List A → List A → List A
[] ++ y = y
(x :: xs) ++ y = x :: (xs ++ y)
data Bit : Set where
z : Bit
o : Bit
data BinNat : Set where
bits : List Bit → BinNat
addZeros : (x : List Bit) → bits (x ++ (z :: [])) ≡ bits x
Now, the obvious relation was the following, which identifies two lists of bits if they are the same or if one differs from the other only in the number of zeros on the most-significant end:
CoverBitList : List Bit → List Bit → Set
CoverBitList [] [] = True
CoverBitList [] (o :: b) = False
CoverBitList [] (z :: b) = CoverBitList [] b
CoverBitList (z :: xs) [] = CoverBitList xs []
CoverBitList (o :: xs) [] = False
CoverBitList (z :: xs) (z :: ys) = CoverBitList xs ys
CoverBitList (z :: xs) (o :: ys) = False
CoverBitList (o :: xs) (z :: ys) = False
CoverBitList (o :: xs) (o :: ys) = CoverBitList xs ys
Cover : BinNat → BinNat → Set
Cover (bits x) (bits y) = CoverBitList x y
Cover (bits x) (addZeros y i) = ?
Cover (addZeros x i) (bits y) = ?
Cover (addZeros x i) (addZeros y j) = ?
I just about fought my way through filling the first two holes, proving along the way coverBitListWellDefinedRight : (x y : List Bit) → CoverBitList x (y ++ (z :: [])) ≡ CoverBitList x y and coverBitListSym : (x y : List Bit) → CoverBitList x y ≡ CoverBitList y x.
But the final hole looks… ghastly. I don't have the intuition to reason about paths between paths yet.
Is there a teachable chunk of intuition I'm missing that will help me fill that hole, and/or is there an easier way to fill the hole, and/or am I doing the right thing at all in defining this Cover type?
