Zulip Chat Archive

Stream: new members

Topic: Pattern matching in tactics


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 30 2021 at 19:22):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 30 2021 at 19:24):

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

view this post on Zulip Enrico Borba (Jan 30 2021 at 19:25):

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

view this post on Zulip 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?)

view this post on Zulip 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: May 14 2021 at 00:42 UTC