## Stream: new members

### Topic: Pattern matching in tactics

#### Enrico Borba (Jan 30 2021 at 19:06):

What's the proper way to use an anonymous constructor as a pattern-matching expression in a tactic proof? For example, I have p: ∃ (h: a ∈ A), a ∉ B, and when outside of a tactic context I can do let ⟨a, ha⟩ := p in .... I'd love to be able to do something like this inside of tactics. Right now what I usually do is

exact let ⟨a, ha⟩ := p in begin
...
end


which is kind of clunky.

Is there a better or more standard way to do this?

#### Kevin Buzzard (Jan 30 2021 at 19:07):

Does cases p with h1 h2work for you? I'm a bit unclear about whether you're constructing data or not.

#### Kevin Buzzard (Jan 30 2021 at 19:10):

example (X : Type) (A B : set X) (a : X) (p: ∃ (h: a ∈ A), a ∉ B) : false :=
begin
cases p with h1 h2,
/-
X : Type
A B : set X
a : X
h1 : a ∈ A
h2 : a ∉ B
-/
sorry
end


#### Kevin Buzzard (Jan 30 2021 at 19:11):

I am a bit confused about what you are calling a here. In your example you'd get a : a ∈ A. As well as cases there are the tactics tactic#rcases and tactic#obtain

#### Enrico Borba (Jan 30 2021 at 19:14):

This is what I was looking for I think. Sorry the example is pretty contrived, I was more asking about just destructing the existential quantifier into it's two parts. I'm a little confused why this works, but thanks again!

#### Kevin Buzzard (Jan 30 2021 at 19:14):

A proof of an existential quantifier is a pair of pieces of information, and cases just takes it apart into the two pieces.

#### Enrico Borba (Jan 30 2021 at 19:17):

I understand that yeah, but I thought that cases only works with inductively defined types, and I hadn't really considered existential quantification as an inductively defined type.

#### Enrico Borba (Jan 30 2021 at 19:18):

But I think I see now that it really only has one constructor, so no additional subgoals are created. As opposed to doing cases on a disjunction.

#### Mario Carneiro (Jan 30 2021 at 19:22):

obtain <a, ha> := p works inside tactics you know

#### Enrico Borba (Jan 30 2021 at 19:23):

obtain is exactly what I'm looking for, and is especially useful since it uses rcases, thanks for pointing that out, hadn't seen it before.

#### Mario Carneiro (Jan 30 2021 at 19:24):

I think it's strictly better than the let-match you have in term mode

#### Enrico Borba (Jan 30 2021 at 19:25):

Yeah, and reads better than cases/rcases. Thanks again

#### Patrick Massot (Jan 30 2021 at 19:39):

Enrico Borba said:

I understand that yeah, but I thought that cases only works with inductively defined types, and I hadn't really considered existential quantification as an inductively defined type.

You can ask Lean to show you the definition of exists. It's a bit shocking that forall is absolutely core builtin while exists is one of hundreds of inductive types. But that's how it is in dependent type theory. In real life you don't have to care about such foundational issues, just learn the relevant syntax and tactics (did you go through https://leanprover-community.github.io/learn.html?)

#### Mario Carneiro (Jan 30 2021 at 19:56):

By the way, in some approaches to DTT forall is a coinductive type (where application is the destructor and funext is the bisimulation theorem)

Last updated: Dec 20 2023 at 11:08 UTC