mutual induction tactic

Stream: metaprogramming / tactics

[Jonathan Chan]

Hi all! First, I was wondering if there's already work underway on a mutual induction tactic (for things in Prop in particular)?

If not, I was thinking of hacking one together myself for now, which would work something like this:
Suppose I had $n$ mutual inductives I₁ ... Iₙ with $k$ constructors total, so that each Iᵢ.rec would have $k$ arguments, and suppose I were in a proof state with $m$ cases case₁ ... caseₘ, each with an element of an inductive h₁ ... hₘ . Then a tactic shaped something like this:

mutual_induction | case₁ => h₁ | ... | caseₘ => hₘ

would do the following:

1. Get the types of h₁ ... hₘ, check that they belong to one of I₁ ... Iₘ, and ensure that they are disjoint so that no types overlap (necessarily, $m \le n$)
2. Get the types of the goals of case₁ ... caseₘ, and infer a motive based on the corresponding h : I
3. In each case, apply recursors I₁.rec ... Iₘ.rec, specializing the $m$ motives by the ones inferred above, and specializing the rest by (λ _ ↦ True)
4. At this point, there should be $m$ duplicates of $k$ new goals, one for each subgoal of every recursor, so deduplicate them in the proof state so that the user only sees $k$ goals, while they are actually applied to each of the $m$ recursors

How should I go about starting something like this? I've written small tactics before that manipulate the current proof state, but not dealing with mutual inductives or with multiple goals at once. I also imagine that a lot of this is done for the usual induction tactic, like steps 2 and 3, so where should I look to find code that I can reuse?

[Aaron Liu]

induction lives in Lean.Elab.Tactic.Inducion, and probably depends on an implementation in Lean.Meta.*. You can find where a tactic lives by writing out the tactic in a by block and doing "go to definition" (default shortcuts : F12, Ctrl-click) in VSCode or the web editor.

[Jonathan Chan]

okay I'm following along Lean.Elab.Tactic.Induction mostly, here's my next problem: how do I get the MVarId of a goal from a bit of syntax? The full syntax looks like this

syntax (name := mutual_induction) "mutual_induction " ("| " ident " => " term)* : tactic

and I get getId of an ident and put that inside an MVarId, but that doesn't seem like the proper way to do it
I haven't found tactics around that manipulate existing goals, and I can't seem to Ctrl-click into what case is doing to select a goal

[Shreyas Srinivas]

So the functions for getting and switching goals work in the TacticM monad

[Shreyas Srinivas]

You can find some examples here: https://leanprover-community.github.io/lean4-metaprogramming-book/main/09_tactics.html#exploring-tacticm

[Shreyas Srinivas]

getMainGoal Lean.Elab.Tactic.getMainTarget is probably what you are looking for

[Jonathan Chan]

I'm actually trying to work under the context of given subgoals that might not be the current main goal
In the end I went for copying Lean.Elab.Tactic.BuiltinTactic.findTag? to get the MVarId associated with the given subgoal

[Shreyas Srinivas]

Oh okay. I think you can get all the goals as well. In general, the functions for manipulating and fetching goals are in this module:

https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Tactic/Basic.html

[Shreyas Srinivas]

For example there are functions like getGoals and getUnsolvedGoals

[Shreyas Srinivas]

I don’t know if it gets the goal from the syntax in the sense that you would like to get it.

[Shreyas Srinivas]

But I imagine that for cases and induction, you essentially supply metavariables to the various arguments of the recursor and then manipulate the goals using the functions in the link. The hypothesis and goals get their names when their mvar is instantiated, but you essentially get their mvarId right away in the tactic code, and use them everywhere further down.

[Jonathan Chan]

I have working examples here now: https://github.com/ionathanch/MutualInduction
I'm thinking of opening an RFC for this soon to see if this might be something worth adding

[Kyle Miller]

Nice! I've never seen a tactic that operates on multiple goals simultaneously like this, it's interesting.

