Stream: general

Topic: question about simp only

ZHAO Jinxiang (Aug 17 2020 at 17:25):

import data.real.basic

def fn_ub (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a
def fn_has_ub (f : ℝ → ℝ) := ∃ a, fn_ub f a

open_locale classical

variable (f : ℝ → ℝ)

-- BEGIN
example (h : ¬ ∀ a, ∃ x, f x > a) : fn_has_ub f :=
begin
push_neg at h,
exact h
end

example (h : ¬ fn_has_ub f) : ∀ a, ∃ x, f x > a :=
begin
simp only [fn_has_ub, fn_ub] at h,
push_neg at h,
exact h
end
-- END


If I change simp only [fn_has_ub, fn_ub] at h to simp only [fn_has_ub] at h,simp only [fn_ub] at h, it will told me:

unnamed_1338.lean:19:29
simplify tactic failed to simplify
state:
f : ℝ → ℝ,
h : ¬Exists (fn_ub f)
⊢ ∀ (a : ℝ), ∃ (x : ℝ), f x > a


Alex J. Best (Aug 17 2020 at 17:30):

simp tries to apply as many lemmas from a big list of lemmas lean knows (that have been tagged as simp-lemmas previously). simp only [...] only tries to apply the lemmas between the [...] this can be faster if you know exactly which lemmas you want to use, but if the list you give doesnt have all the lemmas needed to simplify the statement it won't be able to do anything.

Alex J. Best (Aug 17 2020 at 17:31):

You could try swapping the order of your two simp only statements around.

Alex J. Best (Aug 17 2020 at 17:32):

As simp will apply any lemmas it is allowed to in whatever order it chooses, unlike rw.

Ruben Van de Velde (Aug 17 2020 at 18:31):

Hmm, it doesn't seem to be as simple as that, though. The first simp changes h : ¬ fn_has_ub f to h : ¬Exists (fn_ub f). Then simp only [fn_ub] doesn't work, but simp [fn_ub] does.

Yakov Pechersky (Aug 17 2020 at 19:22):

example (h : ¬ fn_has_ub f) : ∀ a, ∃ x, f x > a :=
begin
simp only [fn_has_ub] at h,
simp only [fn_ub, not_exists] at h,
push_neg at h,
exact h
end


Yakov Pechersky (Aug 17 2020 at 19:25):

The way I think about it hand-wavily is that while simp is working, it is keeping track of all the existential or universal quantifiers it has introduced. But after it has done all it can, like after simp only [fn_has_ub], it has to reform a valid statement, but does not reintroduce an explicit quantifier, which is how you get the strange ¬Exists. That's not something just simp only [fn_ub] can work with, because there is no clear ∃ x to use. So you need to do

example (h : ¬ fn_has_ub f) : ∀ a, ∃ x, f x > a :=
begin
simp only [fn_has_ub] at h,
simp only [not_exists] at h,
simp only [fn_ub] at h,
push_neg at h,
exact h
end


if you want to enter that ¬Exists.

Yakov Pechersky (Aug 17 2020 at 19:27):

More exactly, the first simp only [fn_has_ub] would need to give you some invented a it chose for the universal quantifier. Which it doesn't do for you, just for itself internally.

Last updated: May 13 2021 at 18:26 UTC