Zulip Chat Archive

Stream: new members

Topic: add_pos


view this post on Zulip Antoine Labelle (Nov 25 2020 at 21:30):

Hi! I'm currently learning lean and I'm trying to figure out what is the problem with this tactic

have h₀ : 0 < 1 + exp a,
 {apply add_pos zero_lt_one exp_pos,}

Lean says

type mismatch at application
  add_pos zero_lt_one
term
  zero_lt_one
has type
  0 < 1
but is expected to have type
  0 < ?m_3

What does that mean?

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 21:31):

Can you post a #mwe, i.e. fully working code that we can just cut and paste?

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 21:32):

oh -- you could try exact add_pos zero_lt_one exp_pos,, that might do it.

view this post on Zulip Antoine Labelle (Nov 25 2020 at 21:34):

Thanks, exact works with (exp_pos a) instead of exp_pos. What was the problem with apply?

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 21:35):

Using exact is being a bit more friendly towards the unifier, saying "this is the whole proof". apply is supposed to guess a lot more about what's going on.

view this post on Zulip Antoine Labelle (Nov 25 2020 at 21:36):

Ok, thanks!

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 21:36):

apply isn't really the correct tactic to use here -- if h : P -> Q then apply h turns a goal of Q into a goal of P. That's apply's job. That's not what is happening in your proof.

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 21:36):

You're writing down the exact proof term here, so exact is the tactic to use. But apply does sometimes work in this situation, it's just a bit more hit-and-miss :-)


Last updated: May 18 2021 at 16:25 UTC