std4#243

Stream: PR reviews

[Scott Morrison]

I'm wondering if one of the authors (@Gabriel Ebner, @David Renshaw?) of Mathlib's split_ifs tactic could write a paragraph in the module doc explaining clearly the differences from the core tactic.

I'm happy if it's either a Mathlib PR, it gets added directly to the upstreaming PR at std4#243, or someone just posts something here and I'll incorporate it.

[David Renshaw]

Two differences that come to mind:

1. split only performs a single split at a time, while split_ifs splits all if-then-else expressions
2. split_ifs has an optional with clause that lets you name the new hypotheses. As far as I know, split does not support naming the new hypotheses.

[David Renshaw]

also: split_ifs is restricted to just if-then-else expressions, while split can act on other things too. (maybe any inductive type?)

[David Renshaw]

I'm trying to remember the reason for my comment

We opt not to use those library functions so that we can better mimic
the behavior of mathlib3's `split_ifs`.

[David Renshaw]

I think that maybe just has to do with putting splitIf1 in the TacticM monad rather than MetaM, so that the chaining behavior (andThenOnSubgoals) works out more conveniently.

[David Renshaw]

I do remember thinking "maybe someday these two tactics can be unified, but for now the priority is to expedite the porting effort".

[Eric Wieser]

I think split_ifs is also constructive unlike split