One-way-liveness proof: Tours

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Automata/Tours.lean

Module and namespace names, imports, and formatting are adapted to complexitylib. The machine definitions are shared through Models.FiniteAutomaton.Defs.

theorem Complexity.FiniteAutomaton.permutation_single_entrance {D : Type u_1} [Finite D] (τ : Equiv.Perm D) (U : Set D) (a b : D) (ha : a ∈ U) (ha' : τ a ∉ U) (hin : ∀ d ∉ U, τ d ∈ U → d = b) : τ.SameCycle a b

A finite permutation cannot leave a set without later re-entering it. When there is only one entrance, its entrance dart lies on the same tour.

structure Complexity.FiniteAutomaton.CyclicOrder {D : Type u_1} {V : Type u_2} (vertex : D → V) : Type u_1

A cyclic order on every nonempty fiber of a finite incidence map.

• perm : Equiv.Perm D

  The permutation specifying the cyclic incidence order.

• vertex_eq (d : D) : vertex (self.perm d) = vertex d
• cyclic (d d' : D) : vertex d = vertex d' → self.perm.SameCycle d d'

noncomputable def Complexity.FiniteAutomaton.CyclicOrder.choose {D : Type u_1} {V : Type u_2} [Fintype D] (vertex : D → V) : CyclicOrder vertex

Choose a single cycle on each nonempty finite incidence fiber.

Equations

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

theorem Complexity.FiniteAutomaton.sameCycle_permCongr {D : Type u_1} {D' : Type u_2} (e : D ≃ D') (τ : Equiv.Perm D) {d d' : D} (h : τ.SameCycle d d') : (e.permCongrHom τ).SameCycle (e d) (e d')

structure Complexity.FiniteAutomaton.FunctionalEdges (V : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

Oriented edges of a finite functional graph. Loops and distinct parallel edges are permitted a priori; the source map nevertheless is injective.

• src : E → V

  The source vertex of an edge.

• dst : E → V

  The destination vertex of an edge.

• src_injective : Function.Injective self.src

def Complexity.FiniteAutomaton.FunctionalEdges.Step {V : Type u_1} {E : Type u_2} (G : FunctionalEdges V E) (v w : V) : Prop

A directed edge from one vertex to another.

Equations

• G.Step v w = ∃ (e : E), G.src e = v ∧ G.dst e = w

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.FunctionalEdges.Reach {V : Type u_1} {E : Type u_2} (G : FunctionalEdges V E) (a : V) : V → Prop

Reflexive transitive closure of the functional edge relation.

Equations

• G.Reach = Relation.ReflTransGen G.Step

theorem Complexity.FiniteAutomaton.FunctionalEdges.deterministic {V : Type u_1} {E : Type u_2} (G : FunctionalEdges V E) {v w z : V} (h : G.Step v w) (h' : G.Step v z) : w = z

theorem Complexity.FiniteAutomaton.FunctionalEdges.reach_of_terminal {V : Type u_1} {E : Type u_2} (G : FunctionalEdges V E) {t v : V} (ht : ∀ (e : E), G.src e ≠ t) (h : G.Reach t v) : t = v

theorem Complexity.FiniteAutomaton.FunctionalEdges.successor_reaches {V : Type u_1} {E : Type u_2} (G : FunctionalEdges V E) {t v w : V} (ht : ∀ (e : E), G.src e ≠ t) (hv : G.Reach v t) (hvw : G.Step v w) : G.Reach w t

theorem Complexity.FiniteAutomaton.FunctionalEdges.edge_cut {V : Type u_1} {E : Type u_2} (G : FunctionalEdges V E) {e f : E} (hne : f ≠ e) : G.Reach (G.src f) (G.src e) ↔ G.Reach (G.dst f) (G.src e)

theorem Complexity.FiniteAutomaton.FunctionalEdges.edge_not_return {V : Type u_1} {E : Type u_2} (G : FunctionalEdges V E) {t : V} (ht : ∀ (e : E), G.src e ≠ t) (e : E) (h : G.Reach (G.src e) t) : ¬G.Reach (G.dst e) (G.src e)

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.FunctionalEdges.Dart {E : Type u_2} : Type u_2

An edge together with its source or destination endpoint.

Equations

• Complexity.FiniteAutomaton.FunctionalEdges.Dart = (E × Bool)

def Complexity.FiniteAutomaton.FunctionalEdges.flip {V : Type u_1} {E : Type u_2} (_G : FunctionalEdges V E) : Equiv.Perm (E × Bool)

The involution exchanging the two endpoints of each edge.

Equations

• _G.flip = { toFun := fun (d : E × Bool) => (d.1, !d.2), invFun := fun (d : E × Bool) => (d.1, !d.2), left_inv := ⋯, right_inv := ⋯ }

def Complexity.FiniteAutomaton.FunctionalEdges.vertex {V : Type u_1} {E : Type u_2} (G : FunctionalEdges V E) (d : E × Bool) : V

The vertex incident to the selected edge endpoint.

Equations

• G.vertex d = if d.2 = true then G.dst d.1 else G.src d.1

@[simp]

theorem Complexity.FiniteAutomaton.FunctionalEdges.vertex_false {V : Type u_1} {E : Type u_2} (G : FunctionalEdges V E) (e : E) : G.vertex (e, false) = G.src e

@[simp]

theorem Complexity.FiniteAutomaton.FunctionalEdges.vertex_true {V : Type u_1} {E : Type u_2} (G : FunctionalEdges V E) (e : E) : G.vertex (e, true) = G.dst e

@[simp]

theorem Complexity.FiniteAutomaton.FunctionalEdges.flip_apply {V : Type u_1} {E : Type u_2} (G : FunctionalEdges V E) (d : E × Bool) : G.flip d = (d.1, !d.2)

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.FunctionalEdges.Rotation {V : Type u_1} {E : Type u_2} (G : FunctionalEdges V E) : Type u_2

Every incoming-to-outgoing cyclic order at a vertex is permitted.

Equations

• G.Rotation = Complexity.FiniteAutomaton.CyclicOrder G.vertex

def Complexity.FiniteAutomaton.FunctionalEdges.Rotation.tour {V : Type u_1} {E : Type u_2} {G : FunctionalEdges V E} (R : G.Rotation) : Equiv.Perm (E × Bool)

Traverse an edge, then advance along its vertex rotation.

Equations

• R.tour = R.perm * G.flip

theorem Complexity.FiniteAutomaton.FunctionalEdges.Rotation.tour_vertex {V : Type u_1} {E : Type u_2} {G : FunctionalEdges V E} (R : G.Rotation) (d : E × Bool) : G.vertex (R.tour d) = G.vertex (G.flip d)

theorem Complexity.FiniteAutomaton.FunctionalEdges.Rotation.edge_sameCycle {V : Type u_1} {E : Type u_2} {G : FunctionalEdges V E} (R : G.Rotation) [Finite E] {t : V} (ht : ∀ (e : E), G.src e ≠ t) (e : E) (h : G.Reach (G.src e) t) : R.tour.SameCycle (e, false) (e, true)

theorem Complexity.FiniteAutomaton.FunctionalEdges.Rotation.tour_flip {V : Type u_1} {E : Type u_2} {G : FunctionalEdges V E} (R : G.Rotation) (d : E × Bool) : R.tour (G.flip d) = R.perm d

theorem Complexity.FiniteAutomaton.FunctionalEdges.Rotation.flip_sameCycle {V : Type u_1} {E : Type u_2} {G : FunctionalEdges V E} (R : G.Rotation) [Finite E] {t : V} (ht : ∀ (e : E), G.src e ≠ t) (d : E × Bool) (hd : G.Reach (G.vertex d) t) : R.tour.SameCycle d (G.flip d)

theorem Complexity.FiniteAutomaton.FunctionalEdges.Rotation.perm_sameCycle {V : Type u_1} {E : Type u_2} {G : FunctionalEdges V E} (R : G.Rotation) [Finite E] {t : V} (ht : ∀ (e : E), G.src e ≠ t) (d : E × Bool) (hd : G.Reach (G.vertex d) t) : R.tour.SameCycle d (R.perm d)

theorem Complexity.FiniteAutomaton.FunctionalEdges.Rotation.vertex_pow {V : Type u_1} {E : Type u_2} {G : FunctionalEdges V E} (R : G.Rotation) (n : ℕ) (d : E × Bool) : G.vertex ((R.perm ^ n) d) = G.vertex d

theorem Complexity.FiniteAutomaton.FunctionalEdges.Rotation.vertex_sameCycle {V : Type u_1} {E : Type u_2} {G : FunctionalEdges V E} (R : G.Rotation) [Finite E] {t : V} (ht : ∀ (e : E), G.src e ≠ t) (d d' : E × Bool) (hd : G.Reach (G.vertex d) t) (he : G.vertex d = G.vertex d') : R.tour.SameCycle d d'

theorem Complexity.FiniteAutomaton.FunctionalEdges.Rotation.reach_sameCycle {V : Type u_1} {E : Type u_2} {G : FunctionalEdges V E} (R : G.Rotation) [Finite E] {t : V} (ht : ∀ (e : E), G.src e ≠ t) (d d' : E × Bool) (h : G.Reach (G.vertex d) (G.vertex d')) (ht' : G.Reach (G.vertex d') t) : R.tour.SameCycle d d'

theorem Complexity.FiniteAutomaton.FunctionalEdges.Rotation.basin_sameCycle {V : Type u_1} {E : Type u_2} {G : FunctionalEdges V E} (R : G.Rotation) [Finite E] {t : V} (ht : ∀ (e : E), G.src e ≠ t) (d d' r : E × Bool) (hd : G.Reach (G.vertex d) t) (hd' : G.Reach (G.vertex d') t) (hr : G.vertex r = t) : R.tour.SameCycle d d'

All incidences in the basin of a terminal vertex lie on its one tour.

theorem Complexity.FiniteAutomaton.FunctionalEdges.Rotation.color_eq_of_sameCycle {D : Type u_3} {C : Type u_4} [Finite D] (τ : Equiv.Perm D) (color : D → C) (hc : ∀ (d : D), color (τ d) = color d) {d d' : D} (h : τ.SameCycle d d') : color d = color d'