# Zulip Chat Archive

## Stream: new members

### Topic: push_neg

#### Julian Berman (Oct 26 2020 at 18:14):

How come the third of these lemmas requires explicitly pushing the negation? (If the answer is just "because it does" that's fine enough)

```
lemma all_thingies_then_false {x : finset nat} : x = ∅ ↔ ∀ (y : nat), y ∈ x → false :=
by exact eq_bot_iff
lemma all_thingies_not {x : finset nat} : x = ∅ ↔ ∀ (y : nat), y ∉ x :=
by exact eq_bot_iff
lemma no_thingies {x : finset nat} : x = ∅ ↔ ¬ ∃ (y : nat), y ∈ x :=
by { push_neg, exact eq_bot_iff }
```

I ask mainly because I originally wrote out the third being sure it'd exist somewhere, but then `suggest`

/ `library_search`

didn't find it, till I figured I should just rejigger.

#### Kevin Buzzard (Oct 26 2020 at 18:16):

`not exists`

is not *definitionally* equal to `forall not`

.

#### Julian Berman (Oct 26 2020 at 18:16):

and the corresponding lemma just doesn't exist in mathlib?

#### Julian Berman (Oct 26 2020 at 18:16):

(one using not exists)

#### Kevin Buzzard (Oct 26 2020 at 18:17):

Certainly the lemma that not exists is equivalent to forall not will be in mathlib

#### Julian Berman (Oct 26 2020 at 18:17):

Yeah sorry I mean the corresponding lemma to `eq_bot_iff`

I guess

#### Mario Carneiro (Oct 26 2020 at 18:17):

the forall not formulation is preferred

#### Julian Berman (Oct 26 2020 at 18:17):

Probably what I mean to ask is "is there... yeah what MArio answered :)

#### Julian Berman (Oct 26 2020 at 18:18):

So if I want one or the other I should assume it's defined as a forall

#### Julian Berman (Oct 26 2020 at 18:18):

Cool, thanks!

#### Mario Carneiro (Oct 26 2020 at 18:18):

yeah, these are so-called "idioms" in mathlib

#### Mario Carneiro (Oct 26 2020 at 18:18):

like "use x < y over y > x"

#### Julian Berman (Oct 26 2020 at 18:18):

*nod*

#### Mario Carneiro (Oct 26 2020 at 18:18):

it keeps the number of needed lemmas down

#### Julian Berman (Oct 26 2020 at 18:19):

Makes sense.

#### Kevin Buzzard (Oct 26 2020 at 18:19):

`simp`

converts not exists into forall not.

#### Mario Carneiro (Oct 26 2020 at 18:20):

which means `by simp [eq_bot_iff]`

should also prove the theorem

#### Kevin Buzzard (Oct 26 2020 at 18:21):

`simp`

generally tries to put things into "mathlib normal form". A great example is nonempty (rather than empty) -- there seemed to be about three ways to say that a set was non-empty in mathlib, and relatively recently it was decided to make `x.nonempty`

the "canonical form" and then all the other occurrences were purged from mathlib lemmas other than the simp lemma which turns other ways of saying it into `x.nonempty`

#### Julian Berman (Oct 26 2020 at 18:22):

That's nice, I was pondering that (whether simp encodes the idioms)

#### Kevin Buzzard (Oct 26 2020 at 18:23):

PS `by exact`

cancels :-)

```
lemma all_thingies_then_false {x : finset nat} : x = ∅ ↔ ∀ (y : nat), y ∈ x → false :=
eq_bot_iff
```

#### Julian Berman (Oct 26 2020 at 18:23):

Maybe I'll ask then why `library_search`

doesn't call simp first (or at least call it if it fails)

#### Kevin Buzzard (Oct 26 2020 at 18:24):

Tactics have very well-defined domains

#### Kevin Buzzard (Oct 26 2020 at 18:24):

`library_search`

looks for one lemma in the library which closes the goal immediately. That's its job.

#### Julian Berman (Oct 26 2020 at 18:24):

Kevin Buzzard said:

PS

`by exact`

cancels :-)`lemma all_thingies_then_false {x : finset nat} : x = ∅ ↔ ∀ (y : nat), y ∈ x → false := eq_bot_iff`

aha thanks! I tried \<eq_bot_iff\> and some other random syntax permutations, but not that one, appreciated

#### Mario Carneiro (Oct 26 2020 at 18:25):

