nat_ceil

Stream: new members

[Iocta]

import data.real.basic

example : nat_ceil (1:real)  = (1:nat) :=
_

How to fill this?

[Shing Tak Lam]

Here's a solution, but I'm not sure if it's optimal

example : nat_ceil (1:real)  = (1:nat) :=
begin
  rw show (1 : ℝ) = ↑(1 : ℕ), by norm_num,
  rw nat_ceil_coe,
end

[Bryan Gin-ge Chen]

Here's another solution:

import data.real.basic

example : nat_ceil (1 : real) = (1 : nat) :=
begin
  convert nat_ceil_coe 1,
  rw [nat.cast_one],
end

[Bryan Gin-ge Chen]

Oh wait, this works:

example : nat_ceil (1 : real) = (1 : nat) :=
by rw [←nat.cast_one, nat_ceil_coe]

[Johan Commelin]

Can we write down a general statement for numerals? Doesn't seem to be trivial.

[Kenny Lau]

import data.real.basic

example : nat_ceil (1 : ℝ) = (1 : ℕ) :=
@nat.cast_one ℝ _ _ ▸ nat_ceil_coe 1

example : nat_ceil (1 : ℝ) = (1 : ℕ) :=
by exact_mod_cast @nat_ceil_coe ℝ _ _ 1

[Kenny Lau]

Johan Commelin said:

Can we write down a general statement for numerals? Doesn't seem to be trivial.

what do you mean?

[Jason Orendorff]

Johan Commelin said:

Can we write down a general statement for numerals? Doesn't seem to be trivial.

Isn't nat_ceil_coe that general statement? If you write nat_ceil_coe 5, the result is that nat_ceil (5 : ℝ) = 5.