To replace `induction' h : f x`

Stream: lean4

[Jeremy Tan]

I want to add cases' and induction' to the technical debt counter at #21820, but @Eric Wieser is getting in the way by saying that removing induction' h : f x (which induction currently does not support) makes mathlib worse.

I am countering this by saying that that functionality should be added to plain induction, but I don't know how to do this myself.

[Edward van de Meent]

that aside, is there a reason why cases' should not be added?

[Edward van de Meent]

because i seem to recall that the cases h : x syntax does exist?

[Jeremy Tan]

rcases supports that syntax as well

[Jeremy Tan]

The point with cases' and induction' is that the variables you write after their withs are all on one line. When there are many inductors or many introduced variables per inductor it gets hard to tell which variable goes to which inductor

[Jeremy Tan]

induction, cases, rcases and obtain force you to separate the variables by inductor

[Eric Wieser]

Jeremy Tan said:

I am countering this by saying that that functionality should be added to plain induction

I agree with this suggestion; with the comment that we should wait for this to happen (or be firmly ruled against) before trying to clean up induction' h :s

[Eric Wieser]

cases' and other forms of induction' are indeed fair game to eliminate

[Floris van Doorn]

I agree with Eric that we should not be removing induction' h : f x until that functionality has been implemented in the induction tactic. Is there already a Lean RFC for this feature?

[Jeremy Tan]

File indicating all current uses of cases' and induction':

cases-induction-uses

[Jeremy Tan]

Floris van Doorn said:

I agree with Eric that we should not be removing induction' h : f x until that functionality has been implemented in the induction tactic. Is there already a Lean RFC for this feature?

I don't think so

[Kyle Miller]

I don't remember an RFC for it, and I didn't find one with a quick search.

I've been wanting to see induction h : f x syntax. In theory it shouldn't be hard since cases already has it and both tactics share the same framework.

[Chris Wong]

For posterity: What does induction' h : f x do?

[Jeremy Tan]

Chris Wong said:

For posterity: What does induction' h : f x do?

It inducts over f x, which is at the same time named h

[Jeremy Tan]

Currently plain induction can only induct over an existing variable

[Floris van Doorn]

