Cubing a cube in lean

cubes.lean

import data.fintype algebra.ordered_field

theorem multiset.inj_of_nodup_map {α β} (f : α → β) {s : multiset α} (h : (multiset.map f s).nodup)
  {x y} (h₁ : x ∈ s) (h₂ : y ∈ s) (e : f x = f y) : x = y :=
begin
  rcases multiset.exists_cons_of_mem h₁ with ⟨s, rfl⟩,
  cases multiset.mem_cons.1 h₂, {exact h_1.symm},
  simp only [multiset.map_cons, multiset.nodup_cons, multiset.mem_map] at h,
  cases h.1 ⟨_, h_1, e.symm⟩
end

@[simp] theorem multiset.map_eq_zero
  {α β} {s : multiset α} {f : α → β} : s.map f = 0 ↔ s = 0 :=
by rw [← multiset.card_eq_zero, multiset.card_map, multiset.card_eq_zero]

theorem multiset.ne_zero_of_mem {α} {s : multiset α} {a} (h : a ∈ s) : s ≠ 0 :=
λ h0, multiset.not_mem_zero a (h0 ▸ h)

theorem multiset.exists_min {α β} [decidable_linear_order β]
  {s : multiset α} (f : α → β) (h : s ≠ 0) : ∃ a ∈ s, ∀ b ∈ s, f a ≤ f b :=
begin
  have : (s.map f).to_finset ≠ ∅ :=
    mt (multiset.to_finset_eq_empty.trans multiset.map_eq_zero).1 h,
  cases finset.min_of_ne_empty this with a m,
  rcases multiset.mem_map.1 (multiset.mem_to_finset.1 (finset.mem_of_min m))
    with ⟨a, ha, rfl⟩,
  refine ⟨a, ha, λ b hb, finset.le_min_of_mem _ m⟩,
  exact multiset.mem_to_finset.2 (multiset.mem_map_of_mem _ hb)
end

section cubes

structure cube (α : Type*) [discrete_linear_ordered_field α] (n : ℕ) :=
(side : α)
(p : fin n → α)
(h : 0 < side)

variables {α : Type*} [discrete_linear_ordered_field α] {n : ℕ}

def cube.interior (c : cube α n) : set (fin n → α) :=
{p | ∀ i, c.p i < p i ∧ p i < c.p i + c.side}

instance : has_mem (fin n → α) (cube α n) :=
⟨λ p c, ∀ i, c.p i ≤ p i ∧ p i ≤ c.p i + c.side⟩

theorem cube.p_mem (c : cube α n) : c.p ∈ c :=
λ i, ⟨le_refl _, (le_add_iff_nonneg_right _).2 (le_of_lt c.h)⟩

theorem cube.p_side_mem (c : cube α n) : (λ i, c.p i + c.side) ∈ c :=
λ i, ⟨(le_add_iff_nonneg_right _).2 (le_of_lt c.h), le_refl _⟩

theorem cube.mem_of_mem_interior {c : cube α n} {p} (h : p ∈ c.interior) : p ∈ c :=
λ i, ⟨le_of_lt (h i).1, le_of_lt (h i).2⟩

def cube.center (c : cube α n) (i : fin n) : α := c.p i + c.side / 2

theorem cube.center_mem_interior (c : cube α n) : c.center ∈ c.interior :=
λ i, ⟨(lt_add_iff_pos_right _).2 (half_pos c.h),
      (add_lt_add_iff_left _).2 (half_lt_self c.h)⟩

instance : has_subset (cube α n) :=
⟨λ c1 c2, ∀ i, c2.p i ≤ c1.p i ∧ c1.p i + c1.side ≤ c2.p i + c2.side⟩

theorem cube.subset_iff {c1 c2 : cube α n} : c1 ⊆ c2 ↔ ∀ p, p ∈ c1 → p ∈ c2 :=
⟨λ H p h i, ⟨le_trans (H _).1 (h _).1, le_trans (h _).2 (H _).2⟩,
 λ H i, ⟨(H _ c1.p_mem _).1, (H _ c1.p_side_mem _).2⟩⟩

theorem cube.side_le_of_subset {c1 c2 : cube α (n+1)} (h : c1 ⊆ c2) : c1.side ≤ c2.side :=
(add_le_add_iff_left _).1 $ le_trans
  ((add_le_add_iff_right _).2 (cube.subset_iff.1 h _ c1.p_mem 0).1)
  ((cube.subset_iff.1 h _ c1.p_side_mem 0).2)

