## Stream: new members

### Topic: grasshopper problem

#### Miroslav Olšák (Mar 28 2020 at 10:41):

I am trying to prove the IMO problem 2009-6. It is basically a combinatorial problem about permuting a list of positive integers. I would like to do it according to my informal solution here http://www.olsak.net/mirek/grasshopper-informal. I think I managed to at least formulate the problem:

def list.part_sums : (list ℕ) → (list ℕ)
| []      := [0]
| (a::as) := 0::(as.part_sums.map (+ a))

theorem grasshopper :
forall jumps : list ℕ,
let size := jumps.sum in
forall mines : list ℕ,
( jumps.nodup ∧ mines.length < jumps.length ∧
(forall mine ∈ mines, 0 < mine ∧ mine < size) ∧
(forall jump ∈ jumps, 0 < jump))
→
exists jumps_l : list ℕ,
jumps ~ jumps_l ∧
forall jump ∈ jumps_l.part_sums, forall mine ∈ mines, jump ≠ mine
:= sorry


I tried to start writing a proof but it is in very early stages: http://www.olsak.net/mirek/grasshopper.lean, I am just running into difficulties...
In particular:

• One of the key steps in the proof is taking the maximum jump and keeping the rest of jumps without the maximum jump. But how to do it so that the following is as obvious as it should be:
• the remaining list (set) of jumps is one smaller than the original list of jumps
• all the jumps in the remaining list (set) of jumps are still different.
• after joining the biggest jump and a permutation of remaining jumps, we get a permutation of the original jumps.
• In the linked file I was thinking about resolving this issue by sorting the jumps first, and then just taking them from the beginning. But I don't like the approach very much, it resolves the "taking maximum" issue but I must keep track on sortedness.
• I guess there will be similar issues with taking the minimal mine in step B1 of the informal proof.
• I guess I will need to know that the sum does not depend on the permutation. Is it known by the library? I am not sure how to prove facts about permutations in general.
• Would it be better to work with integers rather than natural numbers? After all, I could get negative numbers in step 4 of the informal proof. This could be circumvented but is it worth the cost?
• Would it be better to define prefix sum directly as the sum of a prefix (I have done it inductively now)? Well, I use the fact that a prefix sum is a sum of a prefix in the informal proof in step B6.

Sorry for not progressing much, I just feel lost and I would like to do it in the right way. Perhaps it would help me to see a part of the proof with some hints about how to search in Lean library for the appropriate lemmata / tactics.

#### Kevin Buzzard (Mar 28 2020 at 11:00):

Is your finite set of jumps allowed to have repeats? Looking at informal question

#### Kevin Buzzard (Mar 28 2020 at 11:00):

Can you put a link to the official version of the question?

#### Kevin Buzzard (Mar 28 2020 at 11:05):

There is a whole bunch of facts about permutations of lists in something like data.list.perm

#### Kevin Buzzard (Mar 28 2020 at 11:06):

A multiset is a list up to permutation, so the definition of the sum of a multiset will somewhere have in it the fact that sum is constant over permutations

#### Mario Carneiro (Mar 28 2020 at 11:06):

I'm thinking, you could prove that the maximum jump is an element of the list, then use a theorem to prove jumps = l1 ++ maxjump :: l2 and use list perm theorems to swap maxjump to the front

#### Kevin Buzzard (Mar 28 2020 at 11:07):

Why not just sort the list? It's not as if you'll ever run the code

#### Mario Carneiro (Mar 28 2020 at 11:08):

It might be easier to work with multisets if you don't care about messing up the order of the remaining elements of the list

#### Mario Carneiro (Mar 28 2020 at 11:09):

because in that case the membership implies jumps = maxjump :: otherjumps and so it's already at the front, the rest is one less in size and so on

#### Kevin Buzzard (Mar 28 2020 at 11:17):

I think they might even be finsets.

#### Miroslav Olšák (Mar 28 2020 at 11:18):

Thank you for the responses.
Sets are for me (by definition) without repetition.
Link to original question: http://imo-official.org/problems/IMO2009SL.pdf, problem C7, variant 2.
Finsets sound reasonable, where can I find how to use finsets? How to express the fact that a list is an arrangement of a finset?

#### Kevin Buzzard (Mar 28 2020 at 11:19):

http://michaelnielsen.org/polymath1/index.php?title=Imo_2009_q6

#### Kevin Buzzard (Mar 28 2020 at 11:20):

Is there a module docstring in data/finset.lean?

