Pattern matching in tactics

Stream: new members

[Enrico Borba]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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

[Enrico Borba]

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]

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

[Enrico Borba]

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

[Patrick Massot]

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]

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