Agda 中的静态平衡树
Statically balanced trees in 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
typecheck:
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
typecheck?
您的 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))
你只需要换个方向重写:
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 accepts this as a possibility, but highlights the equation in
yellow.
Agda 无法从 n + suc m
推断出 n
和 m
,因为 n
上存在模式匹配。在 Agda 邮件列表上有一个关于隐式参数的thread。
我正在通过学习 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
typecheck:
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
typecheck?
您的 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))
你只需要换个方向重写:
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 accepts this as a possibility, but highlights the equation in yellow.
Agda 无法从 n + suc m
推断出 n
和 m
,因为 n
上存在模式匹配。在 Agda 邮件列表上有一个关于隐式参数的thread。