Imo1970 p4

[picrin]

Hi David,

Please see below a formalisation of Imo1970 p4.

The formalisation follows the first solution from the Art of Problem Solving.

Could I suggest that for the review we use the pull request workflow (as opposed to the rebase workflow) -- it would be helpful if you could put comments in the pull request, and I can then fix the problems (and learn in the process). It will take a bit more time, but I think will help us maintain high quality codebase.

As it stands the solution takes ~20 seconds to compile, but as it's quite modular with many small lemmas, it could be optimised on a per-lemma basis. My aim just now was to get everything to typcheck, so some lemmas contain repetitive code, etc...

[dwrensha]

As it stands the solution takes ~20 seconds to compile

Do you know where it's spending the bulk of that time? set_option trace.profiler true in ... breaks things down by tactic.

[picrin]

As it stands the solution takes ~20 seconds to compile

Do you know where it's spending the bulk of that time? set_option trace.profiler true in ... breaks things down by tactic.

I love this option, I can see exactly which functions are slow.

At first sight it looks like ~10% of time is spent in the function that counts even numbers in the interval. I think I can actually probably remove that function altogether I found a better proof later on (counting odd numbers), and I think I can just refactor the code to use that.

[picrin]

I did manage to shave off ~2 seconds from compile time by factroing out the inefficient implementation of exactly_three_odd_numbers, which I found using:

set_option trace.profiler.threshold 1000

set_option trace.profiler true

Before:

10.416134 seconds spent on the following 5 lemmas:

[2.179035] lemma exactly_three_even_numbers
[2.334081] lemma odd_props (n : ℕ) (odd_s : Finset ℕ)
[2.813783] lemma unique_divisor (n : ZMod 3) (a b c : ℕ)
[1.967515] lemma subsets_must_overlap_pigeonhole (s s1 s2 : Finset ℕ) (predicate_s1 : ℕ → Prop)
[1.121720] lemma contradiction_of_finset_icc_1_6 (s1 s2 : Finset ℕ)

After:

8.30901 seconds spent on the following 4 lemmas:

[2.434758] lemma odd_props (n : ℕ)
[2.859301] lemma unique_divisor
[1.896200] lemma subsets_must_overlap_pigeonhole
[1.118751] lemma contradiction_of_finset_icc_1_6

(the reimplementation uses a fraction of a second to implement the lemma piggy-backing on odd_props, which is already pretty efficient and needed somewhere else anyway)

[picrin]

Is there any way to manually check if the website looks good locally? I can see that the CI builds the website, but not sure if that's something that can be tested locally.

[dwrensha]

Is there any way to manually check if the website looks good locally?

lake exe buildWebpage

and then open _site/index.html in a browser.

[picrin]

The website entry does look good locally, but when I press problem statement only or complete solution no code appears in the lean viewer (which may be expected locally, I don't know):

[dwrensha]

but when I press problem statement only or complete solution no code appears in the lean viewer

That's expected.

[dwrensha]

You can collapse these intros to a single line:

    intro s3 rel1 rel2 a a_in_s3

[dwrensha]

For future-proofing, non-terminal simp invocations should be turned into simp only. You can do this by changing into simp? and then accepting the suggestion in the infoview.

[picrin]

I've fixed this in this instance, and all the other instances.

[dwrensha]

A fancier way to do this is:

obtain rfl | rfl | rfl | rfl | rfl | rfl := k_in_explicit_s2 <;> contradiction

[picrin]

What does this code do though? I don't really understand it.

If I did understand it, I think the question for me would be if it's better style than:

cases k_in_explicit_s2 with
      | inl h =>
        subst h
        contradiction
      | inr h_1 =>
        cases h_1 with
        | inl h =>
          subst h
          contradiction
        | inr h_2 =>
          cases h_2 with
          | inl h =>
            subst h
            contradiction
          | inr h_1 =>
            cases h_1 with
            | inl h =>
              subst h
              contradiction
            | inr h_2 =>
              subst h_2
              contradiction

The latter uses very standard idioms (at the cost of some repetition) and is easier to read than the former.

I've put the golfed version in for now, but personally I tend to prefer code that's easy to read over code that's easy to write.

This might be different in the world of tactic-based theorem provers, as tactic-based programs are infamously difficult to read anyway (I think one pretty much has to read them with compiler in hand).

What do you think David?

[dwrensha]

Ah, oops --- I noticed just now that I put one too many rfls in there. The last one is not needed.

My thought process here was as follows:

First, we can use obtain with its pattern syntax to flatten the case analysis:

      obtain h | h_1 | h_2 | h_1 | h := k_in_explicit_s2
      · subst h
        contradiction
      · subst h_1
        contradiction
      · subst h_2
        contradiction
      · subst h_1
        contradiction
      · subst h
        contradiction

Then we note that in all cases we are immediately doing subst h. The rfl keyword for obtain does that automatically. So the above is equivalent to

      obtain rfl | rfl | rfl | rfl | rfl := k_in_explicit_s2
      · contradiction
      · contradiction
      · contradiction
      · contradiction
      · contradiction

Then we notice that each branch is exactly the same, so we can collapse them with the <;> combinator:

      obtain rfl | rfl | rfl | rfl | rfl := k_in_explicit_s2 <;> contradiction

[picrin]

Very clever! I've put it in, but again if we golf code like this it might be difficult to read for beginners. (again, not sure if proof readability is as important as readability of software source code).

[dwrensha]

Please avoid non-terminal simps. Use simp only or simp_all only instead.
In this particular case,

simp only [and_self, and_true]

works.

[picrin]

Oh I missed the simp_all's, just looked at the simps. Will fix this in the next patch.

[dwrensha]

Why the · and indentation here? There is only one goal.

[dwrensha]

This can be made more concise:

    use n, n + 2, n + 4

[dwrensha]

Please delete extraneous newlines.

[dwrensha]

These successive exacts indicate that the proof needs to be structured via · and indentation, so that it focuses on one goal at time. Looks like these subgoals were introduced after apply at_most_one n. You should add cdot and indentation there.

[dwrensha]

Nonterminal simp should have an only.

[picrin]

I've resolved this and all the others (I actually used a wrong regex to search for those earlier).

[dwrensha]

A more concise way:

exact ⟨a, b⟩ 

[dwrensha]

Thanks!
There's probably still a lot of room to simplify this proof. I would welcome follow-up PRs to do that.