Confused about induction tactics

Stream: new members

[Kevin Cheung]

There is a Lean 4 tactic induction and then Mathlib4 has two additional ones: induction' and induction''. For the Mathlib ones, when I went to the mathlib4 docs and revealed "Equations", I got the message "One or more equations did not get rendered due to their size." So I couldn't quite read more about them. How do all these induction tactics differ?

[Yaël Dillies]

You can always look at the source

[Yaël Dillies]

The main difference between them is the syntax

[Kevin Cheung]

So they're equally powerful?

[Kevin Cheung]

I took a look at the source code for induction'':

/- S -/ syntax (name := induction'') "induction''" casesTarget
  (fixingClause <|> generalizingClause)? (" with" (ppSpace colGt withPattern)+)? : tactic

It looks a bit cryptic to me. Do I need to learn metaprogramming in Lean 4 to figure out what this means?

[Ruben Van de Velde]

I've never heard of induction'' :sweat_smile:

[Ruben Van de Velde]

I don't know if there's any real documentation on the differences. induction' basically matches the syntax from lean 3, to make it easier to port existing code. I guess the main notable difference is that you can do induction' x with a b c d e to name things introduced in each of the new subgoals, and induction has a different syntax for that

[Kevin Cheung]

Let me be more specific then. The following is from Mathematics in Lean 4:

import Mathlib.Data.Nat.Prime
import Mathlib.Algebra.BigOperators.Order
import Mathlib.Tactic.Linarith

theorem exists_prime_factor {n : Nat} (h : 2 ≤ n) : ∃ p : Nat, p.Prime ∧ p ∣ n := by
  by_cases np : n.Prime
  · use n, np
  induction' n using Nat.strong_induction_on with n ih

If one opts for induction instead of induction', how should the last line be modified? When I removed ', Lean complained about n after with, saying "unknown tactic". So I suppose that's where the syntax differs since induction expects tactics after with. But is there a way to get things names with induction?

[Sébastien Gouëzel]

induction n using Nat.strong_induction_on with | h n ih => ?_

[Richard Copley]

It would be nice if there were a code action to fill in the case names and arguments, but I think you just have to look at the signature of Nat.strong_induction_on.

If the arguments for the cases are implicit you're out of luck (as far as I know), and in Mathlib they often are. See Finset.induction, for example. It's not usable with induction.

[Kevin Cheung]

Would you say that just use induction' whenever one is using Mathlib?

[Mauricio Collares]

I think there is a code action

Edit: There is a quick fix for induction n, but it disappears with using :(

[Kevin Cheung]

Pardon my ignorance. What is a "code action"?

[Richard Copley]

Kevin Cheung said:

Would you say that just use induction' whenever one is using Mathlib?

Some would say that. I prefer to use induction when possible.

[Kevin Cheung]

In the solution by Sébastien, what exactly is h n ih => ?_ doing?

[Sébastien Gouëzel]

Richard Copley said:

If the arguments for the cases are implicit you're out of luck (as far as I know), and in Mathlib they often are. See Finset.induction, for example. It's not usable with induction.

That's not correct, you just need to resort to the @ version. A quick grep gives me for instance

theorem Associated.prod {M : Type*} [CommMonoid M] {ι : Type*} (s : Finset ι) (f : ι → M)
    (g : ι → M) (h : ∀ i, i ∈ s → (f i) ~ᵤ (g i)) : (∏ i ∈ s, f i) ~ᵤ (∏ i ∈ s, g i) := by
  induction s using Finset.induction with
  | empty =>
    simp only [Finset.prod_empty]
    rfl
  | @insert j s hjs IH =>
    classical
    ...

[Richard Copley]

Right ... perhaps I should have guessed that. It only occurred to me to try {} syntax for implicit arguments (as in (fun {x} y => x * y : {x : ℕ} → (y : ℕ) → ℕ)).

Kevin Cheung said:

In the solution by Sébastien, what exactly is h n ih => ?_ doing?

It supplies the argument fun n ih => ?_ for the parameter h of Nat.strong_induction_on. I think Sébastien meant the ?_ placeholder informally; it's the place where you type your proof tactic block (usually starting on the next line, if it's multiline).

[Kevin Cheung]

Ah! It is starting to make sense. Thank you.

[Ruben Van de Velde]

Kevin Cheung said:

Would you say that just use induction' whenever one is using Mathlib?

No, there's currently no policy that would point in that direction

[Kevin Buzzard]

I would suggest the opposite: avoid any primed tactics, they might disappear one day, they were only there to help the port along and the port is now done.

[Kevin Cheung]

If that's the case, would we see an update to Mathematics in Lean in the near future? It uses induction' a lot.

[Kevin Cheung]

Maybe "a lot" is an exaggeration. It prefers it.

[Kevin Buzzard]

Note that MIL was an early adopter of Lean 4, which would explain the primed tactics there; I don't know if they plan on changing to unprimed. As you can see above there's a learning curve involved with the unprimed versions because you have to learn how to write 2d proofs (but that learning curve is definitely worth embarking on!). This is particularly problematic in the natural number game, where I uses cases' and don't really know how to switch to cases.

[Kevin Cheung]

Interesting situation.

[Kevin Buzzard]

Believe me, the port was a very interesting situation :-) In a parallel universe we're still doing it. It was an extraordinary achievement to get it done so quickly, but we still have a bunch of technical debt, e.g. the primed tactics.

[Patrick Massot]

I’m pretty sure we will end up getting rid of induction' in MIL. But indeed it would have been difficult initially.

[Eric Wieser]

Ruben Van de Velde said:

I've never heard of induction'' :sweat_smile:

I'm pretty sure it's for what was the induction' tactic in Lean 3, but we never ported it?

[Kevin Cheung]

I am not familiar with the term "2d proof". What does this mean in the context of Lean?

[Ruben Van de Velde]

I think it refers to the

induction x with
| case...
| case...

syntax

[Kevin Cheung]

I see.

[Kevin Cheung]

This doesn't seem to look worse than what induction' gives.

[Ruben Van de Velde]

I don't think so - it's just different if you have experience in lean 3

[Kevin Cheung]

I have zero experience in Lean 3. So I wasn't even aware of the primed tactics being ported from Lean 3. I was just starting from scratch with MIL.

[Kevin Buzzard]

Yeah. More precisely, in NNG I name the inductive hypotheses immediately and just get two goals, but I don't know how to do this with induction.