tree - Agda 的静态平衡树

我正在通过学​​习Agda来学习有关依赖类型的知识。

这是一种通过大小平衡的二叉树类型。

open import Data.Nat
open import Data.Nat.Properties.Simple

data T (A : Set) : ℕ -> Set where
  empty : T A 0
  leaf : A -> T A 1
  bal : ∀ {n} -> T A n -> T A n -> T A (n + n)
  heavyL : ∀ {n} -> T A (suc n) -> T A n -> T A (suc (n + n))

一棵树可以完全平衡（bal），或者左子树可能比右子树（heavyL）多包含一个元素。 （在这种情况下，下一个插入将进入右子树。）这个想法是插入将在树的左半部分和右半部分之间翻转，从而有效地（确定地）对输入列表进行改组。

我无法定义insert类型检查的定义：

insert : ∀ {A n} -> A -> T A n -> T A (suc n)
insert x empty = leaf x
insert x (leaf y) = bal (leaf x) (leaf y)
insert x (bal l r) = heavyL (insert x l) r
insert x (heavyL l r) = bal l (insert x r)

Agda拒绝bal l (insert x r)作为heavyL案例的右侧：

.n + suc .n != suc (.n + .n) of type ℕ
when checking that the expression bal l (insert x r) has type
T .A (suc (suc (.n + .n)))

我试图用证明来补充我的定义。

insert x (heavyL {n} l r) rewrite +-suc n n = bal l (insert x r)

...但是我收到相同的错误消息。 （我是否误解了rewrite是什么？）

我还尝试在相同的证明假设下转换等效大小的树：

convertT : ∀ {n m A} -> T A (n + suc m) -> T A (suc (n + m))
convertT {n} {m} t rewrite +-suc n m = t

insert x (heavyL {n} l r) rewrite +-suc n n = bal (convertT l) (convertT (insert x r))

阿格达（Agda）接受了这种可能性，但是用黄色突出显示了等式。我认为我需要显式给出传递给bal构造函数的两个子树的大小：

insert x (heavyL {n} l r) rewrite +-suc n n = bal {n = suc n} (convertT l) (convertT (insert x r))

但是现在我又收到了相同的错误消息！

n + suc n != suc (n + n) of type ℕ
when checking that the expression
bal {n = suc n} (convertT l) (convertT (insert x r)) has type
T .A (suc (suc (n + n)))

我没主意了。我确定我犯了一个愚蠢的错误。我究竟做错了什么？我需要做些什么来定义insert类型检查？

最佳答案

您只需要在另一个方向上进行重写：

open import Relation.Binary.PropositionalEquality

insert : ∀ {A n} -> A -> T A n -> T A (suc n)
insert x empty = leaf x
insert x (leaf y) = bal (leaf y) (leaf y)
insert x (bal l r) = heavyL (insert x l) r
insert x (heavyL {n} l r) rewrite sym (+-suc n n) = bal l (insert x r)

您可以使用爱达（Agda）的大孔机械来确定发生了什么：

insert x (heavyL {n} l r) = {!!}

经过类型检查并将光标放在{!!}内后，您可以键入C-c C-,并获得

Goal: T .A (suc (suc (n + n)))
————————————————————————————————————————————————————————————
r  : T .A n
l  : T .A (suc n)
n  : ℕ
x  : .A
.A : Set

将bal l (insert x r)放入孔中并键入C-c C-.后，您将获得

Goal: T .A (suc (suc (n + n)))
Have: T .A (suc (n + suc n))
————————————————————————————————————————————————————————————
r  : T .A n
l  : T .A (suc n)
n  : ℕ
x  : .A
.A : Set

因此存在不匹配。 rewrite对其进行了修复：

insert x (heavyL {n} l r) rewrite sym (+-suc n n) = {!bal l (insert x r)!}

现在键入C-c C-.（在类型检查之后）可以得到

Goal: T .A (suc (n + suc n))
Have: T .A (suc (n + suc n))
————————————————————————————————————————————————————————————
r  : T .A n
l  : T .A (suc n)
x  : .A
.A : Set
n  : ℕ

然后您可以在孔中键入C-c C-r来完成定义。


阿格达（Agda）接受这种可能性，但强调了
黄色。


Agda无法从n推断m和n + suc m，因为n上存在模式匹配。关于Agda邮件列表上的隐式参数，有一个thread。