match_pattern on Quotient types

Stream: Is there code for X?

[Andrew Carter]

In case I'm XYing it, I'll start by saying that what I'm really trying to do is make an inductive type:

inductive _Memory
| leaf
| node (value: Bool) (t f: _Memory)

where

(.node false .leaf .leaf) = .leaf

which I've achieved with:

def canonical: _Memory → _Memory
| .leaf => .leaf
| .node v f t =>
  match v, f.canonical, t.canonical with
  | false, .leaf, .leaf => .leaf
  | v', f', t' => .node v' f' t'

instance setoid: Setoid _Memory where
  r lhs rhs := lhs.canonical = rhs.canonical
  iseqv := ⟨ λ _ ↦ Eq.refl _, Eq.symm, Eq.trans ⟩

def Memory: Type _ := Quotient _Memory.setoid

def mk (v: Bool) (f t: Memory): Memory := ⟦.node v f.out t.out⟧

instance: Zero Memory where
  zero := ⟦.leaf⟧

but I'd like to be able to use structural recursion directly on type Memory, instead of having to define it on _Memory (admittedly I can also use termination_by, but that also isn't great).

In particular I can prove (I've left it as sorry here -since the proof is a little bit involved) a recOn rule as

@[elab_as_elim] def Memory.recOn.{u} {motive: Memory → Sort u} (m: Memory)
    (leaf: motive .leaf)
    (node: ∀ (b: Bool) (f t: Memory), b ∨ f ≠ 0 ∨ t ≠ 0 → motive f → motive t → motive (.mk b f t)):
  motive m := sorry

but I'd like to be able to write a [match_pattern] def that allows me to inductively define a rule. F.x.

def countOnes: Memory -> Memory
| .leaf => 0
| .node b f t _ => b.toNat + countOnes f + countOnes t

instead of writing

def countOnes (m: Memory): ℕ :=
  Memory.recOn m 0 (λ b _ _ _ f_ih t_ih ↦ b.toNat + f_ih + t_ih)

In particular if I want to write something that pattern matches multiple levels, I can't do it directly with the rec function.

def foo: Memory -> α
| .leaf => sorry
| .node b .leaf t _ => sorry
| .node b (.node b ff ft _) t _ => sorry -- foo ff

The other way I thought about doing it is to define the inductive type with the condition directly, this seems a little built more annoying when building the API, but Lean won't let me use Or or not recursively.
i.e.

inductive Memory
| leaf
| node (value: Bool) (t f: _Memory) (h: t ≠ leaf)
-- 'Memory.node' has a non positive occurrence of the datatypes being declared

and

inductive _Memory
| leaf
| node (value: Bool) (t f: _Memory) (h: value ∨ t ≠ leaf ∨ f ≠ leaf)
-- invalid nested inductive datatype 'Or', nested inductive datatypes parameters cannot contain local variable