DecidableEq for nested inductive types

Stream: general

[Jeremy Avigad]

Consider this definition:

inductive Term where
  | var (x : String)
  | app (f : String) (args : List Term)

I just managed to provide an instance of DecidableEq Term, but it wasn't easy. Is there a better way to do it?

open Term in
mutual
private def aux₁ : DecidableEq Term
| var x, var y => by simp; infer_instance
| var x, app f args => by simp; infer_instance
| app f args, var y => by simp; infer_instance
| app f₁ args₁, app f₂ args₂ => by
rw [app.injEq]
apply @instDecidableAnd _ _ _ (aux₂ args₁ args₂)

private def aux₂ : DecidableEq (List Term)
| [], [] => by simp; infer_instance
| [], y::ys => by simp; infer_instance
| x::xs, [] => by simp; infer_instance
| x::xs, y::ys => by
rw [List.cons.injEq]
apply @instDecidableAnd _ _ (aux₁ x y) (aux₂ xs ys)
end

instance : DecidableEq Term := aux₁

In any case, I am impressed that Lean can handle such recursive definitions.

[Kyle Miller]

With a few helper functions for Decidable, you can write it pretty much like a boolean function directly, which I think is about the bare minimum you'd expect if you had to write an equality function:

instance (p : Prop) : CoeOut (Decidable p) Bool := ⟨@decide p⟩

@[inline] def dtrue {p : Prop} (h : p := by simp) : Decidable p := isTrue h
@[inline] def dfalse {p : Prop} (h : ¬ p := by simp) : Decidable p := isFalse h
@[inline] def decide_by {p : Prop} (q : Prop) [Decidable q] (h : q ↔ p := by simp) : Decidable p :=
  decidable_of_iff q h

inductive Term where
  | var (x : String)
  | app (f : String) (args : List Term)

namespace Term

mutual

protected def deq : (x : Term) → (y : Term) → Decidable (x = y)
  | var x, var y => decide_by (x = y)
  | var .., app .. => dfalse
  | app .., var .. => dfalse
  | app f₁ args₁, app f₂ args₂ => decide_by (f₁ == f₂ && Term.deq_list args₁ args₂)

protected def deq_list : (xs : List Term) → (ys : List Term) → Decidable (xs = ys)
  | [], [] => dtrue
  | [], _::_ => dfalse
  | _::_, [] => dfalse
  | x::xs, y::ys => decide_by (Term.deq x y && Term.deq_list xs ys)

end

instance : DecidableEq Term := Term.deq

[Kyle Miller]

Little warning about your version: if you do by simp; infer_instance or use rw, it's possible to get Decidable terms that can't reduce (for example, it can cause the decide tactic to fail). It's better to use decidable_of_iff, which pushes the rewrite into the proofs. Here, I wrapped that up in decide_by.

[Kyle Miller]

A neat thing that works out with my version is that the compiled code even respects the short-circuiting behavior of &&, so it's as efficient as it looks (if you treat decide_by as being this weird cast you have to insert.)

[Kyle Miller]

(Ideally we could just write deriving DecidableEq, but that doesn't support nested inductives yet.)