# Zulip Chat Archive

## Stream: new members

### Topic: introducing variables

#### Ali Sever (Jul 19 2018 at 21:06):

If I have a Prop that says `∃ a b c, p`

, whats the quickest way of introducing a b c and p? In tactic mode, I have to use `cases`

three times to obtain all of them.

#### Mario Carneiro (Jul 19 2018 at 21:09):

mathlib has `rcases`

for this

#### Mario Carneiro (Jul 19 2018 at 21:09):

`rcases h with ⟨a, b, c, hp⟩`

#### Mario Carneiro (Jul 19 2018 at 21:10):

there is also `rintro`

for introducing and casing at the same time, `rintro ⟨a, b, c, hp⟩`

takes a goal of the form `(∃ a b c, p) -> q`

and splits off the parts and has `q`

as subgoal

#### Ali Sever (Jul 19 2018 at 21:12):

Is there a similar thing for term mode?

#### Mario Carneiro (Jul 19 2018 at 21:13):

`let ⟨a, b, c, hp⟩ := h in ...`

is the equivalent of `rcases`

and `λ ⟨a, b, c, hp⟩,`

is the equivalent of `rintro`

. Neither of those require mathlib

#### Ali Sever (Jul 21 2018 at 10:32):

I have `def col (a b c : point) : Prop := B a b c ∨ B b c a ∨ B c a b`

. I want to prove `col a b c ∧ (some other stuff) → col a' b' c'`

. Depending on the cases of `col a b c`

, all the proofs are the same. So can I name `{a, b, c} = {x, y, z}`

such that `B x y z`

is true. So that when I prove `B x' y' z'`

, I will have proven `col a' b' c'`

?

#### Mario Carneiro (Jul 21 2018 at 10:34):

what is the relation between `x',y',z'`

and `a',b',c'`

?

#### Mario Carneiro (Jul 21 2018 at 10:37):

One option is to prove as a lemma/`have`

something like `\forall x y z, B x y z ∧ (some other stuff) → B x' y' z'`

(where presumably `x'`

is a function of `x`

or something), and then instantiate it three times for the final proof

#### Ali Sever (Jul 21 2018 at 10:37):

I can prove `B a b c → B a' b' c'`

for any order of a,b and c. So if `x = a`

, `x' = a'`

.

#### Ali Sever (Jul 21 2018 at 10:38):

Ah, and then when I do cases, I can just use `lemma _ _ _`

and let lean guess the order.

#### Mario Carneiro (Jul 21 2018 at 10:39):

Depending on how often you need this, it might even be worth making a lemma to abstract this proof pattern

#### Mario Carneiro (Jul 21 2018 at 10:40):

By the way, from your two questions I have a pretty good idea what you are working on ;)

#### Patrick Massot (Jul 21 2018 at 11:20):

@Ali Sever Are you aware of http://geocoq.github.io/GeoCoq/?

#### Mario Carneiro (Jul 21 2018 at 11:20):

wow that's a nice project page

#### Patrick Massot (Jul 21 2018 at 11:25):

Yes, mathlib could use a webdesigner

#### Ali Sever (Jul 21 2018 at 11:27):

Yes, I looked around and I found out they were using the same book I was. I don't know exactly how Coq works, but when I get better at lean, I hope to write some interesting tactics.

#### Patrick Massot (Jul 21 2018 at 11:28):

But the message for Ali was rather more: beware that formalizing elementary geometry can be a lifetime project, especially because of the kind of symmetry issues that appeared in your question. See in particular https://hal.inria.fr/hal-00989781v2

Last updated: May 08 2021 at 09:11 UTC