feat: manage nested inductive types in deriving

[arthur-adjedj]

Adds support for handling nested inductive types in derive handlers

This changes the Deriving codebase a fair bit, I'll probably need to split this into multiple PRs.
In particular, the file FromToJson.lean has been refactored a fair bit.
(Will add a more thorough description once the PR is stable)

Closes #2329

[arthur-adjedj]

WIP

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ea43ebd54a0848bf99b9a080daaf31e4025d2552 --onto a5b8d5b486a3b47650cd4204ddf64716ef991c58. (2024-07-27 13:46:50)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a8740f5ed9b419591d711a57e36e449f5623daf8 --onto 8acdafd5b3957382c02779ada451c14da44e2aca. (2024-08-01 23:07:26)
• 🟡 Mathlib branch lean-pr-testing-3160 build this PR didn't complete normally. (2024-08-15 10:26:43) View Log
• 🟡 Mathlib branch lean-pr-testing-3160 build this PR didn't complete normally. (2024-09-12 06:46:15) View Log
• 🟡 Mathlib branch lean-pr-testing-3160 build this PR didn't complete normally. (2024-09-12 15:56:52) View Log
• ✅ Mathlib branch lean-pr-testing-3160 has successfully built against this PR. (2024-09-13 10:30:43) View Log
• ✅ Mathlib branch lean-pr-testing-3160 has successfully built against this PR. (2024-09-13 12:05:01) View Log
• 💥 Mathlib branch lean-pr-testing-3160 build failed against this PR. (2024-09-13 14:49:00) View Log
• 💥 Mathlib branch lean-pr-testing-3160 build failed against this PR. (2024-09-14 08:31:10) View Log

[nomeata]

Oh, did I miss that this is ready for review? The label still says WIP.

[arthur-adjedj]

Whoops, forgot to change that. This is indeed ready for review, I sent Kim some details in DM regarding that PR, but I might as well put it all in here for documentation purposes:
The PR changes a fair amount of things in the Deriving codebase, namely:

• The derive handlers for FromJson and ToJson have been refactored to be similar to the other implementations. Their logic has stayed the same, but the content was cut into more functions to make it more readable (i.e the implementation to derive for structs and inductives used to be in one big function with huge if-then-elses, so these were split).
• The logic in Util.lean has been modified. Instead of working on inductive types, it now relies on a type NestedOccurence, which represents either base inductives (with the leaf constructor), or a nested occurence in the constructor of another inductive type (as nodes). That way, via an initial traversal the inductive types getting their derivations, we can gather all the different nested occurences appearing in them, to know which functions we need to define in the mutual block to derive the typeclass needed. For example:

inductive Foo (α : Type u) : Type u :=
  | foo : List (Option (Foo α)) → Foo α
deriving DecidableEq

Will generate a mutual block with the definitions:

mutual
  def decEqOptionFoo {α} [DecidableEq α] (x : Option (Foo α)) (x1 : Option (Foo α)) : Decidable (x = x1) := ...
  def decEqListOptionFoo {α} [DecidableEq α] (x : List (Option (Foo α))) (x1 : List (Option (Foo α))) : Decidable (x = x1) := ...
  def decEqFoo {α} [DecidableEq α] (x : Foo α) (x1 : Foo α) : Decidable (x = x1) := ...
end

• Because Util.lean has changed, all the derive handlers needed to be adapted to those changes.

When first working on the PR, I was hoping to be able to use these modifications to Util to get rid of usePartial altogether in the derive handlers. However, the modifications made here are insufficient for this.
One further change I would like to make in a subsequent PR would be to change how the functions for nested occurences are derived. Currently, if a nested occurence (i.e Option (Foo A)) needs to be derived, the derive handler will generate the necessary function. However, if such an instance already exists for i.e Option A, using that instance as the function in the mutual block (i.e with A replaced with Foo A) might prove more sensible. In particular, this would allow us to get rid of usePartial in FromJson, ToJson and Repr without changing their current outputs on nested/mutual types. I plan on looking into this possibility in the future.

The PR currently passes CI/CL on Lean 4, but fails to compile batteries and mathlib.

• For batteries, because I've needed to upstream Sum.elim from the repo, leading to a duplicate definition
• For Mathlib, because their derive handler for ToExpr relies on the lean core deriving mechanism, and would thus need to be adapted to the new API (I am willing to do such a PR)

[arthur-adjedj]

awaiting-review

[nomeata]

Thanks! Maybe worth doing the mathlib adaption on a branch to be sure that it works before we merge?

Would it be too much work to put the JSON refactoring into a PR of it's own, or would that require work that is then thrown away again?

[arthur-adjedj]

I think putting the JSON refactoring in a separate PR is doable and would be beneficial, I'll start working on that.

I'll be making a mathlib PR fixing their derive handler as well. Until this two things are done, and the former has been merged, I'm putting this PR back to WIP

