Proving DecidableEq of inductive type recursively using it

Stream: general

[Juneyoung Lee]

Hello everyone,

How can I prove DecidableEq of an inductive data type using itself in one of constructors as a list, for example:

inductive TestTy where
| case1 | case2 (t:List TestTy)
deriving DecidableEq

... without defining a separate boolean equality function on TestTy?
I gave a small try, but this didn't seem to work because comparing two lists already needed DecidableEq on TestTy:

instance : DecidableEq TestTy := fun a b =>
  match a, b with
  | .case1, .case1 => by simp; exact inferInstance
  | .case2 i1, .case2 i2 =>
    if h: i1 = i2 then isTrue (by rw [h])    <- This doesn't work because equality of two TestTy lists isn't decidable yet
    else isFalse (fun h_eq => TestTy.noConfusion h_eq (fun h2 => absurd h2 h))
  | .. (omit)

[Kenny Lau]

i don't know what the state of the art is, but i don't see the harm of defining a separate boolean equality

(obviously the right response is to hope some lean developers have the time and interest to tackle this problem)

[Kenny Lau]

(or maybe you could get into metaprogramming and write a stronger deriver and get it into mathlib :slight_smile:)

[Aaron Liu]

here we go

inductive TestTy where
| case1 | case2 (t:List TestTy)

mutual

def TestTy.decEq (a b : TestTy) : Decidable (a = b) :=
  match a with
  | .case1 =>
    match b with
    | .case1 => .isTrue rfl
    | .case2 _ => .isFalse TestTy.noConfusion
  | .case2 as =>
    match b with
    | .case1 => .isFalse TestTy.noConfusion
    | .case2 bs =>
      match TestTy.decEqList as bs with
      | .isTrue h => .isTrue (congrArg TestTy.case2 h)
      | .isFalse h => .isFalse fun hc => h (TestTy.case2.inj hc)

def TestTy.decEqList (as bs : List TestTy) : Decidable (as = bs) :=
  match as with
  | [] =>
    match bs with
    | [] => .isTrue rfl
    | _ :: _ => .isFalse List.noConfusion
  | a :: as =>
    match bs with
    | [] => .isFalse List.noConfusion
    | b :: bs =>
      match TestTy.decEq a b with
      | .isTrue hab =>
        match TestTy.decEqList as bs with
        | .isTrue hss => .isTrue (congr (congrArg List.cons hab) hss)
        | .isFalse h => .isFalse fun hc => h (List.cons.inj hc).2
      | .isFalse h => .isFalse fun hc => h (List.cons.inj hc).1

end

[Kenny Lau]

oh boy, mutual

[Aaron Liu]

the other option uses well-founded recursion

[Aaron Liu]

which is irreducible so you can't decide things

[Juneyoung Lee]

That was fast! :) Thank you all.