Grid adjacency graph

Stream: Is there code for X?

[Yaël Dillies]

Is there an easy way to define the grid graph of adjacency of fin n × fin n?

[Kevin Buzzard]

I guess you could define d on fin n and then define d on the product to be the sum, and ask for d=1

[Yaël Dillies]

Yes, that's what I'm thinking too (except for what d = 1 means :thinking:)

[Kyle Miller]

Is this what you're looking for?

def grid_graph (m n : ℕ) : simple_graph (fin m × fin n) :=
{ adj := λ i j, abs ((i.1 : ℤ) - (j.1 : ℤ)) + abs ((i.2 : ℤ) - (j.2 : ℤ)) = 1,
  symm := λ i j h, begin
    simp only [] at h,
    convert h using 2; apply abs_sub_comm,
  end,
  loopless := λ i, by simp }

[Yaël Dillies]

The graph, yes exactly! The way it is written, no, that's exactly what I'm trying to avoid.

[Eric Wieser]

Do we have a has_dist instance for the taxicab norm like that?

[Eric Wieser]

Oh yeah, docs#pi_Lp with p=1

[Eric Wieser]

Although I doubt that works for fin ...

[Kyle Miller]

@Yaël Dillies What are your secret criteria?

Is it that you're actually asking for the box product (often known as the cartesian product) of simple graphs?

def box_product {V W : Type*} (G : simple_graph V) (H : simple_graph W) : simple_graph (V × W) :=
{ adj := λ p q, (G.adj p.1 q.1 ∧ p.2 = q.2) ∨ (p.1 = q.1 ∧ H.adj p.2 q.2),
  symm := λ p q, by simp [and_comm, or_comm, eq_comm, simple_graph.adj_comm],
  loopless := λ p, by simp }

There isn't a path graph yet, but if it had vertex type fin n you'd be set.