[arthur-adjedj]

WIP

[nomeata]

Thanks! Let me know if you need anything from me

[arthur-adjedj]

Sum.elim isn't an absolute necessity for the PR, it's only used once, I just thought this was the best way to code this function and upstreamed what I needed. I could just make the match by hand.

[nomeata]

I think I was wondering whether and why it needs a stage0 update.

[arthur-adjedj]

Hmm, I remember having some build failures on stage2 without it at some point, but it seems to be working without it now. All the better ! I'll remove it.

[nomeata]

Playing around with it a bit I notice that for

inductive Tree where | node : Array Tree → Tree
deriving DecidableEq, BEq

we get

mutual
       set_option match.ignoreUnusedAlts✝ true
       private partial def beqTree✝ (x✝ : @Tree✝) (x✝¹ : @Tree✝) : Bool✝ :=
         let localinst✝ : BEq✝ (@Tree✝) := ⟨beqTree✝⟩;
         match x✝, x✝¹ with
         | @Tree.node a✝, @Tree.node b✝ => a✝ == b✝
         | _, _ => false✝
     end,
     instance : BEq✝ (@Tree✝) :=
       ⟨beqTree✝⟩

but

mutual
       private def decEqListTree✝ (x✝ : @List✝ (@Tree✝)) (x✝¹ : @List✝ (@Tree✝)) : Decidable✝ (x✝ = x✝¹) :=
         match x✝, x✝¹ with
         | @List.nil _, @List.nil _ => isTrue✝ rfl✝
         | List.nil .., List.cons .. => isFalse✝ (by intro h✝; injection h✝)
         | List.cons .., List.nil .. => isFalse✝ (by intro h✝; injection h✝)
         | @List.cons _ a✝ a✝¹, @List.cons _ b✝ b✝¹ =>
           let inst✝ := decEqTree✝ @a✝ @b✝;
           if h✝¹ : @a✝ = @b✝ then by subst h✝¹;
             exact
               let inst✝¹ := decEqListTree✝ @a✝¹ @b✝¹;
               if h✝² : @a✝¹ = @b✝¹ then by subst h✝²; exact isTrue✝¹ rfl✝¹
               else isFalse✝¹ (by intro n✝; injection n✝; contradiction)
           else isFalse✝² (by intro n✝¹; injection n✝¹; contradiction)
       termination_by structural x✝
       private def decEqArrayTree✝ (x✝² : @Array✝ (@Tree✝)) (x✝³ : @Array✝ (@Tree✝)) : Decidable✝ (x✝² = x✝³) :=
         match x✝², x✝³ with
         | @Array.mk _ a✝², @Array.mk _ b✝² =>
           let inst✝² := decEqListTree✝ @a✝² @b✝²;
           if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝² rfl✝²
           else isFalse✝³ (by intro n✝²; injection n✝²; contradiction)
       termination_by structural x✝²
       private def decEqTree✝ (x✝⁴ : @Tree✝) (x✝⁵ : @Tree✝) : Decidable✝ (x✝⁴ = x✝⁵) :=
         match x✝⁴, x✝⁵ with
         | @Tree.node a✝³, @Tree.node b✝³ =>
           let inst✝³ := decEqArrayTree✝ @a✝³ @b✝³;
           if h✝⁴ : @a✝³ = @b✝³ then by subst h✝⁴; exact isTrue✝³ rfl✝³
           else isFalse✝⁴ (by intro n✝³; injection n✝³; contradiction)
       termination_by structural x✝⁴
     end,
     instance : DecidableEq✝ (@Tree✝) :=
       decEqTree✝

Where in the code is the decision made to translate them differently?

I’m a bit worried about the latter. While all DecidableEq are logically equivalent, they do differ in their run-time behavior, and this matters whenever someone writes if t1 = t2, right? Otherwise we wouldn’t have a custom implementation for array in

lean4/src/Init/Data/Array/DecidableEq.lean

Lines 47 to 51 in e9e858a

	instance [DecidableEq α] : DecidableEq (Array α) :=
	fun a b =>
	match h:isEqv a b (fun a b => a = b) with
	| true => isTrue (eq_of_isEqv a b h)
	| false => isFalse fun h' => by subst h'; rw [isEqv_self] at h; contradiction

.

The author of the Tree type above might reasonable expect that decidable equality on their type uses that Array implementation, and not a naive one via list as generated by the deriving code.

But I also don’t see an easy alternative. partial doesn’t make sense for DecidableEq, I assume. Somehow copying the instance code seems hairy.

Maybe after creating decEqArrayTree we could automatically prove a csimp lemma that connects it to the inferred implementation? For DecidableEq at least that proof is simple (DecidableEq is a subsingleton). Would that work?

Which other instances are not using partial here? It seems that most use partial and hence the “right” instance.

