Ring tactic and exponents

Stream: new members

[Benjamin]

Is there a reason why the ring tactic cannot close goals like 2^n*3^n = 6^n or 2^(2*n) = 4^n, where n : Nat? I know that exponentiation is not a ring operation, but ring seems to have some basic support for exponents. Is this intentional? And is there some other tactic that can solve such goals?

[Bjørn Kjos-Hanssen]

This works, but I'm also surprised that omega does not find Nat.mul_pow here.

import Mathlib
example (n : ℕ) : 2^n * (3^n) = 6^n := by
  rw [show 6 = 2 * 3 by omega, Nat.mul_pow]

[Eric Wieser]

You can use the module tactic...

[Eric Wieser]

import Mathlib

example {n : ℕ} : 2^n*3^n = 6^n := by
  rw [show 6 = 3 * 2 from rfl]
  apply Additive.ofMul.injective
  simp [-Nat.reduceMul]
  module

[Eric Wieser]

(as long as you factor everything first)

[Benjamin]

Thanks, but I'm more interested in how to solve this problem in general with a tactic. The difficulty arises when the terms a^n and b^n are far apart, so I'm not sure how to rewrite using <- Nat.mul_pow. I don't think Lean has a tactic for rewriting modulo associativity.

[Benjamin]

For example, if I have a term like 2^n * x * y * 3^n, I'm not sure how to rewrite it to x * y * 6^n.

[Bjørn Kjos-Hanssen]

Actually @Eric Wieser 's method works there:

import Mathlib

example {n x y : ℕ} : 2^n* x*y * 3^n = x*y * 6^n := by
  rw [show 6 = 3 * 2 from rfl]
  apply Additive.ofMul.injective
  simp [-Nat.reduceMul]
  module

As does

import Mathlib

example {n x y : ℕ} : 2^n* x*y * 3^n = x*y * 6^n := by
  rw [show 6 = 3 * 2 from rfl, Nat.mul_pow]
  ring

[Benjamin]

I prefer to rewrite Nat.mul_pow the other way, otherwise I have to implement a tactic to factorize every integer within an expression, which is computationally expensive (and probably tricky to implement).

[Eric Wieser]

It's actually really quite easy to implement that :)

[Benjamin]

Can you elaborate?

[Eric Wieser]

import Mathlib

open Qq

def mkProd {u} {α : Q(Type u)} (inst : Q(One $α)) (inst : Q(Mul $α)) (xs : List Q($α)) : Q($α):=
  go xs.reverse
where go : List Q($α) → Q($α)
  | [] => q(1)
  | [x] => x
  | x :: xs =>
    let rest := go xs
    q($rest * $x)

local elab "factorize_tac" : tactic => do
  Lean.Elab.Tactic.liftMetaFinishingTactic fun m => do
    have h := .mvar m
    let ⟨0, ~q((OfNat.ofNat $en : ℕ) = $rhs), h⟩ := ← inferTypeQ h
      | throwError "Could not infer numeral"
    let .some n := en.rawNatLit?
      | throwError "Not a literal {repr en}: {m}"
    have factors : List Q(Nat) := n.primeFactorsList.map Lean.toExpr
    if factors.length < 2 then
      Lean.Elab.throwAbortTerm
      throwError "Doesn't work on on 0 1"
    have new_rhs : Q(Nat) := mkProd q(inferInstance) q(inferInstance) factors
    have : $new_rhs =Q $en := ⟨⟩
    Lean.commitIfNoEx do
      let .defEq _ := ← isDefEqQ q($rhs) q($new_rhs)
        | throwError "Could not assign RHS"
      h.mvarId!.assignIfDefEq q(rfl : $en = $new_rhs)

/-- This "rw_proc" expands `n` into `a * b * c`. -/
theorem Nat.eq_mul {n : ℕ} {«a * b * c»} (h : ofNat(n) = «a * b * c» := by factorize_tac) :
    ofNat(n) = «a * b * c» :=
  h

example : 60 + 12 + 5 = sorry := by
  rw [Nat.eq_mul]
  rw [Nat.eq_mul (n := nat_lit 12)]

[Eric Wieser]

Eric Wieser said:

It's actually really quite easy to implement that :)

I should clarify; this is easy for me because it is very similar to something I implemented recently

[Benjamin]

Oh, wow, thanks! Did you get this code from somewhere or is it just from a personal project?

[Eric Wieser]

It's derived from #24155, which in turn came from some Lean 3 code I wrote years ago

[Benjamin]

How can I apply this rewrite to every number in an expression? simp [eq_mul] doesn't work for some reason.

tactic 'simp' failed, nested error:
maximum recursion depth has been reached

[Benjamin]

I think it's trying to repeatedly factorize the primes after they've already been factored.

[Eric Wieser]

Indeed, this hack doesn't work with simp

[Eric Wieser]

Here's the version that works with simp but not rw:

import Mathlib

open Qq

def mkProd {u} {α : Q(Type u)} (inst : Q(One $α)) (inst : Q(Mul $α)) (xs : List Q($α)) : Q($α):=
  go xs.reverse
where go : List Q($α) → Q($α)
  | [] => q(1)
  | [x] => x
  | x :: xs =>
    let rest := go xs
    q($rest * $x)

simproc_decl Nat.eq_mul' (_) := .ofQ fun u α e => do
  match u, α, e with
  | 1, ~q(ℕ), ~q(OfNat.ofNat $en) => do
    let .some n := en.rawNatLit? | return .continue
    have factors : List Q(Nat) := n.primeFactorsList.map Lean.toExpr
    if factors.length < 2 then
      return .continue
    have new_rhs : Q(Nat) := mkProd q(inferInstance) q(inferInstance) factors
    have : $new_rhs =Q $en := ⟨⟩
    return .continue <| some <| .mk q($new_rhs) none
  | _, _, _ => return .continue

example : 60 + 12 + 5 = sorry := by
  simp_rw [Nat.eq_mul']
  -- sorry is now cursed lol

[Eric Wieser]

(#general > Exploding sorry @ 💬 for the weird sorry behavior)

[Benjamin]

I think for my application, I can just define something like this:

theorem factorize_exp {n m : ℕ} {«a * b * c»} (h : ofNat(n) = «a * b * c» := by factorize_tac) :
    ofNat(n) ^ m = «a * b * c» ^ m := by rw [h]

[Benjamin]

And then do repeat rw [factorize_exp]

[Eric Wieser]

I think Nat.eq_mul' above should work for you, if you want simp

[Benjamin]

How does simp only compare to repeat rw?

[Benjamin]

Or simp_rw?

[Eric Wieser]

simp_rw [x, y] is simp only [x]; simp only [y], roughly

[Eric Wieser]

The main consideration here is that Nat.eq_mul is a horrible hack, but Nat.eq_mul' is using the system as designed

[Benjamin]

So the simp version is better, you mean?

[Eric Wieser]

For what you're doing, yes

[Benjamin]

And what if I only want to rewrite a numeral when it occurs as the base of an exponential expression, like 60^n? I can do that with eq_mul as I described, but what about with eq_mul'?

[Eric Wieser]

Oh, I guess it's neat that you were able to adapt the unprimed version without touching any meta code