Size of certain finset

Stream: maths

[Chris Birkbeck]

Is there an easy way to prove the size of the following Finset:

def square (m : ℤ) : Finset (ℤ × ℤ) :=
  ((Finset.Icc (-m) (m)) ×ˢ (Finset.Icc (-m) (m))).filter fun x =>
    max x.1.natAbs x.2.natAbs = m

theorem square_size (n : ℕ) (h : 1 ≤ n) : Finset.card (square n) = 8 * n := --This is what I want to prove

I can do this by first doing a horrible case check to show this Finset is the same as :

def square2 (m : ℤ) : Finset (ℤ × ℤ) :=
  ((Finset.Icc (-m) (m)) ×ˢ  {(m)}) ∪
  (Finset.Icc (-m ) (m)) ×ˢ {-(m)} ∪
  ({(m)} : Finset ℤ) ×ˢ (Finset.Icc (-(m) + 1) (m-1)) ∪
  ({-(m)} : Finset ℤ) ×ˢ (Finset.Icc (-(m) + 1) (m-1))

But I was hoping for something nicer.

[Eric Wieser]

Is showing it's the difference of Finset.Icc (-m, -m) (m, m) and Finset.Icc (-m + 1, -m + 1)(m - 1, m-1) any easier?

[Chris Birkbeck]

Hmm I can't immediately tell if that would be any easier

[Alex J. Best]

had a stab at these but gave up as its pretty horrible lol, also please #mwe next time with imports :wink:

import Mathlib.Order.LocallyFinite
import Mathlib.Data.Int.Interval
import Mathlib.Tactic
def square (m : ℤ) : Finset (ℤ × ℤ) :=
  ((Finset.Icc (-m) (m)) ×ˢ (Finset.Icc (-m) (m))).filter fun x =>
    max x.1.natAbs x.2.natAbs = m
lemma square_eq (hm : 1 ≤ m) : square m =
    Finset.Icc (-m,-m) (m,m) \
    Finset.Icc (-(m-1),-(m-1)) (m-1,m-1) := by
  ext ⟨x1,x2⟩
  simp [square, max_eq_iff]
  intros h1 h2 h3 h4
  rcases abs_cases x1 with ⟨su, hh⟩ | ⟨su, hh⟩ <;>
  rcases abs_cases x2 with ⟨su2, hh2⟩ | ⟨su2, hh2⟩ <;>
  simp [*] at *
  .
    aesop
    rw [or_iff_not_imp_left]
    specialize a (le_add_of_nonneg_of_le hh hm)
    aesop
    . specialize a (by sorry) (le_add_of_nonneg_of_le hh2 hm)
      linarith
    . linarith

theorem square_size (n : ℕ) (h : 1 ≤ n) : Finset.card (square n) = 8 * n := --This is what I want to prove
by
  rw [square_eq]
  rw [Finset.card_sdiff]
  . rw [Prod.card_Icc]
    rw [Prod.card_Icc]
    simp only [gt_iff_lt, lt_neg_self_iff, Int.card_Icc, sub_neg_eq_add,
      neg_sub, sub_add_cancel, ← sub_add, ge_iff_le]
    norm_cast
    simp only [Int.toNat_ofNat]
    have : (n - 1 + n) * (n - 1 + n) ≤  (n + 1 + n) * (n + 1 + n)
    . apply mul_le_mul' <;>
        simp <;>
        linarith
    zify [h, this]
    ring
  . intro x h
    simp only [gt_iff_lt, Prod.mk_lt_mk, lt_neg_self_iff, le_neg_self_iff,
      Int.coe_nat_nonpos_iff, Prod.Icc_mk_mk,
      Finset.mem_product, Finset.mem_Icc] at *
    aesop <;>
    linarith

[Eric Wieser]

I thought an induction approach might be more pleasant, but ran into a deterministic timeout in simp only:

import Mathlib.Order.LocallyFinite
import Mathlib.Data.Int.Interval
import Mathlib.Tactic
def square (m : ℤ) : Finset (ℤ × ℤ) :=
  ((Finset.Icc (-m) (m)) ×ˢ (Finset.Icc (-m) (m))).filter fun x =>
    max x.1.natAbs x.2.natAbs = m