[digama0]

I'm not sure I would call the partial instance the "right" one. Especially if one hopes to prove properties about the BEq instance (I have wanted to implement a LawfulBEq deriving instance for some time), partial makes that impossible so I would prefer to not see it used any more than it already is. Instead, we should have better combinators to make it possible to actually implement a terminating function over nested recursive types which doesn't have to break the Array abstraction.

[arthur-adjedj]

Where in the code is the decision made to translate them differently?

This is dictated by the withNested argument of mkContext. This differentiation was made to ensure the behaviour of the usual derive handlers wouldn't change. For example, the FromJson and ToJson instances for Array are quite specific, and having them change in nested inductives would break a lot of code, and lead to unreliable derive handlers.

I’m a bit worried about the latter. While all DecidableEq are logically equivalent, they do differ in their run-time behavior, and this matters whenever someone writes if t1 = t2, right?

Right. This is the biggest issue with the current PR IMO, and I plann on tackling this in a later PR if that's acceptable (I have not yet started working on any proof-of-concept for such a PR).

Somehow copying the instance code seems hairy.

This is my initial solution to the problem, but it would impose some challenges (for example, if some instance is defined using some extern binding, how feasable would it be to add that binding to the "new" function as well ?).
I think doing this would be the most reliable solution though, as it would allow most handlers to get rid of partial altogether. Adding some csimp lemmas to the mix as well might solve all the abovementioned issues, but on non-singleton types, proving these csimp lemmas might prove non-trivial..

Which other instances are not using partial here ?

For now, only DecidableEq gets rid of partial.

I'm not sure I would call the partial instance the "right" one.

I agree that it would be ideal to get rid of partial in the derive handlers altogether, any other ideas on how this should be solved are welcome.

[nomeata]

but on non-singleton types, proving these csimp lemmas might prove non-trivial..

What I mean is that for every Type t, the Type DecidableEq t is a subsingleton (isn't it?) so proving a csimp between the derived and the user defined one should always be trivial?

[arthur-adjedj]

I don't think it would be an issue on DecidableEq, but I would ideally want to find a solution that works for other derive handlers as well (such as BEq, in order to also have non-partial, accurate BEq implementations like Mario asked)

[nomeata]

Would be nice indeed, but I don't really have a good idea. Maybe with #4749 and with all functions involved refined using primitive recursion? But that won't help when a user wrote an off standard method.

For the present PR I am hesitant to merge it while we get the unexpected behavior. Maybe the csimp approach would be good enough.

Or, even less ambitious: somehow keep track of which instances were derived and only derive nested instances where all involved type formers have instances that were also derived and where we thus know that they behave like the one we are writing.

Sorry for not thinking of this issue before!

[arthur-adjedj]

I think the csimp approach is doable. Another solution, albeit hacky-ish, could be to

• keep the current derivation
• we could make a partial DecidableEq instance using Classical theorems, and link that to the derived implementation using implemented_by to get the correct runtime behaviour

For example, the code generated for the array tree would look like this:

inductive Tree where | node : Array Tree → Tree

noncomputable local instance : Inhabited (DecidableEq α) := ⟨Classical.typeDecidableEq _⟩  in
partial def decEqTreePartial (x4 : @Tree) (x5 : @Tree) : Decidable (x4 = x5) :=
  let inst : DecidableEq Tree := decEqTreePartial
  match x4, x5 with
  | @Tree.node a3, @Tree.node b3 =>
    if h4 : @a3 = @b3 then by subst h4; exact isTrue rfl
    else isFalse (by intro n3; injection n3; contradiction)

mutual
  def decEqListTree (x : List Tree) (x1 : List Tree) : Decidable (x = x1) :=
    match x, x1 with
    | @List.nil _, @List.nil _ => isTrue rfl
    | List.nil .., List.cons .. => isFalse (by intro h; injection h)
    | List.cons .., List.nil .. => isFalse (by intro h; injection h)
    | @List.cons _ a a1, @List.cons _ b b1 =>
      let inst := decEqTree a b;
      if h1 : a = b then by subst h1; exact (
          let inst1 := decEqListTree @a1 @b1
          if h2 : a1 = b1 then 
            by subst h2; exact isTrue rfl
          else 
            isFalse (by intro n; injection n; contradiction)
      )
      else isFalse (by intro n1; injection n1; contradiction)
  termination_by structural x
  
  def decEqArrayTree (x2 : @Array (@Tree)) (x3 : @Array (@Tree)) : Decidable (x2 = x3) :=
    match x2, x3 with
    | @Array.mk _ a2, @Array.mk _ b2 =>
      let inst2 := decEqListTree @a2 @b2;
      if h3 : @a2 = @b2 then by subst h3; exact isTrue rfl
      else isFalse (by intro n2; injection n2; contradiction)
  termination_by structural x2

  @[implemented_by decEqTreePartial]
  def decEqTree (x4 : Tree) (x5 : Tree) : Decidable (x4 = x5) :=
    match x4, x5 with
    | Tree.node a3, Tree.node b3 =>
      let inst3 := decEqArrayTree a3 b3;
      if h4 : a3 = b3 then by subst h4; exact isTrue rfl
      else isFalse (by intro n3; injection n3; contradiction)
  termination_by structural x4
end

instance : DecidableEq Tree :=
  decEqTree

[nomeata]

Sorry, but I'm not getting it. What is the purpose of decEqTreePartial, and how does it help?

[arthur-adjedj]

decEqTreePartial is "the right" DecidableEq instance in that it provides the expected runtime behaviour for decEqTree, and will use the already defined DecidableEq instances for List and Array in that example

[nomeata]

Ah, now I see it, on the laptop the code is easier to understand :-)

