split with h

[semorrison]

Proposal

Upgrade the split tactic so split with h names the new hypothesis.

Currently we need split <;> rename_i h as a workaround.

This syntax is available in Mathlib's split_if, but we would prefer not to upstream that implementation to Std.

Impact

Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

[semorrison]

(Implementations welcome.)

[leodemoura]

split with h works well for splitting if-then-elses. The split tactic can also perform case-analysis in match-expression. How would you name them?

[semorrison]

Perhaps like so:

example (n : Nat) : (match n with | 0 => 0 | _ => n+37) ≠ 1 := by
  -- split with m₁ | m₂ h
  split
  rename_i m₁
  rotate_left
  rename_i m₂ h
  rotate_left
  -- case h_1
  -- m₁: Nat
  -- ⊢ 0 ≠ 1
  -- case h_2
  -- n m₂: Nat
  -- h: n = 0 → False
  -- ⊢ n + 37 ≠ 1

This | syntax would then be similar to what rcases introduces for case splits.

Unfortunately it means a slight inconsistency with the if-then-else case, as we probably don't want to expect users to write split with h | h if they want to name both branches h.

[leodemoura]

Unfortunately it means a slight inconsistency with the if-then-else case, as we probably don't want to expect users to write split with h | h if they want to name both branches h.

Exactly. We can address it with documentation. I am happy with the RFC if there is consensus in the community this is a valuable feature. BTW, I am using structured proofs as an alternative for split with m₁ | m₂ h

split 
next m₁ => 
  ...
next m₂ h => 
  ...

[semorrison]

Unfortunately there's going to be a bit of inertia here, and Mathlib has its own split_ifs which is used almost to the exclusion of split there. I'd like to encourage changing that, and ideally eventually replace their split_ifs with the ecosystem-wide split.