В ответе на на мой предыдущий вопрос отмечалось, что с учетом индуктивного типа в Cubical Agda (v2.6.1, версия Cubical repo acabbd9) следует определить отношение к типу данных с помощью рекурсии и затем докажите, что это отношение эквивалентно пути равенства; это позволяет «кодировать / декодировать» или «NoConfusion» доказательства, которые позволяют вам легче доказать равенство.
Итак, у меня есть следующее определение двоичных натуральных чисел как более высокого индуктивного типа: по сути, двоичный натуральный является «a список битов с прямым порядком байтов, но добавление старших значащих нулей не меняет число ». (Я думал, что это казалось наиболее естественным определением, но на самом деле я уже нигде не могу найти подобное определение.)
{-# 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
Теперь очевидное соотношение было следующим, которое идентифицирует два списка битов, если они одинаковы, или если один отличается от другого только числом нулей на самом значимом конце:
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) = ?
Я почти пробился, заполнив первые две дыры, доказывая по пути coverBitListWellDefinedRight : (x y : List Bit) → CoverBitList x (y ++ (z :: [])) ≡ CoverBitList x y и coverBitListSym : (x y : List Bit) → CoverBitList x y ≡ CoverBitList y x.
Но последняя дыра выглядит ... ужасно. У меня пока нет интуиции, чтобы рассуждать о путях между путями.
Есть ли обучаемая порция интуиции, которую мне не хватает, которая поможет мне заполнить эту дыру и / или есть более простой способ заполнить дыра, и / или я делаю все правильно, определяя этот тип Cover?