Pass local hypotheses to tactic

Stream: general

[Abhimanyu Pallavi Sudhir]

Is this how I make a tactic that requires a local hypothesis (represented variously by p, e, and H1)?

import analysis.normed_space
open lean lean.parser tactic interactive interactive.types expr

meta def unfold_eps_del_1 (fε fδ fx : ℝ → ℝ)
(p1 : parse texpr) : tactic unit := do e ← i_to_expr p1, let H1 := expr.get_app_fn e,
`[try {simp only [filter.tendsto_nhds_of_metric, dist], rw sub_zero}],
`[try {simp only [filter.tendsto_punctured]}],
`[try {simp only [filter.tendsto_nhds_of_metric, dist] at H1, rw sub_zero at H1}],
`[try {simp only [filter.tendsto_punctured] at H1}],
`[intros ε ε0],
`[have H11 := H1 (fε ε) _],
`[cases H11 with δ H12],
`[cases H12 with Hδ H13],
`[existsi (fδ δ)],
`[existsi _],
`[intros x xd],
`[try {intro x0}],
`[have H14 := H13 (fx x) _],
`[try {have H15 := H14 _}]

I'm basing this on the code for meta def specialize in library/init/meta/interactive.lean but not sure how it works.

[Abhimanyu Pallavi Sudhir]

Is this right?

[Abhimanyu Pallavi Sudhir]

import analysis.normed_space
open lean lean.parser tactic interactive interactive.types expr

meta def unfold_eps_del_1 (fε fδ fx : ℝ → ℝ)
(p : parse ident) : tactic unit := do H1 ← resolve_name p,
`[try {simp only [filter.tendsto_nhds_of_metric, dist], rw sub_zero}],
`[try {simp only [filter.tendsto_punctured]}],
`[try {simp only [filter.tendsto_nhds_of_metric, dist] at H1, rw sub_zero at H1}],
`[try {simp only [filter.tendsto_punctured] at H1}],
`[intros ε ε0],
`[have H11 := H1 (fε ε) _],
`[cases H11 with δ H12],
`[cases H12 with Hδ H13],
`[existsi (fδ δ)],
`[existsi _],
`[intros x xd],
`[try {intro x0}],
`[have H14 := H13 (fx x) _],
`[try {have H15 := H14 _}]

[Abhimanyu Pallavi Sudhir]

It seems right, but when I try to actually use the tactic by giving it the name of a hypothesis, it fails saying unknown identifier 'a':

def has_derivative_at (f : ℝ → ℝ) (x0 : ℝ) (f'x0 : ℝ)
:= (tendsto (λ h, (f (x0 + h) - f (x0) - f'x0 * h)/h) (nhds 0) (nhds 0))

lemma has_derivative_at_iff_eps_del (f : ℝ → ℝ) (x0 : ℝ) (f'x0 : ℝ)
: has_derivative_at f x0 f'x0 ↔
  ∀ ε > 0, ∃ δ > 0, ∀ h : ℝ, abs h < δ → abs ((f(x0 + h) - f(x0) - f'x0 * h) / h) < ε
  := by simp [has_derivative_at, tendsto_nhds_of_metric, dist]

lemma has_derivative_at_iff_eps_del' (f : ℝ → ℝ) (x0 : ℝ) (f'x0 : ℝ)
: has_derivative_at f x0 f'x0 ↔
  ∀ ε > 0, ∃ δ > 0, ∀ h : ℝ, h ≠ 0 → abs h < δ → abs ((f(x0 + h) - f(x0))/h - f'x0) < ε :=
begin
  split,
  { intro a, rw has_derivative_at_iff_eps_del at a,
    unfold_eps_del_1 id id id a,
  }
end

And when I try this:

lemma has_derivative_at_iff_eps_del' (f : ℝ → ℝ) (x0 : ℝ) (f'x0 : ℝ)
: has_derivative_at f x0 f'x0 ↔
  ∀ ε > 0, ∃ δ > 0, ∀ h : ℝ, h ≠ 0 → abs h < δ → abs ((f(x0 + h) - f(x0))/h - f'x0) < ε :=
begin
  split,
  { intro a, rw has_derivative_at_iff_eps_del at a,
    unfold_eps_del_1 id id id "a",
  }
end

I get unknown identifier 'H1', so I must be doing something wrong.

[Patrick Massot]

Did you read https://github.com/leanprover/mathlib/blob/master/docs/extras/tactic_writing.md?

[Abhimanyu Pallavi Sudhir]

I hadn't seen that -- so I guess get_local is the right command (as opposed to resolve_name)? But this doesn't work either:

import analysis.normed_space
open lean tactic interactive.types expr
open interactive (parse)
open lean.parser (ident)

meta def unfold_eps_del_1 (fε fδ fx : ℝ → ℝ)
(p : parse ident) : tactic unit := do H1 ← get_local p,
`[try {simp only [filter.tendsto_nhds_of_metric, dist], rw sub_zero}],
`[try {simp only [filter.tendsto_punctured]}],
`[try {simp only [filter.tendsto_nhds_of_metric, dist] at H1, rw sub_zero at H1}],
`[try {simp only [filter.tendsto_punctured] at H1}],
`[intros ε ε0],
`[have H11 := H1 (fε ε) _],
`[cases H11 with δ H12],
`[cases H12 with Hδ H13],
`[existsi (fδ δ)],
`[existsi _],
`[intros x xd],
`[try {intro x0}],
`[have H14 := H13 (fx x) _],
`[try {have H15 := H14 _}]

def has_derivative_at (f : ℝ → ℝ) (x0 : ℝ) (f'x0 : ℝ)
:= (tendsto (λ h, (f (x0 + h) - f (x0) - f'x0 * h)/h) (nhds 0) (nhds 0))

lemma has_derivative_at_iff_eps_del (f : ℝ → ℝ) (x0 : ℝ) (f'x0 : ℝ)
: has_derivative_at f x0 f'x0 ↔
  ∀ ε > 0, ∃ δ > 0, ∀ h : ℝ, abs h < δ → abs ((f(x0 + h) - f(x0) - f'x0 * h) / h) < ε
  := by simp [has_derivative_at, tendsto_nhds_of_metric, dist]

lemma has_derivative_at_iff_eps_del' (f : ℝ → ℝ) (x0 : ℝ) (f'x0 : ℝ)
: has_derivative_at f x0 f'x0 ↔
  ∀ ε > 0, ∃ δ > 0, ∀ h : ℝ, h ≠ 0 → abs h < δ → abs ((f(x0 + h) - f(x0))/h - f'x0) < ε :=
begin
  split,
  { intro a, rw has_derivative_at_iff_eps_del at a,
    unfold_eps_del_1 id id id a,
  }
end

[Rob Lewis]

None of the expressions you have enclosed in `[...] refer to the fε fδ fx arguments to unfold_eps_del_1, nor to p or H1. When you write a tactic using this notation and then apply it in a proof, you can imagine that the text inside `[...] just gets copied literally into that point in the proof.

[Rob Lewis]

This notation is useful for very small tactic scripts. But if you want to write a tactic that takes parameters, you really need to learn "non-interactive" tactic mode.