Integer is not one half

Stream: Is there code for X?

[Aaron Liu]

Is there a quick way to prove this? I know I can multiply both sides by two, convert to equality in the integers, and then argue that the lhs is even but the rhs is odd. However, this seems like a bit much just for such a simple-seeming fact.

import Mathlib

example (x : ℤ) : (x : ℝ) ≠ 2⁻¹ := by
  sorry

[Aaron Liu]

If you can make it work for an arbitrary denominator d in a division ring with characteristic not dividing d that would be great too

[Damiano Testa]

example (x : ℤ) : (x : ℝ) ≠ 2⁻¹ := by
  rw [ne_eq, ← mul_one 2⁻¹, eq_inv_mul_iff_mul_eq₀ two_ne_zero]
  norm_cast
  omega

[Damiano Testa]

Oh, I had not read that this is what you already had tried! :man_facepalming:

[Aaron Liu]

That's three whole lines, I was hoping for something shorter. Thanks anyways!

[Damiano Testa]

There should be a lemma that says that an integers that is less than 1 in absolute value is zero.

[Damiano Testa]

docs#Int.abs_lt_one_iff I am not sure if it can be useful here.

[Kenny Lau]

my gut says you should prove that it's between 0 and 1 (by norm_num), and that should give you a contradiction

[Kenny Lau]

(and if it doesn't work, then that means we're missing lemmas)

[Robin Arnez]

example (x : ℤ) : (x : ℝ) ≠ 2⁻¹ := by
  apply_fun (fun x : ℝ => ⌊x⌋ - x)
  norm_num

[Ruben Van de Velde]

I would suggest apply_fun Int.fract, but norm_num doesn't support that

[Kyle Miller]

Another option:

example (x : ℤ) : (x : ℝ) ≠ 2⁻¹ := by
  field_simp; norm_cast; omega

[Kenny Lau]

We really don't have the lemma I said? (there is no integer between n and n+1)

[Ruben Van de Velde]

How would you state it?

[Kenny Lau]

import Mathlib

theorem Int.cast_ne_inv_two (x : ℤ) : (x : ℝ) ≠ 2⁻¹ := by
  intro hx
  have cast_x_pos : 0 < (x : ℝ) := by rw [hx]; norm_num
  have x_pos : 0 < x := by assumption_mod_cast
  rw [Int.lt_iff_add_one_le] at x_pos
  have one_le_x : (1 : ℝ) ≤ x := by assumption_mod_cast
  rw [hx] at one_le_x
  norm_num at one_le_x

[Kenny Lau]

this is close to the proof i stated

[Aaron Liu]

the point is to make it short

[Ruben Van de Velde]

example (x : ℤ) : (x : ℝ) ≠ 2⁻¹ := by
  apply Int.cast_mono.ne_of_lt_of_lt_int 0 <;> norm_num

[Kenny Lau]

import Mathlib

#check Nat.le_and_le_add_one_iff -- note that the theorem exists for `ℕ`

theorem Int.le_and_le_add_one_iff {n m : ℤ} : n ≤ m ∧ m ≤ n + 1 ↔ m = n ∨ m = n + 1 := by omega

theorem Int.not_lt_and_lt_add_one {n m : ℤ} : ¬(n < m ∧ m < n + 1) := by omega

theorem Int.cast_ne_inv_two (x : ℤ) : (x : ℝ) ≠ 2⁻¹ :=
  fun hx ↦ Int.not_lt_and_lt_add_one (n := 0) (m := x)
    (by rw [← Int.cast_lt (R := ℝ), hx, ← Int.cast_lt (R := ℝ), hx]; norm_num)
  -- rw_mod_cast was a bit weak there

This is the proof I had in mind

[Kenny Lau]

if only i could use rw_mod_cast

[Kenny Lau]

ah nice @Ruben Van de Velde you chained two theorems to get the one I wanted

[Kenny Lau]

do we think rw_mod_cast should cover this usecase btw?

[Kenny Lau]

import Mathlib

