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

[Jonathan Chan]

I went back to look at the work I did on the @[mk_all] attribute that generates e.g. List.all:

Jonathan Chan said:

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

In a proof, I tried to simp [List.all], but I got the following error:

trying to realize List.all.eq_1 but `enableRealizationsForConst` must be called for 'List.all' first

What does that mean? At what point should I be calling enableRealizationsForConst? On List.all, I assume?

[Sebastian Ullrich]

As the docstring says, usually at the latest possible point after you add List.all

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Thanks for your work on this @Jonathan Chan! I had recently written a more rudimentary version of this tactic (only proves conjunctions, no generalization functionality). Before I saw this thread, I was planning to add the features you already have - support for multiple goals and generalization - so I am glad others are looking into it :) However, I would like to suggest a flexibility improvement.

The issue is that in the current implementation, one may only specify variables to generalize that are shared across all goals. However, one often wants to generalize different things per goal. For example, in this MWE we get a IH with a useless quantifier up front:

mutual
inductive Foo : Prop
  | foo : Bar → Foo

inductive Bar : Prop
  | bar : Foo → Bar
end

example (n : Nat) : (Foo → n = 0 → Bar) ∧ (Bar → Foo) := by
  refine ⟨fun h _ => ?_, fun h => ?_⟩
  mutual_induction h, h generalizing n
  /-
  case refine_1.foo
  a✝ : Bar
  a_ih✝ : ∀ (n : ℕ), Foo -- generalization not useful
  n : ℕ
  x✝ : n = 0
  ⊢ Bar
  -/
  all_goals sorry

In the actual example, I have a variable l which in the context of one goal is an index (so cannot be generalized), whereas in another goal is not an index and actually must be generalized to prove the goal.

A syntax that could work for this would be a variation of your original proposal:

mutual_induction | case₁ => h₁ (generalizing x₁, ..., xₖ)? | ... | caseₘ => hₘ (generalizing y₁, ..., yₗ)?

This syntax also seems more robust than the current mutual_induction h₁, ..., hₘ because it is invariant under permutations of the goal list.

[Jonathan Chan]

In the actual example linked, it looks to me that as you've written it, the mutual induction should behave as desired: l always will be generalized in the subtheorem about WfCtx Γ (since it's not shared with the others), and l in the other subtheorems about ⊢[l]will be treated as an inductive index. Even if you rewrite the first one to ∀ {Γ A i l}, WfCtx Γ → Lookup Γ i A l → l ≤ univMax, all of Γ, A, i, l need to be generalized over, because they are depended upon by the goal Lookup Γ i A l → l ≤ univMax.

I see what you mean in the example above though, especially if the theorem were something like

example (n : Nat) : (Foo → n = 0 → Bar) ∧ (n = 1 → Bar → Foo) := by ...

where you do want to generalize n in the first goal but you don't want to generalize n in the second goal. Although I feel if the n in the first goal is "different" from the n in the second goal, in that it varies in the first but not the second, maybe you should be pushing the quantifier into the conjuncts for clarity? Otherwise, to use your actual example, it would be like pulling the A argument out of the conjuncts as if it's the "same" A across all of the subtheorems, which it isn't supposed to be. But maybe it would be a handy convenience, since I would be tempted to pull the Γ out.

In any case, the discussion further up this thread seemed to suggest that referring to goal names directly in a tactic is highly unusual behaviour, which is why I had changed my original proposal from explicitly using the goal names to simply listing the variables to induct on in goal order. (I do agree it's more robust to name the goals, which is why I had originally designed it like that.) If we want to keep the goals unnamed, what might generalizing per goal look like? Maybe mutual_induction h₁, h₂ generalizing x₁ ... xₙ, y₁ ... yₙ? But then it would be a big pain repeating all of the variables shared among the goals, which defeats the purpose of sharing them in the first place.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

it looks to me that as you've written it, the mutual induction should behave as desired

Indeed :) But I wrote it like that so that my dumb tactic would work, and it would be nice to write shorter statements.

Even if you rewrite the first one to ∀ {Γ A i l}, WfCtx Γ → Lookup Γ i A l → l ≤ univMax, all of Γ, A, i, l need to be generalized over, because they are depended upon by the goal Lookup Γ i A l → l ≤ univMax.

I am not following you here, sorry. I am interpreting 'x is generalized over' as 'in the motive, x is universally quantified'. But you don't always need to quantify over every variable that the goal depends on; e.g., the previous example doesn't need that for n:

example (n : Nat) : (Foo → n = 0 → Bar) ∧ (Bar → Foo) := by
  refine
    ⟨Foo.rec (motive_1 := fun _ => n = 0 → Bar) (motive_2 := fun _ => Foo) ?foo ?bar,
     Bar.rec (motive_1 := fun _ => n = 0 → Bar) (motive_2 := fun _ => Foo) ?foo ?bar⟩
  case foo => intro b _ _; exact b
  case bar => intro f _; exact f