#### Kevin Buzzard (Mar 28 2020 at 11:21):

Finset just means finite set. The jumps are distinct so a finset would work

#### Mario Carneiro (Mar 28 2020 at 11:25):

if s : finset A and l : list A, then s.1 = lsays that the underlying multiset of s agrees with l

#### Mario Carneiro (Mar 28 2020 at 11:25):

I'm not sure finsets are better than multisets here, though

#### Miroslav Olšák (Mar 28 2020 at 11:26):

Maybe it jumps should be sets and mines multisets?

#### Mario Carneiro (Mar 28 2020 at 11:26):

Even if they are without duplicates, if this isn't important or not easily true by definition there will be extra functions in the way erasing duplicates and such

#### Mario Carneiro (Mar 28 2020 at 11:28):

looks like that will work, given your statement

#### Miroslav Olšák (Mar 28 2020 at 11:29):

OK, I will try to rewrite the problem with finsets / multisets, by the way, what about the prefixes, is there a simple way for quantification over prefixes of a list?

#### Mario Carneiro (Mar 28 2020 at 11:30):

You can write it as a sum of a prefix like you said, but I'm not sure it's that much better

#### Mario Carneiro (Mar 28 2020 at 11:31):

import data.list.basic
#eval (list.inits [1,2,3]).map list.sum -- [0,1,3,6]


#### Miroslav Olšák (Mar 28 2020 at 12:16):

Second formulation, I will try the proving later.

theorem grasshopper :
forall n : ℕ,
forall jumps : finset ℤ,
(forall jump ∈ jumps, (0:ℤ) < jump) →
(jumps.card = n) →
let size := jumps.1.sum in
forall mines : multiset ℤ,
(mines.card < n) →
(forall mine ∈ mines, (0:ℤ) < mine ∧ mine < size)
→
exists jumps_l : list ℤ,
jumps.1 = jumps_l ∧
forall jumps_pref ∈ jumps_l.inits,
list.sum jumps_pref ∉ mines


#### Miroslav Olšák (Mar 28 2020 at 16:46):

What is the way for retrieving maximum from a finset / multiset?

#### Alex J. Best (Mar 28 2020 at 20:15):

finset.max

#### Miroslav Olšák (Mar 28 2020 at 20:56):

And then taking the set of remaining elements?

#### Miroslav Olšák (Mar 28 2020 at 20:57):

Sorry for stupid questions, is there a documentation that I could use instead of asking about every particular command?

#### Miroslav Olšák (Mar 28 2020 at 21:03):

Mario Carneiro said:

because in that case the membership implies jumps = maxjump :: otherjumps and so it's already at the front, the rest is one less in size and so on

I think this should be the answer but I don't understand how to obtain the otherjumps from it. How to write something like

let maxjump := jumps.max in
let otherjumps := SUCH THAT jumps = maxjump :: otherjumps in
...


#### Alex J. Best (Mar 28 2020 at 21:09):

No problem, this chat is for asking questions! So don't worry about it.
The doc for finset is here https://leanprover-community.github.io/mathlib_docs/data/finset.html .

#### Alex J. Best (Mar 28 2020 at 21:12):

As for the remaining elements you could use finset.erase

#### Kevin Buzzard (Mar 28 2020 at 22:24):

If you want to learn how to use blah's in lean then you kind of want to hope that blah.lean has got some documentation at the beginning. If it hasn't then you can do worse than just going through the file reading the definitions and theorem statements (but not the proofs)

#### Mario Carneiro (Mar 28 2020 at 22:31):

@Miroslav Olšák The theorem I was talking about was multiset.exists_cons_of_mem, which you can destruct to get otherjumps

#### Miroslav Olšák (Mar 28 2020 at 23:19):

Hm... I am just running into problems.

• jumps.max  is an option type, and I need to convince Lean that the maxjump really exist (because finset.card jumps = nat.succ n)
• When looking at how to prove that it actually exists, I noticed a slight difference between the mathlib version in the documentation and the version I have on my computer. In particular, I don't have the predicate finset.nonempty, and there is used just s ≠ ∅ instead. I tried to run mathlib-update but without effect. The update looks unnecessary for now but I would preffer to have an up to date library. After trying the update-mathlib script a few times (without effect), it is complaining about "Github API rate limit exceeded." :-/
• I will need to know that maxjump ∈ jumps. This should be possible to accomplish using finset.mem_of_max but how to translate it to the fact that maxjump ∈ jumps.1 to use multiset.exists_cons_of_mem?

