push_neg

Stream: new members

[Julian Berman]

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]

not exists is not definitionally equal to forall not.

[Julian Berman]

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

[Julian Berman]

(one using not exists)

[Kevin Buzzard]

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

[Julian Berman]

Yeah sorry I mean the corresponding lemma to eq_bot_iff I guess

[Mario Carneiro]

the forall not formulation is preferred

[Julian Berman]

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

[Julian Berman]

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

[Julian Berman]

Cool, thanks!

[Mario Carneiro]

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

[Mario Carneiro]

like "use x < y over y > x"

[Julian Berman]

nod

[Mario Carneiro]

it keeps the number of needed lemmas down

[Julian Berman]

Makes sense.

[Kevin Buzzard]

simp converts not exists into forall not.

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

PS by exact cancels :-)

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

[Julian Berman]

Maybe I'll ask then why library_search doesn't call simp first (or at least call it if it fails)

[Kevin Buzzard]

Tactics have very well-defined domains

[Kevin Buzzard]

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

[Julian Berman]

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]

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

[Julian Berman]

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]

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

[Kevin Buzzard]

{simp, library_search} is one tactic

[Julian Berman]

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]

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]

non-terminal simps are evil

[Mario Carneiro]

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

[Julian Berman]

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]

PS finset.eq_empty_iff_forall_not_mem is a thing, which is far closer to what you want

[Mario Carneiro]

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]

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

[Julian Berman]

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]

(and/or knowing about it)

[Kevin Buzzard]

none of those things

[Kevin Buzzard]

I found it by typing eq_empty_iff and pressing ctrl-space

[Kevin Buzzard]

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

[Julian Berman]

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

[Mario Carneiro]

#naming

[Julian Berman]

thanks obviously each of these tips are super helpful

[Kevin Buzzard]

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]

If eq_bot_iff is x = \bot \iff ... then it's not surprising that eq_empty_iff is what we want.

[Julian Berman]

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]

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]

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]

But thanks probably good reminder, I forgot about hint