如何解决如何在agda中通过W类型进行编码?
我正在尝试通过Agda中的W型对列表进行编码,当试图证明我的编码正确时,我得到了以下无法解决的目标。
Goal: g (f (x a)) ≡ x a'
Have: g (f (x a')) ≡ x a'
————————————————————————————————————————————————————————————
a' : A
x : A → W (⊤ ⊔ A) Blist
a : A
A : Type
我假设在等价f (sup (inr a) x) = a ∷ f (x a)
中定义我的前向函数时,不仅需要将x应用于a,而且不知道如何执行此操作。否则,我是不是用B x
来定义错误,还是倒退函数g
中存在其他一些小错误?一种方法如何调试呢?我可以提供所有使用的代码,但我希望为简洁起见可以发现错误。另外请注意,λ≡表示函数可扩展性。
data W (A : Type) (B : A → Type) : Type where
sup : (a : A) → ((b : B a) → W A B) → W A B
Blist : ∀ {A} → ⊤ ⊔ A → Type
Blist (inl x) = ⊥
Blist {A} (inr x) = A
List' : Type → Type
List' A = W (⊤ ⊔ A) Blist
data List (A : Type) : Type where
[] : List A
_∷_ : A → List A → List A
ListsEquiv : ∀ {A} → List' A ≃ List A
ListsEquiv {A} = equiv f g fg gf
where
f : List' A → List A
f (sup (inl top) x) = []
f (sup (inr a) x) = a ∷ f (x a)
g : List A → List' A
g [] = sup (inl tt) abort
g (a ∷ as) = sup (inr a) λ a' → g as
fg : (y : List A) → f (g y) ≡ y
fg [] = refl
fg (x ∷ y) = ap (λ - → x ∷ -) (fg y)
gf : (x : List' A) → g (f x) ≡ x
gf (sup (inl tt) x) = ap (λ - → sup (inl tt) -) (λ≡ (λ x₁ → abort x₁))
gf (sup (inr a) x) = ap (λ - → sup (inr a) -) (λ≡ (λ a' → {!gf (x a')!}))
解决方法
如@HTNW所指出的那样,对Arity索引类型进行编码的方式与对自然数进行编码的方式相同,因此仅基础类型用作索引数据。因此,下面的修改使证明可以顺利通过。
很容易混淆如何将数据存储到Well-order构造函数中,因此容易出现看似简单的错误。
Blist : ∀ {A} → ⊤ ⊔ A → Type
Blist (inl x) = ⊥
Blist (inr x) = ⊤
List' : Type → Type
List' A = W (⊤ ⊔ A) Blist
ListsEquiv : ∀ {A} → List' A ≃ List A
ListsEquiv {A} = equiv f g fg gf
where
f : List' A → List A
f (sup (inl top) x) = []
f (sup (inr a) x) = a ∷ f (x tt)
g : List A → List' A
g [] = sup (inl tt) abort
g (a ∷ as) = sup (inr a) λ a' → g as
fg : (y : List A) → f (g y) ≡ y
fg [] = refl
fg (x ∷ y) = ap (λ - → x ∷ -) (fg y)
gf : (x : List' A) → g (f x) ≡ x
gf (sup (inl tt) x) = ap (λ - → sup (inl tt) -) (λ≡ (λ x₁ → abort x₁))
gf (sup (inr a) x) = ap (λ - → sup (inr a) -) (λ≡ (λ a' → gf (x a')))
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。