proving DecidableEq for inductives

Stream: lean4

[Sébastien Michelland]

I'm trying to provide DecidableEq for a nested/mutual inductive type by hand. Here is a fairly representative MWE:

inductive X :=
  | X1
  | X2
  | X3
  | Pair: (X × X) → X

def X.deq (a: X) (b: X): Decidable (a = b) :=
  match a, b with
  | X1, X1 => isTrue rfl
  | X2, X2 => isTrue rfl
  | X3, X3 => isTrue rfl
  | Pair (a₁,a₂), Pair (b₁,b₂) =>
      match deq a₁ b₁, deq a₂ b₂ with
      | isTrue h₁, isTrue h₂ => isTrue (by rw [h₁,h₂])
      | isFalse h₁, _ => isFalse (fun h => by cases h; cases (h₁ rfl))
      | _, isFalse h₂ => isFalse (fun h => by cases h; cases (h₂ rfl))
  | _, _ => isFalse sorry

The problem "on the surface" is that wildcard pattern does not provide enough information to prove the isFalse case. I'd like to write the function without listing all pairs of constructors, as my real example has quite a lot. Ideally I'd like to define a boolean equality first and then prove that it decides equality in a lemma. How should I go about that?

I've tried some variations on the matching (eg. match on the first argument then nest another match for the second) or using tactic mode to discharge the quadratic number of cases quickly, but none of my attempts feel really convincing.

[Evgeniy Kuznetsov]

inductive X :=
  | X1
  | X2
  | X3
  | Pair: (X × X) → X

def X.deq (a: X) (b: X): Decidable (a = b) := by
  generalize ha: a = a'
  generalize hb: b = b'
  cases a' <;> cases b' <;> try exact isFalse X.noConfusion
  case X1 => exact isTrue rfl
  case X2 => exact isTrue rfl
  case X3 => exact isTrue rfl
  case Pair a b =>
    let (a₁, a₂) := a
    let (b₁, b₂) := b
    exact match deq a₁ b₁, deq a₂ b₂ with
    | isTrue h₁, isTrue h₂ => isTrue (by rw [h₁,h₂])
    | isFalse h₁, _ => isFalse (fun h => by cases h; cases (h₁ rfl))
    | _, isFalse h₂ => isFalse (fun h => by cases h; cases (h₂ rfl))
decreasing_by
  subst ha hb
  simp_wf
  simp_arith

[Sébastien Michelland]

Thanks! This seems like a great start. I just had to change the let-binding on leanprover/lean4:nightly-2022-04-26 to uses cases (it didn't substitute a and b in the goal). I'll have to see if I can generalize it to my actual example now.

[François G. Dorais]

Changing the definition of Pair a bit makes it automatic:

inductive X :=
  | X1
  | X2
  | X3
  | Pair' : X → X → X
deriving DecidableEq

#synth DecidableEq X -- fun a b => instDecidableEqX a b

@[matchPattern]
abbrev X.Pair : X × X → X
| (x₁,x₂) => Pair' x₁ x₂

The matchPattern attribute allows you to use X.Pair in match expressions as if it was an actual constructor.

[Sébastien Michelland]

Yes I'm using deriving for most types, it's really handy. The real occurrence of nesting is with a list; there's some mutual definitions involved too, which makes it advanced enough that I wouldn't try to play with the Lean core either.

I didn't know about @[matchPattern] though, and I have a use for it right now, so thanks a lot for mentioning it.

[Leonardo de Moura]

When we implemented deriving for DecidableEq, we didn't have good support for well-founded recursion. We now have it, and we will eventually add support for nested and mutual inductive types at Lean/Elab/Deriving/DecEq.lean. It is not very high priority right now because Mathlib does not need it.

[Leonardo de Moura]

I pushed support for casesOn applications to the structural and well-founded recursion modules. This is useful for using recursion and cases tactic. For example, we don't need the generalizations steps above nor the decreasing_by anymore. It should work with any tactic that creates casesOn applications (e.g., rcases).
https://github.com/leanprover/lean4/blob/8c23bef39907e2599fb8ade149b7aa68ab4da311/tests/lean/run/casesRec.lean#L35-L49