Zulip Chat Archive

Stream: new members

Topic: cases vs match

Scott Godwin (Apr 29 2023 at 01:58):

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 (Apr 29 2023 at 01:59):

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 (Apr 29 2023 at 07:58):

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

Last updated: Dec 20 2023 at 11:08 UTC