Zulip Chat Archive

Stream: Is there code for X?

Topic: Power of two

Yaël Dillies (Mar 08 2022 at 00:21):

How can I state that a natural is a power of two? For context, I'm defining Sharkovskii's ordering of the natural numbers.

Eric Wieser (Mar 08 2022 at 00:23):

Membership in docs#submonoid.powers?

Yaël Dillies (Mar 08 2022 at 00:23):

Sounds pretty remote to me.

Eric Wieser (Mar 08 2022 at 00:24):

n ∈ submonoid.powers (2 : ℕ)

Yaël Dillies (Mar 08 2022 at 00:24):

This is likely going to be noncomputable, I presume?

Eric Wieser (Mar 08 2022 at 00:24):

It's a Prop?

Eric Wieser (Mar 08 2022 at 00:24):

Do you mean "not decidable"?

Eric Wieser (Mar 08 2022 at 00:25):

I mean, it's trivial to write a suitable decidable instance

Yaël Dillies (Mar 08 2022 at 00:25):

(my resulting def would be noncomputable)

Eric Wieser (Mar 08 2022 at 00:25):

But yes, probably such a decidable instance doesn't yet exist. Write one, and play the "how general can I make this" game?

Yaël Dillies (Mar 08 2022 at 00:28):

And do we have any glue between this and prime factorization? In particular, I want to easily access the exponent of 2 (using docs#padic_val_nat I presume) and the odd part.

Eric Wieser (Mar 08 2022 at 00:33):

do we have docs#nat.log2? docs#nat.log

Eric Wieser (Mar 08 2022 at 00:34):

2 ^ nat.log n 2 = n is maybe a better condition for you

Eric Wieser (Mar 08 2022 at 00:55):

instance nat.decidable_mem_powers : ∀ n, decidable_pred (∈ submonoid.powers n)
|0 := λ x, decidable_of_iff (1 = x ∨ 0 = x) begin
  simp only [submonoid.mem_powers_iff],
  split,
  { rintro (rfl | rfl),
    exact ⟨0, pow_zero _⟩,
    exact ⟨1, zero_pow zero_lt_one⟩ },
  { rintro ⟨_ | n, rfl⟩; simp},
end
|1 := λ x, decidable_of_iff (1 = x) $ by simp [submonoid.mem_powers_iff]
| n@(n' + 2) := λ x, decidable_of_iff (n ^ nat.log n x = x) begin
  simp only [submonoid.mem_powers_iff],
  split,
  { intro h,
    refine ⟨nat.log (n' + 2) x, h⟩, },
  { rintro ⟨m, rfl⟩,
    rw nat.log_pow,
    simp },
end

Yaël Dillies (Mar 08 2022 at 08:18):

Thanks a lot!

Eric Wieser (Mar 08 2022 at 08:29):

I'm sure you can make that less awful!

Yaël Dillies (Mar 08 2022 at 11:17):

Indeed! I managed to merge the 1 and n + 2 cases.

Eric Wieser (Mar 08 2022 at 11:21):

It's possible the proof is easier with nat.clog, I didn't try

Eric Wieser (Mar 08 2022 at 11:22):

Or with nat.log n x = nat.clog n x!

Yaël Dillies (Mar 08 2022 at 11:22):

Sorry, I'm sticking to padic_val_nat :grinning: 

lemma nat.mem_submonoid_powers_iff {a n : ℕ}  (hn : n ≠ 0) :
  a ∈ submonoid.powers n ↔ n ^ padic_val_nat n a = a :=
begin
  refine ⟨_, λ h, ⟨_, h⟩⟩,
  rintro ⟨m, rfl⟩,
  obtain _ | _ | n := n,
  { exact (hn rfl).elim },
  { simp_rw one_pow },
  { rw padic_val_nat_pow_self le_add_self }
end

Eric Wieser (Mar 08 2022 at 11:22):

Do we have anywhere that padic_val_nat = nat.log? Or do they diverge at 0?

Yaël Dillies (Mar 08 2022 at 11:23):

Hint: padic_val_nat 2 9 = 0

Last updated: Dec 20 2023 at 11:08 UTC