cases vs match

Stream: new members

[Scott Godwin]

Hello, I'm starting out learning Lean and am confused in what difference there is in using cases vs match. I understand cases can only be used in tactic mode, but so can match. The few experiments I've done seem to suggest that they different in their pattern matching (cases can't seem to de-structure a record for instance). It seems to me that match is strictly more powerful than cases, when would I want to use the latter?

[Scott Godwin]

I also ran into a situation where just changing cases to match with no other changes got Lean to prove termination whereas it couldn't with cases which is a bit strange to me.

[Marcus Rossel]

I think one situation in which you can't use match is when you want to handle multiple/all cases at once without listing them explicitly. So for example, this doesn't work with match:

example (h : True ∨ True) : True := by
  cases h <;> assumption

Also, you have the option of not closing a branch's goal by using case':

example (h : True ∨ True) : True ∧ True := by
  cases h
  case' inl => constructor
  case' inr => constructor
  all_goals assumption