By the way, I know I can read the sources, which I usually do, I just hoped for a better way. However, the documentation does not seem much different from the sources after all.

#### Mario Carneiro (Mar 28 2020 at 23:30):

The update-mathlib script has been superceded by leanproject

#### Mario Carneiro (Mar 28 2020 at 23:31):

maxjump ∈ jumps and maxjump ∈ jumps.1 should be defeq

#### Mario Carneiro (Mar 28 2020 at 23:33):

You can prove jumps ≠ ∅ (or jumps.nonempty) by contradiction: if jumps = ∅ then finset.card jumps = 0

#### Mario Carneiro (Mar 28 2020 at 23:34):

you can also use finset.card_pos

#### Miroslav Olšák (Mar 29 2020 at 16:05):

I still don't get how to prove maxjump ∈ jumps.1 from maxjump ∈ jumps (maxjump_in_ms from maxjump_in). I managed to get the maximum in the end, but I am not sure if it is the standard way. Here is my testing code.

example :
forall n : ℕ,
forall jumps : finset ℤ,
jumps.card = n.succ →
jumps = jumps -- irrelevant corollary, just for testing
:=
begin
intros,
have : 0 < jumps.card, by simp [a],
have : jumps.nonempty, by exact finset.card_pos.elim_left this,
cases finset.max_of_nonempty this with maxjump maxjump_ex,
have maxjump_in : maxjump ∈ jumps, by exact finset.mem_of_max maxjump_ex,
have maxjump_in_ms : maxjump ∈ jumps.1, sorry,
cases multiset.exists_cons_of_mem maxjump_in_ms with otherjumps otherjumps_ex,
refl -- proving the irrelevant corollary
end


#### Kevin Buzzard (Mar 29 2020 at 16:07):

Can you post a mwe?

mwe?

#### Miroslav Olšák (Mar 29 2020 at 16:11):

what does it mean?

#### Bryan Gin-ge Chen (Mar 29 2020 at 16:14):

MWE = minimal working example. Basically, include all the parts of your file needed (imports, other definitions) so that we can copy+paste it into our editors and see the same thing as you.

#### Kevin Buzzard (Mar 29 2020 at 16:14):

Minimum working example so I can just cut and paste and see your problem on my computer

#### Miroslav Olšák (Mar 29 2020 at 16:15):

OK, above the code I pasted is just

import data.finset


#### Miroslav Olšák (Mar 29 2020 at 16:15):

I want to replace the sorry by something else

#### Miroslav Olšák (Mar 29 2020 at 16:17):

I could make it more minimal, I guess, if it will help.

#### Reid Barton (Mar 29 2020 at 16:20):

Simply by exact maxjump_in,

#### Miroslav Olšák (Mar 29 2020 at 16:22):

It works... Hm, I really thought I tried that.

#### Miroslav Olšák (Mar 29 2020 at 16:25):

By the way, would it be possible to somehow use it directly in multiset.exists_cons_of_mem?

#### Miroslav Olšák (Mar 29 2020 at 16:27):

And I have one more debugging question. Sometimes, I would like to check a type of an expression in the current context but #check appears to not have access to the proving context. Is there another way?

#### Miroslav Olšák (Mar 29 2020 at 16:29):

something like

example (n : ℕ) : n = n
:=
begin
#check n
end


#### Reid Barton (Mar 29 2020 at 16:32):

#check is a top-level command. You could try something like have temp := n, then look at the tactic state for the type of temp

#### Patrick Massot (Mar 29 2020 at 16:34):

We should have a tactic to do that, this is a very reasonable question.

#### Bryan Gin-ge Chen (Mar 29 2020 at 16:41):

@Scott Morrison recently added show_term, so maybe we should add show_type.

#### Reid Barton (Mar 29 2020 at 16:43):

I was going to suggest the name check

#### Bryan Gin-ge Chen (Mar 29 2020 at 16:44):

Oh, then we could rename show_term to print, which surprisingly isn't taken.

#### Kevin Buzzard (Mar 29 2020 at 16:45):

These are great ideas. I know tricks now but when I was a beginner I was always wanting these kinds of things

#### Kevin Buzzard (Mar 29 2020 at 16:45):

I even wanted this today but just put pp.all on and read what I wanted from the output. Imagine trying to tell a beginner to do that

#### Reid Barton (Mar 29 2020 at 16:46):

show_term doesn't really align with print in quite the same way, though.

#### Reid Barton (Mar 29 2020 at 16:47):

Now I wonder, is it possible to run set_option from inside a tactic?