One thought: having theorems that prove a conjunction tends to be a bit odd. One tool we have is mutual recursion, which works for theorems too. In EvenOdd for example, one can write:

section
variable
  -- motives
  (P : ∀ {n}, Even n → Prop)
  (Q : ∀ {n}, Odd n → Prop)
  -- subgoals
  (ezero : P zero)
  (esucc : ∀ n (on : Odd n), Q on → P (succ n on))
  (osucc : ∀ n (en : Even n), P en → Q (succ n en))

include ezero esucc osucc

mutual
theorem evenOddInd_even (n : Nat) (en : Even n) : P en := by
  match en with
  | .zero => exact ezero
  | .succ n' on =>
    apply esucc n' on
    apply evenOddInd_odd
theorem evenOddInd_odd (n : Nat) (on : Odd n) : Q on := by
  match on with
  | .succ n' en =>
    apply osucc n' en
    apply evenOddInd_even
end
end

(Note: this seems to be triggering an "unused variables" bug!)

I think this doesn't work for wtfInd in TypeTheory though. Mutual recursion for evenOddInd is taking advantage of structural recursion on the natural number, but mutually recursing on the proofs of ⊢ Γ and Γ ⊢ a ∶ A doesn't seem to work (maybe there's some termination_by that would work, though I didn't check).

Anyway, I'm wondering if, instead of a tactic, there could be a mutual_induction block to define multiple theorems. Do you think it would be common to do a mutual induction in the middle of another proof, instead of at the top level?

[Jonathan Chan]

Yeah, it seems structural recursion on some mutual inductive predicates doesn't work because the corresponding .brecOn doesn't get generated; not sure why, since I see it is generated for Even/Odd and Le/LeUnder/LeOver in the examples I have, just not for Wf/Wt

Proving mutual theorems with a conjunction is a common pattern in Rocq, especially since you can generate a combined induction principle with Combined Scheme that produces a conjunction, i.e. for Even/Odd you would get something ending in (∀ n (en : Even n), P en) ∧ (∀ n (on : Odd n), Q on)
It would be possible to do the same thing and produce a combined recursor out of all of the recursors that get generated, but I don't like working directly with this kind of recursor because then you need to prove everything in exactly that shape and order, and you need to generalize all your induction dependencies yourself
This tactic was how I imagined working around that, where you're not fixed to a conjunction, and you have the tactic generalizing everything necessary for you, and most importantly infer the motive for you

