## Stream: new members

### Topic: Tools for beta reduction

#### Calle Sönne (Feb 23 2019 at 09:49):

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
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 (Feb 23 2019 at 09:50):

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

#### Mario Carneiro (Feb 23 2019 at 10:04):

you could use dsimp only as well

#### Mario Carneiro (Feb 23 2019 at 10:05):

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 (Feb 23 2019 at 10:08):

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

#### Patrick Massot (Feb 23 2019 at 11:58):

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,
repeat { linarith },
end


#### Calle Sönne (Feb 23 2019 at 13:54):

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 (Feb 23 2019 at 13:59):

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

#### Calle Sönne (Feb 23 2019 at 14:01):

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 (Feb 23 2019 at 14:45):

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

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


#### Kenny Lau (Feb 23 2019 at 14:50):

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 (Feb 23 2019 at 15:06):

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

#### Mario Carneiro (Feb 23 2019 at 15:11):

that would be iterate 2

Last updated: May 15 2021 at 02:11 UTC