覆盖二元自然型的高级归纳类型。

Question

答案 我之前的问题 注意到在Cubical Agda中给定了一个归纳类型(v2.6.1, Cubical repo版本) acabbd9)，应该继续通过递归在数据类型上定义一个关系，然后证明这个关系等同于路径平等；这样就可以进行 "编码解码 "或 "NoConfusion "证明，让你更容易证明平等性。

所以我对二进制自然数的定义如下，作为一种高级的归纳类型：本质上，二进制自然数是 "一个比特的列表，小二烯，但加上最显著的零并不会改变数字"。我认为这似乎是最自然的定义，但实际上我已经在任何地方找不到类似的定义了）。

{-# 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 类型？

Answer 1

我明白了!

诀窍是超级明确地定义所有的东西，这样Agda就可以非常急切地为我减少所有的东西。

coverBitListWellDefinedRight : (x y : List Bit) → CoverBitList x (y ++ (z :: [])) ≡ CoverBitList x y
coverBitListWellDefinedRight [] [] = refl
coverBitListWellDefinedRight [] (z :: y) = coverBitListWellDefinedRight [] y
coverBitListWellDefinedRight [] (o :: y) = refl
coverBitListWellDefinedRight (z :: as) [] = refl
coverBitListWellDefinedRight (o :: as) [] = refl
coverBitListWellDefinedRight (z :: as) (z :: y) = coverBitListWellDefinedRight as y
coverBitListWellDefinedRight (z :: as) (o :: y) = refl
coverBitListWellDefinedRight (o :: as) (z :: y) = refl
coverBitListWellDefinedRight (o :: as) (o :: y) = coverBitListWellDefinedRight as y

coverBitListWellDefinedLeft : (x y : List Bit) → CoverBitList (x ++ (z :: [])) y ≡ CoverBitList x y
coverBitListWellDefinedLeft [] [] = refl
coverBitListWellDefinedLeft [] (z :: y) = refl
coverBitListWellDefinedLeft [] (o :: y) = refl
coverBitListWellDefinedLeft (z :: xs) [] = coverBitListWellDefinedLeft xs []
coverBitListWellDefinedLeft (o :: xs) [] = refl
coverBitListWellDefinedLeft (z :: xs) (z :: ys) = coverBitListWellDefinedLeft xs ys
coverBitListWellDefinedLeft (z :: xs) (o :: ys) = refl
coverBitListWellDefinedLeft (o :: xs) (z :: ys) = refl
coverBitListWellDefinedLeft (o :: xs) (o :: ys) = coverBitListWellDefinedLeft xs ys

Cover : BinNat → BinNat → Set
Cover (bits x) (bits y) = CoverBitList x y
Cover (bits x) (addZeros y i) = coverBitListWellDefinedRight x y i
Cover (addZeros x i) (bits y) = coverBitListWellDefinedLeft x y i
Cover (addZeros [] i) (addZeros [] j) = True
Cover (addZeros [] i) (addZeros (z :: []) j) = True
Cover (addZeros [] i) (addZeros (z :: (z :: y)) j) = Cover (addZeros [] i) (addZeros (z :: y) j)
Cover (addZeros [] i) (addZeros (z :: (o :: y)) j) = False
Cover (addZeros [] i) (addZeros (o :: y) j) = False
Cover (addZeros (z :: []) i) (addZeros [] j) = True
Cover (addZeros (z :: (z :: xs)) i) (addZeros [] j) = Cover (addZeros (z :: xs) i) (addZeros [] j)
Cover (addZeros (z :: (o :: xs)) i) (addZeros [] j) = False
Cover (addZeros (o :: xs) i) (addZeros [] j) = False
Cover (addZeros (z :: []) i) (addZeros (z :: ys) j) = Cover (addZeros [] i) (addZeros ys j)
Cover (addZeros (z :: (z :: xs)) i) (addZeros (z :: ys) j) = Cover (addZeros (z :: xs) i) (addZeros ys j)
Cover (addZeros (z :: (o :: xs)) i) (addZeros (z :: ys) j) = Cover (addZeros (o :: xs) i) (addZeros ys j)
Cover (addZeros (z :: []) i) (addZeros (o :: ys) j) = False
Cover (addZeros (z :: (z :: xs)) i) (addZeros (o :: ys) j) = False
Cover (addZeros (z :: (o :: xs)) i) (addZeros (o :: ys) j) = False
Cover (addZeros (o :: xs) i) (addZeros (z :: ys) j) = False
Cover (addZeros (o :: xs) i) (addZeros (o :: ys) j) = Cover (addZeros xs i) (addZeros ys j)