it would be *way* too expensive to call `simp`

on every lemma in the library

#### Julian Berman (Oct 26 2020 at 18:25):

Kevin Buzzard said:

`library_search`

looks for one lemma in the library which closes the goal immediately. That's its job.

yeah fair enough then some other higher level tactic right?

#### Julian Berman (Oct 26 2020 at 18:25):

not on every lemma in the library, just on the goal

#### Kevin Buzzard (Oct 26 2020 at 18:25):

`{simp, library_search}`

is one tactic

#### Julian Berman (Oct 26 2020 at 18:26):

basically it didn't find `eq_bot_iff`

because my thing was not in mathlib-normal form (and yeah I didn't think of running `simp`

myself because I didn't know I wasn't in normal form)

#### Julian Berman (Oct 26 2020 at 18:26):

but I can commit to memory to run `{simp, library_search}`

instead next time I'm "stuck" if that's a decent idea?

#### Kevin Buzzard (Oct 26 2020 at 18:26):

non-terminal simps are evil

#### Mario Carneiro (Oct 26 2020 at 18:27):

it's fine for `library_search`

since it's not going into mathlib

#### Julian Berman (Oct 26 2020 at 18:27):

right and then `squeeze_simp`

when it finds it etc., hopefully I'm starting to commit at least some of this mental algorithm :D

#### Kevin Buzzard (Oct 26 2020 at 18:27):

PS `finset.eq_empty_iff_forall_not_mem`

is a thing, which is far closer to what you want

#### Mario Carneiro (Oct 26 2020 at 18:27):

once you know what lemma you want, you can better figure out how to make it applicable, whether `simp`

or `rw`

or `apply`

is appropriate

#### Kevin Buzzard (Oct 26 2020 at 18:28):

```
lemma no_thingies {x : finset nat} : x = ∅ ↔ ¬ ∃ (y : nat), y ∈ x :=
by simp [finset.eq_empty_iff_forall_not_mem]
```

#### Julian Berman (Oct 26 2020 at 18:28):

Kevin Buzzard said:

`lemma no_thingies {x : finset nat} : x = ∅ ↔ ¬ ∃ (y : nat), y ∈ x := by simp [finset.eq_empty_iff_forall_not_mem]`

aha, thank you! did you find that from just looking at `finset`

's file?

#### Julian Berman (Oct 26 2020 at 18:28):

(and/or knowing about it)

#### Kevin Buzzard (Oct 26 2020 at 18:28):

none of those things

#### Kevin Buzzard (Oct 26 2020 at 18:29):

I found it by typing `eq_empty_iff`

and pressing ctrl-space

#### Kevin Buzzard (Oct 26 2020 at 18:29):

because I was interested in seeing which lemmas started with `x = empty iff ...`

#### Julian Berman (Oct 26 2020 at 18:29):

got it, yeah I don't think I know the naming conventions well enough yet to do that

#### Mario Carneiro (Oct 26 2020 at 18:30):

#### Julian Berman (Oct 26 2020 at 18:30):

thanks obviously each of these tips are super helpful

#### Kevin Buzzard (Oct 26 2020 at 18:31):

This is a really powerful way to find lemmas. I did it because `simp [eq_bot_iff]`

doesn't work because Lean doesn't realise the definitional equalities (`simp`

and `rw`

work with syntactic equalities) so I wanted to find the same lemma but specifically for finsets.

#### Kevin Buzzard (Oct 26 2020 at 18:32):

If `eq_bot_iff`

is `x = \bot \iff ...`

then it's not surprising that `eq_empty_iff`

is what we want.

#### Julian Berman (Oct 26 2020 at 22:36):

well hooray, I successfully managed to find/use `option.eq_none_iff_forall_not_mem`

just now in a similar situation when suggest + library_search were failing me, so some progress on me learning the naming conventions.

#### Scott Morrison (Oct 27 2020 at 01:56):

Julian Berman said:

but I can commit to memory to run

`{simp, library_search}`

instead next time I'm "stuck" if that's a decent idea?

You might try `hint`

.

#### Julian Berman (Oct 27 2020 at 02:01):

I have vague memories of you telling me that the last time I was stuck (and then following it up by saying `hint`

sometimes says silly things)

#### Julian Berman (Oct 27 2020 at 02:01):

But thanks probably good reminder, I forgot about `hint`

Last updated: May 16 2021 at 22:14 UTC