CubicPathwidth.Alg.Proofs.Targets

Source file CubicPathwidth/Alg/Proofs/Targets.lean of the Lean project (how it is built).

Statements of the paper formalised here: Theorem 10.1.

import CubicPathwidth.Alg.Proofs.G1WFBasics
import CubicPathwidth.Alg.Proofs.G2AddEdge
import CubicPathwidth.Alg.Proofs.G3RemoveNode
import CubicPathwidth.Alg.Proofs.G4Induced
import CubicPathwidth.Alg.Proofs.G5Components
import CubicPathwidth.Alg.Proofs.G6UnionAll
import CubicPathwidth.Alg.Proofs.G7Concat
import CubicPathwidth.Alg.Proofs.G8SeparatorGlue
import CubicPathwidth.Alg.Proofs.B1Bridge
import CubicPathwidth.Alg.Proofs.B2OfSimpleGraph
import CubicPathwidth.Alg.Proofs.C1Perm
import CubicPathwidth.Alg.Proofs.C2PlainLayout
import CubicPathwidth.Alg.Proofs.C3Connector
import CubicPathwidth.Alg.Proofs.C4Switched
import CubicPathwidth.Alg.Proofs.C5ReduceRecord
import CubicPathwidth.Alg.Proofs.C6PdTw2
import CubicPathwidth.Alg.Proofs.C7Undo
import CubicPathwidth.Alg.Proofs.T1AppendIsolated
import CubicPathwidth.Alg.Proofs.T2InitInv
import CubicPathwidth.Alg.Proofs.T3LoopPreserves
import CubicPathwidth.Alg.Proofs.A12Top
import CubicPathwidth.Alg.Proofs.A3T4
import CubicPathwidth.Alg.Proofs.E14Exported

/-!
# Stage 1 targets: validity of the Lean port of `sweep.py`

Every proof file takes the results it depends on as hypotheses; this file
instantiates them. The eight targets of the approved specification are the theorems
`algoT1Valid`, `algoT2aValid`, `algoMixedValid`, `algoT4Valid` and
`algoT1Exported`, `algoT2aExported`, `algoMixedExported`, `algoT4Exported`.
-/

namespace CubicPathwidth.Alg

/-! ## Graph layer and contracts -/

theorem removeNodeSpec : RemoveNodeSpec := removeNodeSpec_of wfBasics

theorem inducedSpec : InducedSpec := inducedSpec_of wfBasics addEdgeSpec

theorem componentsSpec : ComponentsSpec := componentsSpec_of wfBasics

theorem unionAllSpec : UnionAllSpec := unionAllSpec_of wfBasics addEdgeSpec

theorem concatValid : ConcatValid := concatValid_of wfBasics unionAllSpec

theorem separatorGlueValid : SeparatorGlueValid := separatorGlueValid_of wfBasics inducedSpec

theorem validPDBridge : ValidPDBridge := validPDBridge_of wfBasics

theorem plainLayoutValid : PlainLayoutValid := plainLayoutValid_of wfBasics plainOrderPerm

theorem switchedLayoutValid : SwitchedLayoutValid :=
  switchedLayoutValid_of wfBasics switchedOrderPerm connectorOrderMem

theorem reduceRecordSpec : ReduceRecordSpec :=
  reduceRecordSpec_of wfBasics addEdgeSpec removeNodeSpec

theorem pdTw2Valid : PdTw2Valid :=
  pdTw2Valid_of wfBasics inducedSpec componentsSpec separatorGlueValid reduceRecordSpec

theorem undoValid : UndoValid := undoValid_of wfBasics inducedSpec componentsSpec pdTw2Valid

theorem appendIsolatedValid : AppendIsolatedValid := appendIsolatedValid_of wfBasics inducedSpec

theorem t4InitInv : T4InitInv :=
  t4InitInv_of wfBasics inducedSpec componentsSpec reduceRecordSpec

theorem t4LoopPreserves : T4LoopPreserves :=
  t4LoopPreserves_of wfBasics removeNodeSpec inducedSpec componentsSpec reduceRecordSpec

/-! ## The eight targets -/

theorem algoT1Valid : AlgoT1Valid := algoT1Valid_of switchedLayoutValid

theorem algoT2aValid : AlgoT2aValid := algoT2aValid_of plainLayoutValid

theorem algoMixedValid : AlgoMixedValid :=
  algoMixedValid_of wfBasics inducedSpec reduceRecordSpec plainLayoutValid undoValid

theorem algoT4Valid : AlgoT4Valid :=
  algoT4Valid_of wfBasics inducedSpec unionAllSpec concatValid plainLayoutValid undoValid
    t4InitInv t4LoopPreserves appendIsolatedValid

theorem algoT1Exported : AlgoT1Exported :=
  algoT1Exported_of validPDBridge ofSimpleGraphSpec algoT1Valid

theorem algoT2aExported : AlgoT2aExported :=
  algoT2aExported_of validPDBridge ofSimpleGraphSpec algoT2aValid

theorem algoMixedExported : AlgoMixedExported :=
  algoMixedExported_of validPDBridge ofSimpleGraphSpec algoMixedValid

theorem algoT4Exported : AlgoT4Exported :=
  algoT4Exported_of validPDBridge ofSimpleGraphSpec algoT4Valid

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.algoT1Valid
#print axioms CubicPathwidth.Alg.algoT2aValid
#print axioms CubicPathwidth.Alg.algoMixedValid
#print axioms CubicPathwidth.Alg.algoT4Valid
#print axioms CubicPathwidth.Alg.algoT1Exported
#print axioms CubicPathwidth.Alg.algoT2aExported
#print axioms CubicPathwidth.Alg.algoMixedExported
#print axioms CubicPathwidth.Alg.algoT4Exported