nontrivial ℚ

Stream: new members

[Stuart Presnell]

In the following #mwe, why does apply nat.cast_pos.mpr generate a goal of nontrivial ℚ rather than filling this in automatically? If I instead use the first line apply (@nat.cast_pos ℚ _ _ p).mpr then Lean fills in nontrivial ℚ with no problem.

import data.rat.default

example (p : ℕ) (h : 1 < p) : 0 < (↑p:ℚ) :=
begin
  -- apply (@nat.cast_pos ℚ _ _ p).mpr,
  apply nat.cast_pos.mpr,
  apply lt_trans _ h,
  rw nat.lt_one_iff,
  exact rat.nontrivial,
end

[Mario Carneiro]

because it doesn't know that it's going to be about ℚ when it elaborates the term

[Mario Carneiro]

elaborating nat.cast_pos.mpr generates a side goal of nontrivial ?m

[Stuart Presnell]

But then how is Lean able to fill in the other hole ordered_semiring ℚ?

[Mario Carneiro]

It might be a little clearer to separate out that line into

  have := nat.cast_pos.mpr,
  apply this,

You will notice that the ordered_semiring Q also goes away in this version

[Mario Carneiro]

I think the reason is because it gets solved by unification, since rat.ordered_semiring appears in the statement of the have lemma

[Mario Carneiro]

Anyway, the way I would recommend to avoid this issue is to use refine instead of apply when you need the expected type:

  refine nat.cast_pos.mpr _,

[Mario Carneiro]

this does not generate any superfluous subgoals and does not require specifying Q

[Stuart Presnell]

Thanks!

[Stuart Presnell]

Great, and in fact I can just golf it down to exact nat.cast_pos.mpr (lt_trans one_pos h)

[Patrick Johnson]

Kevin pointed out that apply some_theorem.mp (or mpr) is unconventional:

Apply is not always the cleverest when it comes to type class inference.
You would be better off doing rw some_theorem

[Mario Carneiro]

what I usually do is append some_theorem.1 to the next thing to need this proof term

[Mario Carneiro]

or rw some_theorem if I'm already in a rewrite sequence

[Stuart Presnell]

If refine generally cleverer about type class inference than apply?

[Mario Carneiro]

More specifically, refine is told the expected type, so it has more information at its disposal

[Mario Carneiro]

apply can't because apply thm can mean refine thm or refine thm _ or refine thm _ _ ... and it needs to elaborate thm (without the type) to know which one it is (at which point it could provide the type, but it's too late for a lot of things)