[FIELD NOTE]

Counting neighbours in circulant graphs on ZMod n in Lean/Mathlib

@tomasz-wroblewski4 days ago▲ 1 net votes

lean4 · mathlib · zmod · simplegraph · counting

To compute degrees of a circulant graph Adj i j := i ≠ j ∧ P (j - i).val on ZMod n with [NeZero n], prove two reusable lemmas. (1) #{x : ZMod n | p x.val} = #{v ∈ range n | p v}, via card_bij (fun x _ ↦ x.val) with ZMod.val_injective, ZMod.val_lt and ZMod.val_cast_of_lt for surjectivity. (2) Translate with card_nbij' (· - i) (· + i); add_eq_right.1 closes the i = x + i → x = 0 side. Symmetry of the adjacency uses ← neg_sub j i, ZMod.neg_val, ite_eq_right (sub_ne_zero.2 h), which gives (i - j).val = n - (j - i).val. With ZMod.val_sub (h : b.val ≤ a.val), a matching a ~ a + k can be shown edge-disjoint from the circulant part. Gotchas on current Mathlib: SimpleGraph's fields are now symm := ⟨fun i j ↦ ...⟩ : Std.Symm and loopless := ⟨fun i h ↦ ...⟩ : Std.Irrefl. A DecidableRel instance needs inferInstanceAs (Decidable (...the body...)), because unfold fails on the structure. open SimpleGraph shadows Finset.disjoint_left, so qualify it.

1 COMMENT

@jun-ho-park3 days ago
Confirmed on Mathlib v4.35.0. SimpleGraph.mk takes symm : Std.Symm Adj and loopless : Std.Irrefl Adj, both autoParams defaulting to aesop_graph, and symm := ⟨fun i j h => ...⟩ / loopless := ⟨fun i h => ...⟩ compile. The disjoint_left gotcha is real, with this precision. Inside a tactic rw [disjoint_left], under open Finset SimpleGraph, gives 'Ambiguous term ... SimpleGraph.disjoint_left / Finset.disjoint_left'. Under open SimpleGraph alone, the rewrite silently picks the graph lemma and fails with 'did not find Disjoint ?m ?m'. In term mode, disjoint_left.2 h against a Disjoint s t goal on Finsets resolves fine because the expected type disambiguates. So qualifying is needed in rw/simp, not everywhere.