Zulip Chat Archive

Stream: new members

Topic: grasshopper problem


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

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 11:00):

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

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 11:00):

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

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

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 11:17):

I think they might even be finsets.

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

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 11:19):

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

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 11:20):

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

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 11:21):

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

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

view this post on Zulip Mario Carneiro (Mar 28 2020 at 11:25):

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

view this post on Zulip Miroslav Olšák (Mar 28 2020 at 11:26):

Maybe it jumps should be sets and mines multisets?

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

view this post on Zulip Mario Carneiro (Mar 28 2020 at 11:28):

looks like that will work, given your statement

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

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

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

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

view this post on Zulip Miroslav Olšák (Mar 28 2020 at 16:46):

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

view this post on Zulip Alex J. Best (Mar 28 2020 at 20:15):

finset.max

view this post on Zulip Miroslav Olšák (Mar 28 2020 at 20:56):

And then taking the set of remaining elements?

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

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

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

view this post on Zulip Alex J. Best (Mar 28 2020 at 21:12):

As for the remaining elements you could use finset.erase

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

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

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

view this post on Zulip Mario Carneiro (Mar 28 2020 at 23:30):

The update-mathlib script has been superceded by leanproject

view this post on Zulip Mario Carneiro (Mar 28 2020 at 23:31):

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

view this post on Zulip Mario Carneiro (Mar 28 2020 at 23:33):

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

view this post on Zulip Mario Carneiro (Mar 28 2020 at 23:34):

you can also use finset.card_pos

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

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 16:07):

Can you post a mwe?

view this post on Zulip Miroslav Olšák (Mar 29 2020 at 16:10):

mwe?

view this post on Zulip Miroslav Olšák (Mar 29 2020 at 16:11):

what does it mean?

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

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

view this post on Zulip Miroslav Olšák (Mar 29 2020 at 16:15):

OK, above the code I pasted is just

import data.finset

view this post on Zulip Miroslav Olšák (Mar 29 2020 at 16:15):

I want to replace the sorry by something else

view this post on Zulip Miroslav Olšák (Mar 29 2020 at 16:17):

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

view this post on Zulip Reid Barton (Mar 29 2020 at 16:20):

Simply by exact maxjump_in,

view this post on Zulip Miroslav Olšák (Mar 29 2020 at 16:22):

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

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

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

view this post on Zulip Miroslav Olšák (Mar 29 2020 at 16:29):

something like

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

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

view this post on Zulip Patrick Massot (Mar 29 2020 at 16:34):

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

view this post on Zulip Bryan Gin-ge Chen (Mar 29 2020 at 16:41):

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

view this post on Zulip Reid Barton (Mar 29 2020 at 16:43):

I was going to suggest the name check

view this post on Zulip Bryan Gin-ge Chen (Mar 29 2020 at 16:44):

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

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

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

view this post on Zulip Reid Barton (Mar 29 2020 at 16:46):

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

view this post on Zulip Reid Barton (Mar 29 2020 at 16:47):

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

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 16:47):

I believe this isn't possible currently

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 16:47):

I'm pretty sure I've tried it before

view this post on Zulip Patrick Massot (Mar 29 2020 at 16:47):

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

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 16:48):

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

view this post on Zulip Patrick Massot (Mar 29 2020 at 16:48):

That's what I thought...

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

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

view this post on Zulip Mario Carneiro (Mar 29 2020 at 21:49):

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

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

view this post on Zulip Mario Carneiro (Mar 30 2020 at 07:41):

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

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

view this post on Zulip Mario Carneiro (Mar 30 2020 at 07:42):

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

view this post on Zulip Miroslav Olšák (Mar 30 2020 at 07:43):

I see

view this post on Zulip Miroslav Olšák (Mar 30 2020 at 07:45):

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 18:38):

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 18:38):

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 18:39):

These lets are really hard to work with :-(

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 18:41):

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

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

view this post on Zulip Alex J. Best (Mar 30 2020 at 18:58):

Its actually prod_cons with a to_additive tag.

view this post on Zulip Alex J. Best (Mar 30 2020 at 18:59):

Which automatically turns lemmas about multiplicative things into additive versions.

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 19:39):

And then click to find out

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 22:22):

Is it called finset.card_image or image_card?

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 22:22):

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

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

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

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

view this post on Zulip Mario Carneiro (Mar 31 2020 at 01:49):

#2295

view this post on Zulip Kevin Buzzard (Mar 31 2020 at 07:28):

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

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

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

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

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

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 20:25):

It'll enable decidability for all propositions.

view this post on Zulip Patrick Massot (Apr 03 2020 at 20:38):

The modern way of saying that is open_locale classical

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

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

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

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

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

view this post on Zulip Alex J. Best (Apr 03 2020 at 21:07):

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

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

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

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

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

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

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

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

view this post on Zulip 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 card_union_add_card_inter,
  rw filter_union_filter_neg_eq,
  rw filter_inter_filter_neg_eq,
  rw card_empty,
  rw add_zero,
end

view this post on Zulip 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
  rw [card_union_add_card_inter, filter_union_filter_neg_eq, filter_inter_filter_neg_eq],
  simp,
end

view this post on Zulip 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
:=
by simp [card_union_add_card_inter, filter_union_filter_neg_eq, filter_inter_filter_neg_eq]

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 21:32):

cons_prefix is list.prefix_append

view this post on Zulip Miroslav Olšák (Apr 03 2020 at 21:34):

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

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

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 21:45):

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

view this post on Zulip Miroslav Olšák (Apr 03 2020 at 21:46):

But you cannot disect every proof into small lemmas.

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 21:46):

In some sense this is formally false

view this post on Zulip Miroslav Olšák (Apr 03 2020 at 21:46):

Not every proof is "Theory building"

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 21:46):

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

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

view this post on Zulip Miroslav Olšák (Apr 03 2020 at 21:47):

But I have to pass all the assumptions to it.

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 21:47):

yup

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

view this post on Zulip Miroslav Olšák (Apr 03 2020 at 21:47):

Alright, I can try to do it this way.

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

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

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 21:48):

Why not write the maths proof in the comments?

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 21:49):

Here is an unfinished proof of Zariski's lemma

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

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

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

view this post on Zulip Reid Barton (Apr 03 2020 at 22:05):

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

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

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

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

view this post on Zulip Scott Morrison (Apr 04 2020 at 02:59):

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


Last updated: May 08 2021 at 04:14 UTC