grasshopper problem

Stream: new members

[Miroslav Olšák]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

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]

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]

I think they might even be finsets.

[Miroslav Olšák]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Miroslav Olšák]

Maybe it jumps should be sets and mines multisets?

[Mario Carneiro]

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]

looks like that will work, given your statement

[Miroslav Olšák]

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]

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]

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

[Miroslav Olšák]

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]

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

[Alex J. Best]

finset.max

[Miroslav Olšák]

And then taking the set of remaining elements?

[Miroslav Olšák]

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

[Miroslav Olšák]

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]

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]

As for the remaining elements you could use finset.erase

[Kevin Buzzard]

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]

@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]

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]

The update-mathlib script has been superceded by leanproject

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

you can also use finset.card_pos

[Miroslav Olšák]

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]

Can you post a mwe?

[Miroslav Olšák]

mwe?

[Miroslav Olšák]

what does it mean?

[Bryan Gin-ge Chen]

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]

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

[Miroslav Olšák]

OK, above the code I pasted is just

import data.finset

[Miroslav Olšák]

I want to replace the sorry by something else

[Miroslav Olšák]

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

[Reid Barton]

Simply by exact maxjump_in,

[Miroslav Olšák]

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

[Miroslav Olšák]

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

[Miroslav Olšák]

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]

something like

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

[Reid Barton]

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

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

[Bryan Gin-ge Chen]

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

[Reid Barton]

I was going to suggest the name check

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Reid Barton]

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

[Kevin Buzzard]

I believe this isn't possible currently

[Kevin Buzzard]

I'm pretty sure I've tried it before

[Patrick Massot]

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

[Kevin Buzzard]

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

[Patrick Massot]

That's what I thought...

[Reid Barton]

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]

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]

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

[Miroslav Olšák]

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]

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

[Mario Carneiro]

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]

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

[Miroslav Olšák]

I see

[Miroslav Olšák]

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

[Miroslav Olšák]

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]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

These lets are really hard to work with :-(

[Kevin Buzzard]

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]

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

[Miroslav Olšák]

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]

Its actually prod_cons with a to_additive tag.

[Alex J. Best]

Which automatically turns lemmas about multiplicative things into additive versions.

[Miroslav Olšák]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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]

And then click to find out

[Miroslav Olšák]

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]

Is it called finset.card_image or image_card?

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

@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]

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

[Mario Carneiro]

#2295

[Kevin Buzzard]

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

[Kevin Buzzard]

@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]

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]

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]

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]

It'll enable decidability for all propositions.

[Patrick Massot]

The modern way of saying that is open_locale classical

[Patrick Massot]

(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]

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]

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]

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]

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]

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

[Alex J. Best]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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 ←card_union_add_card_inter,
  rw filter_union_filter_neg_eq,
  rw filter_inter_filter_neg_eq,
  rw card_empty,
  rw add_zero,
end

[Kevin Buzzard]

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
  rw [←card_union_add_card_inter, filter_union_filter_neg_eq, filter_inter_filter_neg_eq],
  simp,
end

[Kevin Buzzard]

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
:=
by simp [←card_union_add_card_inter, filter_union_filter_neg_eq, filter_inter_filter_neg_eq]

[Kevin Buzzard]

cons_prefix is list.prefix_append

[Miroslav Olšák]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Miroslav Olšák]

But you cannot disect every proof into small lemmas.

[Kevin Buzzard]

In some sense this is formally false

[Miroslav Olšák]

Not every proof is "Theory building"

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Miroslav Olšák]

But I have to pass all the assumptions to it.

[Kevin Buzzard]

yup

[Kevin Buzzard]

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

[Miroslav Olšák]

Alright, I can try to do it this way.

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Why not write the maths proof in the comments?

[Kevin Buzzard]

Here is an unfinished proof of Zariski's lemma

[Kevin Buzzard]

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]

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]

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

[Reid Barton]

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

[Scott Morrison]

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]

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]

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]

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