Need help with using Fin n in a proof

Stream: new members

[Aatman Supkar]

import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Analysis.RCLike.Basic

universe u

open List

/-- We define an interval to just be a pair of points. If start > finish, we just have an empty interval. Meant to be treated as closed intervals. -/
structure Interval (α : Type u) [LinearOrder α] where
  start : α
  finish : α

/-- Boxes need to be 'axis-parallel', and can thus be defined as a list of intervals. -/
abbrev Box (α : Type u) [LinearOrder α] n := List.Vector (Interval α) n

/-- Given two intervals of the same type, returns their intersection. -/
@[simp]
def IntervalIntersection {α : Type u} [LinearOrder α] (i j : (Interval α)) : Interval α:=
  {start := max i.start j.start, finish := min i.finish j.finish}

/-- Given two boxes of the same type, returns their intersection. -/
@[simp]
def BoxIntersection {α : Type u} [LinearOrder α] {n : ℕ} (b1 b2 : Box α n) : Box α n :=
  List.Vector.ofFn (fun i ↦ IntervalIntersection (b1.get i) (b2.get i))

/-- Hypothesis that characterises when a given interval is non-empty. -/
@[simp]
def nonempty_interval {α : Type u} [LinearOrder α] (i : Interval α) : Prop :=
  i.start ≤ i.finish

@[simp]
def nonempty_box {n : ℕ} {α : Type u} [LinearOrder α] (b : Box α n) : Prop :=
  ∀ i : Fin n, nonempty_interval (b.get i)

/-- Each vertex `v ∈ G` is mapped to a non-empty box of dimension `n` via `Map`. Two distinct vertices `u,v ∈ G` intersect if and only if their corresponding boxes `Map u, Map v` intersect. The resulting box representation is said to be of dimension `n`. -/
structure BoxRepresentation (α : Type u) [LinearOrder α] (m : ℕ) {n : ℕ} (G : SimpleGraph (Fin n)) where
  Map : Fin n → Box α m
  h1 (i : Fin n): nonempty_box (Map i)
  h2 : ∀ u v : Fin n, (u = v) ∨ (nonempty_box (BoxIntersection (Map u) (Map v)) ↔ G.Adj u v)

/-- The boxicity of a graph `G` is the smallest number of dimensions `n` needed for a box representation of dimension `n` to exist. -/
@[simp]
noncomputable def GraphBoxicity {n : ℕ} (G : SimpleGraph (Fin n)) : ℕ :=
  sInf {m | ∃ f : Fin n → Box ℝ m, ∃ R : BoxRepresentation ℝ m G, R.Map = f}

/-- A discrete version of boxicity using `Fin n`. Is supposed to be the same as boxicity. -/
@[simp]
noncomputable def GraphBoxicity' {n : ℕ} (G : SimpleGraph (Fin n)) : ℕ :=
  sInf {m | ∃ f : Fin n → Box (Fin n) m, ∃ R : BoxRepresentation (Fin n) m G, R.Map = f}

/-- Determining when the intersection of two non-empty intervals are supposed to be non-empty. -/
theorem interval_int_nonempty_iff_ineq {α : Type u} [LinearOrder α] (I J : Interval α):
  (nonempty_interval I) → (nonempty_interval J) → (nonempty_interval (IntervalIntersection I J) ↔ I.start ≤ J.finish ∧ J.start ≤ I.finish) := by
  intro h1 h2
  apply Iff.intro
  simp_all only [nonempty_interval, IntervalIntersection]
  by_cases ha : I.start ≤ J.finish <;> by_cases hb : J.start ≤ I.finish <;> intro hc <;> simp_all
  simp_all only [nonempty_interval, IntervalIntersection]
  by_cases ha : I.start ≤ J.finish <;> by_cases hb : J.start ≤ I.finish <;> intro hc <;> simp_all

-- def fin_succ {n : ℕ} (i : ℕ) (h : i < n) : ℕ (i < n + 1 : Prop) :=
--   let successor := i + 1
--   ⟨successor, Nat.add_lt_of_lt_sub (h)⟩