I would prefer writing mutual structural recursion though (Agda is where I really started so that's how I think about things). So it seems the solution would be to fix whatever generates .brecOn to also do it for really all mutual inductives, and you would get mutual structural recursion out of that
But anything you can write with the induction tactic you can also do with structural recursion, and I think they each have their place in spite of that, so I think it would be reasonable to have both mutual recursion and a mutual induction tactic coexist

I think it would be nice to be able to declare a mutual theorem though, which generates multiple proof obligations at once. Maybe that's what you were describing, but I'm imagining you would still prove it using a tactic, while at the top level you have multiple definitions instead of a conjoined one. So something like this:

theorems
| evenOddInd_even (n : Nat) (en : Even n) : P en
| evenOddInd_odd (n : Nat) (on : Odd n) : Q on := by
  -- there are two goals here named `evenOddInd_even` and `evenOddInd_odd`
  mutual_induction | evenOddInd_even => en | evenOddInd_odd => on
  sorry

You can't really do the two proofs separately, since invoking induction on one of the inductives requires proving the subcases for all constructors, and you don't want to duplicate that work. I suppose you could chop up the proofs and at the end of the mutual block try to match up all the pieces? But I imagine you could be trying to invoke half of a mutual induction deep in one proof and then trying to complete the other half outside of it with a mismatched context...

[Kyle Miller]

What do you think about combining the first few lines into a mutual_induction that does intro and specifies the induction premises?

theorem evenOddInv :
    (∀ n m, m = n + 1 → Even m → Odd n)
    ∧ (∀ n m, m = n + 1 → Odd  m → Even n) := by
  mutual_induction n m e h => h, n m e h => h
  case zero => injection e
  all_goals injection e with e; subst e; assumption

[Kyle Miller]

Yeah, I was thinking of something similar with a theorems command.

Given the above idea, what do you think of a theorems command that leaves a single tactic goal that's a conjunction of the theorems?

theorems (n : Nat)
| evenOddInd_even (en : Even n) : P en
| evenOddInd_odd (on : Odd n) : Q on := by
  -- there is a single goal `(Even n -> P en) /\ (Odd n -> Q on)`
  -- (also `evenOddInd_even (n : Nat) : Even n -> P e n`
  -- and `evenOddInd_odd (n : Nat) : Odd n -> Q on` can be used recursively)
  mutual_induction en => en, on => on
  sorry

[Jonathan Chan]

I like the intro variables to the left of the arrow, that would be handy
all of my examples do some sort of intros beforehand anyway

[Jonathan Chan]

I'm not sure about the conjunction
for theorems, you might as well just push each declaration as new goals anyway, instead of constructing a conjunction out of all of them, then having the mutual induction tactic immediately break it into two/multiple

[Kyle Miller]

This seems to be an unprecedented use of goals though, especially if the main use case of mutual_inductive is to run it after constructor (when in the middle of a proof). Basically, why try to merge contexts if you can start with the fact that the contexts are consistent?

[Jonathan Chan]

the other benefit of entering with two separate goals is that en and on would already be in their local contexts (they probably should be, if they're to the left of the colon), so you wouldn't even need to intro them by putting their names to the left of the arrows

[Kyle Miller]

Yeah, that's a nice benefit. The only alternative I can think of is something like

theorems (n : Nat)
  | evenOddInd_even (en : Even n) : P en => en
  | evenOddInd_odd (on : Odd n) : Q on => on := by
  -- initialized with mutual induction with targets en and on
  sorry

which isn't the greatest.

[Kyle Miller]

Do you see any case for custom mutual induction principles? Some sort of mutual_induction ... using ...?

[Jonathan Chan]

All three of the extensions to induction (using, generalizing, with) would probably also be similarly useful for mutual induction, but they're just harder to implement lol
I currently assume that the motives in each of the recursors are all in the same order and at the very front, and I'm guessing that custom induction principles would be permitted to not do that, which means instantiating each recursor will mean searching through the whole type looking for a match for every motive (not a blocking technical issue. but an annoying one)
It would also be pretty messy to add with I think, would that look like mutual_induction h₁ with ..., h₂ with ... or mutual_induction h₁, h₂ with ... | ...? And there's a bunch of syntax manipulation going on in the existing induction tactic when it comes to dealing with with that I don't totally understand
generalizing would probably be the easiest to implement, although you would need multiple clauses or else it would look kind of weird referring to free variables across contexts, so mutual_induction x₁ y₁ => h₁ generalizing x₁, x₂ y₂ => h₂ generalizing x₂
idk if that would be the same RFC or not? it's a lot of features to plan for all at once

[Jonathan Chan]

Oh if proving conjunctions is more keeping in style than manipulating multiple goals though, I think you might as well just generate a Rocq-style Combined Scheme mutual induction principle, which is probably much easier to implement and far less tactic code to maintain
That's basically what my mutual inductives proofs look like at the moment, I manually define a combined recursor and apply that, unification works pretty well at getting the right motive

[Joachim Breitner]

I should mention that it's likely on my roadmap for the next quarter to find syntax that allows mutual definitions/theorems with a shared body, and a mutual induction tactic that can be used with that. inspired by Isabelle's and in theorem statements a bit. I'll certainly look at the lessons learned here, once I get to it.

[Kyle Miller]

@Jonathan Chan I know you've been talking about an RFC; here's my feeling on what would be helpful:

• Keep developing mutual_induction and keep using it. Your GitHub project with examples is great.
• Maybe write a document that you put in the repo that collects the various ways Rocq and other theorem provers you're familiar with can handle mutually inductive theorems.

I'm speaking for Joachim here, but these would be very useful for Joachim to work out what would be compatible with the Lean FRO roadmap. Then he and/or you together could write the RFC, with the benefit of some experience with prototype implementations.

[Joachim Breitner]

Speaking of command-level syntax, I was wondering if we find something that takes a “bodyless declaration” (def, theorem, sometimes maybe a mix), but otherwise with the syntax unchanged (so that it can have attributes, docstrings etc.) and encloses it, like mutual … end does.

Maybe joint … by … or (Isabelle-inspired) … and … and … := :

joint
theorem  evenOddInd_even (n : Nat)  (en : Even n) : P en => en
theorem  evenOddInd_even (n : Nat)  (on : Even n) : Q on => on
by
  -- now there are two goals
mutual_induction …  with
| …

I currently believe that two goals are better, because the theorem declarations can have different sets of parameters before the :, so the contexts are different, and to put them into a conjunction you’d have to revert them again.

There may be applications for such joint definitions independent of mutual induction, so I would not bake the tactic application into the command syntax.

[Mario Carneiro]

how is this different from mutual theorem?

[Aaron Liu]

induction can recurse.

[Mario Carneiro]

I mean compared to Joachim's joint theorem syntax

[Aaron Liu]

You need all the goals in one place.

[Jonathan Chan]

While I was doing some debugging and figuring out how to handle missing motives, I realized I could use the tactic on nested inductives, but it's not really the right way to do it, so I was thinking about how to get the nested induction principles I really want, and I thought I'd write down some thoughts. (Should this be in a new topic? I'm not sure in what channel it would go...)

Using rose trees as the running example:

inductive RoseTree α : Type where
  | node : α → List (RoseTree α) → RoseTree α

What I would usually want (which isn't as general as RoseTree.rec I think) is for my RoseTree motive to automatically apply to all elements of the list, so I would define (this is the usual technique, nothing new)

inductive List.All {α} (P : α → Prop) : List α → Prop where
  | nil : All P []
  | cons : ∀ {x xs}, P x → All P xs → All P (x :: xs)

so that my specialized induction principle is instead

theorem RoseTree.elim {α} (P : RoseTree α → Prop)
  (hnode : ∀ {x t}, List.All P t → P (node x t)) : ∀ t, P t := by
  intro t
  induction t using RoseTree.rec (motive_2 := List.All P)
  case node ih => exact hnode ih
  case nil => constructor
  case cons => constructor <;> assumption

but since All just follows the structure of the list and the placement of the parameters, I think it should be possible to automatically generate All for any given inductive and its strictly-positive parameters that are sorts, the same way below is generated, and then you could proof-search for the specialized elim of a nested inductive the same way you do for brecOn.

Speaking of below, you could also specialize its second motive using All, so that you have something like this:

inductive RoseTree.belowAll {α} {motive : RoseTree α → Prop} : RoseTree α → Prop where
  | node : ∀ {x t}, List.All motive t → List.All belowAll t → belowAll (node x t)

which lets you prove a strong induction principle for RoseTree that says:

theorem RoseTree.brecOnAll {α} {P : RoseTree α → Prop}
  (hnode : ∀ {t}, RoseTree.belowAll (motive := P) t → P t) :
  ∀ t, P t := by
  intro t
  apply hnode
  induction t using RoseTree.elim
  case _ ts =>
    constructor
    induction ts <;> constructor
    apply hnode; assumption; assumption; assumption

I think belowAll should be straightforward to automatically generate just by spotting where all the occurrences of nested induction are and applying the nesting inductive's Allthere, but I'm not so sure about the proof search for brecOnAll, especially since the way I've proven it involves a second recursor from the nesting inductive (List). I'm also not familiar with how structural recursion gets compiled to brecOn, but it feels to me that intuitively this brecOnAll has the right amount of expressivity for it.

(Actually I think it would be really neat if Lean implemented what the Deep Induction paper does, but maybe that's a bit overkill...)

[Jonathan Chan]

And now more of a practical metaprogramming question: Is there a way to do the kind of thing that Lean.Meta.IndPredBelow does as a library instead of directly in the Lean internals? I'd like to avoid having to recompile Lean every time I make a change, and I can imagine you wouldn't want to always generate an All for every single suitable inductive, it would be better to import the functionality as a library to generate it when you need it.

[Kyle Miller]

One practical way to run code as a library is to create an attribute. Example usage:

@[mk_all]
inductive RoseTree α : Type where
  | node : α → List (RoseTree α) → RoseTree α

You don't have to recompile Lean, but you do have to opt in per type.

[Kyle Miller]

This is pretty common. You can see this with @[ext] and @[mk_iff].

[Kyle Miller]

@[ext] is even in core. I'm not sure anyone gave the rationale for why it shouldn't always attempt to run. One reason might be that @[ext] lets you name the ext lemma. A more immediate reason is that there's no existing interface to hook the ext code into to have it automatically run.

[Kyle Miller]

(I think it could be reasonable having an interface to register code to run after definitions are made.)

[Jonathan Chan]

Where's @[ext] implemented? I guess ctrl-click doesn't work attributes

[Aaron Liu]

docs#Prod.ext

[Aaron Liu]

You can check the imports for the implementation?

[Aaron Liu]

Found it: docs#Lean.Elab.Tactic.Ext.extExtension

[Kyle Miller]

Jonathan Chan said:

Where's @[ext] implemented? I guess ctrl-click doesn't work attributes

It works, but you need to have the corresponding Lean module loaded. Having import Lean should be sufficient, if you don't already have Mathlib imported.

[Kyle Miller]

Mathlib/Tactic/MkIffOfInductiveProp.lean might be a better example. With @[ext], it is also maintaining an environment extension, since the ext tactic needs a database of ext lemmas to refer to. I assume @[mk_all] doesn't need to register the All type for a given inductive type.

With @[mk_iff], the attribute is simply for running some code.

[Aaron Liu]

Kyle Miller said:

Jonathan Chan said:

Where's @[ext] implemented? I guess ctrl-click doesn't work attributes

It works, but you need to have the corresponding Lean module loaded. Having import Lean should be sufficient, if you don't already have Mathlib imported.

Half the time I want the parser and half the time I want the elaborator. Half the time I don't get what I want.

[Kyle Miller]

There's also "go to declaration", which goes to where you want another half the time.

[Kyle Miller]

Somehow mk_iff manages to make it only go to uses of the generated iff lemma no matter what you do.

[Aaron Liu]

Kyle Miller said:

There's also "go to declaration", which goes to where you want another half the time.

I think that does the same thing

[Aaron Liu]

Kyle Miller said:

Somehow mk_iff manages to make it only go to uses of the generated iff lemma no matter what you do.

It uses reference witchcraft (to_additive does it too I think)

[Floris van Doorn]

to_additive does it here

[Jonathan Chan]

I've got a six-way mutual induction example now:
https://github.com/ionathanch/MutualInduction/blob/main/CBPV/Normal.lean#L151
joint theorem syntax would be super helpful lol
the other consideration is that it's not super convenient doing generalizations on every target before mutual induction, like I end up doing this

  case' srcom  => generalize e : renameCom ξ _ = m' at r
  case' srval  => generalize e : renameVal ξ _ = v' at r
  case' sncom  => generalize e : renameCom ξ _ = m' at snm
  case' snval  => generalize e : renameVal ξ _ = v' at snv
  case' snecom => generalize e : renameCom ξ _ = m' at snem
  case' sneval => generalize e : renameVal ξ _ = v' at snev
  mutual_induction snev, snem, snv, snm, r, r generalizing ξ

and I'm not sure what kind of syntax would be helpful to make that more convenient