structure Hex.Perm (n : Nat) : Type

A permutation of the vertex set Fin n, stored as the array of images: vertex i maps to vec[i]. The two proof fields record that the array is duplicate-free and contains every vertex; both are decidable, and carrying both makes the inverse constructible directly.

• vec : Vector (Fin n) n

  The image array: vertex i maps to vec[i].

• nodup : self.vec.toList.Nodup

  The image array has no duplicate entries.

• complete (i : Fin n) : i ∈ self.vec.toList

  Every vertex occurs in the image array.

@[inline]

def Hex.Perm.get {n : Nat} (p : Perm n) (i : Fin n) : Fin n

Apply a permutation to a vertex.

Equations

• p.get i = p.vec[i]

@[instance_reducible]

instance Hex.Perm.instCoeFunForallFin {n : Nat} : CoeFun (Perm n) fun (x : Perm n) => Fin n → Fin n

Equations

• Hex.Perm.instCoeFunForallFin = { coe := Hex.Perm.get }

theorem Hex.Perm.get_toList {n : Nat} (p : Perm n) (i : Fin n) : p.vec.toList[↑i] = p.get i

theorem Hex.Perm.get_ne {n : Nat} (p : Perm n) {i j : Fin n} (h : i ≠ j) : p.get i ≠ p.get j

Distinct vertices have distinct images.

theorem Hex.Perm.get_inj {n : Nat} (p : Perm n) {i j : Fin n} (h : p.get i = p.get j) : i = j

A permutation is injective.

theorem Hex.Perm.get_surj {n : Nat} (p : Perm n) (i : Fin n) : ∃ (j : Fin n), p.get j = i

A permutation is surjective.

theorem Hex.Perm.ext_vec {n : Nat} {p q : Perm n} (h : p.vec = q.vec) : p = q

Two permutations with the same image array are equal.

theorem Hex.Perm.ext {n : Nat} {p q : Perm n} (h : ∀ (i : Fin n), p.get i = q.get i) : p = q

Extensional equality of permutations.

theorem Hex.Perm.ext_iff {n : Nat} {p q : Perm n} : p = q ↔ ∀ (i : Fin n), p.get i = q.get i

@[instance_reducible]

instance Hex.Perm.instDecidableEq {n : Nat} : DecidableEq (Perm n)

Equations

• p.instDecidableEq q = if h : p.vec = q.vec then isTrue ⋯ else isFalse ⋯

theorem Hex.Perm.nodup_ofFn_toList {n : Nat} {f : Fin n → Fin n} (hf : ∀ (i j : Fin n), f i = f j → i = j) : (Vector.ofFn f).toList.Nodup

The image array of every vertex in order is duplicate-free and complete whenever the entry function is injective and surjective.

theorem Hex.Perm.complete_ofFn_toList {n : Nat} {f : Fin n → Fin n} (hf : ∀ (i : Fin n), ∃ (j : Fin n), f j = i) (i : Fin n) : i ∈ (Vector.ofFn f).toList

def Hex.Perm.ofFn {n : Nat} (f : Fin n → Fin n) (hinj : ∀ (i j : Fin n), f i = f j → i = j) (hsurj : ∀ (i : Fin n), ∃ (j : Fin n), f j = i) : Perm n

Build a permutation from an injective-and-surjective entry function.

Equations

