Zulip Chat Archive

Stream: new members

Topic: push_neg


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

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 18:16):

not exists is not definitionally equal to forall not.

view this post on Zulip Julian Berman (Oct 26 2020 at 18:16):

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

view this post on Zulip Julian Berman (Oct 26 2020 at 18:16):

(one using not exists)

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 18:17):

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

view this post on Zulip Julian Berman (Oct 26 2020 at 18:17):

Yeah sorry I mean the corresponding lemma to eq_bot_iff I guess

view this post on Zulip Mario Carneiro (Oct 26 2020 at 18:17):

the forall not formulation is preferred

view this post on Zulip Julian Berman (Oct 26 2020 at 18:17):

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

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

view this post on Zulip Julian Berman (Oct 26 2020 at 18:18):

Cool, thanks!

view this post on Zulip Mario Carneiro (Oct 26 2020 at 18:18):

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

view this post on Zulip Mario Carneiro (Oct 26 2020 at 18:18):

like "use x < y over y > x"

view this post on Zulip Julian Berman (Oct 26 2020 at 18:18):

nod

view this post on Zulip Mario Carneiro (Oct 26 2020 at 18:18):

it keeps the number of needed lemmas down

view this post on Zulip Julian Berman (Oct 26 2020 at 18:19):

Makes sense.

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 18:19):

simp converts not exists into forall not.

view this post on Zulip Mario Carneiro (Oct 26 2020 at 18:20):

which means by simp [eq_bot_iff] should also prove the theorem

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

view this post on Zulip Julian Berman (Oct 26 2020 at 18:22):

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

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

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

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 18:24):

Tactics have very well-defined domains

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

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

view this post on Zulip Mario Carneiro (Oct 26 2020 at 18:25):

it would be way too expensive to call simp on every lemma in the library

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

view this post on Zulip Julian Berman (Oct 26 2020 at 18:25):

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

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 18:25):

{simp, library_search} is one tactic

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

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

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 18:26):

non-terminal simps are evil

view this post on Zulip Mario Carneiro (Oct 26 2020 at 18:27):

it's fine for library_search since it's not going into mathlib

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

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

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

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

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

view this post on Zulip Julian Berman (Oct 26 2020 at 18:28):

(and/or knowing about it)

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 18:28):

none of those things

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 18:29):

I found it by typing eq_empty_iff and pressing ctrl-space

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 18:29):

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

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

view this post on Zulip Mario Carneiro (Oct 26 2020 at 18:30):

#naming

view this post on Zulip Julian Berman (Oct 26 2020 at 18:30):

thanks obviously each of these tips are super helpful

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

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

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

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

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

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