Zulip Chat Archive

Stream: new members

Topic: builtin tactics


view this post on Zulip Olli (Sep 15 2018 at 13:00):

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

view this post on Zulip Kenny Lau (Sep 15 2018 at 13:04):

simp*

view this post on Zulip Olli (Sep 15 2018 at 13:07):

thanks

view this post on Zulip Olli (Sep 15 2018 at 13:30):

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

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

view this post on Zulip Chris Hughes (Sep 15 2018 at 13:36):

rcases

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

view this post on Zulip Kenny Lau (Sep 15 2018 at 19:21):

Lean can't possibly know which constructor to use

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

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

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

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