• Hex.Perm.ofFn f hinj hsurj = { vec := Hex.Vector.ofFn' f, nodup := ⋯, complete := ⋯ }

@[simp]

theorem Hex.Perm.get_ofFn {n : Nat} (f : Fin n → Fin n) (hinj : ∀ (i j : Fin n), f i = f j → i = j) (hsurj : ∀ (i : Fin n), ∃ (j : Fin n), f j = i) (i : Fin n) : (ofFn f hinj hsurj).get i = f i

def Hex.Perm.ofVector? {n : Nat} (v : Vector (Fin n) n) : Option (Perm n)

Checked construction: accepts exactly the duplicate-free complete vertex arrays.

Equations

• Hex.Perm.ofVector? v = if h : v.toList.Nodup ∧ ∀ (i : Fin n), i ∈ v.toList then some { vec := v, nodup := ⋯, complete := ⋯ } else none

theorem Hex.Perm.isSome_ofVector? {n : Nat} (v : Vector (Fin n) n) : (ofVector? v).isSome = true ↔ v.toList.Nodup ∧ ∀ (i : Fin n), i ∈ v.toList

theorem Hex.Perm.vec_of_ofVector? {n : Nat} {v : Vector (Fin n) n} {p : Perm n} (h : ofVector? v = some p) : p.vec = v

def Hex.Perm.id (n : Nat) : Perm n

The identity permutation.

Equations

• Hex.Perm.id n = Hex.Perm.ofFn (fun (i : Fin n) => i) ⋯ ⋯

@[simp]

theorem Hex.Perm.get_id {n : Nat} (i : Fin n) : (Perm.id n).get i = i

def Hex.Perm.comp {n : Nat} (p q : Perm n) : Perm n

Composition: (p.comp q).get i = p.get (q.get i).

Equations

• p.comp q = Hex.Perm.ofFn (fun (i : Fin n) => p.get (q.get i)) ⋯ ⋯

@[simp]

theorem Hex.Perm.get_comp {n : Nat} (p q : Perm n) (i : Fin n) : (p.comp q).get i = p.get (q.get i)

@[inline]

def Hex.Perm.scatterStep {n : Nat} (p : Perm n) (v : Vector (Fin n) n) (i : Fin n) : Vector (Fin n) n

One scatter step: record i at position p.get i.

Equations

• p.scatterStep v i = v.set (↑(p.get i)) i ⋯

def Hex.Perm.invVec {n : Nat} (p : Perm n) : Vector (Fin n) n

The image array of the inverse, built by one scatter pass over the vertices: each i is written at position p.get i. Every position is written, because p is surjective.

Equations

• p.invVec = List.foldl p.scatterStep (Hex.Vector.ofFn' fun (i : Fin n) => i) (List.finRange n)

theorem Hex.Perm.scatter_unchanged {n : Nat} (p : Perm n) (l : List (Fin n)) (v : Vector (Fin n) n) (q : Fin n) : (∀ (j : Fin n), j ∈ l → p.get j ≠ q) → (List.foldl p.scatterStep v l)[↑q] = v[↑q]

A scatter pass leaves untouched every position that is not the image of an element of the list.

theorem Hex.Perm.scatter_get {n : Nat} (p : Perm n) (l : List (Fin n)) (v : Vector (Fin n) n) {i : Fin n} : i ∈ l → (List.foldl p.scatterStep v l)[↑(p.get i)] = i

A scatter pass writes i at position p.get i for every i in the list.

def Hex.Perm.preimage {n : Nat} (p : Perm n) (i : Fin n) : Fin n

The vertex mapping to i, read off the scattered inverse array.

Equations

• p.preimage i = p.invVec[↑i]

@[simp]

theorem Hex.Perm.preimage_get {n : Nat} (p : Perm n) (i : Fin n) : p.preimage (p.get i) = i

@[simp]

theorem Hex.Perm.get_preimage {n : Nat} (p : Perm n) (i : Fin n) : p.get (p.preimage i) = i

theorem Hex.Perm.preimage_inj {n : Nat} (p : Perm n) {i j : Fin n} (h : p.preimage i = p.preimage j) : i = j

theorem Hex.Perm.nodup_toList {n : Nat} {v : Vector (Fin n) n} (hv : ∀ (i j : Fin n), v[↑i] = v[↑j] → i = j) : v.toList.Nodup

The image array of a permutation is duplicate-free whenever its entries are pairwise distinct.

def Hex.Perm.inv {n : Nat} (p : Perm n) : Perm n

The inverse permutation: the scattered inverse array.

Equations

• p.inv = { vec := p.invVec, nodup := ⋯, complete := ⋯ }

theorem Hex.Perm.get_inv {n : Nat} (p : Perm n) (i : Fin n) : p.inv.get i = p.preimage i

@[simp]

theorem Hex.Perm.get_inv_get {n : Nat} (p : Perm n) (i : Fin n) : p.get (p.inv.get i) = i

@[simp]

theorem Hex.Perm.inv_get_get {n : Nat} (p : Perm n) (i : Fin n) : p.inv.get (p.get i) = i

def Hex.Perm.check {n : Nat} (v : Vector (Fin n) n) : Option (Perm n)

Check a vertex array in linear time: scatter a candidate inverse, then check both inverse identities. The checks also reject repeated entries; no pairwise membership scan is needed.

Equations

• One or more equations did not get rendered due to their size.

@[csimp]

theorem Hex.Perm.ofVector?_eq_check : @ofVector? = @check

The linear checker accepts exactly the original checked constructor's inputs and returns the same proof-carrying permutation.

@[simp]

theorem Hex.Perm.comp_id {n : Nat} (p : Perm n) : p.comp (Perm.id n) = p

@[simp]

theorem Hex.Perm.id_comp {n : Nat} (p : Perm n) : (Perm.id n).comp p = p

theorem Hex.Perm.comp_assoc {n : Nat} (p q r : Perm n) : (p.comp q).comp r = p.comp (q.comp r)

@[simp]

theorem Hex.Perm.comp_inv_self {n : Nat} (p : Perm n) : p.comp p.inv = Perm.id n

@[simp]

theorem Hex.Perm.inv_comp_self {n : Nat} (p : Perm n) : p.inv.comp p = Perm.id n

@[simp]

theorem Hex.Perm.inv_inv {n : Nat} (p : Perm n) : p.inv.inv = p

@[simp]

theorem Hex.Perm.inv_id {n : Nat} : (Perm.id n).inv = Perm.id n

theorem Hex.Perm.inv_comp {n : Nat} (p q : Perm n) : (p.comp q).inv = q.inv.comp p.inv

def Hex.Perm.ofNatArray? (n : Nat) (a : Array Nat) : Option (Perm n)

Checked permutation construction from raw entries, for literal data emitted by tactics: entries must be in range, duplicate-free, and complete.

Equations

• Hex.Perm.ofNatArray? n a = if h : a.size = n ∧ ∀ (i : Nat) (hi : i < a.size), a[i] < n then Hex.Perm.ofVector? (Hex.Vector.ofFn' fun (i : Fin n) => ⟨a[↑i], ⋯⟩) else none