casesm / constructorm on no match: error or not?

Stream: mathlib4

[David Renshaw]

casesm and constructor_matching/constructorm in mathlib4 are more forgiving when there is no match:

mathlib3:

example : true ∧ true :=
begin
  constructor_matching [_ ∨ _], -- error here. no match
  sorry
end

mathlib4:

example : True ∧ True := by
  constructorm (_ ∨ _) -- no error!
  constructorm (_ ∧ _) <;> exact True.intro

Is this what we want? I was tripped up by it while implementing tauto.

[Floris van Doorn]

No, tactics should generally not succeed if they didn't do anything.

[David Renshaw]

What about the * version of these tactics?
In mathlib3:

example : true ∧ true := begin
  constructor_matching* [_ ∨ _], -- no error
  constructor_matching [_ ∧ _]; exact true.intro,
end

[David Renshaw]

This makes sense to me -- the * means "zero or more times".

[Floris van Doorn]

No strong opinion here. We generally want a "one or more times" tactic inside a begin-end block. But a "zero or more times" tactic is useful to define other tactics.

[James Gallicchio]

Lean4 has the try tactic for 0 or 1 times, and repeat for zero or more times. Not sure if those existed in lean3 but they seem to cover most use cases nicely.

[Floris van Doorn]

yes, they also exist in Lean 3

[Kevin Buzzard]

It's confusing that simp in lean 4 succeeds if it does nothing

[David Renshaw]

casesm/constructorm issue fixed in https://github.com/leanprover-community/mathlib4/pull/1552

[Floris van Doorn]

just to clarify (because I was confused myself): this fixes the constructorm/casesm issue succeeding without progress, not simp succeeding without progress.