theorem
Hex.GraphIso.Nauty.Sparse.mark_neighbors_map
{n : Nat}
(G H : SparseGraph n)
(p : Perm n)
(hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v)
(vertex : Fin n)
(s t : RefineSt n)
(ptn : Array Nat)
(level : Nat)
(hi : Index.Valid n s.lab ptn level s.cellstart s.cellend)
(hj : Index.Valid n t.lab ptn level t.cellstart t.cellend)
(hp : s.lab.toList.Perm (List.range n))
(hq : t.lab.toList.Perm (List.range n))
(hs : ptn.size = n)
(hend : ptn[n - 1]! ≤ level)
(hc : cellsPerm ptn level t.lab (Array.map (renamingOf p).toFun s.lab))
(hm : Scratch.Marks n s.stamp s.marks)
(hvm : Scratch.Marks n s.stamp s.vmarks)
(hn : Scratch.Marks n t.stamp t.marks)
(hvn : Scratch.Marks n t.stamp t.vmarks)
:
have r :=
(have marks := s.marks;
have touched := #[];
have hitVertices := s.vmarks;
do
let __s ←
forIn [G.offsets[↑vertex]!:G.offsets[↑vertex + 1]!] (marks, touched, hitVertices)
fun (e : Nat) (__s : Array Nat × Array Nat × Array Nat) =>
have marks := __s.fst;
have __s := __s.snd;
have touched := __s.fst;
have hitVertices := __s.snd;
have j := (Graph.ofGraph G).neighbor e;
have hitVertices := hitVertices.set! j (s.stamp + 1);
have k := s.cellstart[j]!;
if (k != n && marks[k]! != s.stamp + 1) = true then
have marks := marks.set! k (s.stamp + 1);
have touched := touched.push k;
pure (ForInStep.yield (marks, touched, hitVertices))
else pure (ForInStep.yield (marks, touched, hitVertices))
have marks : Array Nat := __s.fst
have __s : Array Nat × Array Nat := __s.snd
have touched : Array Nat := __s.fst
have hitVertices : Array Nat := __s.snd
pure (marks, touched, hitVertices)).run;
have u :=
(have marks := t.marks;
have touched := #[];
have hitVertices := t.vmarks;
do
let __s ←
forIn [H.offsets[↑(p.get vertex)]!:H.offsets[↑(p.get vertex) + 1]!] (marks, touched, hitVertices)
fun (e : Nat) (__s : Array Nat × Array Nat × Array Nat) =>
have marks := __s.fst;
have __s := __s.snd;
have touched := __s.fst;
have hitVertices := __s.snd;
have j := (Graph.ofGraph H).neighbor e;
have hitVertices := hitVertices.set! j (t.stamp + 1);
have k := t.cellstart[j]!;
if (k != n && marks[k]! != t.stamp + 1) = true then
have marks := marks.set! k (t.stamp + 1);
have touched := touched.push k;
pure (ForInStep.yield (marks, touched, hitVertices))
else pure (ForInStep.yield (marks, touched, hitVertices))
have marks : Array Nat := __s.fst
have __s : Array Nat × Array Nat := __s.snd
have touched : Array Nat := __s.fst
have hitVertices : Array Nat := __s.snd
pure (marks, touched, hitVertices)).run;
sortCells r.snd.fst = sortCells u.snd.fst ∧ ∀ (v : Fin n), (r.snd.snd[↑v]! == s.stamp + 1) = (u.snd.snd[↑(p.get v)]! == t.stamp + 1)
The executed singleton neighbour loops agree on the sorted touched cells and on transported mark predicates. Their generations, retained mark values and native neighbour orders may differ.