Stream: new members
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?
Reid Barton (Jun 05 2020 at 15:18):
The usual recommendation is
dsimp only  at h
Patrick Massot (Jun 05 2020 at 15:30):
You can even omit the empty list.
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
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