lemma square_eq (n : ℕ) : square n.succ =
    Finset.Icc ((-n.succ,-n.succ) : ℤ × ℤ) (n.succ,n.succ) \
    Finset.Icc (-(n),-(n)) (n,n) := by
  induction n with
  | zero =>
    simp only  -- this causes it to hang
    sorry
  | succ n ih =>
    sorry

[Alex J. Best]

If only we still had omega :sad:

[Eric Rodriguez]

oh E_2, i'll have a stab in a couple seconds

[Eric Rodriguez]

rfl proves the zero step

[Eric Rodriguez]

but I'm not too sure how this is an inductive approach

[Eric Rodriguez]

as in, I don't really see an obvious induction argument for this

[Eric Wieser]

I hit the timeout before thinking about it

[Eric Wieser]

But I would guess a more viable aproach is to show that (square n.succ).disjUnion (Finset.Icc (-(n),-(n)) (n,n)) sorry = Finset.Icc ((-n.succ,-n.succ) : ℤ × ℤ) (n.succ,n.succ)

[Eric Wieser]

Which should also make it easier to get the cardinality at the end

[Eric Rodriguez]

def square (m : ℤ) : Finset (ℤ × ℤ) :=
  ((Finset.Icc (-m) (m)) ×ˢ (Finset.Icc (-m) (m))).filter fun x =>
    max x.1.natAbs x.2.natAbs = m

lemma square_eq (n : ℕ) : square (n + 1) =
  (((Finset.Icc (-(n + 1) : ℤ) (n + 1)).map ⟨(·, ((n + 1) : ℤ)), fun a b h ↦ by sorry⟩).disjUnion
    ((Finset.Icc (-(n + 1) : ℤ) (n + 1)).map ⟨(·, (-(n + 1) : ℤ)), fun a b h ↦ by sorry⟩)
  (Finset.disjoint_iff_ne.mpr <| fun a ha b hb ↦ by simp only [Finset.mem_map] at ha hb; obtain ⟨k, -, rfl⟩ := ha; obtain ⟨m, -, rfl⟩ := hb; linarith)) ∪
  (((Finset.Icc (-(n + 1) : ℤ) (n + 1)).map ⟨(((n + 1) : ℤ), ·), fun a b h ↦ by sorry⟩).disjUnion
    ((Finset.Icc (-(n + 1) : ℤ) (n + 1)).map ⟨((-(n + 1) : ℤ), ·), fun a b h ↦ by sorry⟩)
    (Finset.disjoint_iff_ne.mpr <| fun a ha b hb ↦ by simp only [Finset.mem_map] at ha hb; obtain ⟨k, -, rfl⟩ := ha; obtain ⟨m, -, rfl⟩ := hb; linarith)) := by
  apply le_antisymm
  · intro a h
    sorry
  · intro a h
    sorry


theorem Finset.card_union [DecidableEq α] {s t : Finset α} : (s ∪ t).card = s.card + t.card - (s ∩ t).card :=
eq_tsub_of_add_eq (card_union_add_card_inter s t)

example (m : ℕ) : (square $ m + 1).card = 8 * (m + 1) := by
  rw [square_eq, Finset.card_union]
  have : Int.toNat (↑m + 1 + 1 - (-1 + -↑m)) = (2 * (m + 1) + 1)
  · ring_nf
    rfl
  simp only [Finset.card_map, Finset.card_disjUnion, neg_add_rev, gt_iff_lt, lt_add_neg_iff_add_lt, Int.card_Icc, ge_iff_le, this]
  apply Nat.sub_eq_of_eq_add
  have : 2 * (m + 1) + 1 + (2 * (m + 1) + 1) + (2 * (m + 1) + 1 + (2 * (m + 1) + 1)) = 8 * (m + 1) + 4
  · ring
  rw [this, add_right_inj]
  sorry

[Eric Rodriguez]

I think this is a good approach

[Eric Rodriguez]

the sorrys in the definition of square_eq are by aesop, I just removed them for speed

