Zulip Chat Archive

Stream: new members

Topic: Casting Problem


view this post on Zulip Dan Stanescu (Jun 04 2020 at 13:43):

This example may be a little more verbose than needed, but is there a way to solve it?

import data.real.basic

example (N : ) (a : ) (ha: 0 < 1/a) (hN : N = nat_ceil ( (1:)/ a ) ) :
    0 < N :=
begin
    have H1 := lt_of_lt_of_le ha (le_nat_ceil ( (1:)/a )),
    rw  hN at H1,
    have H2 : N = N, norm_cast, rw H2,
    exact H1, -- fails
end

view this post on Zulip Jalex Stark (Jun 04 2020 at 13:44):

i haven't tried your code yet because I"m not at a computer, but I bet things will be easier for you if you use integers instead of naturals

view this post on Zulip Jalex Stark (Jun 04 2020 at 13:46):

I don't think H2 means what you want it to mean

view this post on Zulip Dan Stanescu (Jun 04 2020 at 13:47):

Yes but I just can't in this example. It's part of a bigger proof. I can bet you're right about H2.

view this post on Zulip Jalex Stark (Jun 04 2020 at 13:51):

this works

example (N : ) (a : ) (ha: 0 < 1/a) (hN : N = nat_ceil ( (1:)/ a ) ) :
    0 < N :=
begin
    have H1 := lt_of_lt_of_le ha (le_nat_ceil ( (1:)/a )),
    rw  hN at H1,
    revert H1, norm_cast,
    exact id
end

view this post on Zulip Jalex Stark (Jun 04 2020 at 13:52):

the only way I know to get norm_cast to do what i want is to put all the information it needs into the goal state

view this post on Zulip Jalex Stark (Jun 04 2020 at 13:55):

actually in this case norm_cast at H1 does fine

view this post on Zulip Jalex Stark (Jun 04 2020 at 13:56):

here's my final answer

example (N : ) (a : ) (ha: 0 < 1/a) (hN : N = nat_ceil ( (1:)/ a ) ) :
    0 < N :=
begin
    have := lt_of_lt_of_le ha (le_nat_ceil ( (1:)/a )),
    norm_cast at this, rwa hN,
end

view this post on Zulip Dan Stanescu (Jun 04 2020 at 14:00):

And I thought I had exhausted all ways to ask norm_cast to do the job!

view this post on Zulip Dan Stanescu (Jun 04 2020 at 14:00):

Thanks @Jalex Stark !

view this post on Zulip Jalex Stark (Jun 04 2020 at 14:01):

Jalex Stark said:

the only way I know to get norm_cast to do what i want is to put all the information it needs into the goal state

actually it's push_cast that I get this headache with. I think norm_cast always tries to remove coercions


Last updated: May 13 2021 at 16:25 UTC