theorem cube.interior_subset {c1 c2 : cube α (n+1)} (h : c1 ⊆ c2) : c1.interior ⊆ c2.interior :=
λ p H i, ⟨lt_of_le_of_lt (h i).1 (H i).1, lt_of_lt_of_le (H i).2 (h i).2⟩

theorem cube.eq_of_subset_side_le {c1 c2 : cube α (n+1)} (h1 : c1 ⊆ c2) (h2 : c2.side ≤ c1.side) : c1 = c2 :=
begin
  cases c1, cases c2, simp only,
  refine ⟨le_antisymm (cube.side_le_of_subset h1) h2,
    funext $ λ i, le_antisymm _ (h1 i).1⟩,
  exact (add_le_add_iff_right _).1 (le_trans (h1 i).2 ((add_le_add_iff_left _).2 h2))
end

theorem cube.subset_antisymm {c1 c2 : cube α (n+1)} (h1 : c1 ⊆ c2) (h2 : c2 ⊆ c1) : c1 = c2 :=
cube.eq_of_subset_side_le h1 (cube.side_le_of_subset h2)

def unit_cube (α : Type*) [discrete_linear_ordered_field α] (n : ℕ) :
  cube α n := ⟨1, λ _, 0, zero_lt_one⟩

def proj (p : fin (n+1) → α) (i : fin n) : α := p i.succ

def cons (a : α) (p : fin n → α) (i : fin (n+1)) : α := fin.cases a p i

def cube.proj (c : cube α (n+1)) : cube α n :=
⟨c.side, proj c.p, c.h⟩

theorem forall_fin_succ {P : fin (n+1) → Prop} :
  (∀ i, P i) ↔ P 0 ∧ (∀ i:fin n, P i.succ) :=
⟨λ H, ⟨H 0, λ i, H _⟩, λ ⟨H0, H1⟩ i, fin.cases H0 H1 i⟩

theorem mem_iff_proj {c : cube α (n+1)} {p : fin (n+1) → α} :
  p ∈ c ↔ (c.p 0 ≤ p 0 ∧ p 0 ≤ c.p 0 + c.side) ∧ proj p ∈ c.proj :=
forall_fin_succ

@[simp] theorem proj_cons (a : α) (p : fin n → α) : proj (cons a p) = p :=
funext $ λ i, by simp [proj, cons]

theorem no_cubes_partition_aux (n2 : 2 ≤ n) (cubes : multiset (cube α (n+1))) :
  ∀ (base : cube α n) (bottom : α) (h : bottom < 1)
    (nd : (cubes.map cube.side).nodup)
    (dj : cubes.pairwise (λ c1 c2 : cube α (n+1), c1.interior ∩ c2.interior = ∅))
    (fill : ∀ p : fin (n+1) → α,
      bottom ≤ p 0 → p 0 ≤ 1 → proj p ∈ base → ∃ c ∈ cubes, p ∈ c)
    (bound : ∀ c : cube α (n+1), c ∈ cubes → bottom ≤ c.p 0 ∧ c.p 0 + c.side ≤ 1)
    (tight : ∃ k > bottom, ∀ (c ∈ cubes) (p : fin (n+1) → α),
      p ∈ c → p 0 < k → proj p ∈ base),
    ∃ c:cube α (n+1), c ∈ cubes ∧ c.p 0 = bottom ∧ c.proj = base :=