theorem Int.cast_ne_inv_two (x : ℤ) : (x : ℝ) ≠ 2⁻¹ := by
  refine (mul_left_inj' Real.pi_ne_zero).ne.1 (Real.sin_ne_zero_iff.1 ?_ x)
  rw [inv_mul_eq_div, Real.sin_pi_div_two]; simp

[Kenny Lau]

we should really have computable reals, then we can just decide everything :melt:

[Kenny Lau]

like now the proof I want is to convert this to a statement in Q, and then decide it

[Kenny Lau]

... we have Rat.isInt : ℚ -> Bool but not the proof that it actually does what it says

[Aaron Liu]

What about docs#Rat.eq_num_of_isInt

[Aaron Liu]

I guess we don't have the reverse direction

[Aaron Liu]

But the reverse direction is also just rfl

[Kenny Lau]

oh wait there is some CanLift stuff just below

[Kenny Lau]

import Mathlib

theorem Rat.isInt_iff (q : ℚ) : q.isInt ↔ ∃ x : ℤ, x = q :=
  ⟨fun h ↦ Rat.canLift.prf _ (eq_of_beq h), fun ⟨_, hn⟩ ↦ hn ▸ rfl⟩

theorem Int.cast_ne_inv_two (x : ℤ) : (x : ℝ) ≠ 2⁻¹ := by
  rw [show (2⁻¹ : ℝ) = (2⁻¹ : ℚ) by simp]
  intro h
  exact Ne.elim (by decide) ((Rat.isInt_iff (2⁻¹)).2 ⟨x, by exact_mod_cast h⟩)
  -- doesn't work

Why does this decide not work??

[Aaron Liu]

Is Rat.inv irreducible?

[Kenny Lau]

ok +kernel works then

import Mathlib

theorem Rat.isInt_iff (q : ℚ) : q.isInt ↔ ∃ x : ℤ, x = q :=
  ⟨fun h ↦ Rat.canLift.prf _ (eq_of_beq h), fun ⟨_, hn⟩ ↦ hn ▸ rfl⟩

theorem Int.cast_ne_inv_two (x : ℤ) : (x : ℝ) ≠ 2⁻¹ := by
  rw [show (2⁻¹ : ℝ) = (2⁻¹ : ℚ) by simp]
  intro h
  exact Ne.elim (by decide +kernel) ((Rat.isInt_iff (2⁻¹)).2 ⟨x, by exact_mod_cast h⟩)

[Kenny Lau]

also I wish the mod_cast stuff was more powerful so that I can omit the first rw lol

[Kenny Lau]

import Mathlib

theorem Rat.isInt_iff (q : ℚ) : q.isInt ↔ ∃ x : ℤ, x = q :=
  ⟨fun h ↦ Rat.canLift.prf _ (eq_of_beq h), fun ⟨_, hn⟩ ↦ hn ▸ rfl⟩

instance (q : ℚ) : Decidable (∃ x : ℤ, x = q) :=
  decidable_of_decidable_of_iff q.isInt_iff

theorem Int.cast_ne_inv_two (x : ℤ) : (x : ℝ) ≠ 2⁻¹ := by
  rw [show (2⁻¹ : ℝ) = (2⁻¹ : ℚ) by simp]
  norm_cast; revert x; rw [← not_exists]; decide +kernel

[Aaron Liu]

Why Rat.canLift.prf?

[Kenny Lau]

idk how else to do it

[Aaron Liu]

We have Rat.eq_num_of_isInt

[Kenny Lau]

that works too, but is not really shorter

[Aaron Liu]

I guess that's true

[Kenny Lau]

import Mathlib

theorem Rat.isInt_iff (q : ℚ) : q.isInt ↔ ∃ x : ℤ, x = q :=
  ⟨fun h ↦ ⟨_, (eq_num_of_isInt h).symm⟩, fun ⟨_, hn⟩ ↦ hn ▸ rfl⟩

instance (q : ℚ) : Decidable (∃ x : ℤ, x = q) :=
  decidable_of_decidable_of_iff q.isInt_iff

instance (q : ℚ) : Decidable (∀ x : ℤ, (x : ℚ) ≠ q) :=
  decidable_of_decidable_of_iff not_exists

theorem Int.cast_ne_inv_two (x : ℤ) : (x : ℝ) ≠ 2⁻¹ := by
  rw [show (2⁻¹ : ℝ) = (2⁻¹ : ℚ) by simp]
  norm_cast; decide +revert +kernel

[Yaël Dillies]

My gut feeling is to reduce your statement to Int.fract ... != 0 and run norm_num

[Ruben Van de Velde]

Ruben Van de Velde said:

I would suggest apply_fun Int.fract, but norm_num doesn't support that

[Ruben Van de Velde]

I tried to add support by blindly copy/pasting code around, but somehow it didn't really work

[Eric Wieser]

At one point this was on my to-do list

[Eric Wieser]

Maybe make a draft PR with what you have?

[Ruben Van de Velde]

Eric Wieser said:

Maybe make a draft PR with what you have?

#26428