Dyadic numbers

Stream: maths

[Apurva Nakade]

I'm working on constructing dyadic surreals by first constructing dyadic rationals and then constructing a map from dyadic rationals to pre-games.
Below is the code I have so far. Just wanted to do a sanity check before I start proving theorems about them.
In particular, I couldn't find many examples of bundled objects in the library so I'm not entirely about the format.

import data.rat.basic
import data.nat.prime
import ring_theory.subring
import tactic.linarith

namespace rat

def is_dyadic (q : ℚ) : Prop := ∃ (m : ℤ) (n : ℕ), q.num = m ∧ q.denom = 2^n

lemma denom_pow_two_mul_denom_pow_two (m₁ m₂ : ℤ) (n₁ n₂ : ℕ) :
  ∃ k : ℕ, (rat.mk m₁ (2 ^ n₁) * rat.mk m₂ (2 ^ n₂)).denom = 2 ^ k :=
begin
  set x := rat.mk m₁ (2 ^ n₁) with hx,
  set y := rat.mk m₂ (2 ^ n₂) with hy,
  have : (x * y).denom ∣ 2 ^ (n₁ + n₂), by
  { calc (x * y).denom ∣ x.denom * y.denom : mul_denom_dvd _ _
                   ... ∣ x.denom * 2 ^ n₂
                       : begin
                           rw [mul_dvd_mul_iff_left (denom_ne_zero x), hy],
                           have := denom_dvd m₂ (2^n₂),
                           norm_cast,
                           norm_cast at this,
                           assumption,
                         end
                   ... ∣ 2 ^ n₁ * 2 ^ n₂
                       : begin
                           have := nat.one_le_two_pow n₂,
                           have htwo : 2 ^ n₂ ≠ 0, by linarith,
                           rw [mul_dvd_mul_iff_right htwo, hx],
                           have := denom_dvd m₁ (2 ^ n₁),
                           norm_cast,
                           norm_cast at this,
                           exact this,
                         end
                  ... = 2 ^ (n₁ + n₂) : (pow_add 2 n₁ n₂).symm },
  obtain ⟨k, ⟨_, hk⟩ ⟩ := (@nat.dvd_prime_pow _ nat.prime_two (n₁ + n₂) (x * y).denom).1 this,
  use [k, hk],
end

lemma denom_pow_two_add_denom_pow_two (m₁ m₂ : ℤ) (n₁ n₂ : ℕ) :
  ∃ k : ℕ, (rat.mk m₁ (2 ^ n₁) + rat.mk m₂ (2 ^ n₂)).denom = 2 ^ k :=
begin
  set x := rat.mk m₁ (2 ^ n₁) with hx,
  set y := rat.mk m₂ (2 ^ n₂) with hy,
  have : (x + y).denom ∣ 2 ^ (n₁ + n₂),
  { calc (x + y).denom ∣ x.denom * y.denom : add_denom_dvd _ _
                   ... ∣ x.denom * 2 ^ n₂
                       : begin
                           rw [mul_dvd_mul_iff_left (denom_ne_zero x), hy],
                           have := denom_dvd m₂ (2^n₂),
                           norm_cast,
                           norm_cast at this,
                           assumption,
                         end
                   ... ∣ 2 ^ n₁ * 2 ^ n₂
                       : begin
                           have := nat.one_le_two_pow n₂,
                           have htwo : 2 ^ n₂ ≠ 0, by linarith,
                           rw [mul_dvd_mul_iff_right htwo, hx],
                           have := denom_dvd m₁ (2 ^ n₁),
                           norm_cast,
                           norm_cast at this,
                           exact this,
                         end
                  ... = 2 ^ (n₁ + n₂) : (pow_add 2 n₁ n₂).symm },
  obtain ⟨k, ⟨_, hk⟩ ⟩ := (@nat.dvd_prime_pow _ nat.prime_two (n₁ + n₂) (x + y).denom).1 this,
  use [k, hk],
end

