implementing ReflBEq or DecidableEq instance

Stream: lean4

[Pavel Klimov]

I have following proof

theorem test (a : List Nat): ((a.zip (a.map (fun x => x ^ 2))).all fun (x, y) => x ^ 2 = y) := by
  induction a with
  | nil => rfl
  | cons x xs ih =>
    simp [List.zip, List.map] at ih ⊢
    trivial

I suppose it works because of BEq.rfl theorem, which states

BEq.rfl.{u_1} {α : Type u_1} [BEq α] [ReflBEq α] {a : α} : (a == a) = true

Why I think so? Well... More close to my actual case is following code

inductive MyType
| a
| b
deriving BEq

def myFunc : Nat → MyType
| 1 => .a
| _ => .b

theorem test1 (a : List Nat): ((a.zip (a.map (fun x => myFunc x))).all fun (x, y) => myFunc x == y) := by
  induction a with
  | nil => rfl
  | cons x xs ih =>
    simp [List.zip, List.map] at ih ⊢
    trivial

You may ask "why not use deriving DecidableEq instead?". I'll answer a bit later. But you should see here this proof doesn't work anymore. So, while trying to prove it manually, I arrived at theorem "BEq.rfl", and found out that if I add instance ReflEq:

instance : ReflBEq MyType where
rfl := by
intro v
induction v
. rfl
. rfl

Then proof of theorem test1 will work once again. But here comes the twist. The type for which I want to implement ReflBEq actually something like:

inductive Node
| leaf
| node (children : List Node)
deriving BEq

And here, I can't use deriving DecidableEq, it says

default handlers have not been implemented yet, class: 'DecidableEq' types: [Node]

And induction tactic says

'induction' tactic does not support nested inductive types, the eliminator 'Node.rec' has multiple motives

So I tried tactic cases, and then very fist case has goal

⊢ (Node.leaf == Node.leaf) = true

And rfl doesn't work anymore. And I don't know how to prove it. I don't even know how to unfold ==. I tried rw [BEq.beq], and it did something, but then I don't know what to do next.

I also tried to use recursors:

instance : ReflBEq Node where
  rfl := by
    intro v
    exact (Node.rec
      (motive_1 := fun y => (y == y) = true)
      (motive_2 := fun y => (List.all y (fun z => z == z)) = true)
      (leaf := by rfl)
      (node := fun children => by simp_all)
      (nil := by simp)
      (cons := fun head tail => by intro z; simp_all)
      v
    )

Lines nil, cons works, but leaf and node asking proofs of same cases as in cases tactic.

Then I tried to implement BEq instance myself, to be able to use its definition, but then I also stuck, but this time I was able to write implementation, but I'm unable to prove its termination:

def Node.size : Node →  Nat
| .leaf => 0
| .node children => 1 + (children.map fun x => x.size).max?.getD 0

--mutual
def singleEq : Node → Node → Bool
  | .leaf, .leaf => true
  | .node children, .node children1 =>
    children.length == children1.length
    && (children.zip children1).all fun (a, b) =>
      have hm : a.size < (Node.node children).size := by
        rw [Node.size];
        induction children with
        | nil => sorry
        | cons x xs ih => sorry
      singleEq a b
  | _, _ => false
termination_by a => a.size

I'm new to formal proofs, so probably I'm doing something wrong, for example metrics of decreasing I pick is wrong, etc.

So... My question is following: How can I define ReflBEq, or, perhaps DecidableEq in case like that? What should I do?

[Aaron Liu]

try writing a BEq or DecidableEq yourself!

[Aaron Liu]

you can copy off of #general > Proving DecidableEq of inductive type recursively using it @ 💬 if you get stuck

[Pavel Klimov]

If you read carefully, you will see that I tried to implement them myself
Thanks for the link, will check it out.

[Pavel Klimov]

I was able to implement DecidableEq for my type. It has 7 constructors, so my question is: is it normal to have 49 cases? It's because TestTy.noConfusion each time has different specification. And, when I have

| case3 (num : Nat) (v : TestTy)

to have its proof using tactics?

[Stefan Kusterer]

Hi Pavel,
to your question

It has 7 constructors, so my question is: is it normal to have 49 cases?

I guess you need to check all combinations, which gives you n^2 cases for n constructors.
I'm not sure of it makes sense in your case, but maybe you can use multiple types instead of one and in combination with inheritance.
I had a similar issue with DeciableLT - my code can be found here.

Regards, Stefan

[Pavel Klimov]

Can I avoid using recursors? Is it really good to have ReflBEq? Because my proof is working with only DecidableEq, but as a practice I tried to define ReflBEq. This is what I got:

mutual

def Node.beq : Node → Node → Bool
| .leaf, .leaf => true
| .node children1, .node children2 => Node.listBeq children1 children2
| _, _ => false

def Node.listBeq : List Node → List Node → Bool
| .nil, .nil => true
| x1 :: xs1, x2 :: xs2 => Node.beq x1 x2 && Node.listBeq xs1 xs2
| _, _ => false

end

instance : BEq Node where
  beq := Node.beq

instance : BEq (List Node) where
  beq := Node.listBeq

instance : ReflBEq Node where
  rfl := by
    intro v
    exact (Node.rec
    (motive_1 := fun x => (Node.beq x x) = true)
    (motive_2 := fun y => (Node.listBeq y y) = true)
    (leaf := by rfl)
    (node := fun y => by
      induction y with
      | nil => simp_all; trivial
      | cons x xs ih => intro ih1; trivial
    )
    (nil := by trivial)
    (cons := fun head tail => by intro z; simp_all!)
    v
  )

[Pavel Klimov]

Also, why it doesn't work if I write == instead of Node.beq and Node.listBeq?