Is there or-elimination with match?

Stream: lean4

[Mark Wilhelm]

I see you can decompose an "exists" with a match, can you decompose an "or" with a match?

[Henrik Böving]

I'm assuming you are referring to just pattern matching on an expression of type or and yes we can indeed pattern match on them, in fact we can pattern match on anything inductive, for example the proof of commutativity of or can be done via pattern matching:

theorem or_comm (A B : Prop) : A ∨ B → B ∨ A
| Or.inl a => Or.inr a
| Or.inr b => Or.inl b

If it's an inductive you can match on it!

[Arthur Paulino]

You can use cases. If you have h : ... ∨ ...

cases h with
  | inl h' => ...
  | inr h' => ...

[Henrik Böving]

Yeah cases is basically the tactic variant of match

[Mark Wilhelm]

I'm getting "unknown identifier 'cases'" -- do I need any import for this?

[Henrik Böving]

Note that structure is just syntactic sugar around an inductive with one type so you can also match on it / use cases on it in a proof if you want to argue over the fields over some arbitrary structure.

Regarding the identifier, you need to be in tactic mode to use it:

theorem or_comm_alt (A B : Prop) : A ∨ B → B ∨ A := by
  intro h
  cases h with
  | inl a => exact Or.inr a
  | inr b => exact Or.inl b

[Mark Wilhelm]

still poking at it, but I think this is what I needed, thank you

[Simon Hudon]

@Mark Wilhelm Are you in a tactic block? Did you write by somewhere before cases?