Use option for tactic throughout file

Stream: mathlib4

[Mitchell Lee]

Hello, is there a way to make linear_combination use a particular tactic (in my case, I want it to use (try simp only [Int.negSucc_eq, Int.ofNat_eq_coe, Nat.succ_eq_add_one]); (try push_cast); ring_nf) as the normalization tactic throughout an entire file?

Or, more generally, is there a way to specify a particular option for a tactic throughout a file?

[Mitchell Lee]

The use case is this: I want to define the Chebyshev polynomials at negative integers and use linear_combination to prove things about them. Here's a stripped down version of what I have. Note how often you see linear_combination (norm := ((try simp only [Int.negSucc_eq, Int.ofNat_eq_coe, Nat.succ_eq_add_one]); (try push_cast); ring_nf)). I'm sure there must be a way to not have to type that every time.

import Mathlib

open Polynomial

/-- `T n` is the `n`-th Chebyshev polynomial of the first kind. -/
noncomputable def T : ℤ → ℤ[X]
  | 0 => 1
  | 1 => X
  | (n : ℕ) + 2 => 2 * X * T (n + 1) - T n
  | -((n : ℕ) + 1) => 2 * X * T (-n) - T (-n + 1)
  termination_by n => Int.natAbs n + Int.natAbs (n - 1)

theorem T_add_two : ∀ n, T (n + 2) = 2 * X * T (n + 1) - T n
  | (k : ℕ) => T.eq_3 k
  | -(k + 1 : ℕ) => by
    linear_combination (norm := ((try simp only [Int.negSucc_eq, Int.ofNat_eq_coe, Nat.succ_eq_add_one]); (try push_cast); ring_nf))
      T.eq_4 k

theorem T_add_one (n : ℤ) : T (n + 1) = 2 * X * T n - T (n - 1) := by
  linear_combination (norm := ((try simp only [Int.negSucc_eq, Int.ofNat_eq_coe, Nat.succ_eq_add_one]); (try push_cast); ring_nf))
    T_add_two (n - 1)

theorem T_sub_two (n : ℤ) : T (n - 2) = 2 * X * T (n - 1) - T n := by
  linear_combination (norm := ((try simp only [Int.negSucc_eq, Int.ofNat_eq_coe, Nat.succ_eq_add_one]); (try push_cast); ring_nf))
    T_add_two (n - 2)

theorem T_sub_one (n : ℤ) : T (n - 1) = 2 * X * T n - T (n + 1) := by
  linear_combination (norm := ((try simp only [Int.negSucc_eq, Int.ofNat_eq_coe, Nat.succ_eq_add_one]); (try push_cast); ring_nf))
    T_add_two (n - 1)

theorem T_eq (n : ℤ) : T n = 2 * X * T (n - 1) - T (n - 2) := by
  linear_combination (norm := ((try simp only [Int.negSucc_eq, Int.ofNat_eq_coe, Nat.succ_eq_add_one]); (try push_cast); ring_nf))
    T_add_two (n - 2)

@[simp]
theorem T_neg_one : T (-1) = X := (by ring : 2 * X * 1 - X = X)

theorem T_neg (n : ℤ) : T (-n) = T n := by
  induction n using T.induct with
  | case1 => rfl
  | case2 => simp [T]
  | case3 n ih1 ih2 =>
    have h₁ := T_add_two n
    have h₂ := T_sub_two (-n)
    linear_combination (norm := ((try simp only [Int.negSucc_eq, Int.ofNat_eq_coe, Nat.succ_eq_add_one]); (try push_cast); ring_nf))
      (2 * (X : ℤ[X])) * ih1 - ih2 - h₁ + h₂
  | case4 n ih1 ih2 =>
    have h₁ := T_add_one n
    have h₂ := T_sub_one (-n)
    linear_combination (norm := ((try simp only [Int.negSucc_eq, Int.ofNat_eq_coe, Nat.succ_eq_add_one]); (try push_cast); ring_nf))
      (2 * (X : ℤ[X])) * ih1 - ih2 + h₁ - h₂

[Kim Morrison]

Define a macro.

[Mitchell Lee]

Thank you for the answer. Unfortunately, I know very little about metaprogramming, so I am not sure how to do that. I managed to make a macro for (try simp only [Int.negSucc_eq, Int.ofNat_eq_coe, Nat.succ_eq_add_one]); (try push_cast); ring_nf), which makes things a little less verbose, but I don't know how to make a macro for linear_combination (norm := ((try simp only [Int.negSucc_eq, Int.ofNat_eq_coe, Nat.succ_eq_add_one]); (try push_cast); ring_nf)).

[Kyle Miller]

I'm curious, how did you make that first macro?

[Kyle Miller]

Is the issue that you aren't sure how to pass in the argument to linear_combination? Here's an option.

macro "my_tactic " t?:(term)? : tactic =>
  `(tactic| linear_combination
      (norm := ((try simp only [Int.negSucc_eq, Int.ofNat_eq_coe, Nat.succ_eq_add_one]); (try push_cast); ring_nf))
      $[$t?:term]?)

theorem T_sub_one (n : ℤ) : T (n - 1) = 2 * X * T n - T (n + 1) := by
  my_tactic T_add_two (n - 1)

[Mitchell Lee]

I did this:

macro "int_ring_nf" : tactic => `(tactic | (
  try simp only [Int.negSucc_eq, Int.ofNat_eq_coe, Nat.succ_eq_add_one]
  try push_cast
  ring_nf))

[Mitchell Lee]

Thanks! I'll see if I can use this. But maybe I'll just stick to specifying the option explicitly.

Kyle Miller said:

Is the issue that you aren't sure how to pass in the argument to linear_combination? Here's an option.

macro "my_tactic " t?:(term)? : tactic =>
  `(tactic| linear_combination
      (norm := ((try simp only [Int.negSucc_eq, Int.ofNat_eq_coe, Nat.succ_eq_add_one]); (try push_cast); ring_nf))
      $[$t?:term]?)

theorem T_sub_one (n : ℤ) : T (n - 1) = 2 * X * T n - T (n + 1) := by
  my_tactic T_add_two (n - 1)