match proof irrelevance

Stream: lean4

[Chris B]

Is there a way to get a match to simplify when it gets hung up on proofs? In the example below, I can't reduce the definition of bangStar to !, which I think is a result of it not recognizing that any (_ : 0 < 10) are definitionally equal. If I put another ⟨0, h'⟩ case first, I get a redundant alternative error, so apparently Lean does know (somewhere) that they're the same.

def bangStar : ∀ (f : Fin 10), Char
| ⟨0, _⟩ => '!'
| ⟨1, _⟩ => '!'
| _ => '*'

example : ∀ (a : Fin 10), bangStar a = '!' ∨ bangStar a = '*'
| ⟨0, _⟩ => by
  simp only [bangStar]
  _
| ⟨1, _⟩ => _
| _ => _

[Leonardo de Moura]

You can use the split tactic. It can split match and if-then-else expressions.

def bangStar : ∀ (f : Fin 10), Char
| 0 => '!'
| 1 => '!'
| _ => '*'

example : ∀ (a : Fin 10), bangStar a = '!' ∨ bangStar a = '*' := by
  intro a
  delta bangStar
  split <;> simp

[Chris B]

That's super useful, thank you. I'll try to come up with some good examples and add that to the tactic section of the manual unless you think split will change in the near future.

[Leonardo de Moura]

Thanks. We improve split in the future, but we do not expect any changes in the current functionality.