Zulip Chat Archive

Stream: new members

Topic: Simplifying lambda expressions


view this post on Zulip Rick Koenders (Jun 05 2020 at 15:17):

Is there a way (in tactic mode) to simplify lambda expressions that are applied to an element? So a way to transform (λ n : ℕ, foo n) x into foo x. So far I have found that simp will do this, but squeeze_simp does not say what lemma is used to simplify this expression (probably because they are definitionally equal). In my code I'd like to use this at this point (irrelevant context removed):

import tactic

example (a :   ) (h :  x : , ¬(λ (n : ), a n  0) x) :  n : , a n = 0 :=
begin
    simp only [not_not, ne.def] at h, -- Found this using squeeze_simp
    exact h,
end

Note that using tactics like rw ne.def at h and rw not_not at h do not work: Lean does "not find instance of the pattern in the target expression".
Can you prove this without using simp? If it is possible, is using simp here preferred over that alternative?

view this post on Zulip Reid Barton (Jun 05 2020 at 15:18):

The usual recommendation is dsimp only [] at h

view this post on Zulip Patrick Massot (Jun 05 2020 at 15:30):

You can even omit the empty list.

view this post on Zulip Rick Koenders (Jun 05 2020 at 15:33):

Just found out that the reason rw not_not at h doesn't work is because of the ∀, not because of the λ. The following is a valid proof without simp:

example (a :   ) (h :  x : , ¬(λ (n : ), a n  0) x) :  n : , a n = 0 :=
begin
    intro n,
    have hn := h n,
    rw not_not at hn,
    exact hn,
end

Thanks for the suggestions everyone.


Last updated: May 14 2021 at 07:19 UTC