Zulip Chat Archive

Stream: new members

Topic: Lifting results


view this post on Zulip Eric Astor (Feb 15 2021 at 05:10):

I'm not sure how to lift results across a cast. For example, if I have n : ℕ and want to establish the goal 0 ≤ (n : ℝ), how can I prove it? I know zero_le n : 0 ≤ n, but I'm not sure how to establish this 0 ≤ ↑n.

view this post on Zulip Damiano Testa (Feb 15 2021 at 05:26):

There are a lot of norm_num type results that can do this. In this case, norm_num works, but is a little slow, and library_search also works.

lemma nat_to_real_nonneg {n : } : (0 : )  n :=
begin
  --library_search finds this
  exact nat.cast_nonneg n,
end

view this post on Zulip Johan Commelin (Feb 15 2021 at 05:40):

Another useful lemma is norm_cast. It will try to remove as many \u up-arrows as it can.

view this post on Zulip Mario Carneiro (Feb 15 2021 at 05:46):

I don't think norm_num knows anything about this, you are probably seeing the result of simp

view this post on Zulip Mario Carneiro (Feb 15 2021 at 05:47):

but this sort of thing is generally norm_cast's job


Last updated: May 13 2021 at 06:15 UTC