multiset.strong_induction_on cubes $
λ cubes IH base bottom h nd dj fill low tight, begin
  have : ∃ c : cube α (n+1), c ∈ cubes ∧ c.p 0 = bottom ∧
    ∀ b : cube α (n+1), b ∈ cubes → b.p 0 = bottom → c.side ≤ b.side,
  { have : cubes.filter (λ c, c.p 0 = bottom) ≠ ∅,
    { rcases fill (cons bottom base.p) (le_refl _) (le_of_lt h) _ with ⟨c, h, m⟩,
      { exact multiset.ne_zero_of_mem
          (multiset.mem_filter.2 ⟨h, le_antisymm (m 0).1 (low _ h).1⟩) },
      rw proj_cons, exact base.p_mem },
    rcases multiset.exists_min cube.side this with ⟨c, hc, ha⟩,
    simp at hc ha, cases hc with hc hc0,
    exact ⟨c, hc, hc0, ha⟩ },
  rcases this with ⟨c, hc, hc0, ha⟩,
  have : ∃ b > 0, ∀ c' : cube α (n+1), c' ∈ cubes → c'.p 0 = bottom → c'.side < c.side + b → c' = c,
  { classical,
    by_cases h0 : cubes.filter (λ c' : cube α (n + 1), c'.p 0 = bottom ∧ c' ≠ c) = 0,
    { refine ⟨1, zero_lt_one, λ c' hc' hc0' h, by_contradiction $ λ hn, _⟩,
      refine multiset.ne_zero_of_mem _ h0,
      swap, exact multiset.mem_filter.2 ⟨hc', hc0', hn⟩ },
    { rcases multiset.exists_min cube.side h0 with ⟨c', hc', ha'⟩,
      simp at hc' ha', rcases hc' with ⟨hc', hc0', hn⟩,
      refine ⟨c'.side - c.side, sub_pos.2 (lt_of_le_of_ne (ha _ hc' hc0') _), _⟩,
      { exact mt (multiset.inj_of_nodup_map _ nd hc hc') (ne.symm hn) },
      { intros d hd hd0 hl, rw add_sub_cancel'_right at hl,
        by_contra, exact not_le_of_lt hl (ha' _ hd hd0 a) } } },
  rcases this with ⟨b, b0, hb⟩,
  -- for some reason this is very slow
  -- by_cases hi : ∃ i : fin n, c.proj.p i < base.p i ∧ c.proj.p i + c.side < base.p i + base.side,
  -- by_cases hj : ∀ i : fin n, c.proj.p i < base.p i ∧ c.proj.p i + c.side < base.p i + base.side,
  refine classical.by_cases
    (λ hi : ∃ i : fin n, c.proj.p i < base.p i ∧ c.proj.p i + c.side < base.p i + base.side,
      classical.by_cases
        (λ hj : ∀ i : fin n, c.proj.p i < base.p i ∧ c.proj.p i + c.side < base.p i + base.side, _)
        (λ hj, _))
    (λ hi, _),
  { clear hi,
    sorry /- use the IH -/ },
  { simp only [not_forall] at hj,
    cases hi with i hi, cases hj with j hj,
    sorry /- consider the four corners in i,j dimensions to get a contradiction -/ },
  { simp [not_exists] at hi,
    refine ⟨c, hc, hc0, sorry⟩ },
end

theorem no_cubes_partition (n3 : 3 ≤ n)
  (cubes : multiset (cube α n))
  (nd : (cubes.map cube.side).nodup)
  (dj : cubes.pairwise (λ c1 c2 : cube α n, c1.interior ∩ c2.interior = ∅))
  (box : ∀ p, p ∈ unit_cube α n ↔ ∃ c ∈ cubes, p ∈ c) :
  cubes = unit_cube α n :: 0 :=
begin
  cases n, {cases n3},
  have ss : ∀ c ∈ cubes, c ⊆ unit_cube α (n+1) :=
    λ c hc, cube.subset_iff.2 (λ p hp, (box _).2 ⟨_, hc, hp⟩),
  rcases no_cubes_partition_aux (nat.le_of_succ_le_succ n3)
    cubes (unit_cube _ _) 0 zero_lt_one nd dj _ _ _ with ⟨c, hc, cb, e⟩,
  { have : c = unit_cube α (n+1) :=
      cube.eq_of_subset_side_le (ss _ hc) (ge_of_eq (congr_arg cube.side e:_)),
    subst this, clear cb e,
    rcases multiset.exists_cons_of_mem hc with ⟨s, rfl⟩,
    congr, refine multiset.eq_zero_of_forall_not_mem (λ c hc, _),
    refine quot.induction_on s _ hc dj, simp, intros l hc' dj,
    have := (multiset.pairwise_coe_iff_pairwise _).1 dj,
    swap, exact λ c1 c2, eq.trans (set.inter_comm _ _),
    refine flip set.ne_empty_of_mem ((list.pairwise_cons.1 this).1 _ hc')
      ⟨_, cube.center_mem_interior _⟩,
    exact cube.interior_subset (ss _ (multiset.mem_cons_of_mem hc))
      (cube.center_mem_interior _) },
  { intros p p0 p1 m,
    rw [← zero_add (1:α)] at p1,
    exact (box _).1 (mem_iff_proj.2 ⟨⟨p0, p1⟩, m⟩) },
  { intros c hc, rw ← zero_add (1:α), exact ss c hc 0 },
  { exact ⟨1, zero_lt_one, λ c hc p hp h1,
      (mem_iff_proj.1 ((box p).2 ⟨c, hc, hp⟩)).2⟩ }
end

end cubes