migrating to dependent induction lemmas

Stream: mathlib4

[Jireh Loreaux]

Patrick Massot said:

Sure. But there is no point saying apply is bad and induction should be used if induction fails just as much. That’s why I stuck to apply which is simpler.

The above is from another thread. I've decided to finally fix this problem by migrating the existing foo_induction lemmas to their dependent counterparts so that they work correctly with the induction tactic.

I've started on this in #17543. However, before I continue by fixing the fallout and migrating similar lemmas, I would like some feedback. In particular are you happy with the way I've changed the Subsemigroup and Submonoid lemmas (note some changes to: argument order / implicitness / argument names)? I've checked that these all work correctly with the induction tactic.

When proving, e.g., closure_induction₂, do we prefer the compact refine style, or the structured induction version (the latter is included as a comment in the code)? Please let me know your thoughts at least @Eric Wieser , @Patrick Massot and @Heather Macbeth .

[Eric Wieser]

Jireh Loreaux said:

When proving, e.g., closure_induction₂, do we prefer the compact refine style, or the structured induction version (the latter is included as a comment in the code)?

I think standard golfing rules apply ("author's choice") for lemmas like this one. I'd maybe argue that closure_induction₂ shouldn't exist at all, since it really is just two inductions in the obvious way.

[Jireh Loreaux]

Eric Wieser said:

I'd maybe argue that closure_induction₂ shouldn't exist at all, since it really is just two inductions in the obvious way.

if you're in a situation where you need to do it enough times, you might change your mind :smiley:

[Patrick Massot]

Thanks Jireh! I like the structured versions.

[Jireh Loreaux]

Ready for review at #17543. I tried to keep the diff small (still 800 lines!) unless the structured versions provided more clarity.

[Jireh Loreaux]

On the PR @Bhavik Mehta suggests that we should keep the non-dependent versions around for two reasons:

1. to avoid need to give Lean the motive explicitly when proving a non-dependent version.
2. to avoid superfluous underscores which are just noise.

It seems that (1) is not really an issue (that is, there was essentially only one place this needed to occur, and it was actually reasonable). For (2), I considered making the dependent hypotheses implicit. That is, in the statement of, for example Submonoid.closure_induction, the mul hypothesis would look like:

theorem closure_induction {s : Set M} {p : (x : M) → x ∈ closure s → Prop}
    (mem : ∀ (x) (h : x ∈ s), p x (subset_closure h)) (one : p 1 (one_mem _))
    (mul : ∀ x {hx} y {hy}, p x hx → p y hy → p (x * y) (mul_mem hx hy)) {x} (hx : x ∈ closure s) :
    p x hx :=
  sorry

This would work reasonably well to avoid underscores when these arguments are superfluous, and it would greatly reduce the diff on this PR.

However, it seems there is one major drawback, and it has to do with the induction tactic itself. When you call the above lemma with induction, for example, to prove:

theorem dense_induction {p : M → Prop} (s : Set M) (closure : closure s = ⊤) (mem : ∀ x ∈ s, p x)
    (one : p 1) (mul : ∀ x y, p x → p y → p (x * y)) (x : M) : p x := by
  induction closure.symm ▸ mem_top x using closure_induction with
  | mem _ h => exact mem _ h
  | one => exact one
  | mul x y ihx ihy => exact mul x y ihx ihy

if you did (in the mul arm) for some reason want to access the hypotheses hx✝ : x ∈ Submonoid.closure s and hy✝ : y ∈ Submonoid.closure s, you would have to use rename_i (gross), as the syntax

  | mul x y {hx hy} ihx ihy => sorry

doesn't work. @Eric Wieser I'm interested in your thoughts here too.

[Bhavik Mehta]

Hmm I'm not sure it's worth it - in the cases that you do want access to those parts, this is super unpleasant...

[Jireh Loreaux]

I know, but I'm more wondering if we should ask core to change the induction tactic to allow for this. It would be nice if it didn't introduce all the variables as shadowed if you don't provide them anyway. I think there are a few rough edges around the induction tactic still.

[Jireh Loreaux]

(probably the same also applies to cases, but I haven't checked yet.)

[Jireh Loreaux]

:idea: I just found out about this syntax which allows access to naming implicit variables.

  | @mul x y hx hy ihxy ihy => sorry

[Jireh Loreaux]

Unfortunately, it doesn't work to prevent the introduction of the induction hypotheses via @mul => sorry, which is too bad.