And the purpose of

noncomputable local instance : Inhabited (DecidableEq α) := ⟨Classical.typeDecidableEq _⟩  in

is merely to to avoid

failed to compile partial definition 'decEqTreePartial', failed to show that type is inhabited and non empty

right?

Would it be better or worse to omit that and use unsafe instead of partial then? That definition is only used in implementedBy, so we might as well hide it from the kernel completely.

Hmm, not bad overall. Better or worse than this variant?

inductive Tree where | node : Array Tree → Tree

mutual
  def decEqListTree (x : List Tree) (x1 : List Tree) : Decidable (x = x1) :=
    match x, x1 with
    | @List.nil _, @List.nil _ => isTrue rfl
    | List.nil .., List.cons .. => isFalse (by intro h; injection h)
    | List.cons .., List.nil .. => isFalse (by intro h; injection h)
    | @List.cons _ a a1, @List.cons _ b b1 =>
      let inst := decEqTree a b;
      if h1 : a = b then by subst h1; exact (
          let inst1 := decEqListTree @a1 @b1
          if h2 : a1 = b1 then 
            by subst h2; exact isTrue rfl
          else 
            isFalse (by intro n; injection n; contradiction)
      )
      else isFalse (by intro n1; injection n1; contradiction)
  termination_by structural x
  
  def decEqArrayTree (x2 : @Array (@Tree)) (x3 : @Array (@Tree)) : Decidable (x2 = x3) :=
    match x2, x3 with
    | @Array.mk _ a2, @Array.mk _ b2 =>
      let inst2 := decEqListTree @a2 @b2;
      if h3 : @a2 = @b2 then by subst h3; exact isTrue rfl
      else isFalse (by intro n2; injection n2; contradiction)
  termination_by structural x2

  def decEqTree (x4 : Tree) (x5 : Tree) : Decidable (x4 = x5) :=
    match x4, x5 with
    | Tree.node a3, Tree.node b3 =>
      let inst3 := decEqArrayTree a3 b3;
      if h4 : a3 = b3 then by subst h4; exact isTrue rfl
      else isFalse (by intro n3; injection n3; contradiction)
  termination_by structural x4
end

instance : DecidableEq Tree :=
  decEqTree

-- now patch up the implementations of any nested derived instance

def realDecEqArrayTree (x2 : @Array (@Tree)) (x3 : @Array (@Tree)) : Decidable (x2 = x3) := inferInstance

@[csimp]
theorem decEqArrayTree_eq : @decEqArrayTree = @realDecEqArrayTree := by
  ext t1 t2; apply Subsingleton.allEq 

It's still not perfect in the cases where the nested type has a manually written (maybe more efficient) DecidableEq instance that the user plans to use in kernel reduction (e.g. using by decide).

[arthur-adjedj]

The local instance is just used to avoid the error message, and using unsafe might just be better indeed.

In both cases, having a non-ideal kernel reduction seems unavoidable sadly. The ultimate solution would still be to use the already existing instance in the mutual block, but that would open another can of worms I don't have the time to get into currently, hence why I'd like to work on that in a follow-up PR.

If we assume that this is a temporary hack, I would tend towards using the unsafe approach instead of the csimp one, simply for ease of implementation, but I'm not against choosing csimp. Any opinion is welcomed.

[nomeata]

Either hack is fine with me, if we want a hack at all. I'm not sure if the feature “derivable decidable equality for nested induction” itself is worth introducing hacks and complications for - how pressing is it for our users? I'll also check back with Leo, as the reporter of #2329.

[nomeata]

Ah, forgot to report back.

I don’t think we had a good solution either.

The safest bet would be to fail instead of deriving possibly bad nested inductives, with a good error message that points to a github issue where users can complain.

The next safest bet might be an internal attribute that we use to track “this type’s DecidableEq instance is derived”, and do the construction for those types whose instance is itself derived, because for them we know we are generating equivalent code. Not very satisfying, though.