#### Kevin Buzzard (Mar 29 2020 at 16:47):

I believe this isn't possible currently

#### Kevin Buzzard (Mar 29 2020 at 16:47):

I'm pretty sure I've tried it before

#### Patrick Massot (Mar 29 2020 at 16:47):

Kevin, Reid means "from inside a tactic", not "from a tactic block"

#### Kevin Buzzard (Mar 29 2020 at 16:48):

In which case I retract my assertion about having tried it before

#### Patrick Massot (Mar 29 2020 at 16:48):

That's what I thought...

#### Reid Barton (Mar 29 2020 at 16:49):

Right, I mean can we write a tactic which is a substitute for the top-level command set_option (and presumably would set an option only for the remainder of the current definition... I'm not really sure how much sense this idea makes).

#### Patrick Massot (Mar 29 2020 at 16:50):

If the only goal is to set pp options then I'm sure the meta function can take relevant arguments, without going through the set_option machinery

#### Mario Carneiro (Mar 29 2020 at 21:49):

I think there is; look for uses of the options structure

#### Miroslav Olšák (Mar 30 2020 at 07:38):

What am I doing wrong?

import data.finset
example (X:finset ℤ) : (finset ℤ)
:= finset.map (λ(x:ℤ), x-(5:ℤ))) X


Gives error

type mismatch at application
finset.map (λ (x : ℤ), x - 5)
term
λ (x : ℤ), x - 5
has type
ℤ → ℤ : Type
but is expected to have type
?m_1 ↪ ?m_2 : Type (max ? ?)


Note that with multisets it works just fine.

example (X:multiset ℤ) : (multiset ℤ)
:= multiset.map (λ(x:ℤ), x-(5:ℤ)) X


#### Mario Carneiro (Mar 30 2020 at 07:41):

finset.map takes an embedding, which is an injective function

#### Mario Carneiro (Mar 30 2020 at 07:42):

if you don't care about having to deduplicate the list afterward, possibly changing the size of the set, then use finset.image instead

#### Mario Carneiro (Mar 30 2020 at 07:42):

