question about simp only

Stream: general

[ZHAO Jinxiang]

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]

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]

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

[Alex J. Best]

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

[Ruben Van de Velde]

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]

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]

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]

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.