theorem dyadic.mul_mem (x y : ℚ) : x.is_dyadic → y.is_dyadic → (x * y).is_dyadic :=
begin
  rintros ⟨mx, ⟨nx, ⟨hmx, hnx⟩⟩⟩ ⟨my, ⟨ny, ⟨hmy, hny⟩⟩⟩,
  have hx : x = rat.mk x.num x.denom, from rat.num_denom.symm,
  have hy : y = rat.mk y.num y.denom, from rat.num_denom.symm,
  set q := rat.mk mx (2 ^ nx) * rat.mk my (2 ^ ny) with hq,
  have hq' : q = x * y, by { rw [hq, hx, hy, hmx, hnx, hmy, hny], simp },
  obtain ⟨k, hk⟩ := denom_pow_two_mul_denom_pow_two mx my nx ny,
  unfold is_dyadic,
  use [q.num, k],
  split,
  { rw ←hq' },
  { rw [←hq', hk] }
end

theorem dyadic.add_mem (x y : ℚ) : x.is_dyadic → y.is_dyadic → (x + y).is_dyadic :=
begin
  rintros ⟨mx, ⟨nx, ⟨hmx, hnx⟩⟩⟩ ⟨my, ⟨ny, ⟨hmy, hny⟩⟩⟩,
  have hx : x = rat.mk x.num x.denom, from num_denom.symm,
  have hy : y = rat.mk y.num y.denom, from num_denom.symm,
  set q := rat.mk mx (2 ^ nx) + rat.mk my (2 ^ ny) with hq,
  have hq' : q = x + y, by { rw [hq, hx, hy, hmx, hnx, hmy, hny], simp },
  obtain ⟨k, hk⟩ := denom_pow_two_add_denom_pow_two mx my nx ny,
  unfold is_dyadic,
  use [q.num, k],
  split,
  { rw ←hq' },
  { rw [←hq', hk] }
end

theorem dyadic.neg_mem (x : ℚ): x.is_dyadic → (-x).is_dyadic :=
begin
  rintros ⟨m, ⟨n, ⟨hm, hn⟩⟩⟩,
  unfold is_dyadic,
  use [-m, n],
  simp [hm, hn],
end

def dyadic : subring ℚ :=
{ carrier := { x : ℚ | x.is_dyadic },
  one_mem' := by { use 1, use 0, norm_num },
  mul_mem' := dyadic.mul_mem,
  zero_mem' := by { use 0, use 0, norm_num },
  add_mem' := dyadic.add_mem,
  neg_mem' := dyadic.neg_mem }

end rat

Any suggestions would be very helpful. Thanks!

[Kevin Buzzard]

Definition of is_dyadic: I don't think you need m!

[Apurva Nakade]

oh lol :rolling_on_the_floor_laughing: ofc

[Apurva Nakade]

Thanks!

[Kevin Buzzard]

                           norm_cast,
                           norm_cast at this,
                           assumption,

There's a tactic for that: assumption_mod_cast.

[Apurva Nakade]

Perfect!

[Kevin Buzzard]

Instead of use, use you can use a vector: one_mem' := by { use [1, 0], norm_num },. However often when you're using a vector you can get away with the pointy-bracket constructor, e.g. in your case you could do one_mem' := ⟨1, 0, by norm_num⟩,

[Apurva Nakade]

Fixed! Here's the slightly cleaner code:

import data.rat.basic
import data.nat.prime
import ring_theory.subring
import tactic.linarith

namespace rat

def is_dyadic (q : ℚ) : Prop := ∃ (n : ℕ), q.denom = 2^n

lemma denom_pow_two_mul_denom_pow_two (m₁ m₂ : ℤ) (n₁ n₂ : ℕ) :
  ∃ k : ℕ, (rat.mk m₁ (2 ^ n₁) * rat.mk m₂ (2 ^ n₂)).denom = 2 ^ k :=
begin
  set x := rat.mk m₁ (2 ^ n₁) with hx,
  set y := rat.mk m₂ (2 ^ n₂) with hy,
  have : (x * y).denom ∣ 2 ^ (n₁ + n₂), by
  { calc (x * y).denom ∣ x.denom * y.denom : mul_denom_dvd _ _
                   ... ∣ x.denom * 2 ^ n₂
                       : begin
                           rw [mul_dvd_mul_iff_left (denom_ne_zero x), hy],
                           have := denom_dvd m₂ (2^n₂),
                           assumption_mod_cast,
                         end
                   ... ∣ 2 ^ n₁ * 2 ^ n₂
                       : begin
                           have := nat.one_le_two_pow n₂,
                           have htwo : 2 ^ n₂ ≠ 0, by linarith,
                           rw [mul_dvd_mul_iff_right htwo, hx],
                           have := denom_dvd m₁ (2 ^ n₁),
                           assumption_mod_cast,
                         end
                  ... = 2 ^ (n₁ + n₂) : (pow_add 2 n₁ n₂).symm },
  obtain ⟨k, ⟨_, hk⟩ ⟩ := (@nat.dvd_prime_pow _ nat.prime_two (n₁ + n₂) (x * y).denom).1 this,
  use [k, hk],
end

lemma denom_pow_two_add_denom_pow_two (m₁ m₂ : ℤ) (n₁ n₂ : ℕ) :
  ∃ k : ℕ, (rat.mk m₁ (2 ^ n₁) + rat.mk m₂ (2 ^ n₂)).denom = 2 ^ k :=
begin
  set x := rat.mk m₁ (2 ^ n₁) with hx,
  set y := rat.mk m₂ (2 ^ n₂) with hy,
  have : (x + y).denom ∣ 2 ^ (n₁ + n₂),
  { calc (x + y).denom ∣ x.denom * y.denom : add_denom_dvd _ _
                   ... ∣ x.denom * 2 ^ n₂
                       : begin
                           rw [mul_dvd_mul_iff_left (denom_ne_zero x), hy],
                           have := denom_dvd m₂ (2^n₂),
                           assumption_mod_cast,
                         end
                   ... ∣ 2 ^ n₁ * 2 ^ n₂
                       : begin
                           have := nat.one_le_two_pow n₂,
                           have htwo : 2 ^ n₂ ≠ 0, by linarith,
                           rw [mul_dvd_mul_iff_right htwo, hx],
                           have := denom_dvd m₁ (2 ^ n₁),
                           assumption_mod_cast,
                         end
                  ... = 2 ^ (n₁ + n₂) : (pow_add 2 n₁ n₂).symm },
  obtain ⟨k, ⟨_, hk⟩ ⟩ := (@nat.dvd_prime_pow _ nat.prime_two (n₁ + n₂) (x + y).denom).1 this,
  use [k, hk],
end

theorem dyadic.mul_mem (x y : ℚ) : x.is_dyadic → y.is_dyadic → (x * y).is_dyadic :=
begin
  rintros ⟨nx, hnx⟩ ⟨ny, hny⟩,
  have hx : x = rat.mk x.num x.denom, from rat.num_denom.symm,
  have hy : y = rat.mk y.num y.denom, from rat.num_denom.symm,
  set q := rat.mk x.num (2 ^ nx) * rat.mk y.num (2 ^ ny) with hq,
  have hq' : q = x * y, by { rw [hx, hy, hnx, hny], assumption_mod_cast },
  obtain ⟨k, hk⟩ := denom_pow_two_mul_denom_pow_two x.num y.num nx ny,
  unfold is_dyadic,
  use k,
  rw [←hq', hk],
end

theorem dyadic.add_mem (x y : ℚ) : x.is_dyadic → y.is_dyadic → (x + y).is_dyadic :=
begin
  rintros ⟨nx, hnx⟩ ⟨ny, hny⟩,
  have hx : x = rat.mk x.num x.denom, from num_denom.symm,
  have hy : y = rat.mk y.num y.denom, from num_denom.symm,
  set q := rat.mk x.num (2 ^ nx) + rat.mk y.num (2 ^ ny) with hq,
  have hq' : q = x + y, by { rw [hx, hy, hnx, hny], assumption_mod_cast },
  obtain ⟨k, hk⟩ := denom_pow_two_add_denom_pow_two x.num y.num nx ny,
  unfold is_dyadic,
  use k,
  rw [←hq', hk],
end

theorem dyadic.neg_mem (x : ℚ): x.is_dyadic → (-x).is_dyadic :=
begin
  rintros ⟨n, hn⟩,
  unfold is_dyadic,
  use n,
  simp [hn],
end

def dyadic : subring ℚ :=
{ carrier := { x : ℚ | x.is_dyadic },
  one_mem' := ⟨0, by norm_num⟩,
  mul_mem' := dyadic.mul_mem,
  zero_mem' := ⟨0, by norm_num⟩,
  add_mem' := dyadic.add_mem,
  neg_mem' := dyadic.neg_mem }

end rat

[Eric Wieser]

Instead of dyadic.neg_mem, use is_dyadic.neg since then dot notation works

[Apurva Nakade]

I see, will do. I'm also curious about why all the variable names have ' on them like why one_mem' instead of one_mem'? :thinking:

[Kevin Buzzard]

Take a look at the difference between subring.one_mem and subring.one_mem'.

[Apurva Nakade]

Didn't realize subring.one_mem was a theorem too.
I see, so it "gets rid of the carrier" and identifies the subring s with s.carrier. Nice!

[Kevin Buzzard]

Exactly. The point is that you can't define the coercion before you define the structure, but when you define the structure you have to name the fields, so we put primes in the fields and then define the coercion later and then write the "preferred form" without the prime.

[Eric Wieser]

This also comes up with ring_hom.map_one / ring_hom.map_one'

[Kevin Buzzard]

@Apurva Nakade this slightly different approach, using mk_nat rather than mk, seems to make proofs shorter. I only did mul,but I am cautiously optimistic about add.

import data.rat.basic
import data.nat.prime
import ring_theory.subring
import tactic.linarith

namespace rat

def is_dyadic (q : ℚ) : Prop := ∃ (n : ℕ), q.denom = 2^n

theorem denom_dvd' (n : ℤ) (d : ℕ) : ((mk_nat n d).denom) ∣ d := by exact_mod_cast denom_dvd n d

theorem num_denom'' {a : ℚ} : mk_nat a.num a.denom = a := num_denom

lemma denom_pow_two_mul_denom_pow_two (m₁ m₂ : ℤ) (n₁ n₂ : ℕ) :
  ∃ k : ℕ, (rat.mk_nat m₁ (2 ^ n₁) * rat.mk_nat m₂ (2 ^ n₂)).denom = 2 ^ k :=
begin
  let x := rat.mk m₁ (2 ^ n₁ : ℕ),
  let y := rat.mk m₂ (2 ^ n₂ : ℕ),
  have : (x * y).denom ∣ 2 ^ (n₁ + n₂), by
  { calc (x * y).denom ∣ x.denom * y.denom : mul_denom_dvd _ _
                   ... ∣ x.denom * 2 ^ n₂ : mul_dvd_mul_left _ (denom_dvd' _ _)
                   ... ∣ 2 ^ n₁ * 2 ^ n₂ : mul_dvd_mul_right (denom_dvd' _ _) _
                   ... = 2 ^ (n₁ + n₂) : (pow_add 2 n₁ n₂).symm },
  obtain ⟨k, -, hk⟩ := (nat.dvd_prime_pow nat.prime_two).1 this,
  exact ⟨k, hk⟩,
end

theorem dyadic.mul_mem (x y : ℚ) : x.is_dyadic → y.is_dyadic → (x * y).is_dyadic :=
begin
  rintros ⟨nx, hnx⟩ ⟨ny, hny⟩,
  obtain ⟨k, hk⟩ := denom_pow_two_mul_denom_pow_two x.num y.num nx ny,
  use k,
  rwa [← hnx, ← hny, num_denom'', num_denom''] at hk,
end

end rat

[Apurva Nakade]

Works almost verbatim for add as well.
Thanks for these proofs. I'm always amazed at just how subtle this nat vs int issue is.

[Kevin Buzzard]

Yes. The shortened proofs came from me asking the question "what do I actually want the calc block in the proof of denom_pow_two_mul_denom_pow_two to look like?". We both saw that it didn't look like what we wanted it to look like. You worked around the issue by making the proof messier, but I am proposing keeping the proof looking nice and hence I am being forced to change the statement (you had (2 : int)^n before, which is hard to identify with (2 : nat)^n; you worked around it but I just removed int completely).

[Eric Wieser]

You can golf that a little further with docs#mul_dvd_mul

[Apurva Nakade]

I'm now trying to define a map from \int [2^{-1}] to the surreals. Sadly, because we don't have a ring structure on surreals, I cannot use the universal property of localization. My plan is to instead construct a map

def dyadic : localization (powers 2) →+ surreal := sorry

by hand. I am getting a bit stuck on defining maps out of powers 2. It is defined as a subtype and hence has an existential quantifier in it that I'm finding hard to eliminate. Here's an mwe:

import set_theory.surreal
import ring_theory.localization
import tactic

namespace surreal

def powers_half : ℕ → surreal := sorry

def powers_two : submonoid ℤ :=
{ carrier  := powers 2,
  one_mem' := powers.one_mem,
  mul_mem' := λ _ _, powers.mul_mem }

@[simp]
noncomputable def dyadic_mk : ℤ × powers_two → surreal :=
λ ⟨m, a, ha⟩, m • powers_half $ classical.some ha

@[simp]
theorem dyadic_mk' {m n} : dyadic_mk (m, ⟨2 ^ n, n, rfl⟩) = m • powers_half n :=
begin
  dsimp,
 sorry,
end
end surreal

I tried searching for examples of usage of classical.some_spec but am still not able to figure it out. I have a feeling that I'm not using classical.some properly.

Any suggestions on how to do this? Thanks,

[Yakov Pechersky]

One suggestion is to not use destructor notation in lambdas in a def

[Yakov Pechersky]

And use prod.fst, prod.snd, subtype.val, and subtype.prop

[Apurva Nakade]

Ah I see, I'll try this out. Ty,

[Yakov Pechersky]

If you have 0, 1, and addition defined for surreal, then you can use nat.cast for powers_half, I'm pretty sure

[Yakov Pechersky]

I think your proof should be just rfl

[Yaël Dillies]

Yeah, generally the wedges make defs quite opaque and hard to work with. i've learnt it to my expense!

[Kevin Buzzard]

I'm assuming we're sending n to $2^{-n}$ here so I'm not sure 0,1,+ is good enough!

[Apurva Nakade]

yeah, that's correct n \mapsto 2^{-n}.

[Apurva Nakade]

i have the necessary definitions and lemmas for 1/2 so that part shouldn't be a problem.

[Kevin Buzzard]

The proof can't be rfl because pure logic doesn't tell you that if there exists an x such that 2^x = n then this x is unique.

[Kevin Buzzard]

I'm not entirely clear about why we're introducing def powers_two but before going any further after making that definition, if this is the way you want to proceed, you should probably make an API for it which defines exp and log which biject it with nat, and use those functions instead of classical.some .

[Kevin Buzzard]

powers_two is just a highly inconvenient way of dealing with nat. You'd be better off working with nat directly at this point.

[Apurva Nakade]

I'm trying to get to def dyadic : localization (powers 2) →+ surreal := sorry

[Apurva Nakade]

I already have a proof that the rat.dyadic is the localization of \int away from 2.

[Kevin Buzzard]

Sure, but you have got stuck before localization (powers 2) comes into the picture.

[Kevin Buzzard]

No I take that back, I see your point. You're stuck precisely because you don't have the API.

[Kevin Buzzard]

So this is nothing to do with surreal, you just want to write down the equiv between powers_two and nat.

[Apurva Nakade]

Exactly, Yes!

[Apurva Nakade]

I'm just not able to prove anything about log : powers_two \to \nat :P

[Kevin Buzzard]

And you're using classical.some to write down one direction, and 2^n to write down the other, and your question is how to prove that these maps are inverse to each other.

[Yakov Pechersky]

Here's what I have so far

import set_theory.surreal
import ring_theory.localization
import tactic

namespace surreal

def powers_half : ℕ → surreal := sorry

def powers_two : submonoid ℤ := submonoid.powers 2

lemma mem_powers_iff {α : Type*} [monoid α] (z x : α) :
  x ∈ submonoid.powers z ↔ ∃ n : ℕ, z ^ n = x := iff.rfl

@[simp]
noncomputable def dyadic_mk : ℤ × powers_two → surreal :=
λ p, p.fst • powers_half (classical.some p.snd.prop)

@[simp]
theorem dyadic_mk' {m n} : dyadic_mk (m, ⟨2 ^ n, n, rfl⟩) = m • powers_half n :=
begin
  dsimp,
  generalize_proofs h,
  congr,
  simp only [powers_two, mem_powers_iff, subtype.coe_mk] at h,
  sorry
end

end surreal

[Apurva Nakade]

Kevin Buzzard said:

And you're using classical.some to write down one direction, and 2^n to write down the other, and your question is how to prove that these maps are inverse to each other.

Yes

[Apurva Nakade]

Yakov Pechersky said:

Here's what I have so far

import set_theory.surreal
import ring_theory.localization
import tactic

namespace surreal

def powers_half : ℕ → surreal := sorry

def powers_two : submonoid ℤ := submonoid.powers 2

lemma mem_powers_iff {α : Type*} [monoid α] (z x : α) :
  x ∈ submonoid.powers z ↔ ∃ n : ℕ, z ^ n = x := iff.rfl

@[simp]
noncomputable def dyadic_mk : ℤ × powers_two → surreal :=
λ p, p.fst • powers_half (classical.some p.snd.prop)

@[simp]
theorem dyadic_mk' {m n} : dyadic_mk (m, ⟨2 ^ n, n, rfl⟩) = m • powers_half n :=
begin
  dsimp,
  generalize_proofs h,
  congr,
  simp only [powers_two, mem_powers_iff, subtype.coe_mk] at h,
  sorry
end

end surreal

I know there are functions in nat.pow that'll prove this from here,
Thanks a lot!

[Apurva Nakade]

I'll make a better API for log : powers 2 \to \nat once I understand this proof.

[Apurva Nakade]

Wait, I feel like we must use classical.some_spec somewhere

[Yakov Pechersky]

There is no int.pow_right_injective afaict

[Yakov Pechersky]

@[simp]
theorem dyadic_mk' {m n} : dyadic_mk (m, ⟨2 ^ n, n, rfl⟩) = m • powers_half n :=
begin
  dsimp,
  generalize_proofs h,
  congr,
  simp only [powers_two, mem_powers_iff, subtype.coe_mk] at h,
  suffices : (2 : ℤ) ^ (classical.some h) = 2 ^ n,
  { sorry },
  { exact classical.some_spec h }
end

[Yakov Pechersky]

@[simp]
theorem dyadic_mk' {m n} : dyadic_mk (m, ⟨2 ^ n, n, rfl⟩) = m • powers_half n :=
begin
  dsimp,
  generalize_proofs h,
  congr,
  simp only [powers_two, mem_powers_iff, subtype.coe_mk] at h,
  suffices : (2 : ℤ) ^ (classical.some h) = 2 ^ n,
  { have h2 : (2 : ℤ) = (2 : ℕ) := rfl,
    simp_rw [h2, ←int.coe_nat_pow, int.coe_nat_inj'] at this,
    convert nat.pow_right_injective le_rfl this,
    ext m,
    simp_rw [h2, ←int.coe_nat_pow, int.coe_nat_inj'] },
  { exact classical.some_spec h }
end

[Yakov Pechersky]

There's probably some neater way to do this.

[Apurva Nakade]

Thanks a lot! All the coe_ suggest that I should work in the world of nat as long as I can before jumping to submonoid.powers 2.
I'll create more intermediate lemmas and break this proof down into smaller ones.

Also, I would never have known to use generalize_proofs h !!

[Yakov Pechersky]

This is just an example of what I think is a good rule of thumb, avoid explicit (not provided via a variable) proofs in lemma statements if you rely on the proof itself.

[Yakov Pechersky]

lemma int.exists_nat_eq_of_nonneg {x : ℤ} (h : 0 ≤ x) : ∃ (y : ℕ), (y : ℤ) = x :=
begin
  cases x,
  { simp },
  { refine absurd h _,
    simp },
end

lemma int.pow_right_injective {x : ℤ} (h : 2 ≤ x) : function.injective (λ (n : ℕ), x ^ n) :=
begin
  intros n m hnm,
  obtain ⟨y, rfl⟩ : ∃ (y : ℕ), (y : ℤ) = x := int.exists_nat_eq_of_nonneg ((zero_le_two).trans h),
  have : 2 ≤ y,
  { rw ←int.coe_nat_le,
    simpa using h },
  apply nat.pow_right_injective this,
  simpa [←int.coe_nat_pow, int.coe_nat_inj'] using hnm
end

@[simp]
theorem dyadic_mk' {m n} : dyadic_mk (m, ⟨2 ^ n, n, rfl⟩) = m • powers_half n :=
begin
  dsimp,
  generalize_proofs h,
  congr,
  simp only [powers_two, mem_powers_iff, subtype.coe_mk] at h,
  apply int.pow_right_injective le_rfl,
  simpa using classical.some_spec h
end

[Yakov Pechersky]

Of course, int.pow_right_injective isn't as general as it could be.

[Apurva Nakade]

Finally have a complete construction of a map rat.dyadic →+ surreals :D

import data.rat.basic
import data.nat.prime
import ring_theory.localization
import tactic
import set_theory.surreal

namespace surreal

-- already PRed this
def dyadic_map : localization (@submonoid.powers ℤ _ 2) →+ surreal := sorry

end surreal

namespace rat

def is_dyadic (q : ℚ) : Prop := ∃ (n : ℕ), q.denom = 2^n

-- TODO: move this data.rat.basic
theorem denom_dvd' (n : ℤ) (d : ℕ) : ((mk_nat n d).denom) ∣ d := by exact_mod_cast denom_dvd n d

-- TODO: move this data.rat.basic
theorem num_denom'' {a : ℚ} : mk_nat a.num a.denom = a := num_denom

-- TODO: move this data.rat.basic
lemma denom_pow_two_mul_denom_pow_two (m₁ m₂ : ℤ) (n₁ n₂ : ℕ) :
  ∃ k : ℕ, (mk_nat m₁ (2 ^ n₁) * mk_nat m₂ (2 ^ n₂)).denom = 2 ^ k :=
begin
  let x := mk m₁ (2 ^ n₁ : ℕ),
  let y := mk m₂ (2 ^ n₂ : ℕ),
  have : (x * y).denom ∣ 2 ^ (n₁ + n₂), by
  { calc (x * y).denom ∣ x.denom * y.denom : mul_denom_dvd _ _
                   ... ∣ 2 ^ n₁ * 2 ^ n₂   : mul_dvd_mul (denom_dvd' _ _) (denom_dvd' _ _)
                   ... = 2 ^ (n₁ + n₂)     : (pow_add 2 n₁ n₂).symm },
  obtain ⟨k, -, hk⟩ := (nat.dvd_prime_pow nat.prime_two).1 this,
  exact ⟨k, hk⟩,
end

-- TODO: move this data.rat.basic
lemma denom_pow_two_add_denom_pow_two (m₁ m₂ : ℤ) (n₁ n₂ : ℕ) :
  ∃ k : ℕ, (mk_nat m₁ (2 ^ n₁) + mk_nat m₂ (2 ^ n₂)).denom = 2 ^ k :=
begin
  let x := mk m₁ (2 ^ n₁ : ℕ),
  let y := mk m₂ (2 ^ n₂ : ℕ),
  have : (x + y).denom ∣ 2 ^ (n₁ + n₂), by
  { calc (x + y).denom ∣ x.denom * y.denom : add_denom_dvd _ _
                   ... ∣ 2 ^ n₁ * 2 ^ n₂   : mul_dvd_mul (denom_dvd' _ _) (denom_dvd' _ _)
                   ... = 2 ^ (n₁ + n₂)     : (pow_add 2 n₁ n₂).symm },
  obtain ⟨k, -, hk⟩ := (nat.dvd_prime_pow nat.prime_two).1 this,
  exact ⟨k, hk⟩,
end

theorem dyadic.mul (x y : ℚ) : x.is_dyadic → y.is_dyadic → (x * y).is_dyadic :=
begin
  rintros ⟨nx, hnx⟩ ⟨ny, hny⟩,
  obtain ⟨k, hk⟩ := denom_pow_two_mul_denom_pow_two x.num y.num nx ny,
  use k,
  rwa [← hnx, ← hny, num_denom'', num_denom''] at hk,
end

theorem dyadic.add (x y : ℚ) : x.is_dyadic → y.is_dyadic → (x + y).is_dyadic :=
begin
  rintros ⟨nx, hnx⟩ ⟨ny, hny⟩,
  obtain ⟨k, hk⟩ := denom_pow_two_add_denom_pow_two x.num y.num nx ny,
  use k,
  rwa [← hnx, ← hny, num_denom'', num_denom''] at hk,
end

theorem dyadic.neg (x : ℚ): x.is_dyadic → (-x).is_dyadic :=
λ ⟨n, hn⟩, ⟨n, by simp[hn]⟩

def dyadic : subring ℚ :=
{ carrier   := { x : ℚ | x.is_dyadic },
  one_mem'  := ⟨0, by norm_num⟩,
  mul_mem'  := dyadic.mul,
  zero_mem' := ⟨0, by norm_num⟩,
  add_mem'  := dyadic.add,
  neg_mem'  := dyadic.neg }

lemma dyadic.coe_eq_iff (a b : dyadic) : a = b ↔ a.val = b.val :=
by { simp only [set_like.coe_eq_coe, subtype.val_eq_coe] }

def int.localization_away_two_dyadic : localization_map.away_map 2 dyadic :=
{ to_fun         := λ n : ℤ, (n : dyadic),
  map_one'       := by norm_num,
  map_mul'       := by norm_num,
  map_zero'      := rfl,
  map_add'       := by norm_num,
  map_units'     := begin
                      rintro ⟨_, a, ha⟩,
                      rw is_unit_iff_exists_inv,
                      let b := mk' 1 (2^a) (pow_pos zero_lt_two a) (nat.coprime_one_left (2^a)),
                      use [b, a],
                      simp only [dyadic.coe_eq_iff, subring.coe_mul, subring.coe_one,
                                subring.coe_int_cast, subtype.coe_mk, subtype.val_eq_coe],
                      have : b = ((2 ^ a) : ℚ)⁻¹,
                        by { rw [eq_inv_iff, inv_def'],
                             simp only [nat.cast_bit0, int.cast_one, nat.cast_one,
                                        div_one, nat.cast_pow] },
                      rw [this, ← ha],
                      simp only [int.cast_pow, int.cast_bit0, int.cast_one],
                      refine rat.mul_inv_cancel _ _,
                      apply ne_of_gt,
                      simp only [zero_lt_bit0, pow_pos, zero_lt_one],
                    end,
  surj'          := begin
                      rintro ⟨a, b, h⟩,
                      use [a.num, 2 ^ b, b],
                      simp [dyadic.coe_eq_iff],
                      norm_cast,
                      rw [← h, mul_denom_eq_num],
                    end,
  eq_iff_exists' := begin
                      intros x y,
                      norm_cast,
                      split,
                      { intro hxy,
                        use 1,
                        simpa only [mul_one, submonoid.coe_one] },
                      { rintro ⟨⟨c, _, hc⟩, hxy⟩,
                        have : (c:ℤ) ≠ 0,
                          by { apply ne_of_gt, rw ← hc, apply pow_pos, dec_trivial },
                        exact mul_right_cancel' this hxy },
                    end }

noncomputable def dyadic_to_surreal : dyadic →+ surreal :=
add_monoid_hom.comp surreal.dyadic_map
  (localization.ring_equiv_of_quotient int.localization_away_two_dyadic).symm

end rat

[Eric Wieser]

A quick comment: dyadic.mul should be called is_dyadic.mul etc, for dot notation

[Eric Wieser]

And dyadic.coe_eq_coe is just docs#subtype.ext_iff_val

[Apurva Nakade]

I see, thanks. Will fix it!

[Apurva Nakade]

Ah, it's not of the form coe_..., that's why I couldn't find it.

[Eric Wieser]

You can also avoid needing val_eq_coe if you use subtype.ext_iff without the trailing _val

[Eric Wieser]

subtype.val usually shouldn't appear anywhere in a lemma, since coe is the preferred spelling

[Apurva Nakade]

Awesome, thanks!

[Apurva Nakade]

Those simps are just the outputs of squeeze_simps. I don't actually understand what's happening there and in the various norm_cast :P
Coercions are too CSy for me.