(notice that the arrow in the error message is hooked, that's not a regular arrow)

I see

#### Miroslav Olšák (Mar 30 2020 at 07:45):

well, it is a bijection, but I think finset.image will be simpler here

#### Miroslav Olšák (Mar 30 2020 at 07:57):

Now, I want to split a finset (mines) into two parts according to whether the element is smaller than maxjump or not. I am thinking of constructing them using finset.filter, proving that the parts are disjoint, that their union is the original mines, and finaly proving that the sum of the sizes of the two parts is equal to mines.card using finset.card_union_add_card_inter. Is there a more straightforward way for partitioning a finset (and keeping track on its size)?

#### Mario Carneiro (Mar 30 2020 at 08:16):

I think these should have you covered:

theorem filter_union_filter_neg_eq (s : finset α) : s.filter p ∪ s.filter (λa, ¬ p a) = s :=
by simp only [filter_not, union_sdiff_of_subset (filter_subset s)]

theorem filter_inter_filter_neg_eq (s : finset α) : s.filter p ∩ s.filter (λa, ¬ p a) = ∅ :=
by simp only [filter_not, inter_sdiff_self]


#### Miroslav Olšák (Mar 30 2020 at 17:19):

Now, I am trying to prove a basic fact about the remaining jumps. However, I am not sure how to relate the fact jumps.val = maxjump :: jumps_res.val to the sum of a multiset. Actually, I don't even understand where the multiset.sum comes from and how to handle setoids. MWE:

example :
∀ maxjump : ℤ,
∀ jumps : finset ℤ,
∀ jumps_res : finset ℤ,
let size := jumps.val.sum in
let size_res := jumps_res.val.sum in
jumps.val = maxjump :: jumps_res.val →
size_res = size - maxjump
:=
begin
intros,
sorry,
end


#### Kevin Buzzard (Mar 30 2020 at 18:38):

You are going to need a lemma which says multiset.sum (a :: L) = a + multiset.sum L

#### Kevin Buzzard (Mar 30 2020 at 18:38):

and you should be able to find that in multiset.lean, soon after sum is defined.

#### Kevin Buzzard (Mar 30 2020 at 18:38):

and it will be called something like multiset.sum_cons if it's there

#### Kevin Buzzard (Mar 30 2020 at 18:39):

These lets are really hard to work with :-(

#### Kevin Buzzard (Mar 30 2020 at 18:41):

import data.finset
import tactic

example :
∀ maxjump : ℤ,
∀ jumps : finset ℤ,
∀ jumps_res : finset ℤ,
let size := jumps.val.sum in
let size_res := jumps_res.val.sum in
jumps.val = maxjump :: jumps_res.val →
size_res = size - maxjump
:=
begin
intros,
show multiset.sum jumps_res.val = multiset.sum jumps.val - maxjump,
rw a,
rw multiset.sum_cons,
ring,
end


#### Kevin Buzzard (Mar 30 2020 at 18:41):

Note that I guessed the name of the lemma you wanted without knowing anything about multisets.

#### Miroslav Olšák (Mar 30 2020 at 18:52):

Well, it was tricky because multiset.sum_cons is not directly defined in multiset.lean. Then one have to just guess a name and hope...

#### Alex J. Best (Mar 30 2020 at 18:58):

Its actually prod_cons with a to_additive tag.

#### Miroslav Olšák (Mar 30 2020 at 19:05):

Ah, it is "hidden" in the source code but listed in the docs. I guess, I should use the docs more :-).

#### Kevin Buzzard (Mar 30 2020 at 19:18):

If you are working with multiset then you should look at every definition of the form multiset.X and read the statement of every theorem of the form multiset.X. Then you will have a feeling for how to use multisets.

#### Kevin Buzzard (Mar 30 2020 at 19:19):

Don't worry about reading the proofs though. The proofs are irrelevant -- in fact every theorem you see will be of a trivial nature and you will be able to prove it in your head.

#### Kevin Buzzard (Mar 30 2020 at 19:19):

The idea is that you should prove harder theorems about multisets using the basic results supplied to you by the library.

#### Kevin Buzzard (Mar 30 2020 at 19:23):

My instinct is that you should start by looking through multiset.lean and then skim through the docs.

#### Kevin Buzzard (Mar 30 2020 at 19:24):

This is currently the canonical way to learn multisets. I actually printed out multiset.lean when I was learning, and used to browse through it from time to time. Don't worry about the proofs though.

#### Miroslav Olšák (Mar 30 2020 at 19:27):

Yes, however looking at multiset.lean was not much helpful in this case (which is basically why I struggled with it). Just later I realized that the docs could help (although they originally seemed to me almost identical to the source code).

#### Kevin Buzzard (Mar 30 2020 at 19:28):

I was just looking through the lean file again. I agree it's very difficult to read. There are a whole bunch of trivial things which are set up which just look confusing and are mathematically irrelevant. Maybe the docs are easier to read?

#### Kevin Buzzard (Mar 30 2020 at 19:29):

As I'm sure you realise, multiset.card is the definition, and then multiset.card_join etc are the theorems.

#### Kevin Buzzard (Mar 30 2020 at 19:39):

Having looked at the docs I think the most sensible approach to learn how to use multisets is to read all the definitions and then just glance through some of the theorems to get an idea of what is there. An interesting game which would teach you something would be to read the definition then take a look at some of the theorem names and guess what the statement of the theorem is

#### Kevin Buzzard (Mar 30 2020 at 19:39):

And then click to find out

#### Miroslav Olšák (Mar 30 2020 at 21:42):

Mario Carneiro said:

if you don't care about having to deduplicate the list afterward, possibly changing the size of the set, then use finset.image instead

I don't care about possible shrinking of the set, however, I cannot find even a lemma for inequality:

lemma card_image_le (s : finset ℤ) (f : ℤ → ℤ) : (finset.image f s).card ≤ s.card


Is there something like that? If not, proving injectivity will be probably easier.

#### Kevin Buzzard (Mar 30 2020 at 22:22):

Is it called finset.card_image or image_card?

#### Kevin Buzzard (Mar 30 2020 at 22:22):

It seems like the sort of thing which would be in the library

#### Kevin Buzzard (Mar 30 2020 at 22:29):

Yeah you're right, I can't find it in the docs. You should change int to a general type alpha and post in #maths with a title such as finset.card_image_le and see if you can get someone to fill it in

#### Miroslav Olšák (Mar 30 2020 at 22:39):

@Mario Carneiro could probably tell us. I guess it could be proved using multiset.card_le_of_le and multiset.erase_dup_le but it is not worth it in my case since equality can be handled more easily, and my f is just a subtraction of a constant.

#### Mario Carneiro (Mar 31 2020 at 01:24):

import data.finset

namespace multiset
theorem to_finset_card_le {α} [decidable_eq α] (m : multiset α) : m.to_finset.card ≤ m.card :=
card_le_of_le (erase_dup_le _)
end multiset

namespace finset
open multiset
theorem card_image_le {α β} [decidable_eq β] {f : α → β} {s : finset α} : card (image f s) ≤ card s :=
by simpa only [multiset.card_map] using (s.1.map f).to_finset_card_le
end finset


#2295

#### Kevin Buzzard (Mar 31 2020 at 07:28):

Isn't it amazing how these people can get the proofs onto one line?

#### Kevin Buzzard (Mar 31 2020 at 20:16):

@Miroslav Olšák this has now been merged so if you update your project with leanproject up then you will have access to finset.card_image_le.

#### Miroslav Olšák (Apr 02 2020 at 10:59):

So I have written the "trivial case" of the Grasshopper problem: https://github.com/mirefek/my-lean-experiments/blob/master/grasshopper.lean. Suggestions are welcomed.

#### Miroslav Olšák (Apr 03 2020 at 20:22):

Now, I tried a different IMO problem, and I think I have some issues with "decidability". Universal quantivifacion on arrays seems not to have the decidable type class, while it works with lists... Is there a reason for that, or is it some sort of bug?

example (seq : list ℕ) : decidable (∀ l ∈ seq, true)
:= by apply_instance -- works
example (seq : array 5 ℕ) : decidable (∀ l ∈ seq, true)
:= by apply_instance -- error


And by the way, could I just tell Lean that I don't care about decidability because I work in classical logic, so that it will not miss any decidable predicate anywhere?

#### Ryan Lahfa (Apr 03 2020 at 20:24):

Miroslav Olšák said:

Now, I tried a different IMO problem, and I think I have some issues with "decidability". Universal quantivifacion on arrays seems not to have the decidable type class, while it works with lists... Is there a reason for that, or is it some sort of bug?

example (seq : list ℕ) : decidable (∀ l ∈ seq, true)
:= by apply_instance -- works
example (seq : array 5 ℕ) : decidable (∀ l ∈ seq, true)
:= by apply_instance -- error


And by the way, could I just tell Lean that I don't care about decidability because I work in classical logic, so that it will not miss any decidable predicate anywhere?

What you want is local attribute [instance] classical.prop_decidable I believe in your file.

#### Ryan Lahfa (Apr 03 2020 at 20:25):

It'll enable decidability for all propositions.

#### Patrick Massot (Apr 03 2020 at 20:38):

The modern way of saying that is open_locale classical

#### Patrick Massot (Apr 03 2020 at 20:38):

(Beware this cannot be written right after the import because the parser doesn't know open_locale is not the name of a file to import)

#### Kevin Buzzard (Apr 03 2020 at 20:54):

Miroslav Olšák said:

So I have written the "trivial case" of the Grasshopper problem: https://github.com/mirefek/my-lean-experiments/blob/master/grasshopper.lean. Suggestions are welcomed.

Your

lemma lt_of_le_ne (a b : ℤ) (h1 : a ≤ b) (h2 : a ≠ b) : (a < b)


-- you are thinking about things the wrong way. This is a standard fact, therefore it's in the library, but you are a newcomer so you don't know all the naming conventions. So how do you find it? Answer: := by library_search, which tells you that this is already there, and is called lt_of_le_of_ne (note the naming convention :-) )

#### Miroslav Olšák (Apr 03 2020 at 20:55):

Can I also get rid of the warnings that I am using classical logic? By the way, open_locale classical works better because it puts the warning only where it actually needs classical. The other option, local attribute [instance] classical.prop_decidable, puts these warnings almost everywhere.

#### Kevin Buzzard (Apr 03 2020 at 20:56):

Just put

noncomputable theory
open_locale classical


at the top of your file and you should never get any warnings about constructive or computable issues.

#### Miroslav Olšák (Apr 03 2020 at 21:04):

Oh, library_search is interesting, no idea how it works. It told me that injectivity of subtraction can be proved from λ {b c_1 : ℤ}, (add_right_inj (-c)).mp

#### Alex J. Best (Apr 03 2020 at 21:07):

Its amazing, definitely my most used non-core tactic. But sometimes the terms are ... interesting

#### Alex J. Best (Apr 03 2020 at 21:07):

There is an option to view several suggestions I believe, so that maybe the second or third is better

#### Kevin Buzzard (Apr 03 2020 at 21:12):

lemma finset_rest {s : finset ℤ} {x : ℤ} (x_in_s : x ∈ s) :
∃ r : finset ℤ, s.val = x::r.val
:=


My guess is that you should not be proving this lemma. We already have the function you want -- and better, it's not some abstract existence statement, it's concrete. It's called finset.erase s x, and just after its definition there are 19 theorems proved about it. You are breaking the interface by starting to talk about multisets -- as a mathematician you should not really need to look at s.val for s a finset.

#### Alex J. Best (Apr 03 2020 at 21:13):

Maybe now this is the suggest tactic instead of an option for library search im thinking of.

#### Kevin Buzzard (Apr 03 2020 at 21:15):

Similarly do you really need finset_cons_subset? Why is finset.subset_insert not enough for you? This is the version of the lemma you want within the finset interface.

#### Alex J. Best (Apr 03 2020 at 21:16):

Indeed running def aa (a b c :ℤ ) (h : a -b = c -b): a = c := by suggest 50 the second result is the one you would probably have wanted sub_right_inj.mp h

#### Miroslav Olšák (Apr 03 2020 at 21:17):

hm, my prefix_eq_head seems to not be findable by library search even in a more basic form, even though it is kind of dual to existing list.prefix_cons_inj

#### Miroslav Olšák (Apr 03 2020 at 21:22):

I cannot really avoid multisets entirely, jumps.1 = jumps_l does not work wthout the .1.
Using multiset.exists_cons_of_mem was suggested by @Mario Carneiro for the task of being aware that when I order the smaller set to a list, and append the erased element, the result will be an ordering of the original finset.

#### Kevin Buzzard (Apr 03 2020 at 21:27):

theorem sum_filter_split {p : ℤ → Prop} [decidable_pred p] (s : finset ℤ) :
s.card = (s.filter p).card + (s.filter (λa, ¬ p a)).card
:=
begin
let s1 := s.filter p,
let s2 := s.filter (λa, ¬ p a),
have inter_empty : s1 ∩ s2 = ∅,
by exact finset.filter_inter_filter_neg_eq s,
have union_full : s1 ∪ s2 = s,
by exact finset.filter_union_filter_neg_eq s,
have : (s1 ∪ s2).card + (s1 ∩ s2).card = s1.card + s2.card,


let let have have have. You are thinking forwards. Lean's proofs come out much better if you write them backwards. All the lemmas you need to prove sum_filter_split are already in mathlib.

open finset

theorem sum_filter_split {p : ℤ → Prop} [decidable_pred p] (s : finset ℤ) :
s.card = (s.filter p).card + (s.filter (λa, ¬ p a)).card
:=
begin
rw filter_union_filter_neg_eq,
rw filter_inter_filter_neg_eq,
rw card_empty,
end


#### Kevin Buzzard (Apr 03 2020 at 21:29):

Those last two lemmas are tagged with simp so

theorem sum_filter_split {p : ℤ → Prop} [decidable_pred p] (s : finset ℤ) :
s.card = (s.filter p).card + (s.filter (λa, ¬ p a)).card
:=
begin
simp,
end


#### Kevin Buzzard (Apr 03 2020 at 21:30):

and then finally

theorem sum_filter_split {p : ℤ → Prop} [decidable_pred p] (s : finset ℤ) :
s.card = (s.filter p).card + (s.filter (λa, ¬ p a)).card
:=


#### Kevin Buzzard (Apr 03 2020 at 21:32):

cons_prefix is list.prefix_append

#### Miroslav Olšák (Apr 03 2020 at 21:34):

How do you do it that you don't write the finset. prefixes? open finset?

#### Kevin Buzzard (Apr 03 2020 at 21:36):

lemma l_nonneg_sum {l : list ℤ} (h1 : ∀ x ∈ l, (0:ℤ) < x)
: l.sum ≥ 0


The data type with all the juicy lemmas about sums is finset. Do you really need sums of lists? Note that this lemma is suboptimal in the sense that h1 should demand 0 \le x not 0 < x.

#### Kevin Buzzard (Apr 03 2020 at 21:37):

Note that we already have finset.sum_nonneg. Given that you don't care about the order of summation it feels to me that you could/should be using multisets or finsets here.

#### Miroslav Olšák (Apr 03 2020 at 21:42):

The lemma l_nonneg_sum is carefully chosen to suit pref_nonneg_sum, which I need later. It is mostly about lists, although it originates from a finset at the beginning. And yes, it is something I found rather annoying, I would like Lean to realize it somewhat automatically but I am not sure if it is possible.

#### Kevin Buzzard (Apr 03 2020 at 21:42):

And in some sense the most important comment: I definitely would not start formalising grasshopper like that on line 150 or so, and just launching into some huge proof. Look at the development of finset.lean. 99% of the proofs are just a couple of lines long. That's the style you should be aiming for. Those earlier lemmas in your file -- there are sometimes better proofs but at least your proofs are short. If you start writing some huge proof then when you get to the heart of the matter you will find that you have to wait 5 seconds after every keystroke while Lean recompiles your entire lemma again.

However this slowdown might not have happened to you yet, and it's a very "mathematician" thing to do -- launch into the proof and just start dealing with the issues as they arise rather than factoring them out -- so if you think it's the best way to get you to a proof then go for it :-)