[Eric Rodriguez]

the sorrys in that theorem just follow by boring ass case bashing

[Eric Rodriguez]

and the last sorry is that the corners have size 4, the expression looks really ugly but it's probably fairly simple with judicious use of simp

[Eric Rodriguez]

(stuff looks a lot better with set_option pp.proofs.withType false)

[Bhavik Mehta]

import Mathlib.Order.LocallyFinite
import Mathlib.Data.Int.Interval
import Mathlib.Tactic
import Mathlib.Data.Finset.Basic

def square (m : ℤ) : Finset (ℤ × ℤ) :=
  ((Finset.Icc (-m) (m)) ×ˢ (Finset.Icc (-m) (m))).filter fun x =>
    max x.1.natAbs x.2.natAbs = m

-- a re-definition in simp-normal form
lemma square_eq (m : ℤ) :
  square m = ((Finset.Icc (-m) (m)) ×ˢ (Finset.Icc (-m) (m))).filter fun x => max |x.1| |x.2| = m :=
  by simp [square]

open Finset

lemma mem_square_aux {m : ℤ} {i} : i ∈ Icc (-m) m ×ˢ Icc (-m) m ↔ max |i.1| |i.2| ≤ m :=
  by simp [abs_le]

lemma square_disj {n : ℤ} : Disjoint (square (n+1)) (Icc (-n) n ×ˢ Icc (-n) n) := by
  rw [square_eq]
  simp only [Finset.disjoint_left, mem_filter, mem_square_aux]
  intros x y
  simp_all

-- copied from the nat version, probably it already exists somewhere?
lemma Int.le_add_one_iff {m n : ℤ} : m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1 :=
  ⟨fun h =>
    match eq_or_lt_of_le h with
    | Or.inl h => Or.inr h
    | Or.inr h => Or.inl <| lt_add_one_iff.1 h,
    Or.rec (fun h => le_trans h <| le.intro 1 rfl) le_of_eq⟩

lemma square_union {n : ℤ} :
    square (n+1) ∪ Icc (-n) n ×ˢ Icc (-n) n = Icc (-(n+1)) (n+1) ×ˢ Icc (-(n+1)) (n+1) := by
  ext x
  rw [mem_union, square_eq, mem_filter, mem_square_aux, mem_square_aux,
    and_iff_right_of_imp le_of_eq, Int.le_add_one_iff, or_comm]

lemma square_disjunion (n : ℤ) :
  (square (n+1)).disjUnion (Icc (-n) n ×ˢ Icc (-n) n) square_disj =
    Icc (-(n+1)) (n+1) ×ˢ Icc (-(n+1)) (n+1) :=
  by rw [disjUnion_eq_union, square_union]

theorem square_size (n : ℕ) : Finset.card (square (n + 1)) = 8 * (n + 1) := by
  have : (((square (n+1)).disjUnion (Icc (-n : ℤ) n ×ˢ Icc (-n : ℤ) n) square_disj).card : ℤ) =
    (Icc (-(n+1 : ℤ)) (n+1) ×ˢ Icc (-(n+1 : ℤ)) (n+1)).card
  · rw [square_disjunion]
  rw [card_disjUnion, card_product, Nat.cast_add, Nat.cast_mul, card_product, Nat.cast_mul,
    Int.card_Icc, Int.card_Icc, Int.toNat_sub_of_le, Int.toNat_sub_of_le,
    ←eq_sub_iff_add_eq] at this
  · rw [←Nat.cast_inj (R := ℤ), this, Nat.cast_mul, Nat.cast_ofNat, Nat.cast_add_one]
    ring_nf
  · linarith
  · linarith

using Erics' ideas, but without the case bashing

[Chris Birkbeck]

Oh amazing, thank you! I was out and missed all the discussion, but I'll definitely profit from the results :)

[Bhavik Mehta]

The key ideas are to use Eric W's idea of showing the disjoint union, and then expressing everything in terms of max |x| |y| makes the case-work a lot simpler

[Chris Birkbeck]

Yes, I hadn't thought about showing the disjoint union. That's a really nice way to do it