Statically balanced trees in Agda

Question

I'm teaching myself about dependent types by learning Agda.

Here's a type for binary trees balanced by their size.

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))

A tree can either be completely balanced (bal), or the left subtree could contain one more element than the right subtree (heavyL). (In that case, the next insertion would go into the right subtree.) The idea is that insertions would flip between the left and right halves of the tree, effectively (deterministically) shuffling an input list.

I can't make this definition of 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 rejects bal l (insert x r) as the right-hand side of the heavyL case:

.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)))

I attempted to patch up my definition with a proof...

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

... but I get the same error message. (Have I misunderstood what rewrite does?)

I also tried converting trees of equivalent sizes under the same proof assumption:

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 accepts this as a possibility, but highlights the equation in yellow. I figured I need to explicitly give the size of the two subtrees that I was passing to the bal constructor:

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

But now I get the same error message again!

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)))

I'm out of ideas. I'm sure I've made a stupid mistake. What am I doing wrong? What do I need to do to make my definition of insert typecheck?

Answer 1

Your rewrite attempt almost works, but the equality it's using is going the wrong direction. To get it working in the right direction, you can either flip it:

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

or use a with clause:

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

Another possibility is to perform the substitution yourself on the right-hand side:

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

Answer 2

You just need to rewrite in the another direction:

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)

You can use Agda's great hole machinery to figure out what's going on:

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

after typechecking and placing the cursor inside {!!}, you can type C-c C-, and get

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

After placing bal l (insert x r) in the hole and typing C-c C-. you'll get

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

So there is a mismatch. rewrite fixes it:

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

Now typing C-c C-. (after typechecking) gives

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  : ℕ

and you can finish the definition by typing C-c C-r in the hole.

Agda accepts this as a possibility, but highlights the equation in yellow.

Agda can't infer n and m from n + suc m, because there is pattern matching on n. There was a thread about implicit arguments on the Agda mailing list.