Casting Problem

Stream: new members

[Dan Stanescu]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Dan Stanescu]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

actually in this case norm_cast at H1 does fine

[Jalex Stark]

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

[Dan Stanescu]

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

[Dan Stanescu]

Thanks @Jalex Stark !

[Jalex Stark]

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