casesm changed behaviour !4#1744

Stream: mathlib4

[Lukas Miaskiwskyi]

While porting Data.Sign (!4#1744), I have noticed that casesmdoes not seem to work as it did in lean 3, most importantly, it does not seem to act on the goal anymore, but only on hypotheses.

For example, proving le_total in instance : LinearOrder SignType of the PR above used to be

le_total a b := by casesm*_ <;> decide

In lean 4 however, neither casesm* (_ ∨ _) nor casesm* _ do anything to the goal ⊢ a ≤ b ∨ b ≤ a. But, as a silly example, if I move the goal into the hypotheses with by_contra h; rw [not_or] at h;, then casesm* (_ ∧ _) very happily acts on the new hypothesish: ¬a ≤ b ∧ ¬b ≤ a. Notably, casesm* _ still does not do anything.

Is this an intended change?

[David Renshaw]

I don't think casesm is supposed to act on the goal in Lean 3. https://github.com/leanprover-community/mathlib/blob/ed60ee25ed00d7a62a0d1e5808092e1324cee451/src/tactic/lean_core_docs.lean#L149-L164

cases_matching p applies the cases tactic to a hypothesis h : type
if type matches the pattern p.

[David Renshaw]

Do you have a #mwe where casesm works on the goal in Lean 3?

[Lukas Miaskiwskyi]

David Renshaw said:

Do you have a #mwe where casesm works on the goal in Lean 3?

Thanks for the response, constructing the #mwe made me see my misunderstanding: Neither in lean 3 nor in lean 4 does casesm act on the goal, but the difference is that in lean3, casesm _ recognizes that a and b are of inductive types and deconstructs them. In lean 4, not anymore.

In lean3:

inductive two_points
  | zero
  | one

namespace two_points
theorem mwe : ∀ (x : two_points), x = zero ∨ x = one := λ x, by casesm _; simp -- works
end two_points

In lean 4:

import Mathlib.Tactic.CasesM

inductive twoPoints
  | zero
  | one

namespace twoPoints
theorem mwe : ∀ (x : twoPoints), x = zero ∨ x = one := fun x ↦ by casesm _ <;> simp -- no match
end twoPoints

So the question is now: Is that intended?

[Lukas Miaskiwskyi]

Created an issue to not lose track of this: mathlib4#2018

One of these days I'll learn how to write tactics, then I won't be so helpless with these things :)