[Agda] Type unification problem in Braun Tree

[Liang-Ting Chen]

Hi, all
I try to write Braun trees like that,

data BTree (A : Set) : ℕ -> Set where
  <> : BTree A 0
  <_,_,_>-0 : {n : ℕ} -> A -> BTree A (suc n) -> BTree A n -> BTree A ((1 +
n) * 2)
  <_,_,_>-1 : {n : ℕ} -> A -> BTree A n -> BTree A n -> BTree A (1 + (n *
2))

to keep whether left subtree is greater than right subtree or not, and its
size.

We could know whether a BTree is a <_,_,_>-0 or <_,_,_>-1 by its parity,
that is ,
| BTree A n | = k * 2 iff <_,_,_>-0 and | BTree A n | = 1 + k * 2 iff
<_,_,_>-1
So, there is a type called parity:

data Parity : ℕ -> Set where
  even : (k : ℕ) -> Parity (k * 2)
  odd  : (k : ℕ) -> Parity (1 + k * 2)

parity : (n : ℕ) -> Parity n
parity 0 = even 0
parity (suc n) with parity n
parity (suc .(k * 2))    | even k = odd k
parity (suc .(1 + k * 2))| odd  k = even (suc k)

But, I got a error when I write an insert function:

_⊕_ : {n : ℕ}{A : Set} -> A -> BTree A n -> BTree A (1 + n)
_⊕_ {0} x <> = < x >
_⊕_ {suc n} x t with parity n
_⊕_ {suc .(k * 2)}     x (< y , s , t >-1) | even k = ?
_⊕_ {suc .(1 + k * 2)} x (< y , s , t >-0) | odd  k = ?

In last two line, agda reports that k != n, where t should be type BTree A
(suc (k * 2)) and BTree A (suc (suc (k * 2))) respectly.
I need to unify k == n by giving a proof of it, right ? I tried some
attempts but they didn't work.

Or, is there any better way to pattern maching on non-constructor index
which is an injective function ?

Here is the complete code about it.
--
open import Data.Nat

data Parity : ℕ -> Set where
  even : (k : ℕ) -> Parity (k * 2)
  odd  : (k : ℕ) -> Parity (1 + k * 2)

parity : (n : ℕ) -> Parity n
parity 0 = even 0
parity (suc n) with parity n
parity (suc .(k * 2))    | even k = odd k
parity (suc .(1 + k * 2))| odd  k = even (suc k)

{- Bool denote the difference: 0 means |left tree| > |right tree|, 1 means
|left tree| = |right tree| -}

data BTree (A : Set) : ℕ -> Set where
  <> : BTree A 0
  <_,_,_>-0 : {n : ℕ} -> A -> BTree A (suc n) -> BTree A n -> BTree A ((1 +
n) * 2)
  <_,_,_>-1 : {n : ℕ} -> A -> BTree A n -> BTree A n -> BTree A (1 + (n *
2))

<_> : forall {A} -> A -> BTree A 1
< x > = < x , <> , <> >-1

_⊕_ : {n : ℕ}{A : Set} -> A -> BTree A n -> BTree A (1 + n)
_⊕_ {0} x <> = < x >
_⊕_ {suc n} x t with parity n
_⊕_ {suc .(k * 2)}     x (< y , s , t >-1) | even k = ?
_⊕_ {suc .(1 + k * 2)} x (< y , s , t >-0) | odd  k = ?

-- 
sincerely,
Liang-Ting
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20081105/e5a7926a/attachment-0001.html