Tools for beta reduction

Stream: new members

[Calle Sönne]

I have following code:

lemma limit_start_irrelevant (a : ℕ → ℝ) (k : ℕ) {l : ℝ} (h : is_limit (λ n, a (n+k)) l) : is_limit a l :=
begin
  intros ε Hε,
  cases h ε Hε with N H,
  use N + k,
  intros n Hn,
  have ineq : k ≤ n, rw add_comm at Hn, exact (le_trans (nat.le_sub_right_of_add_le Hn) (nat.sub_le_self n N)),
  specialize H (n - k) (nat.le_sub_right_of_add_le Hn),  -- Tactic state 1 here
  simp only at H, -- Tactic state 2 here
  rwa [add_comm, ←nat.add_sub_assoc ineq, add_comm, nat.add_sub_cancel] at H,
end

Tactic state 1:

a : ℕ → ℝ,
k : ℕ,
l : ℝ,
h : is_limit (λ (n : ℕ), a (n + k)) l,
ε : ℝ,
Hε : ε > 0,
N n : ℕ,
Hn : n ≥ N + k,
ineq : k ≤ n,
H : |(λ (n : ℕ), a (n + k)) (n - k) - l| < ε
⊢ |a n - l| < ε

Tactic state 2:

a : ℕ → ℝ,
k : ℕ,
l : ℝ,
h : is_limit (λ (n : ℕ), a (n + k)) l,
ε : ℝ,
Hε : ε > 0,
N n : ℕ,
Hn : n ≥ N + k,
ineq : k ≤ n,
H : |a (n - k + k) - l| < ε
⊢ |a n - l| < ε

Right now I am forced to use simp only to beta reduce H, because otherwise rw doesnt work. Is there any special tools for beta reduction I could use? Simp only feels unnecessary.

[Calle Sönne]

I see that I can use convert H as well, but this also feels like overkill.

[Mario Carneiro]

you could use dsimp only as well

[Mario Carneiro]

If you play with the options you can get it to simplify almost nothing except beta reduction, but there isn't a dedicated command for it

[Kevin Buzzard]

If you want to change H to something definitionally equal, you can just write "change [thing you want] at H"

[Patrick Massot]

As Kevin wrote, you can use change to force rewriting to something definitionaly equivalent. But in this case you want to use convert anyway, because you also want to make Lean realize you need n-k+k=n or something like that. What is it you don't like in my version:

lemma limit_start_irrelevant {a : ℕ → ℝ} (k : ℕ) {l : ℝ} (h : M1P1.is_limit (λ n, a (k+n)) l) : M1P1.is_limit a l :=
begin
  intros ε Hε,
  cases h ε Hε with N H,
  use k + N,
  intros n Hn,
  have key : n - k ≥ N := nat.le_sub_left_of_add_le Hn,
  convert H (n-k) _,
  apply int.coe_nat_inj,
  rw [int.coe_nat_add, int.coe_nat_sub],
  repeat { linarith },
end

[Calle Sönne]

I like your version much better, but I wont learn anything if I just copy-paste it into my file. I was comparing my code to yours and rewriting it in the process.

[Calle Sönne]

Also, speaking about your code, The last line: repeat { linarith }, seems to remove 3 goals. Why is that?

[Calle Sönne]

The last goal is instantly solved by one of the hypothesis, so does linarith (or repeat?) just try the hypothesis on the next goal to see if it works?

[Johan Commelin]

@Calle Sönne repeat {linarith}, is just the same as

linarith,
linarith,
linarith,
linarith,
...
-- until one of them fails

[Kenny Lau]

private meta def repeat_aux (t : tactic unit) : list expr → list expr → tactic unit
| []      r := set_goals r.reverse
| (g::gs) r := do
  ok ← try_core (set_goals [g] >> t),
  match ok with
  | none := repeat_aux gs (g::r)
  | _    := do
    gs' ← get_goals,
    repeat_aux (gs' ++ gs) r
  end

/-- This tactic is applied to each goal. If the application succeeds,
    the tactic is applied recursively to all the generated subgoals until it eventually fails.
    The recursion stops in a subgoal when the tactic has failed to make progress.
    The tactic `repeat` never fails. -/
meta def repeat (t : tactic unit) : tactic unit :=
do gs ← get_goals, repeat_aux t gs []

[Calle Sönne]

Ah, for some reason I thought it meant reapeat once.

[Mario Carneiro]

that would be iterate 2