Zulip Chat Archive

Stream: general

Topic: question about simp only


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

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

view this post on Zulip Alex J. Best (Aug 17 2020 at 17:31):

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

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

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

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

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

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