Script.lean

inductive ElementaryTietzeMove :
    Presentation.{u} → Presentation.{u} → Type (u + 1) where
  /-- Replace a relator set by another set generating the same normal closure. -/
  | replaceRelators
      {X : Type u} {R S : Set (FreeGroup X)}
      (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
      (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
      ElementaryTietzeMove
        (Presentation.ofRelators R) (Presentation.ofRelators S)
  /-- Rename every generator through an equivalence of generator types. -/
  | renameGenerators
      {X Y : Type u} (R : Set (FreeGroup X)) (e : X ≃ Y) :
      ElementaryTietzeMove
        (Presentation.ofRelators R)
        (Presentation.ofRelators (FreeGroup.freeGroupCongr e '' R))
  /-- Adjoin generators together with relators identifying them with prescribed words. -/
  | adjoinGenerators
      {X Y : Type u} (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
      ElementaryTietzeMove
        (Presentation.ofRelators R)
        (Presentation.ofRelators (Presented.adjoinGeneratorsRelators R word))
  /-- Eliminate a family of generators by substituting their defining words. -/
  | substituteDefinedGenerators
      {X Y : Type u} (R : Set (FreeGroup (Sum X Y)))
      (word : Y → FreeGroup X) :
      ElementaryTietzeMove
        (Presentation.ofRelators
          (Presented.relatorsWithDefinedGenerators R word))
        (Presentation.ofRelators
          (Presented.relatorsAfterSubstitutingDefinedGenerators R word))
  /-- Delete a family of generators whose defining relators make them trivial. -/
  | deleteTrivialGenerators
      {X Y : Type u} (R : Set (FreeGroup (Sum X Y))) :
      ElementaryTietzeMove
        (Presentation.ofRelators (Presented.relatorsWithTrivialGenerators R))
        (Presentation.ofRelators
          (Presented.relatorsAfterDeletingTrivialGenerators R))
  /--
  Transport to a sum decomposition of the generator type and then substitute the defining words.
  -/
  | substituteDefinedGeneratorsAlongEquiv
      {Z X Y : Type u} (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
      (word : Y → FreeGroup X) :
      ElementaryTietzeMove
        (Presentation.ofRelators
          (Presented.relatorsWithDefinedGeneratorsAlongEquiv R e word))
        (Presentation.ofRelators
          (Presented.relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv R e word))
  /-- Transport to a sum decomposition and then delete the generators made trivial by relators. -/
  | deleteTrivialGeneratorsAlongEquiv
      {Z X Y : Type u} (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
      ElementaryTietzeMove
        (Presentation.ofRelators
          (Presented.relatorsWithTrivialGeneratorsAlongEquiv R e))
        (Presentation.ofRelators
          (Presented.relatorsAfterDeletingTrivialGeneratorsAlongEquiv R e))

inductive Kind where
  /-- A relator-set replacement. -/
  | replaceRelators
  /-- A renaming of generators. -/
  | renameGenerators
  /-- An adjunction of generators with defining relators. -/
  | adjoinGenerators
  /-- A substitution eliminating generators with specified defining words. -/
  | substituteDefinedGenerators
  /-- A deletion of generators made trivial by their defining relators. -/
  | deleteTrivialGenerators
deriving DecidableEq, Repr

def kind {P Q : Presentation.{u}} : ElementaryTietzeMove P Q → Kind
  | .replaceRelators _ _ => .replaceRelators
  | .renameGenerators _ _ => .renameGenerators
  | .adjoinGenerators _ _ => .adjoinGenerators
  | .substituteDefinedGenerators _ _ => .substituteDefinedGenerators
  | .deleteTrivialGenerators _ => .deleteTrivialGenerators
  | .substituteDefinedGeneratorsAlongEquiv _ _ _ => .substituteDefinedGenerators
  | .deleteTrivialGeneratorsAlongEquiv _ _ => .deleteTrivialGenerators

def toCertificate {P Q : Presentation.{u}}
    (m : ElementaryTietzeMove P Q) : PresentationEquivCertificate P Q

inductive VerifiedTietzeScript :
    Presentation.{u} → Presentation.{u} → Type (u + 1) where
  /-- The empty script at a presentation. -/
  | nil (P : Presentation.{u}) : VerifiedTietzeScript P P
  /-- Prepend an elementary move to a verified script beginning at its target presentation. -/
  | cons {P Q R : Presentation.{u}}
      (head : ElementaryTietzeMove P Q)
      (tail : VerifiedTietzeScript Q R) : VerifiedTietzeScript P R

def singleton {P Q : Presentation.{u}} (m : ElementaryTietzeMove P Q) :
    VerifiedTietzeScript P Q

def replaceRelators
    {X : Type u} {R S : Set (FreeGroup X)}
    (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
    (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
    VerifiedTietzeScript
      (Presentation.ofRelators R) (Presentation.ofRelators S)

def renameGenerators
    {X Y : Type u} (R : Set (FreeGroup X)) (e : X ≃ Y) :
    VerifiedTietzeScript
      (Presentation.ofRelators R)
      (Presentation.ofRelators (FreeGroup.freeGroupCongr e '' R))

def adjoinGenerators
    {X Y : Type u} (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
    VerifiedTietzeScript
      (Presentation.ofRelators R)
      (Presentation.ofRelators (Presented.adjoinGeneratorsRelators R word))

def substituteDefinedGenerators
    {X Y : Type u} (R : Set (FreeGroup (Sum X Y)))
    (word : Y → FreeGroup X) :
    VerifiedTietzeScript
      (Presentation.ofRelators (Presented.relatorsWithDefinedGenerators R word))
      (Presentation.ofRelators
        (Presented.relatorsAfterSubstitutingDefinedGenerators R word))

def deleteTrivialGenerators
    {X Y : Type u} (R : Set (FreeGroup (Sum X Y))) :
    VerifiedTietzeScript
      (Presentation.ofRelators (Presented.relatorsWithTrivialGenerators R))
      (Presentation.ofRelators (Presented.relatorsAfterDeletingTrivialGenerators R))

def substituteDefinedGeneratorsAlongEquiv
    {Z X Y : Type u} (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
    (word : Y → FreeGroup X) :
    VerifiedTietzeScript
      (Presentation.ofRelators
        (Presented.relatorsWithDefinedGeneratorsAlongEquiv R e word))
      (Presentation.ofRelators
        (Presented.relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv R e word))

def deleteTrivialGeneratorsAlongEquiv
    {Z X Y : Type u} (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
    VerifiedTietzeScript
      (Presentation.ofRelators
        (Presented.relatorsWithTrivialGeneratorsAlongEquiv R e))
      (Presentation.ofRelators
        (Presented.relatorsAfterDeletingTrivialGeneratorsAlongEquiv R e))

def deleteTrivialGeneratorsOfPredicate
    {Z : Type u} (R : Set (FreeGroup Z)) (delete : Z → Prop)
    [DecidablePred delete] :
    VerifiedTietzeScript
      (Presentation.ofRelators
        (Presented.relatorsWithTrivialGeneratorsOfPredicate R delete))
      (Presentation.ofRelators
        (Presented.relatorsAfterDeletingTrivialGeneratorsOfPredicate R delete))

def trans {P Q R : Presentation.{u}}
    (s : VerifiedTietzeScript P Q) (t : VerifiedTietzeScript Q R) :
    VerifiedTietzeScript P R

def toCertificate {P Q : Presentation.{u}}
    (s : VerifiedTietzeScript P Q) : PresentationEquivCertificate P Q

def trace {P Q : Presentation.{u}}
    (s : VerifiedTietzeScript P Q) : List ElementaryTietzeMove.Kind

def moveCount {P Q : Presentation.{u}} (s : VerifiedTietzeScript P Q) : ℕ

def cost {P Q : Presentation.{u}}
    (s : VerifiedTietzeScript P Q)
    (weight : ElementaryTietzeMove.Kind → ℕ) : ℕ

theorem trace_nil (P : Presentation.{u}) :
    (VerifiedTietzeScript.nil P).trace = []

theorem trace_cons
    {P Q R : Presentation.{u}} (head : ElementaryTietzeMove P Q)
    (tail : VerifiedTietzeScript Q R) :
    (VerifiedTietzeScript.cons head tail).trace = head.kind :: tail.trace

theorem trace_singleton
    {P Q : Presentation.{u}} (move : ElementaryTietzeMove P Q) :
    (singleton move).trace = [move.kind]

theorem moveCount_nil (P : Presentation.{u}) :
    (VerifiedTietzeScript.nil P).moveCount = 0

theorem moveCount_cons
    {P Q R : Presentation.{u}} (head : ElementaryTietzeMove P Q)
    (tail : VerifiedTietzeScript Q R) :
    (VerifiedTietzeScript.cons head tail).moveCount = tail.moveCount + 1

theorem moveCount_singleton
    {P Q : Presentation.{u}} (move : ElementaryTietzeMove P Q) :
    (singleton move).moveCount = 1

theorem moveCount_trans
    {P Q R : Presentation.{u}} (s : VerifiedTietzeScript P Q)
    (t : VerifiedTietzeScript Q R) :
    (s.trans t).moveCount = s.moveCount + t.moveCount

theorem cost_nil
    (weight : ElementaryTietzeMove.Kind → ℕ) (P : Presentation.{u}) :
    (VerifiedTietzeScript.nil P).cost weight = 0

theorem cost_cons
    (weight : ElementaryTietzeMove.Kind → ℕ)
    {P Q R : Presentation.{u}} (head : ElementaryTietzeMove P Q)
    (tail : VerifiedTietzeScript Q R) :
    (VerifiedTietzeScript.cons head tail).cost weight =
      weight head.kind + tail.cost weight

theorem cost_singleton
    (weight : ElementaryTietzeMove.Kind → ℕ)
    {P Q : Presentation.{u}} (move : ElementaryTietzeMove P Q) :
    (singleton move).cost weight = weight move.kind