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

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"

nod

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

it keeps the number of needed lemmas down

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?

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

#naming

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