tree - Agda 中的静态平衡树

Question

我通过学习 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类型检查？

Answer 1

您的 rewrite尝试几乎有效，但它使用的相等性走向错误的方向。为了让它朝着正确的方向工作，你可以翻转它:

open import Relation.Binary.PropositionalEquality
-- ...
insert x (heavyL {n} l r) rewrite sym (+-suc n n) = bal l (insert x r)

或使用 with条款:

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

另一种可能性是在右侧自己执行替换:

open import Relation.Binary.PropositionalEquality
-- ...
insert x (heavyL {n} l r) = subst (T _) (+-suc (suc n) n) (bal l (insert x r))