def Hex.Perm.Cycle.Invariant {n : Nat} (p : Perm n) (seen : Vector Bool n) : Prop

The old marks are a union of complete cycles.

Equations

• Hex.Perm.Cycle.Invariant p seen = ∀ (x : Fin n), seen[↑(p.get x)] = seen[↑x]

structure Hex.Perm.Cycle.State {n : Nat} (p : Perm n) (old seen : Vector Bool n) (c : Array (Fin n)) (next : Fin n) : Prop

A visit appends fresh points and marks exactly those appended points.

• follows : Follows p c next
• distinct : c.toList.Nodup
• marked (x : Fin n) : seen[↑x] = true ↔ old[↑x] = true ∨ x ∈ c
• disjoint (x : Fin n) : x ∈ c → old[↑x] = false
• fresh : old[↑next] = false

theorem Hex.Perm.Cycle.State.initial {n : Nat} (p : Perm n) (seen : Vector Bool n) (x : Fin n) (hx : seen[↑x] = false) : State p seen seen #[] x

theorem Hex.Perm.Cycle.State.mem_of_seen {n : Nat} {p : Perm n} {old seen : Vector Bool n} {c : Array (Fin n)} {x : Fin n} (s : State p old seen c x) (hx : seen[↑x] = true) : x ∈ c

theorem Hex.Perm.Cycle.State.not_mem {n : Nat} {p : Perm n} {old seen : Vector Bool n} {c : Array (Fin n)} {x : Fin n} (s : State p old seen c x) (hx : seen[↑x] ≠ true) : ¬x ∈ c

theorem Hex.Perm.Cycle.State.push {n : Nat} {p : Perm n} {old seen : Vector Bool n} {c : Array (Fin n)} {x : Fin n} (s : State p old seen c x) (ho : Invariant p old) (hx : seen[↑x] ≠ true) : State p old (seen.set (↑x) true ⋯) (c.push x) (p.get x)

theorem Hex.Perm.Cycle.State.seen_of_full {n : Nat} {p : Perm n} {old seen : Vector Bool n} {c : Array (Fin n)} {x : Fin n} (s : State p old seen c x) (ho : Invariant p old) (hc : n ≤ c.size) : seen[↑x] = true

At zero fuel there are already at least n distinct entries. A further fresh point would give n+1 distinct elements of Fin n.

theorem Hex.Perm.Cycle.visit_valid {n : Nat} (p : Perm n) (old seen : Vector Bool n) (c : Array (Fin n)) (x : Fin n) (fuel : Nat) (s : State p old seen c x) (ho : Invariant p old) (bound : n ≤ fuel + c.size) : have result := p.visit fuel x seen c; Valid p result.snd ∧ (∀ (y : Fin n), result.fst[↑y] = true ↔ old[↑y] = true ∨ y ∈ result.snd) ∧ ∀ (y : Fin n), y ∈ result.snd → old[↑y] = false

The actual visit loop returns a complete cycle, with exact new marks and no overlap with the cycles that were already marked.

theorem Hex.Perm.Cycle.marked_invariant {n : Nat} {p : Perm n} {old seen : Vector Bool n} {c : Array (Fin n)} (ho : Invariant p old) (hc : Valid p c) (hm : ∀ (x : Fin n), seen[↑x] = true ↔ old[↑x] = true ∨ x ∈ c) : Invariant p seen

theorem Hex.Perm.Cycle.visit_append {n : Nat} (p : Perm n) (fuel : Nat) (x : Fin n) (seen : Vector Bool n) (c : Array (Fin n)) : ∃ (tail : Array (Fin n)), (p.visit fuel x seen c).snd = c ++ tail

Visiting preserves the entries already appended, in their original order.

theorem Hex.Perm.Cycle.visit_first {n : Nat} (p : Perm n) (x : Fin n) (seen : Vector Bool n) (hx : seen[↑x] = false) : ∃ (hc : 0 < (p.visit n x seen #[]).snd.size), (p.visit n x seen #[]).snd[0] = x

theorem Hex.Perm.Cycle.visit_complete {n : Nat} (p : Perm n) (seen : Vector Bool n) (x : Fin n) (ho : Invariant p seen) (hx : seen[↑x] = false) : have result := p.visit n x seen #[]; Valid p result.snd ∧ (∀ (y : Fin n), result.fst[↑y] = true ↔ seen[↑y] = true ∨ y ∈ result.snd) ∧ ∀ (y : Fin n), y ∈ result.snd → seen[↑y] = false

Starting at an unmarked point produces its whole cycle and marks exactly that cycle in addition to the old marks.