removing unprimed closure induction principles

Stream: mathlib4

[Eric Wieser]

The other thing we might want to do is delete lemmas like docs#Submodule.span_induction, as only the primed versions work with the induction keyword

[Jireh Loreaux]

Why would we delete them? Those lemmas are surely useful.

[Jireh Loreaux]

In fact, I bet they are likely the version used more often.

[Eric Wieser]

Only because in Lean3 neither version worked with induction (and the primed ones came much later)

[Eric Wieser]

My claims are:

• Now that we _can_ use induction x using foo, we should prefer it over refine foo x _ (fun _ _ _=> _) _ _ _
• The primed versions are strictly more general (syntactically) than the unprimed ones
• Only the primed versions work with induction, so with the spelling preference above there would never be a reason to use the unprimed ones

[Jireh Loreaux]

Except that if you have an unbundled x and a hypothesis hx : x ∈ ..., then you have to first lift x to ... using hx, right? Or does it just work as induction ⟨x, hx⟩ using foo (I suspect not)?

[Eric Wieser]

docs#Submodule.span_induction' doesn't take a subtype, but I think there are a few stray primed induction principles that do but shouldn't

[Eric Wieser]

I think you can just write induction hx using foo or maybe induction x, hx using foo

[Eric Wieser]

(I think whether you need x, depends on whether it was explicit in the induction principle)

[Notification Bot]

9 messages were moved here from #mathlib4 > Linter idea: h1 h2 hypotheses in induction by Eric Wieser.

[Jireh Loreaux]

oops, sorry! I didn't actually click on the docs link because I assumed I knew what it said! In that case I don't see any reason to preserve the unprimed versions.

[Eric Wieser]

Your comment was still helpful, it reminded me that there are some lemmas stated the way you expected

[Jireh Loreaux]

And yours was too, as I have a PR which adds the wrong version of some primed lemmas! :laughing:

[Jireh Loreaux]

@Eric Wieser do the correctly stated primed versions need @[elab_as_elim]?

[Eric Wieser]

Yes, but that's not sufficient to verify that they work unfortunately