Creating a simple tactic

Stream: new members

[Lauri Oksanen]

I am playing with a tactic related to convergence of sequences as defined in Buzzard's course material. The following code works:

def TendsTo (a : ℕ → ℝ) (t : ℝ) : Prop :=
  ∀ ε > 0, ∃ B : ℕ, ∀ n, n ≥ B → |a n - t| < ε

infix:50 " ∞⟶ " => TendsTo

example {a : ℕ → ℝ} {t c : ℝ} (h : a ∞⟶ t) :
  (a · + c) ∞⟶ t + c
:= by
  rw [TendsTo] at *
  peel h
  ring_nf at *
  assumption

section
  open Lean Elab.Tactic
  elab "ring_in_tendsTo" h:ident : tactic => do
    evalTactic (← `(tactic|
      rw [TendsTo] at *;
      peel 5 $(mkIdent h.getId);
      ring_nf at *;
      assumption
    ))
end

example {a : ℕ → ℝ} {t c : ℝ} (h : a ∞⟶ t) :
  (a · + c) ∞⟶ t + c
:= by ring_in_tendsTo h

I have two questions:

1. How can I get rid of 5 after peel in the definition of the tactic? When I use peel in the usual way, it is not needed.
2. How can I parametrize the symbol TendsTo in the definition of the tactic? That is, I would like to do something like (the below code does not work):

section
  open Lean Elab.Tactic
  elab "ring_in" d:ident h:ident : tactic => do
    evalTactic (← `(tactic|
      rw [$(??? d)] at *;
      peel 5 $(mkIdent h.getId);
      ring_nf at *;
      assumption
    ))
end

[Aaron Liu]

macro (name := ringIn) "ring_in" d:ident h:ident : tactic =>
  `(tactic|
    (
    rw [$d:ident] at *;
    peel $h:ident;
    ring_nf at *;
    assumption
    )
  )

Of course, you can use elab too, but for simple stuff like this I like macro better.

[Lauri Oksanen]

Thanks a lot!