/-- Graph boxicity equals its discrete variant on all graphs. -/
theorem graphBoxicity_eq_graphBoxicity' {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] :
    GraphBoxicity G = GraphBoxicity' G := by
  unfold GraphBoxicity GraphBoxicity'
  let S1 : Set ℕ := {m | ∃ f : Fin n → Box ℝ m, ∃ R : BoxRepresentation ℝ m G, R.Map = f}
  let S2 : Set ℕ := {m | ∃ f : Fin n → Box (Fin n) m, ∃ R : BoxRepresentation (Fin n) m G, R.Map = f}
  have h1 : S2 ⊆ S1 := by
    intro m h
    simp [S2] at h
    let ⟨f, R, h'⟩ := h
    simp [S1]
    let g1 (i : Interval (Fin n)) : Interval ℝ :=
      {start := ↑(i.start), finish := ↑(i.finish)}
    have h1a : ∀ i : Interval (Fin n), nonempty_interval (g1 i) ↔ nonempty_interval i := by
      simp only [nonempty_interval, Nat.cast_le, Fin.val_fin_le, implies_true]
    let g2 (b : Box (Fin n) m) : Box ℝ m :=
        List.Vector.ofFn (fun i ↦ g1 ((b.get i) : Interval (Fin n)))
    have h1b : ∀ b : Box (Fin n) m, nonempty_box b ↔ nonempty_box (g2 b) := by
      intro b
      simp only [nonempty_box, nonempty_interval, Vector.get_ofFn, Nat.cast_le, Fin.val_fin_le, g2]
    have h1c (b1 b2 : Box (Fin n) m) : BoxIntersection (g2 b1) (g2 b2) = g2 (BoxIntersection b1 b2) := by
      simp only [BoxIntersection, IntervalIntersection, Vector.get_ofFn, Fin.coe_sup, Nat.cast_max,
        Fin.coe_inf, Nat.cast_min, g2, g1]
    have h1d : ∀ u v : Fin n, (u = v) ∨ (nonempty_box (BoxIntersection (g2 (f u)) (g2 (f v))) ↔ G.Adj u v) := by
      intro u
      intro v
      cases Decidable.em (u = v)
      apply Or.inl
      assumption
      apply Or.inr
      rw [h1c, ← h1b]
      have h1d1 := R.h2 u v
      cases h1d1 with
      | inl => contradiction
      | inr hw => rwa[← h']
    have h1e (i : Fin n) : nonempty_box (g2 (f i)) := by
      intro i1
      have h1e1 := R.h1
      simp_all [h', g2]
    exact ⟨g2 ∘ f, ⟨⟨g2 ∘ f, h1e, h1d⟩, rfl⟩⟩
  have h2 : S1 ⊆ S2 := by
    intro m h
    simp [S1] at h
    let ⟨f, R, h'⟩ := h
    simp [S2]
    have interval_dim_list (i : Fin n) := List.Vector.ofFn (fun j ↦ (f i).get j)
    have discretise_real (x : ℝ) (j : Fin m): Fin n := sorry
    have discretise_interval (i : Fin n) (j: Fin m) : Interval (Fin n) :=
      ⟨discretise_real ((f i).get j).start j , discretise_real ((f i).get j).finish j⟩
    have discretise_box (i : Fin n): Box (Fin n) m:=
      List.Vector.ofFn (fun j ↦ discretise_interval i j)
    have h2a : ∀ (i : Fin n) (j : Fin m), nonempty_interval ((f i).get j) ↔ nonempty_interval (discretise_interval i j) := by sorry
    have h2aa (i : Fin n) : nonempty_box ((f i)) ↔ nonempty_box (discretise_box i) := by sorry
    have h2b : ∀ (i j : Fin n), nonempty_box (BoxIntersection (f i) (f j)) ↔ nonempty_box (BoxIntersection (discretise_box i) (discretise_box j)) := by sorry
    have h2c : ∀ (i j : Fin n), (i = j) ∨ (nonempty_box (BoxIntersection (discretise_box i) (discretise_box j)) ↔ G.Adj i j) := by
      intro i j
      cases Decidable.em (i = j)
      apply Or.inl
      assumption
      apply Or.inr
      have h2c1 := R.h2 i j
      cases h2c1 with
      | inl => contradiction
      | inr hw =>
        aesop
    have h2d : ∀ i : Fin n, nonempty_box (discretise_box i) := by
      sorry
    exact ⟨discretise_box, ⟨discretise_box, h2d, h2c⟩, rfl⟩
  have h3 : S1 = S2 := by
    apply Set.Subset.antisymm
    assumption
    assumption
  exact congrArg sInf h3

I'm trying to figure out this last proof, but I don't know how to begin defining discretise_real.

Proof idea: Given a box representation of a graph G with n vertices, over the reals, map each box's kth interval as follows:
Make a list of all the kth intervals across all the boxes. Now assign to each interval's start or end point x the number of start points that come before x in the list above. I need this to be Fin n as well, and not just a natural. This assignment preserves all intersection properties, and should thus be able to map any real presentation to a Fin n one.

The issue with trying to define the above is:
a) If I try to create the integer iteratively using List.foldl, I need the type of the integer to be preserved in the foldl's input function, so I define it to be Fin n to start with. I'm not sure how to synthesise a proof that upon each addition, the integer still doesn't cross n-1.
b) I tried List.foldl with a (Nat, h : Prop) pair instead, but turns out you can't create such a pair for some reason?

Help with the rest of the proof would also be appreciated, but what matters to me most right now is being able to define discretise_real correctly. I am not sure if the comments in the code explain the setup sufficiently, so please let me know anything I should elaborate on.

[Matt Diamond]

on a side note, docs#Interval and docs#NonemptyInterval exist in Mathlib (though NonemptyInterval is a Type, not a Prop)

[Matt Diamond]

btw it might help if you included a definition of discretise_real even if the code doesn't work, just to help people understand what you're aiming at... you can definitely create (Nat, Prop) pairs (that's what Fin is, in a sense)

[Aatman Supkar]

Ah, apologies. In my head I did write it here, when I actually did not.

Aatman Supkar said:

Proof idea: Given a box representation of a graph G with n vertices, over the reals, map each box's kth interval as follows:
Make a list of all the kth intervals across all the boxes. Now assign to each interval's start or end point x the number of start points that come before x in the list above.

This assignment is precisely what I wish for discretise_real to be.

Matt Diamond said:

you can definitely create (Nat, Prop) pairs (that's what Fin is, in a sense)

Apologies, I meant something like (Nat, proof of given Nat being less than some integer) pairs. Even if I do that, proving that the natural is strictly less than n is slightly tricky. It needs me to figure out how to use the fact that since x itself will not be one of the indices greater than x, not all intervals contribute a start point.

At this point I'm also facing issues with understanding how I'm supposed to partition my work into the right blocks to tackle one at a time. Like, if I don't know exactly what I want to provide in the upcoming step which I haven't even worked out, what should my current step be achieving? I'm slightly lost here.