Using @[pattern] and binary_nat

Stream: new members

[Andrew Carter]

I'm trying to get a definition working for binary numbers that recurses by doubling of bits (i.e. you can take 2 32-bit numbers and get a 64-bit number). But I don't want to expose the number of bits in the type. I tried following along with vector/rbtree to construct one but I realize now that pattern matching for vector doesn't even do what I would expect.

I'd like to be able to write a function like:

def is_zero: binary_nat → Prop
| (binary_nat.bit b) := b = ff
| (binary_nat.intro high low proof) := is_zero high ∧ is_zero low

But I'm having trouble avoiding encoding the proof in the type somehow, i.e. I can get something like this working

def is_zero (n: ℕ): binary_nat n → Prop
| (binary_nat.bit b) := b = ff
| (binary_nat.intro high low) := is_zero high ∧ is_zero low

where I've encoded the height of the "tree" in the type itself (which then makes the type annoying to work with).

I see rbtree uses a well_formed side-car constructor, although it doesn't seem to have a [pattern] attributes, but vector does, although even
for vector I can't find where the pattern matching is used, for example this doesn't work:

def is_zero: Π {n}, vector bool n → Prop
| (0) (vector.nil) := true
| (n+1) (vector.cons x xs) := (x = ff) ∧ is_zero xs

The closest I think I have something working has been:

namespace data
namespace binary_nat

inductive node : Type
| bit (b: bool): node
| intro (u l: node): node

namespace node
def height: node → ℕ
| (bit _) := 0
| (intro u l) := (height u) + 1
end node

inductive well_formed: ℕ → node → Prop
| wf_bit (b: bool): well_formed 0 (node.bit b)
| wf_intro {n m: node} (wn: well_formed n.height n) (wm: well_formed m.height m) (hp: n.height = m.height): well_formed ((n.intro m).height) (n.intro m)

end binary_nat
def binary_nat := { n: binary_nat.node // binary_nat.well_formed n.height n }
namespace binary_nat

@[pattern] def bit (b: bool): binary_nat := ⟨ node.bit b, well_formed.wf_bit b⟩

@[pattern] def intro: Π (high low: binary_nat), high.val.height = low.val.height → binary_nat
| ⟨ high_val, high_proof⟩ ⟨ low_val, low_proof ⟩ h := ⟨ node.intro high_val low_val, well_formed.wf_intro high_proof low_proof h ⟩

But lean doesn't seem to think intro looks enough like a constructor,
"invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
intro high low proof"
Alternatively the issue might be getting out high/low back from intro,
"don't know how to synthesize placeholder (high)"
I'm not sure which of these error messages is the root cause.

Any pointers to existing types that achieve something similar would be appreciated (or an explanation of how to make vector work so I can follow along).Or if its impossible to do what I want to do, that would be nice to know too.