## Stream: new members

### Topic: builtin tactics

#### Olli (Sep 15 2018 at 13:00):

is there an even simpler way to write { left, assumption} <|> { right, assumption } ?

#### Kenny Lau (Sep 15 2018 at 13:04):

simp*

thanks

#### Olli (Sep 15 2018 at 13:30):

is there a way to do pattern matching in tactic mode?

#### Olli (Sep 15 2018 at 13:32):

if there was I would think it'd be with the let tactic, but I can't seem to get it to work

rcases

#### Olli (Sep 15 2018 at 19:19):

how come I can't just repeat constructor here:

example {p q} : ¬(p ∨ q) → ¬p ∧ ¬q :=
begin
intro h,
constructor;
intro hpq;
apply h,
constructor, assumption,
constructor, assumption
-- Doesn't work because before assumption state is:
-- p q : Prop,
-- h : ¬(p ∨ q),
-- hpq : q
-- ⊢ p
end


but yet this works:

example {p q} : ¬(p ∨ q) → ¬p ∧ ¬q :=
begin
intro h,
constructor;
intro hpq;
apply h,
constructor, assumption,
apply or.inr hpq
end


#### Kenny Lau (Sep 15 2018 at 19:21):

Lean can't possibly know which constructor to use

#### Olli (Sep 15 2018 at 19:22):

hmm I see, I was originally trying to write it as repeat { constructor, assumption }, but yeah I think I understand how this is ambigious

#### Kevin Buzzard (Sep 15 2018 at 20:28):

Some symmetries in maths are lost in computer science. Or and And are different types of things. And only has one constructor (to prove and p q you have to supply both a proof of p and a proof of q all in one go) but Or has two (to prove or p q you have two choices). If you look at the definitions as inductive types by right clicking on and or or in a working Lean session and peeking at the definition you will see this. For inductive types with one constructor like and or subtype or group the constructor tactic does a predictable thing. For types like or with more than one constructor the tactic just, I think, chooses the first one, so for or I think constructor does the same as left.

#### Olli (Sep 15 2018 at 20:43):

yeah it's probably a good idea to avoid using constructor with types having more than one constructor then?

so far my strategy for solving these exercises has been just staring at the tactic state while trying to make progress and not giving too much thought to what is happening in the bigger picture, and this is working surprisingly well, but there are some traps like this that lead to dead-ends

#### Mario Carneiro (Sep 15 2018 at 20:48):

you can use constructor as long as only one of the constructors is applicable

Last updated: May 13 2021 at 21:12 UTC