feat(archive/imo): formalise 1979 Q1

[kbuzzard]

---

[eric-wieser]

Is it really this hard to prove that filter even (range 1320) = map double (range 660)? That's awful!

[eric-wieser]

I can do it with slightly fewer lines with

example : filter even (range 1320) = map double (range 660) :=
begin
  ext a,
  simp only [mem_filter, mem_range, mem_map, double],
  split,
  { rintros ⟨x, m, rfl⟩,
    refine ⟨m, _, rfl⟩,
    rw mem_range,
    linarith },
  { rintros ⟨a, ha, rfl⟩,
    refine ⟨_, a, rfl⟩,
    rw mem_range at ha,
    change 2 * a < 1320,
    linarith, }
end

[shingtaklam1324]

In this case, the general form of the lemma seems to be easier to prove

example (n : ℕ) : filter even (range (2*n)) = map double (range n) :=
begin
  induction n with k IH,
  { refl },
  { rw [mul_succ, range_succ, range_succ, range_succ, map_insert, filter_insert, if_neg, 
        filter_insert, if_pos, IH];
    simp with parity_simps }
end

[jsm28]

I'd think a more general form takes a monotone function, filters an interval on membership of the image of that function and shows the result is the image of an interval given suitable conditions on the orders involved. With special cases for arithmetic progressions, i.e. images of intervals under functions a * x + b in nat or int being equivalent to filtering intervals on some modular arithmetic condition, and versions for odd and even being special cases of that. (And most of that making sense for both set and finset.) That may not make proofs significantly simpler, but it fits in with mathlib principles, and those more general lemmas about intervals, monotone functions and arithmetic progressions seem plausibly appropriate for mathlib proper.

[kbuzzard]

I've gone with @eric-wieser 's proof.

[kbuzzard]

Having said that, I now feel guilty because one of the main gains that we're getting from formalising IMO solutions is that it shows up gaps in the library...

[bryangingechen]

My suggestions are just a few style comments.

I've only glanced at the proofs so far, but their length suggests to me that we might be missing some API for manipulating sums. I don't have any concrete suggestions yet, but what was your feeling when you were writing the proofs?

[kbuzzard]

I've come back to this and tried to tidy up all the sum proofs, and I think @jsm28 is right. There are some sum lemmas missing in finset.Ico; I think that it's probably best if I do this properly and add them. I'm still working on this PR so I'll leave it as awaiting-author.

[jcommelin]

Is this a module doc?

Suggested change

	/-
	/-!

[kbuzzard]

Just to clarify what's going on here -- I wanted the parity stuff for another reason so I PR'ed it independently; I embarked upon adding some finset.Ico stuff so I could streamline the sum proofs, but then I heard here that @Vierkantor was in the middle of refactoring it all on the fin_range branch so I'm leaving this for now. I'm happy to close this or wait until fin_range is PR'ed. In the mean time I might PR the non-IMO part of this PR separately.

[YaelDillies]

Now that all the finset.Ixx stuff has been generalized, this can go forward.

[MantasBaksys]

I have pushed a new commit, where I've updated the file to use finset.Icc, updated the proof to compile, golfed it slightly and deleted definitions, which I and @YaelDillies thought were unnecessary.

[jcommelin]

How hard would it be to do this refactor? I think these IMO files should be showcases that look as nice as possible.

[YaelDillies]

@kbuzzard, what did you exactly mean by that? I can't make sense of the "ℚ-valued" bit. Surely you meant "with_top ℤ-valued"? If that's really the case, the refactor is arguable.

[jcommelin]

I think he meant ℝ-valued, although the norms of p-adic numbers are all in the image of coe : ℚ → ℝ.

[kbuzzard]

I meant that valuations have problems with v(0) but norms don't, |0|=0. We have |p^n|=p^{-n} so \Q will do.

[jcommelin]

Suggested change

	/-- The injection ℕ ↪ ℕ sending any n ∈ ℕ to 2 * n
	-/
	/-- The injection `ℕ ↪ ℕ` sending any `n ∈ ℕ` to `2 * n` -/

[urkud]

@kbuzzard Could you please move this PR to https://github.com/leanprover-community/mathzoo ?

[kbuzzard]

@YaelDillies are you still thinking about working on this?

[kbuzzard]

I'm merging master and I find that there is some missing API for padic_norm. I've added some in #16074 . @urkud The problem with putting the lemma in mathzoo is that API won't be there; the last time they bumped mathlib was March.

[kbuzzard]

Yael reopened this but I'm going to close it again because I see no point in working on a Lean 3 version of this, with mathlib4 so near.

[eric-wieser]

because I see no point in working on a Lean 3 version of this, with mathlib4 so near.

Mathport can always translate it!