all rational numbers whose denominators are a power of 2

Stream: new members

[Lars Ericson]

I'm having trouble expressing "all rational numbers whose denominators are 1 or a power of 2". This is my first pass:

import data.rat.basic
import ring_theory.coprime
def binrat := {x : ℚ // ∃ (a : ℕ ) (b : ℕ ), b ≥ 0 ∧ (is_coprime a (2^b)) ∧  x = ⟨ a , 2^b ⟩ }

I'm getting error

type mismatch at application
  x = rat.mk' ↑a (2 ^ b)
term
  rat.mk' ↑a (2 ^ b)
has type
  0 < 2 ^ b → ↑a.nat_abs.coprime (2 ^ b) → ℚ
but is expected to have type
  ℚ

[Yakov Pechersky]

Why not

import data.rat.basic

def binrat := {x : ℚ // ∃ (p : ℕ), x.denom = 2 ^ p }

?

[Mario Carneiro]

Yeah, the author is being a bit silly there. Of course 1 is a power of 2

[Mario Carneiro]

@Lars Ericson That's maybe an example of what I was talking about earlier. The mathematician is writing for a human audience, which may not find it obvious that 1 is a power of 2 and so explicitly called it out. When formalizing, you definitely want to get rid of those junk disjuncts because they will only make the predicate harder to manipulate

[Johan Commelin]

@Lars Ericson rational numbers are not pairs of two natural numbers.