# Zulip Chat Archive

## 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