Rewriting a term involving a fixed but arbitrary constant

Stream: new members

[Benjamin]

I'm trying to create a tactic that rewrites a term of the form (c+n)! into (c+n)*((c-1)+n)!, where c is any concrete positive integer (so not a variable). How can I do this?

I can prove a theorem stating (1+n)! = (1+n) * n !, but feeding this to simp doesn't simplify an expression of the form (2+n)!. I've also tried instead giving simp a theorem stating ((succ m)+n)! = ((succ m)+n) * (m+n)!, but this doesn't simplify (2+n)! either.

[Riccardo Brasca]

Note that (c+n)! = (c+n)*((c-1)+n)! is false if c = 0.

[Benjamin]

Right, c is a concrete positive integer.

[Benjamin]

For example, I want to rewrite (7+n)! into (7+n)*(6+n)!.

[Riccardo Brasca]

import Mathlib

open Nat

example (n : ℕ) : (7+n)! = (7+n)*(6+n)! := by
  rw [succ_add, factorial_succ]

works

[Benjamin]

That works, thanks. But for some reason, running ring_nf before the rewrite makes it break. Any idea why that is?

[Benjamin]

I think it has something to do with ring_nf making 7 a instOfNatAtLeastTwo.

[Benjamin]

It's very odd because ring_nf does not visibly change the goal.

[Benjamin]

I found that using erw instead of rw for succ_add works, even after applying ring_nf. I'm not sure why though.

[Eric Wieser]

I think relying on this is probably poor form anyway, and you should split the numeral yourself:

import Mathlib

open Nat

example (n : ℕ) : (7+n)! = (7+n)*(6+n)! := by
  ring_nf -- to break `succ_add`
  rw [(show 7 = 6 + 1 by norm_num), succ_add, factorial_succ]
  sorry

[Eric Wieser]

In theory you could write some clever lemmas with ofNat()s in it, but I don't know if ofNat(n.succ) is actually well-behaved.

[Benjamin]

How should I do this if I'm writing a tactic where I don't know what the numeral is going to be?

[Eric Wieser]

In a tactic, you can match against OfNat.ofNat n to get the numeral

[Benjamin]

Do you mind giving an example of how I would modify this tactic?

macro "ring_fact" : tactic =>
  `(tactic| repeat first
  | fail_if_no_progress ring_nf
  | simp only [Nat.factorial_zero, Nat.factorial_succ]
  | erw [Nat.succ_add])

[Eric Wieser]

Ah, what I'm proposing would have to be an elab not a macro