Two questions about the Finset API

Stream: general

[Adam Kurkiewicz]

Hi all, I'm working on Compfiles IMO 1970 P4

To be able to make progress, I need to learn how to work with the Finset API.

For a good start I'd like to be able to show that the Finset {n, n+1} contains exactly one even number.

I think I've got the general outline of the proof right, but I'm struggling to show two lemmas. One lemma is to show equality of two Finsets given equality of the underlying Multisets. The other lemma is explicitly unraveling a BigSum operator.

Any pointers?

Here is my code so far:

import Mathlib.Tactic

def S (n : ℕ) : Finset ℕ := Finset.Icc n (n + 1)

variable (n : ℕ)

def even_numbers_in_S (n : ℕ) : Finset ℕ :=
  (S n).filter (λ x => Even x)

lemma even_numbers_in_S_card (n : ℕ) : (even_numbers_in_S n).card = 1 := by
  cases Nat.even_or_odd n
  case inl h =>
    dsimp[even_numbers_in_S]
    rw [Finset.card_filter (λ x => Even x) (S n)]

    have explicit_multiset : (S n).val = {n, n + 1} := by
      dsimp [S]
      dsimp [Finset.Icc]
      dsimp [LocallyFiniteOrder.finsetIcc]
      have : n + 1 + 1 - n = 2 := by omega
      rw [this]
      rfl

    have explicit_finset : (S n) = {n, n + 1} := by
      sorry

    rw [explicit_finset]

    have explicit_sum : (∑ a ∈ {n, n + 1}, if Even a then 1 else 0) = (if Even n then 1 else 0) + (if Even (n + 1) then 1 else 0) := by
      dsimp[BigOperators.bigsum]
      sorry

    rw [explicit_sum]

    have first_component : (if Even n then 1 else 0) = 1 := by
      split_ifs
      rfl

    have second_component : (if Even (n + 1) then 1 else 0) = 0 := by
      split_ifs with h_2
      have h_3 := Even.add_one h
      exact (Nat.not_even_iff_odd.mpr h_3) h_2
      rfl

    rw [first_component]
    rw [second_component]

  case inr h =>
    sorry

[Ruben Van de Velde]

Is there a reason to go through multisets?

    have explicit_finset : (S n) = {n, n + 1} := by
      ext
      simp [S]
      omega

[Adam Kurkiewicz]

I couldn't prove this for Finsets somehow

[Bhavik Mehta]

Indeed, when working with finsets you shouldn't need to think about multisets, as far as possible

[Ruben Van de Velde]

For the sum:

    have explicit_sum : (∑ a ∈ {n, n + 1}, if Even a then 1 else 0) = (if Even n then 1 else 0) + (if Even (n + 1) then 1 else 0) := by
      rw [Finset.sum_insert (by simp), Finset.sum_singleton]

[Adam Kurkiewicz]

Fantastic, thank you both!!!

[Bhavik Mehta]

I think only Ruben deserves thanks for the above! But I will give you a slightly shorter proof of explicit_finset:

  have explicit_finset : (S n) = {n, n + 1} := by
    rw [S, ← Nat.Icc_insert_succ_left (by simp), Finset.Icc_self]

Then note that {n, n+1} is notation for insert (n+1) {n}, and you're filtering over that set. So lemmas combining filter and insert together with lemmas about filter and singleton could be helpful. Since you're dealing with parity calculations, you might also like to know about the parity_simps set

[Yaël Dillies]

Here is a shorter proof of the whole thing

import Mathlib.Algebra.Ring.Parity
import Mathlib.Order.Interval.Finset.Nat

open Finset

def S (n : ℕ) : Finset ℕ := Icc n (n + 1)

def even_numbers_in_S (n : ℕ) : Finset ℕ := (S n).filter (Even ·)

lemma even_numbers_in_S_card (n : ℕ) : (even_numbers_in_S n).card = 1 := by
  obtain hn | hn := n.even_or_odd <;>
  simp [even_numbers_in_S, S, ← Ico_insert_right, filter_insert, filter_singleton,
    Nat.not_even_iff_odd.2, hn.add_odd odd_one, hn]

[Adam Kurkiewicz]

That's fantastic, thank you all! Your lean skills are through the roof :)

In the example that Ruben gave, how did you know that simp[S] is going to turn a ∈ S n into n ≤ a ∧ a ≤ n + 1. Is it something worth memorising, or is the rule of thumb to usually try simp[X], whenever X is some complex object that needs breaking down into simpler definitions?

[Ruben Van de Velde]

Well, you just defined S, so the only thing you can do is replace it by it's definition, which simp does. In fact, my first attempt was to do that before the ext, which just left me with a goal that the two sets were equal. From experience, the typical way to prove that is with ext, and then I knew (but it would have made sense to try anyway) that simp would make progress on the x \in ... goals