Zulip Chat Archive

Stream: new members

Topic: all rational numbers whose denominators are a power of 2


view this post on Zulip Lars Ericson (Dec 24 2020 at 04:15):

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
  

view this post on Zulip Yakov Pechersky (Dec 24 2020 at 04:35):

Why not

import data.rat.basic

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

?

view this post on Zulip Mario Carneiro (Dec 24 2020 at 06:21):

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

view this post on Zulip Mario Carneiro (Dec 24 2020 at 06:23):

@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

view this post on Zulip Johan Commelin (Dec 24 2020 at 06:24):

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


Last updated: May 10 2021 at 23:11 UTC