Adding an instance of LawfulBEq to my nested inductive type

Stream: new members

[Pawel Welsberg]

Hi, I am still new to Lean. I'd appreciate your feedback.
I am adding an instance of LawfulBEq to my nested inductive type and I got an error:

Deriving `LawfulBEq` for nested inductives is not supported

This is when I am just using deriving keyword:

inductive File : Type
| directory (path : String) (children : Option (List File))
| file (path : String)
  deriving Repr, LawfulBEq

With a bit of help I got this manual solution (that seems to work fine):

inductive File : Type
| directory (path : String) (children : Option (List File))
| file (path : String)
  deriving Repr

mutual
  private def beqFile : File → File → Bool
    | .file p, .file p' => p == p'
    | .directory p c, .directory p' c' => p == p' && beqOpt c c'
    | _, _ => false
  private def beqOpt : Option (List File) → Option (List File) → Bool
    | some xs, some ys => beqList xs ys
    | none, none => true
    | _, _ => false
  private def beqList : List File → List File → Bool
    | x::xs, y::ys => beqFile x y && beqList xs ys
    | [], [] => true
    | _, _ => false
end

instance : BEq File := ⟨beqFile⟩

mutual
  private theorem beqFile_eq : beqFile a b = true → a = b := by
    cases a <;> cases b <;> intro h <;> simp_all [beqFile]
    case directory.directory p c p' c' =>
      cases hp : (p == p') with
      | false => cases hc : beqOpt c c' <;> simp_all
      | true => cases hc : beqOpt c c' with
        | false => simp_all
        | true => simp_all [LawfulBEq.eq_of_beq hp, beqOpt_eq hc]
  private theorem beqOpt_eq : beqOpt c d = true → c = d := by
    cases c <;> cases d <;> intro h <;> simp_all [beqOpt]
    case some.some => simp_all [beqList_eq h]
  private theorem beqList_eq : beqList xs ys = true → xs = ys := by
    cases xs <;> cases ys <;> intro h <;> simp_all [beqList]
    case cons.cons x xs y ys =>
      cases hx : beqFile x y with
      | false => cases hxs : beqList xs ys <;> simp_all
      | true => cases hxs : beqList xs ys with
        | false => simp_all
        | true => simp_all [beqFile_eq hx, beqList_eq hxs]
end

mutual
  private theorem beqFile_rfl : beqFile a a = true := by cases a <;> simp [beqFile, beqOpt_rfl]
  private theorem beqOpt_rfl : beqOpt c c = true := by cases c <;> simp [beqOpt, beqList_rfl]
  private theorem beqList_rfl : beqList xs xs = true := by cases xs <;> simp [beqList, beqFile_rfl, beqList_rfl]
end

instance : LawfulBEq File where
  eq_of_beq h := beqFile_eq h
  rfl := beqFile_rfl

which looks good to me but seems quite long.

I just need to compare two values of a type that contains Files (So BEq is not enough, it needs LawfulBEq).

Any suggestions how to make this shorter? There is no business logic in the above code (LawfulBEq instance) and seems like it should be shorter or automated.

[Eric Paul]

Here's a slightly shorter version with some uses of grind:

inductive File : Type
| directory (path : String) (children : Option (List File))
| file (path : String)
  deriving Repr

mutual
  private def beqFile : File → File → Bool
    | .file p, .file p' => p == p'
    | .directory p c, .directory p' c' => p == p' && beqOpt c c'
    | _, _ => false
  private def beqOpt : Option (List File) → Option (List File) → Bool
    | some xs, some ys => beqList xs ys
    | none, none => true
    | _, _ => false
  private def beqList : List File → List File → Bool
    | x::xs, y::ys => beqFile x y && beqList xs ys
    | [], [] => true
    | _, _ => false
end

instance : BEq File := ⟨beqFile⟩

mutual
  private theorem beqFile_eq : beqFile a b = true → a = b := by grind [beqOpt_eq _, beqFile, File]
  private theorem beqOpt_eq : beqOpt c d = true → c = d := by
    cases c <;> cases d <;> grind [beqList_eq _, beqOpt]
  private theorem beqList_eq : beqList xs ys = true → xs = ys := by
    cases xs <;> cases ys <;> simp_all [beqList] <;> grind [beqFile_eq _, beqList_eq _]
end

mutual
  private theorem beqFile_rfl : beqFile a a = true := by cases a <;> simp [beqFile, beqOpt_rfl]
  private theorem beqOpt_rfl : beqOpt c c = true := by cases c <;> simp [beqOpt, beqList_rfl]
  private theorem beqList_rfl : beqList xs xs = true := by cases xs <;> simp [beqList, beqFile_rfl, beqList_rfl]
end

instance : LawfulBEq File where
  eq_of_beq h := beqFile_eq h
  rfl := beqFile_rfl

[Pawel Welsberg]

Looks better. Previously File was just using deriving BEq but I upgraded to Lean 4.27.0 and I needed to implement LawfulBEq. And from 6 additional characters it went up to 30+ lines.
For some unknown for me reason it is erroring and highlighting grinding with the following:

unknown free variable `_fvar.3089`

I think it could be:
https://github.com/leanprover/lean4/issues/11930

[Pawel Welsberg]

Thank you @Eric Paul for your replay. I may use sorry for now to keep my code clean and simple.