#### Kevin Buzzard (Apr 03 2020 at 21:44):

Your first sorry has as a goal

⊢ ∃ (jumps_l : list ℤ),
jumps.val = ↑jumps_l ∧
∀ (jumps_pref : list ℤ), jumps_pref ∈ list.inits jumps_l → list.sum jumps_pref ∉ mines


I see -- you are using lists to order the finsets. Maybe you do have to work with lists too. But there are a lot of lemmas about lists :-)

#### Miroslav Olšák (Apr 03 2020 at 21:45):

You are right, I am running into issues with speed which is annoying and slowing me down.

#### Kevin Buzzard (Apr 03 2020 at 21:45):

It is a very common issue I see at the Xena project.

#### Miroslav Olšák (Apr 03 2020 at 21:46):

But you cannot disect every proof into small lemmas.

#### Kevin Buzzard (Apr 03 2020 at 21:46):

In some sense this is formally false

#### Miroslav Olšák (Apr 03 2020 at 21:46):

Not every proof is "Theory building"

#### Kevin Buzzard (Apr 03 2020 at 21:46):

because every have you write in your proof can be factored out as a sublemma.

#### Kevin Buzzard (Apr 03 2020 at 21:47):

I'm not saying the lemmas have to be interesting. They can have names like grasshoper_aux_3

