Trying to define `LawfulBEq` instance

Stream: new members

[Ben Selfridge]

Hi all,

I have this data type:

inductive Term
| Var : Nat → Term
deriving BEq, Repr

And I am trying to fill in the sorrys here:

instance instLawfulBEq : LawfulBEq Term where
  eq_of_beq := sorry
  rfl := sorry

[Eric Paul]

Here's a related conversation you might find useful: #new members > Problem deriving LawfulBEq
It seemed to recommend deriving DecidableEq instead.

[Ben Selfridge]

Thanks, very helpful -- however, now I am in a rabbit hole trying to define a DecidableEq instance; I'm getting the "default handlers have not been implemented yet, class: 'DecidableEq' types: [Term]" error when I try to derive it.

[Matt Diamond]

I don't think a function from Nat is going to have decidable equality unless the codomain is a subsingleton... we can't check all the inputs

[Ben Selfridge]

Let me explain better. I want to write code that evaluates (Var 3 == Var 3) for branching purposes, and I want to be able to reason about it. I'm having trouble doing that because I'm unable to convert between (Var 3 == Var 3) = true and (Var 3 = Var 3).

[Vlad Tsyrklevich]

can you provide an #mwe?

[Chris Bailey]

Unless you need to do it by defining BEq first, it's probably easier to do it the other way (derive DecidableEq, then define BEq in terms of that). The derived instances are usually behind auxiliary definitions and might have slightly artificial looking definitions, but Eq is just Eq.

inductive Term
| Var : Nat → Term
deriving DecidableEq, Repr

instance : BEq Term where
  beq a b := a = b

instance instLawfulBEq : LawfulBEq Term where
  eq_of_beq := by simp only [beq_iff_eq, imp_self, implies_true]
  rfl := by simp only [beq_self_eq_true, implies_true]

open Term

example : ((Var 3 == Var 3) = true) = (Var 3 = Var 3) := by
  simp only

[Ben Selfridge]

Here is a #mwe:

mutual

inductive Foo where
| Foo : Foo
| Bar : Bar → Foo
deriving DecidableEq

inductive Bar where
| Bar : Bar
deriving DecidableEq

inductive Baz where
| Bar : Bar → Baz
| Baz : Baz → Baz

structure Barf where
  p : Option Baz

end

[Ben Selfridge]

Idk if it's minimal, but it's as minimal as i could make it.

[Ben Selfridge]

I'm unable to derive DecidableEq here. But if I comment out the Barf declaration, it all works fine.

[Ben Selfridge]

Here it is, even more minimal:

mutual

inductive Foo where
| Foo : Foo
deriving DecidableEq

structure Barf where
  p : Option Foo
deriving DecidableEq

end

[Chris Bailey]

Is your actual problem with Term or with a mutual inductive?

[Ben Selfridge]

Looks like it's with a mutual inductive.

[Chris Bailey]

These are not mutual. Foo is not defined in terms of Barf.

[Ben Selfridge]

I know. But why does that matter? If I comment out the deriving clauses, it works fine. Also note: I need the mutual declaration in my actual code, even though it's not necessary in this MWE.

[Ben Selfridge]

Screenshot 2025-03-22 at 12.08.39 AM.png
Screenshot 2025-03-22 at 12.08.55 AM.png

[Chris Bailey]

Ben Selfridge said:

I know. But why does that matter? If I comment out the deriving clauses, it works fine. Also note: I need the mutual declaration in my actual code, even though it's not necessary in this MWE.

Then it's not really an MWE I'm afraid. It matters because not all deriving handlers work the same (or at all) for mutual inductives.

[Ben Selfridge]

Do you have any suggestions as to how I could define DecidableEq inside that mutual inductive?

[Ben Selfridge]

Also, can you explain to me why I am getting the red squiggly line under DecidableEq?

[Ben Selfridge]

I am so confused by your responses, I have to be honest with you. :(

[Chris Bailey]

You'll have to write it manually. The red squiggly is because the metaprogram for deriving DecidableEq works for inductive types, but has not yet been extended to work for mutual or nested inductive types, hence needing to do it manually.

An example of doing it manually with an actual mutual would be like:

mutual

inductive A
  | base : A
  | mk : A -> B -> A


inductive B
  | base : B
  | mk : B -> A -> B

end

mutual

instance instDecidableEqA : DecidableEq A :=
  fun
  | .base, .base => isTrue rfl
  | .base, .mk _ _ => isFalse (fun hf => by simp at hf)
  | .mk _ _, .base => isFalse (fun hf => by simp at hf)
  | .mk a₁ b₁, .mk a₂ b₂ =>
    match instDecidableEqA a₁ a₂ with
    | isTrue ht =>
      match instDecidableEqB b₁ b₂ with
      | isTrue ht' =>  isTrue <| (A.mk.injEq _ _ _ _).mpr ⟨ht, ht'⟩
      | isFalse hf' => isFalse (fun hf => hf' ((A.mk.injEq _ _ _ _).mp hf).right)
    | isFalse hf' => isFalse (fun hf => hf' ((A.mk.injEq _ _ _ _).mp hf).left)

instance instDecidableEqB : DecidableEq B :=
  fun
  | .base, .base => isTrue rfl
  | .base, .mk _ _ => isFalse (fun hf => by simp at hf)
  | .mk _ _, .base => isFalse (fun hf => by simp at hf)
  | .mk b₁ a₁, .mk b₂ a₂ =>
    match instDecidableEqA a₁ a₂ with
    | isTrue ht =>
      match instDecidableEqB b₁ b₂ with
      | isTrue ht' => isTrue <| (B.mk.injEq _ _ _ _).mpr ⟨ht', ht⟩
      | isFalse hf' => isFalse (fun hf => hf' ((B.mk.injEq _ _ _ _).mp hf).left)
    | isFalse hf' => isFalse (fun hf => hf' ((B.mk.injEq _ _ _ _).mp hf).right)

end

Or this one (which is a nested inductive, but still): #lean4 > DecidableEq and List in inductive type @ 💬

[Chris Bailey]

Actually the A/B one is sort of a loaded example, hold on.

[Ben Selfridge]

This is starting to look pretty spooky for something that seems so simple...

[Chris Bailey]

It's just case analysis. If you want everything to work out of the box and be simple, I would try to restate the problem without using a mutual inductive.

[Chris Bailey]

Or use BEq without worrying about the lawful part, in which case it literally is just case analysis as you would write in any other language that doesn't concern itself with proofs.

[Ben Selfridge]

I'll take a closer look at this tomorrow. Thank you very much for your responses

[Ben Selfridge]

Ok. Finally got all the DecidableEq instances written, thanks to your suggestions. It was incredibly tedious and I am not good enough with tactic combinators yet to know how to shorten it, but at least it's done. Thanks!