Zulip Chat Archive

Stream: new members

Topic: floor of Real

Ralf Stephan (Jun 08 2024 at 18:25):

How can this be proved? My understanding is the floor returns a Z, still nothing works.

import Mathlib
set_option autoImplicit false

example : ⌊(3 : ℝ)⌋₊ = 3 := by sorry

Yaël Dillies (Jun 08 2024 at 18:27):

docs#Int.floor_intCast

Ralf Stephan (Jun 08 2024 at 18:31):

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
⌊↑?z⌋

Yaël Dillies (Jun 08 2024 at 18:31):

Don't rewrite!

Yaël Dillies (Jun 08 2024 at 18:31):

example : ⌊(3 : ℝ)⌋₊ = 3 := Int.floor_intCast 3

Ralf Stephan (Jun 08 2024 at 18:33):

~~Unexpected, thanks.~~

Ralf Stephan (Jun 08 2024 at 18:34):

Nope, does NOT work.

Yaël Dillies (Jun 08 2024 at 18:35):

You might have to do some norm_cast massaging

Bbbbbbbbba (Jun 08 2024 at 19:25):

example : ⌊(3 : ℝ)⌋₊ = 3 := Nat.floor_coe 3 is the one for natural numbers

Yaël Dillies (Jun 08 2024 at 19:28):

Whoops sorry I missed the ₊

Ralf Stephan (Jun 08 2024 at 20:56):

Nat.floor_coe is marked as simp but simp? "made no progress".

Ruben Van de Velde (Jun 08 2024 at 21:00):

Yeah, because this is not actually a cast, but an ofNat

Ralf Stephan (Jun 08 2024 at 21:01):

And two calls deep is too much for simp?

Ruben Van de Velde (Jun 08 2024 at 21:01):

I wonder why there isn't a parallel theorem about ofNat - probably historical reasons

Ruben Van de Velde (Jun 08 2024 at 21:01):

What do you mean by two calls?

Ralf Stephan (Jun 08 2024 at 21:02):

The ofNat after the floor.

Ralf Stephan (Jun 08 2024 at 21:03):

Of course they are not really called.

Ruben Van de Velde (Jun 08 2024 at 21:22):

No, this is the missing lemma:

import Mathlib
set_option autoImplicit false

@[simp]
theorem Nat.floor_ofNat {α : Type*} [LinearOrderedSemiring α] [FloorSemiring α] (n : ℕ) [n.AtLeastTwo] :
    ⌊no_index (OfNat.ofNat n : α)⌋₊ = n := by
  rw [← Nat.cast_eq_ofNat, Nat.floor_coe]

example : ⌊(3 : ℝ)⌋₊ = 3 := by
  simp