expand_nums tactic

Stream: Is there code for X?

[Asei Inoue]

How to write a tactic to expand positive integers to sum of 1s?

For example, it should rewrite 3 to 1 +1+1.

[Asei Inoue]

Background: I want to create my own (toy) tactic to treat expression in semiring.
I know ring tactic in mathlib, but I want to do DIY and want a leight-weight tactic for this task.

[Asei Inoue]

The task can be divided into two parts:

• A tactic to identify numeric literals in an equation.
• A tactic to expand a numeric literal n into 1 + 1 + .. + 1.

The latter is almost complete since, once we determine which numeric literals we want to expand, we can apply the following logic for expansion:

private def oneSum (n : Nat) :=
  match n with
  | 0 => 0
  | n + 1 => oneSum n + 1

private theorem Nat.oneSumEq : ∀ (n : Nat), oneSum n = n
  | 0 => rfl
  | n + 1 => by
    rw [oneSum]
    rw [Nat.oneSumEq n]

example : 3 = 2 + 1 := by
  rw [← Nat.oneSumEq 3]
  try repeat rewrite [oneSum]
  rewrite [show 0 + 1 = 1 by rfl]
  guard_target =ₛ 1 + 1 + 1 = 2 + 1

  rfl

[Yaël Dillies]

This should be easy to do with a simproc, except for the "matching the numerals " part. I am not at a computer (and won't be in the foreseeable future), but I will be explaining what a simproc is and how to write one to an audience in Imperial tomorrow afternoon.

[Asei Inoue]

my current answer is :

import Lean

private def oneSum (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | n + 1 => oneSum n + 1

private theorem Nat.oneSumEq : ∀ (n : Nat), n = oneSum n := by
  intro n
  match n with
  | 0 => rfl
  | n + 1 =>
    rw [oneSum]
    rw [← Nat.oneSumEq n]

open Lean Elab.Tactic Elab.Term

elab "expand_numerals" : tactic => do
  for i in [2 : 20] do
    let iexpr := toExpr i
    evalTactic <| ← `(tactic| try rewrite [Nat.oneSumEq $(← exprToSyntax iexpr) ])

example (n : Nat) : (n + m) * (n + m) = n * n + 2 * m * n + m * m := by
  expand_numerals
  repeat rewrite [oneSum]
  simp only [Nat.add_mul, Nat.mul_add, Nat.zero_mul, Nat.mul_zero]
  ac_rfl

[Asei Inoue]

I don't want to manually specify the number of upper limits

[Robin Arnez]

This seems to work:

theorem unfoldNat (x : Nat) : no_index (OfNat.ofNat (x + 2) : Nat) = no_index (OfNat.ofNat (x + 1) : Nat) + 1 :=
  rfl

theorem unfoldNatZero (x : Nat) : no_index (OfNat.ofNat (0 + x) : Nat) = x :=
  Nat.zero_add x

example (n : Nat) : (n + m) * (n + m) = n * n + 10 * m * n + m * m := by
  simp only [unfoldNat, unfoldNatZero]
  -- ...

[Asei Inoue]

@Robin Arnez
Thank you!
what is no_index?

[Robin Arnez]

I don't remember 100% but it was some kind of thing with simp

[Robin Arnez]

It seems to work fine without though

[Aaron Liu]

Robin Arnez said:

This seems to work:

theorem unfoldNat (x : Nat) : no_index (OfNat.ofNat (x + 2) : Nat) = no_index (OfNat.ofNat (x + 1) : Nat) + 1 :=
  rfl

theorem unfoldNatZero (x : Nat) : no_index (OfNat.ofNat (0 + x) : Nat) = x :=
  Nat.zero_add x

example (n : Nat) : (n + m) * (n + m) = n * n + 10 * m * n + m * m := by
  simp only [unfoldNat, unfoldNatZero]
  -- ...

You should use the ofNat(x + 1) elaborator.

[Robin Arnez]

Yeah, you're right, I think it does exactly this.