Zulip Chat Archive

Stream: new members

Topic: nontrivial ℚ


Stuart Presnell (Jan 20 2022 at 13:37):

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 (Jan 20 2022 at 13:40):

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

Mario Carneiro (Jan 20 2022 at 13:41):

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

Stuart Presnell (Jan 20 2022 at 13:41):

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

Mario Carneiro (Jan 20 2022 at 13:45):

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 (Jan 20 2022 at 13:47):

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 (Jan 20 2022 at 13:50):

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 (Jan 20 2022 at 13:50):

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

Stuart Presnell (Jan 20 2022 at 13:51):

Thanks!

Stuart Presnell (Jan 20 2022 at 13:53):

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

Patrick Johnson (Jan 20 2022 at 13:57):

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 (Jan 20 2022 at 13:59):

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

Mario Carneiro (Jan 20 2022 at 14:00):

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

Stuart Presnell (Jan 20 2022 at 14:00):

If refine generally cleverer about type class inference than apply?

Mario Carneiro (Jan 20 2022 at 14:00):

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

Mario Carneiro (Jan 20 2022 at 14:01):

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)


Last updated: Dec 20 2023 at 11:08 UTC