Zulip Chat Archive

Stream: new members

Topic: Tools for beta reduction


view this post on Zulip 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 ε ,
  cases 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 23 2019 at 10:04):

you could use dsimp only as well

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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 ε ,
  cases 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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 []

view this post on Zulip Calle Sönne (Feb 23 2019 at 15:06):

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

view this post on Zulip Mario Carneiro (Feb 23 2019 at 15:11):

that would be iterate 2


Last updated: May 15 2021 at 02:11 UTC