induction on mutual inductives fails

Stream: lean4

[Jakob von Raumer]

mutual
inductive A : Type
| a : A

inductive B : Type
| b : B
end

example (x : PSigma fun (a : A) => True) : A := by
  cases x with | mk x₁ x₂ => ?_
  induction x₁

gives a tactic 'introN' failed, insufficient number of binders on the induction call. Should this be working by now or is this not implemented yet?

[Jakob von Raumer]

(Adding noncomputable is no remedy, so it's not the code generation)

[Jakob von Raumer]

Also worth adding that if I put (y : A) (z : True) in the premises of the example, it works, so maybe there's just some whnfing missing

[Jakob von Raumer]

Here's an example without PSigma:

mutual
inductive A0 : Type

inductive A1 : Type
end

inductive B : A0 → Prop
| b0 : B a

theorem foo (a : A0) (b : B a) : True := by
  induction a

[Leonardo de Moura]

@Jakob von Raumer Yes, the current induction tactic does not support mutually inductive types. Note that cases supports them.
The key issue is that the induction tactic uses the A0.rec recursor, and it has multiple motives. The current induction tactic supports only recursors with one motive. This is why cases works, A0.casesOn has a single motive.
That being said, I will add a better error message.

[Jakob von Raumer]

How high is the priority to add the support? I'm preparing code for a publication and having to show some apply @A0.rec _ _ is a bit messy...

[Jakob von Raumer]

What's funny is that removing the (b : B a) in the second example makes it go through...

[Leonardo de Moura]

Jakob von Raumer said:

What's funny is that removing the (b : B a) in the second example makes it go through...

It worked by "accident". If you add constructors to A0 and A1, it will fail at some point.

mutual
inductive A0 : Type
  | mk : A1 → A0

inductive A1 : Type
end

inductive B : A0 → Prop
| b0 : B a

theorem foo (a : A0) : True := by
  induction a <;> admit

[Leonardo de Moura]

Jakob von Raumer said:

How high is the priority to add the support? I'm preparing code for a publication and having to show some apply @A0.rec _ _ is a bit messy...

It is a very low priority :(
Even if we add it, you will still need to provide the other motives. The tactic induction a would only infer the motive corresponding to A0.

[Leonardo de Moura]

Note that, if we are willing to write the other motives, it is not too much work to write one extra motive for A0. Named arguments help a bit. We can write

   apply C.recOn (motive_1 := ...) ... (motive_n := ...) c

[Jakob von Raumer]

Even if we add it, you will still need to provide the other motives. The tactic induction a would only infer the motive corresponding to A0.

That's the expected behaviour, isn't it? Or would it set all others to PUnit?

[Leonardo de Moura]

That's the expected behaviour, isn't it?

Yes, it is. My point was that if we are already willing to provide the other motives, then providing an extra one is not that big of a deal. That is, the user is already aware of what motives are, and how they work. If feels like that the induction tactic would be a minor improvement over

   apply C.recOn (motive_1 := ...) ... (motive_n := ...) c

in this case.

Or would it set all others to PUnit?

I think setting the others to PUnit would only work on simple cases. For example, the types in the mutual block are not really recursive, but in this case, we could use cases instead.

[Mac]

Leonardo de Moura said:

That is, the user is already aware of what motives are, and how they work. If feels like that the induction tactic would be a minor improvement over

   apply C.recOn (motive_1 := ...) ... (motive_n := ...) c

in this case.

True, however, I think from a readability/aesthetic perspective even induction c (motive_1 := ...) ... (motive_n := ...) (or the like) is much cleaner. It allows readers of the code to get a handle on what's going on (i.e., induction) even if they don't fully understand what motives are. It also removes the need to specify C.recOn, which may be annoying and space consuming depending upon how long a name C is (and may also be confusing to more novice readers).

[Leonardo de Moura]

@Mac I am not disputing whether it is more readable and/or cleaner. My main point was to justify why this feature is a low-priority right now. We have a huge list of higher priority issues to address. Moreover, this feature is not needed to port Mathlib.

[Sebastian Ullrich]

Fwiw, I think induction c (motive_1 := ...) would be the wrong abstraction level anyway. In Isabelle, mutual induction is done over a meta-level conjunction of an appropriate number of goals, as well as an appropriately sized list of induction variables, from which the motives can be derived (if Isabelle even does something like that). We don't have meta-level conjunctions (except for the list of open goals, but I don't think induction working on more than the main goal would be ergonomic), but regular ones seem fine as well.

[Leonardo de Moura]

In Isabelle, mutual induction is done over a meta-level conjunction of an appropriate number of goals, as well as an appropriately sized list of induction variables, from which the motives can be derived (if Isabelle even does something like that)

If the user is willing to provide the different goals, then I think let rec is a good solution for Lean.
It already works in tactic mode, and we will have support for mutual recursion as soon as we have: https://github.com/leanprover/lean4/issues/176