add_pos

Stream: new members

[Antoine Labelle]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Antoine Labelle]

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

[Kevin Buzzard]

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.

[Antoine Labelle]

Ok, thanks!

[Kevin Buzzard]

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.

[Kevin Buzzard]

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 :-)