#### Miroslav Olšák (Apr 03 2020 at 21:47):

But I have to pass all the assumptions to it.

yup

#### Kevin Buzzard (Apr 03 2020 at 21:47):

but I have seen students proving the same thing three times because they cannot be bothered to factor out a lemma.

#### Miroslav Olšák (Apr 03 2020 at 21:47):

Alright, I can try to do it this way.

#### Kevin Buzzard (Apr 03 2020 at 21:47):

In fact you don't have to pass all the assumptions to it, just all the ones you use.

#### Kevin Buzzard (Apr 03 2020 at 21:48):

This way it becomes easier to analyse what is going on. People don't like reading large proofs either, they are hard to follow, especially if they don't have any comments like yours don't.

#### Kevin Buzzard (Apr 03 2020 at 21:48):

Why not write the maths proof in the comments?

#### Kevin Buzzard (Apr 03 2020 at 21:49):

Here is an unfinished proof of Zariski's lemma

#### Kevin Buzzard (Apr 03 2020 at 21:50):

I am in the middle of writing it, but I am writing comments everywhere so it reads just like a maths proof.

#### Miroslav Olšák (Apr 03 2020 at 22:03):

I am used to try to avoid repetition from programming, at least when it seems reasonable. But it still felt better to prove the lemmata inside the proving context since I have access to objects which stay mostly constant during the proof.

#### Reid Barton (Apr 03 2020 at 22:05):

If you have a lot of objects which stay constant during a big proof then parameters is useful.

#### Reid Barton (Apr 03 2020 at 22:05):

You don't see it in mathlib because mathlib mostly doesn't contain big proofs.

#### Scott Morrison (Apr 04 2020 at 02:47):

Or just use variables. I prefer that to parameters, mostly. You still have to pass the arguments when calling functions, but you don't need to write the arguments as hypotheses of lemmas (which is the more verbose part, as you'd need to write the types). I think it's a feature that you still need to pass the arguments, as it keeps me from getting confused about what depends on what.

#### Reid Barton (Apr 04 2020 at 02:51):

It can easily be like 5x as verbose to pass the arguments though. I guess one thing that could help would be to pack everything into a structure.

#### Reid Barton (Apr 04 2020 at 02:52):

I don't know how I would have done something like https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/homotopy_theory/topological_spaces/pushout_lemmas.lean#L163 without parameters.

#### Scott Morrison (Apr 04 2020 at 02:59):

... on the subject of that repository ...?

Last updated: May 08 2021 at 04:14 UTC