1/2 is not an integer

Stream: Is there code for X?

[Ruben Van de Velde]

Does anyone have a not stupid approach to this?

example : ∀ (x : ℤ), ¬(x : ℚ) = 1 * 2⁻¹ :=
begin
  admit,
end

(Stupid proof follows)

example : ∀ (x : ℤ), ¬(x : ℚ) = 1 * 2⁻¹ :=
begin
  intros x hx,
  norm_num at hx,
  apply_fun rat.denom at hx,
  rw rat.coe_int_denom at hx,
  have : (1 / 2 : ℚ) = ((1 : ℤ) / (2 : ℤ)), norm_num,
  rw this at hx,
  rw ←rat.mk_eq_div at hx,
  rw [rat.denom_mk, if_neg (@two_ne_zero ℤ _ _)] at hx,
  norm_num at hx,
end

[Yaël Dillies]

What about using docs#int.floor (or ceil or fract)? norm_num can calculate those.

[Junyan Xu]

slightly shorter:

import data.rat

example : ∀ (x : ℤ), ¬(x : ℚ) = 1 * 2⁻¹ :=
begin
  intro x,
  field_simp,
  norm_cast,
  intro h,
  replace h := dvd_of_mul_left_eq _ h,
  norm_num at h,
end

[Eric Rodriguez]

I think there's a proof embedded in https://github.com/leanprover-community/mathlib/blob/131c39a4f35bc8e8fdb93e832bacd585667ec919/src/number_theory/number_field.lean#L49

[Ruben Van de Velde]

Yaël Dillies said:

What about using docs#int.floor (or ceil or fract)? norm_num can calculate those.

Oh, good idea. I'd started thinking in the direction of a norm_num extension to calculate rat.denom, but using things that it already supports is easier

[Violeta Hernández]

I wonder if there is value in predicates like real.integral or real.rational

[Alex J. Best]

I think a norm_num extension for rat.denom would be independently useful. But there doesn't even seem to be too many lemmas about rat.denom so I think we have a fair bit to do here

[Mario Carneiro]

there isn't much needed. The hard part is proving that the numbers are coprime

[Heather Macbeth]

Not really recommending this, but:

example : ∀ (x : ℤ), ¬(x : ℚ) = 1 * 2⁻¹ :=
begin
  intros x hx,
  apply int.bit0_ne_bit1 x 0,
  apply @int.cast_injective ℚ,
  push_cast [bit0, bit1, hx],
  ring,
end

[Mario Carneiro]

a hack to make dec_trivial work:

example (x : ℤ) : ¬(x : ℚ) = 1 * 2⁻¹ :=
λ h, begin
  have := rat.coe_int_denom x,
  rw [h, one_mul, ← nat.cast_two] at this,
  revert this, dec_trivial
end

[Yakov Pechersky]

namespace rat

@[simp] lemma coe_int_inv_num (x : ℤ) : (x : ℚ)⁻¹.num = int.sign x :=
by simp [inv_def', div_num_denom, num_mk]

@[simp] lemma coe_int_inv_denom (x : ℤ) : (x : ℚ)⁻¹.denom = if x = 0 then 1 else x.nat_abs :=
by simp [inv_def', div_num_denom, denom_mk]

example : ∀ (x : ℤ), ¬(x : ℚ) = 1 * 2⁻¹ :=
begin
  intro,
  rw [one_mul, ←int.cast_two, rat.ext_iff, coe_int_inv_num, coe_int_inv_denom],
  norm_num
end

end rat

[Yakov Pechersky]

I guess that's similar to Ruben's original proof

[Alex J. Best]

@Yakov Pechersky nice, will you PR these lemmas? They seem useful! And go some of the way towards helping the lack of denom lemmas we have (in particular I think they would be useful in another project of mine :smile:)

[Ruben Van de Velde]

Ruben Van de Velde said:

Yaël Dillies said:

What about using docs#int.floor (or ceil or fract)? norm_num can calculate those.

Oh, good idea. I'd started thinking in the direction of a norm_num extension to calculate rat.denom, but using things that it already supports is easier

Trying this, I can't manage to make norm_num calculate with either fract or floor, unfortunately

[Damiano Testa]

You can also use that the units of ℤ are ±1 and then obfuscate everything:

example : ∀ (x : ℤ), ¬(x : ℚ) = 1 * 2⁻¹ :=
λ x h, have 1 = x * 2, from int.cast_inj.mp $ ((mul_inv_eq_iff_eq_mul₀
  (@two_pos ℚ _ _).ne').mp h.symm).trans $ by norm_cast,
by rcases int.is_unit_eq_one_or (is_unit_of_mul_eq_one x 2 this.symm) with rfl | rfl;
  linarith

[Yakov Pechersky]

#15863

[Violeta Hernández]

Yes, norm_num doesn't work with fract. If someone could make that work it would help me out with something I'm working with.

[Eric Wieser]

Done in #16502, but I don't think the version there makes sense to merge