DecidableEq and List in inductive type

Stream: lean4

[Alcides Fonseca]

Is there any way to direve DecidableEq across lists of self DecidableEqs?

In particular, I am trying to achieve the following:

open List
open String

inductive Term where
| var : String → Term
| app : String → List Term → Term
deriving BEq, Repr --, DecidableEq

DecidableEq is commented because it fails (due to the List of Terms in the app constructor). I am halfway towards creating the instance by hand (which will be very painfully as in our project we have many more constructors, and it will create n^2 comparisons, and I am still stuck in trying to use list1 = list2 in a dite, which also fails (for the same reason).

I have dealt with a similar problem by encoding the list as part of the term (with a boolean type parameter to separate the list from the actual term), but I also wanted to avoid going that route.

Is there any useful info that I am missing?

Thanks in advance!

[Arthur Adjedj]

The derive handler for DecidableEq doesn't yet support nested inductive types, hence the error when trying to derive that instance. I need to get around to making that work at some point... in the meantime, here's a working instance:

open Term

mutual
  def decEqTerm : DecidableEq Term
    | var _, app _ _ | app _ _, var _ => .isFalse fun h => by injection h
    | var s₁ , var s₂ =>
      if h : s₁ = s₂ then .isTrue (by subst h; rfl)
      else .isFalse fun h => by injection h; contradiction
    | app s₁ l₁, app s₂ l₂ =>
      if h : s₁ = s₂ then
         match decEqListTerm l₁ l₂ with
          | .isTrue t => .isTrue (by subst h; subst t; rfl)
          | isFalse _ => .isFalse fun t => by injection t; contradiction
      else .isFalse fun h => by injection h; contradiction

  def decEqListTerm : DecidableEq (List Term)
    | [],[] => .isTrue rfl
    | h::t,[] | [], h::t => .isFalse fun h => by injection h
    | h₁::t₁,h₂::t₂ =>
      match decEqTerm h₁ h₂ with
        | .isTrue h => match decEqListTerm t₁ t₂ with
          | .isTrue t => .isTrue (by subst h₁; subst t; rfl)
          | isFalse _ => .isFalse fun t => by injection t; contradiction
        | isFalse _ => .isFalse fun h => by injection h; contradiction
end

instance : DecidableEq Term := decEqTerm

[Alcides Fonseca]

I was completely missing the mutual definition! That makes total sense!

I wish I needn't need to considerate all pairs in the first case of decEqTerm, but I'll wait eagerly for the nested inductive types!

Thank you so much for the help, Arthur!

[Joachim Breitner]

Arthur, I was just looking at that module to see what's missing for decidable equality for nested inductives. I hope to have mutual structural recursion over nested inductives soonish. Once that's there, the deriving code can be adjusted, I assume. Is that something you'd be want to implement then?

[Joachim Breitner]

And I guess for mutual non-nested inductive it's already possible (on my branch there)

[Arthur Adjedj]

Hi Joachim,
Deriving DecidableEq for mutual inductive types has already been supported since lean4#2591, although it uses wellfounded recursion and is, thus, quite slow. It might be interesting to see whether the definitions generated by the derive handler could be generated in a structural manner once your PR lands.

I have an old PR which aims to support deriving DecidableEq for nested inductive types (lean4#3160), but it still requires a bit of work. Examples such as the one in this thread should already work, but things get harder once you start nesting your inductive inside more complex inductive types. For example, if this Term definition was to nest inside an array instead of a List, you would need to not only make a definition to derive DecidableEq for Array Term, but also one for List Term since it appears in the instantiated definition of Array. Managing such cases is the last building block missing fom my PR.

[Joachim Breitner]

Nice! It seems to be in good hands. Let me know if you face issues using structural recursion, should you try. (I guess for decidable equality it doesn't really matter how it is implemented, as one doesn't need the DefEqs?)

[Arthur Adjedj]

Having the better reduction behaviour from structural recursion would make decide much more usable when working with mutual/nested types.