Lemma about box products

Stream: graph theory

[Bernardo Anibal Subercaseaux Roa]

Hi, I'm struggling with the following lemma saying that if we have a walk on the box product of G and H, and we take its projections onto G and H, the original walk's length is the sum of the two projected lengths. It seems that I'm almost done in the first sorry, but there's an Ec.req that I don't know how to deal with. Any help would be appreciated!

import Mathlib


namespace SimpleGraph
variable {G : SimpleGraph α} {H : SimpleGraph β}

lemma len_sum_projections {a₁ a₂ : α} {b₁ b₂ : β} [DecidableEq α]  [DecidableEq β] [DecidableRel G.Adj] [DecidableRel H.Adj] (w : (G □ H).Walk (a₁, b₁) (a₂, b₂)) :
  w.ofBoxProdLeft.length + w.ofBoxProdRight.length = w.length :=
  match w with
  | Walk.nil => by
    simp [Walk.length, Walk.ofBoxProdLeft, Walk.ofBoxProdRight]

  | Walk.cons x w' => by
    next a b c =>
      simp
      unfold Walk.ofBoxProdLeft Walk.ofBoxProdRight
      unfold Or.by_cases
      by_cases h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2
      . simp [h₁]
        rw [← len_sum_projections w']
        ring_nf
        field_simp
        sorry -- this is the goal I can't close
      . sorry

[Ilmārs Cīrulis]

import Mathlib


namespace SimpleGraph
variable {G : SimpleGraph α} {H : SimpleGraph β}

lemma len_sum_projections {a₁ a₂ : α} {b₁ b₂ : β} [DecidableEq α]  [DecidableEq β] [DecidableRel G.Adj] [DecidableRel H.Adj] (w : (G □ H).Walk (a₁, b₁) (a₂, b₂)) :
  w.ofBoxProdLeft.length + w.ofBoxProdRight.length = w.length :=
  match w with
  | Walk.nil => by
    simp [Walk.length, Walk.ofBoxProdLeft, Walk.ofBoxProdRight]

  | Walk.cons x w' => by
    next a b c =>
      simp
      unfold Walk.ofBoxProdLeft Walk.ofBoxProdRight
      unfold Or.by_cases
      by_cases h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2
      . simp [h₁]
        rw [← len_sum_projections w']
        ring_nf
        field_simp
        congr
        . exact h₁.2
        . simp
      . sorry

[Bernardo Anibal Subercaseaux Roa]

thanks!

[Bernardo Anibal Subercaseaux Roa]

with this I was able to prove

lemma boxProd_edist (x y : α × β) :
  G.edist x.1 y.1 + H.edist x.2 y.2 = (G □ H).edist x y

perhaps this would be useful to people and it's worth contributing to Mathlib?

[Bernardo Anibal Subercaseaux Roa]

For context, my goal is to formalize a result I proved with my advisor on the packing-chromatic number of the integer square lattice (vertices are pairs of integers, edges when their Manhattan distance is 1), and to prove that the distance between (a, b) and (x, y) is |a - x| + |b - y| the simplest way I found was to first prove the distance in the infinite integer path is abs of the difference, and then use this box product lemma to infer the distance in the square lattice

[Bhavik Mehta]

That lemma looks useful, yes!

[Eric Wieser]

Though it should be stated the other way around

[Bernardo Anibal Subercaseaux Roa]

Thanks, indeed it makes more sense to state it in the other direction. The code is here. Should I just do a PR to mathlib following the guidelines or try to simplify/improve certain aspects of the proof first?