Implementing a weirdly described function

Stream: new members

[Aatman Supkar]

Given a graph G with n vertices, one may associate with it an m-dimensional box representation, where each vertex is mapped to an axis-parallel box (a.k.a. Cartesian product of intervals) in \R ^ m. This map must satisfy the property that every box is non-empty, and that two vertices are adjacent iff their image boxes intersect.

I wish to prove that given a representation as such, one can make a similar representation over (Fin n)^m (here the boxes are products of contiguous subsets). The proof idea is as follows:

If f : Fin n \to Vector (Box R) m is used to define the graph representation over G, we construct a g : Fin n \to Vector (Box (Fin n)) m as follows:
We fix a 'dimension' (equiv. we fix an index for each box) and we put the intervals down on \R, and we scan left to right. Maintain an integer x which is initially at 0. Each time an interval start is seen, it is mapped to x, and x is then incremented. If an interval end is seen, this end is mapped to x, without altering x. When multiple points coincide, the start points are processed first.

My claim is that g generated via this process is our required representation over Fin n. But I don't know in the least as to how I'd describe g in Lean. Any ideas?

[Aatman Supkar]

import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Order.CompleteLatticeIntervals
import Mathlib.Order.CompleteLattice

universe u

structure Interval (α : Type u) [LinearOrder α] where
  start : α
  finish : α

abbrev Box (α : Type u) [LinearOrder α] n := Vector (Interval α) n

@[simp]
def IntervalIntersection {α : Type u} [LinearOrder α] (i j : (Interval α)) : Interval α:=
  {start := max i.start j.start, finish := min i.finish j.finish}

@[simp]
def BoxIntersection {α : Type u} [LinearOrder α] {n : ℕ} (b1 b2 : Box α n) : Box α n :=
  Vector.ofFn (fun i ↦ IntervalIntersection (b1.get i) (b2.get i))

@[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)

structure GraphRepresentation (α : 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)

theorem exists_real_implies_exists_fin_graph_repr {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]:
    (∃ m : ℕ, ∃ f : Fin n → Box ℝ n, ∃ R : GraphRepresentation ℝ m G, R.Map = f) → (∃ f1 : Fin n → Box (Fin n) n, ∃ R1 : GraphRepresentation (Fin n) m G, R1.Map = f1)  := sorry

The theorem doesn't occur in my file directly in this way, and is required inside a proof, so I've written it out in a way which I think is what I need. Please let me know if more code is required for context, which I've been omitting to avoid making this too long.

[Aaron Liu]

Can you please post a #mwe? (include imports too)

[Aatman Supkar]

Working example for map in graph representations:

example f {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel (G.Adj)] (v w : Fin n) : Interval ℝ :=
    if v = w then {start := 0, finish := 1}
    else if G.Adj v w then {start := 1, finish := 2}
    else {start := 2, finish := 3}

I'll write one down for graph representations themselves soon.

Aaron Liu said:

(include imports too)

Added!