I am probably reading your sentence wrong?

Although I feel if the n in the first goal is "different" from the n in the second goal, in that it varies in the first but not the second, maybe you should be pushing the quantifier into the conjuncts for clarity?

I kind of agree with you here, but other times I am happy with hyper-efficient tactics that sacrifice some readability.

But maybe it would be a handy convenience, since I would be tempted to pull the Γ out.

Exactly.

In any case, the discussion further up this thread seemed to suggest that referring to goal names directly in a tactic is highly unusual behaviour, which is why I had changed my original proposal from explicitly using the goal names to simply listing the variables to induct on in goal order

It's unusual to refer to multiple goals at all, whether by names or by indices; from that POV perhaps a definition-level mutual theorem or theorems syntax is better. But if you are already doing it, IMO the more robust and readable syntax is preferrable.

[Joachim Breitner]

I should mention that Isabelle has had a support for mutual induction (including generalization separate sets of variables for each goal etc.) for years. I recommend to compare with their syntax and feature set, and if you diverge from how they handle things, then with a reason :-)

[Jonathan Chan]

To clarify this:

But you don't always need to quantify over every variable that the goal depends on

I have in my notes (the README) that for mutual induction, to compute the motive, you need to generalize over all transitive dependencies of the indices as well as dependencies of the goal within each context/conjunct. The first part makes sense to me, since they'll change with the indices, but I can't recall why this needs to be done for the goal too, I'll have to go back and look into my examples...

[Jonathan Chan]

After presenting some of this stuff to some people and hearing their comments, and also because it would be super useful to me personally, I've started back on implementing a joint theorem syntax as further above. I've implemented it just as a macro that turns something like this

joint (n : Nat)
  theorem evenInv (h : Even (n + 1)) : Odd n
  theorem oddInv  (h : Odd (n + 1) ) : Even n
by tac...

into this

def _evenInv_oddInv_ : Array ((A : Sort _) ×' A) := by
  refine
    #[⟨∀ (n : Nat) (h : Even (n + 1)), Odd n, λ (n : Nat) (h : Even (n + 1)) ↦ ?evenInv⟩,
      ⟨∀ (n : Nat) (h : Odd (n + 1)), Even n, λ (n : Nat) (h : Odd (n + 1)) ↦ ?oddInv⟩]
  tac...

theorem evenInv (n : Nat) (h : Even (n + 1)) : Odd n := _evenInv_oddInv_[0].snd
theorem oddInv (n : Nat) (h : Odd (n + 1)) : Even n := _evenInv_oddInv_[1].snd

It mostly works so far, but I have some cosmetic issues:

• If I have unsolved goals at tac, instead of a red squiggle under by like usual, the squiggle appears under joint
• Even though I use h in my proof in tac, it's greyed out as unused in the declaration (presumably since the tactics' h refers to the h in the lambda I introduced

How should I fix these issues? As an attempt at the first problem, I tried copying the SourceInfo for the original by into the info for the generated definition's by, but that just showed the proof state at the definition's by when my cursor is next to the original by, which isn't what I want

[Chris Henson]

I didn't realize from the talk that this was over Sort, that gives context to your question about coercing binders. In the case where all the declarations are in Prop, can anything be done differently that might help with the error reporting?

This command is independent of the mutual induction tactic, right? It would help to post it here or in a branch of your repo.

[Jonathan Chan]

I don't think it matters that the binders eventually need to have types that fit in Sort since the coercion is just coercing syntax, that was really about using forall-shaped binders as lambda-shaped binders
If ultimately it is a proof in Prop the level gets solved to Sort 0 = Prop anyway, and it shouldn't matter whether it's a proof or not since you should also be able to use by tactic mode to generate relevant terms

[Jonathan Chan]

The code so far for the macro is in the same repo here: https://github.com/ionathanch/MutualInduction/blob/main/Joint.lean

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I made a PR fixing some of these, with explanations as to what is caused by what. There are still some annoyingly duplicated 'Goals accomplished' messages.

[Jonathan Chan]

Thanks!

[Jonathan Chan]

I have a strange bug now: hovering over joint theorem names doesn't give me its type except when hovering over the very last one. so

joint
  theorem zero : True
  theorem one : True
  theorem two : True
by all_goals constructor

putting my cursor at zero and one don't give me their types, but at two does. In fact it's specifically the last definition returned here:

return mkNullNode (#[jointDef] ++ nthThms)

If I reverse nthThms, for instance, then only zero gets a type on hover.
How do I... begin to debug this? I've been printing out syntax ranges of a bunch of bits of syntax, but nothing stands out (they all have disjoint ranges, in particular).

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Have you tried copying the range of the tokens zero/one/two into the names of the generated theorems?

[Jonathan Chan]

I'm passing those tokens around directly to the generated theorems, so they're the exact same tokens there
I tried explicitly setting the canonical field in the SyntaxInfo of those pieces of syntax to true but that didn't change anything