It creates a new variable y and an equality h : f x = y (or h : y = f x, I don't recall) and then inducts on y.

[Jeremy Tan]

Can someone review my open depriming PRs

[Kevin Buzzard]

There are 1200 open PRs right now, I'm sure people will get to you in the end.

[Joachim Breitner]

Floris van Doorn said:

It creates a new variable y and an equality h : f x = y (or h : y = f x, I don't recall) and then inducts on y.

That’s essentially

generalize h : f x = y
induction y

right? Or maybe is it?

generalize h : f x = y
induction y generalizing x

I was just looking at the induction code in lean, and indeed the code paths between cases and `induction are quite similar.

(And the mathlib tactics prevented me from refactoring that module without breaking the mathlib builds, so getting rid of the primed tactics would be beneficial.)

[Jireh Loreaux]

Joachim, that's a chicken-or-egg problem: if we first remove the primed tactics, then we have to remove all the places they were used, but then we're losing the uses of the functionality you would be implementing in the induction tactic.

[Eric Wieser]

We can remove all the uses of cases' first

[Jireh Loreaux]

@Jeremy Tan if you want an action item, split off the part of your PRs that handle remove uses of cases'. These can be merged more easily.

[Jeremy Tan]

My computer is tied up right now training a text classifying model, but I'll get to that

[Jeremy Tan]

It still has 14 hours or so to go

[Kyle Miller]

I strongly suggest not depriming induction' at the moment. I've been wanting to implement the major premise naming feature for awhile, so assuming the feature will appear at some point, removing uses of induction' is unnecessary and ties up review time. Presence of induction' is not actively harmful (while @Joachim Breitner makes a good point about them appearing in mathlib makes changing induction harder, my thought here is that no matter what changes we make, we should deprecate induction' instead of outright removing it, so we're going to have to fix the mathlib tactic anyway).

[Joachim Breitner]

Jireh Loreaux said:

Joachim, that's a chicken-or-egg problem: if we first remove the primed tactics, then we have to remove all the places they were used, but then we're losing the uses of the functionality you would be implementing in the induction tactic.

Sorry, I wasn’t trying to imply that that having induction'code in mathlib would stop me or anyone from extending lean’s induction.

[Joachim Breitner]

Kyle Miller said:

I've been wanting to implement the major premise naming feature for awhile

Nice! Shouldn’t be hard.™
If you happen to do it soon, please wait for https://github.com/leanprover/lean4/pull/7069 to be merged or build on top of of it to avoid merge conflicts.

[Jeremy Tan]

@Kyle Miller the above PR has been merged

[Bhavik Mehta]

Joachim Breitner said:

Or maybe is it?

generalize h : f x = y
induction y generalizing x

I believe it's this one. I use this pattern quite often in practice, so I find this improvement to induction really valuable.

[Kyle Miller]

@Bhavik Mehta I checked induction', and it doesn't do that generalization:

example (xs : List Nat) : xs.length ≥ 0 := by
  induction' h : xs.length
/-
case zero
xs : List ℕ
h : xs.length = 0
⊢ 0 ≥ 0

case succ
xs : List ℕ
n✝ : ℕ
a✝ : xs.length = n✝ → n✝ ≥ 0
h : xs.length = n✝ + 1
⊢ n✝ + 1 ≥ 0
-/

I'm not sure having it generalize everything that the target depends on is something we'd want in general. That could potentially generalize the entire local context...

[Bhavik Mehta]

Oof, put that way I agree that could be pretty painful in general. As long as there's an option to generalise more (ie generalizing still works) I'm just as happy with the first of Joachim's suggestions

[Kyle Miller]

Great, since I think I have it working that way :-)

[Kyle Miller]

lean4#7103

(@Joachim Breitner I forgot to heed your advice, and there's definitely a merge conflict. I'll get to fixing that once I get mathlib building...)

[Kyle Miller]

I'm looking forward to fixing up generalize ... induction's in core. I've tested the feature on this one:

@[simp] theorem Array.forIn'_yield_eq_foldlM' [Monad m] [LawfulMonad m]
    (l : List α) (f : (a : α) → a ∈ l → β → m γ) (g : (a : α) → a ∈ l → β → γ → β) (init : β) :
    forIn' l init (fun a m b => (fun c => .yield (g a m b c)) <$> f a m b) =
      l.attach.foldlM (fun b ⟨a, m⟩ => g a m b <$> f a m b) init := by
  simp only [forIn'_eq_foldlM]
  induction h : l.attach generalizing init <;> simp_all

[Kyle Miller]

It's merged.

Part of the change was to modify how induction processes its targets, to follow how cases has already been doing it. It used to be that if any of the targets wasn't a free variable, it would generalize all of them indiscriminately — this causes free variables to become "detached" from any hypotheses about them that happen to be in the local context. Using multi-target induction principles is somewhat rare, so I'm not surprised that no one noticed.

The first theorem that ran into the issue was docs#natCast_eq_one, which uses a multi-target induction principle:

lemma natCast_eq_one {n : ℕ} (nezero : n ≠ 0) : (n : α) = 1 := by
  induction n, Nat.one_le_iff_ne_zero.mpr nezero using Nat.le_induction with
  | base => exact Nat.cast_one
  | succ x _ hx => rw [Nat.cast_add, hx, Nat.cast_one, add_idem 1]

The second target is Nat.one_le_iff_ne_zero.mpr nezero, which is not a free variable, so this causes induction to introduce a new variable n' that replaces n in the goal, and induction is done on that. This means the pre-existing nezero hypothesis (which is still in terms of n) isn't automatically added to the generalizing set, and so the induction hypothesis doesn't depend on proving nezero.

After the change, n is not generalized, so nezero does get added to the generalizing set, and the induction hypothesis has a surprising extra x ≠ 0 requirement, with nezero transformed to x + 1 ≠ 0.

Fixing it was straightforward: rewrite nezero in place. This way there's no lingering hypothesis in the context.

lemma natCast_eq_one {n : ℕ} (nezero : n ≠ 0) : (n : α) = 1 := by
  rw [← Nat.one_le_iff_ne_zero] at nezero
  induction n, nezero using Nat.le_induction with
  | base => exact Nat.cast_one
  | succ x _ hx => rw [Nat.cast_add, hx, Nat.cast_one, add_idem 1]

The only mathlib fixes needed were of this type, where some code golf had been done inside the induction targets.

[Ruben Van de Velde]

Yeah, those changes seem unproblematic

[Eric Wieser]

Kyle Miller said:

After the change, n is not generalized, so nezero does get added to the generalizing set, and the induction hypothesis has a surprising extra x ≠ 0 requirement, with nezero transformed to x + 1 ≠ 0.

I guess something like

induction n, Nat.one_le_iff_ne_zero.mpr (clear% nezero) using Nat.le_induction with

would work too, assuming clear% is possibly to implement?

[Kyle Miller]

Term elaboration can only locally affect the local context, which is some Reader state, so that's not possible.

[Ruben Van de Velde]

And if it was possible, I'm not sure I'd want to see it in mathlib :)

[Jireh Loreaux]

@Kyle Miller do I understand correctly that lean4#7103 addresses all of the existing issues with induction so that it is feature-complete with respect to induction'? And therefore the only remaining issue is whether we want to leave the syntax for induction' available / used in Mathlib?

[Kyle Miller]

Yeah, that's my understanding, though with the caveat that some people might want a more convenient-looking one-line induction than induction x with | c1 a b c => ?_ | c2 d e => ?_