Rules for pattern matching in lambda expression

Stream: new members

[Martin C. Martin]

In

import data.set.lattice

variable {α : Type*}
variables (s t : set α)

example : ∀ x, x ∈ s ∪ s ∩ t → x ∈ s :=
λ x h, sorry

Is there a way to replace h with something to match the disjunction? I tried ⟨h, h'⟩ and ⟨h | h'⟩ but neither works. Is this because lambdas follow the rules for intros rather than rintros, i.e. they don't do recursive matching? Why not? In other words, why not allow recursive matching everywhere that non-recursive matching is allowed? Why have intros at all, and not just rintros?

[Kevin Buzzard]

(h | h'). I agree about rintros but you can't just change core lean!

[Mario Carneiro]

lambda does recursive matching, but it does not use the same syntax as rintro

[Mario Carneiro]

you have to use actual terms as patterns rather than this | stuff

[Martin C. Martin]

Good afternoon Kevin. That fails for me too. At the pipe it says invalid declaration, ')' expected.

import data.set.lattice

variable {α : Type*}
variables (s t : set α)

example : ∀ x, x ∈ s ∪ s ∩ t → x ∈ s :=
λ x (h | h'), sorry

[Mario Carneiro]

to write a pattern using | you should write it like

fun
| x, .inl h => sorry
| x, .inr h => sorry

or

fun | x, .inl h | x, .inr h => sorry

if both branches are the same

[Mario Carneiro]

the syntax Kevin is suggesting is by rintro x (h | h')

[Mario Carneiro]

oh this is lean 3

[Mario Carneiro]

in lean 3 there is no pattern matching syntax for lambda with multiple alternatives, you have to use

λ x h, match h with
| or.inl h := sorry
| or.inr h := sorry
end

[Mario Carneiro]

and in this case rintro (which is also available in lean 3) is the clear winner

[Martin C. Martin]

Thanks Mario!