Defining `BEq` for nested inductive type

Stream: general

[Yicheng Qian]

Suppose we want to define BEq for

inductive Tree (α : Type _) where
  | leaf : α → Tree α
  | node : Array (Tree α) → Tree α

and prove it's lawful. We cannot use deriving because it uses partial and the definition comes out opaque. The natural way to define BEq for Tree would be

def Tree.beq₁ [BEq α] : Tree α → Tree α → Bool
| .leaf x, .leaf y => x == y
| .node xs, .node ys => Array.isEqv xs ys Tree.beq₁
| _, _ => false
termination_by x y => (x, y)

but this doesn't work. I tried various ways and settled on this:

def Tree.beq₂ [BEq α] : Tree α → Tree α → Bool
| .leaf x, .leaf y => x == y
| .node xs, .node ys =>
  xs.size == ys.size &&
    (Array.zipWith (fun ⟨x, _⟩ y => Tree.beq₂ x y) xs.attach ys).all id
| _, _ => false

but this looks unnatural. What's the canonical way of defining BEq for Tree?

[Kyle Miller]

Usually the way to do this is to derive DecidableEq instead (which provides the lawful BEq instance for you), though that does add the restriction that the type alpha must have DecidableEq, and in any case the deriving handler doesn't work here.

[Mario Carneiro]

we really need a derive LawfulBEq... The BEq instance is very difficult to access after the fact because derive uses funny names with number components in them

[Kyle Miller]

(and/or come up with a standard for the names of derived instances)

[Kyle Miller]

(and/or hook the deriving handler system into the same sort of reserved name system as for equation lemmas and have them autoderive on demand, so that deriving handlers can chain)

[Kyle Miller]

but this looks unnatural

I don't really see any better way to do this, except to define a version of Array.isEqv that encapsulates this attach business.

Maybe you could hook it into the @[wf_preprocess] simp lemmas to turn Array.isEqv into it automatically. That would let you write your function the first way, but have the termination system automatically transform it into the second way.

[Mario Carneiro]

does that actually work? I remember requesting that but I don't know if anything came of it

[Kyle Miller]

Yeah, it works, and it's been there for about 2-3 releases

[Kyle Miller]

I didn't prove the wf_preprocess lemma, but it appears to work here, and you don't even need termination_by:

inductive Tree (α : Type _) where
  | leaf : α → Tree α
  | node : Array (Tree α) → Tree α

def Array.isEqvAttach (xs ys : Array α) (p : (x : α) → x ∈ xs → (y : α) → y ∈ ys → Bool) : Bool :=
  xs.size == ys.size && (Array.zipWith (fun ⟨x, hx⟩ ⟨y, hy⟩ => p x hx y hy) xs.attach ys.attach).all id

@[wf_preprocess] theorem Array.isEqvAttach_wf
    (xs ys : Array α) (p : α → α → Bool) :
    Array.isEqv (wfParam xs) ys p = Array.isEqvAttach xs ys (fun x _ y _ => p (wfParam x) (wfParam y)) := by
  simp [Array.isEqvAttach, wfParam]
  sorry

def Tree.beq [BEq α] : Tree α → Tree α → Bool
  | .leaf x, .leaf y => x == y
  | .node xs, .node ys => Array.isEqv xs ys Tree.beq
  | _, _ => false

[Mario Carneiro]

why is only xs marked as wfParam?

[Mario Carneiro]

but x and y are marked as wfParam on the rhs

[Kyle Miller]

I don't know how to design these @[wf_preprocess] lemmas. I figured that it's going to go through the LHS argument :shrug: (And why put wfParam on both arguments inside? It doesn't hurt, but probably it should only be on the LHS one.)

I would expect that you would want three flavors of it, depending on which arguments are part of the well-founded recursion.