CubicPathwidth.Alg.Proofs2.Targets

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

Statements of the paper formalised here: Theorem 10.1, Lemma A.28, Lemma A.34.

import CubicPathwidth.Alg.Proofs2.A1TopWidth
import CubicPathwidth.Alg.Proofs2.A2MixedWidth
import CubicPathwidth.Alg.Proofs2.A3T4Width
import CubicPathwidth.Alg.Proofs2.AlgoT4Cor5
import CubicPathwidth.Alg.Proofs2.AlgoT4Internal
import CubicPathwidth.Alg.Proofs2.AlgoT4NoFallback
import CubicPathwidth.Alg.Proofs2.AlgoT4Thm4
import CubicPathwidth.Alg.Proofs2.CommitBound
import CubicPathwidth.Alg.Proofs2.D1KeyStepAt
import CubicPathwidth.Alg.Proofs2.D4LoopFuel
import CubicPathwidth.Alg.Proofs2.DeletionBound
import CubicPathwidth.Alg.Proofs2.K1Theorem1
import CubicPathwidth.Alg.Proofs2.K2Theorem2a
import CubicPathwidth.Alg.Proofs2.K3Mixed
import CubicPathwidth.Alg.Proofs2.L1PlainBags
import CubicPathwidth.Alg.Proofs2.L2PlainWidth
import CubicPathwidth.Alg.Proofs2.L3Connected
import CubicPathwidth.Alg.Proofs2.L4Connector
import CubicPathwidth.Alg.Proofs2.L5SwitchedWidth
import CubicPathwidth.Alg.Proofs2.N1ConnectorNoFallback
import CubicPathwidth.Alg.Proofs2.N2AlgoT1NoFallback
import CubicPathwidth.Alg.Proofs2.N3MixedNoFallback
import CubicPathwidth.Alg.Proofs2.OpsRecordFrame
import CubicPathwidth.Alg.Proofs2.R1ReduceFuel
import CubicPathwidth.Alg.Proofs2.R2ReduceMaximal
import CubicPathwidth.Alg.Proofs2.R3Records
import CubicPathwidth.Alg.Proofs2.R4TorsoSim
import CubicPathwidth.Alg.Proofs2.R5RecordMono
import CubicPathwidth.Alg.Proofs2.R6Confluent
import CubicPathwidth.Alg.Proofs2.R7Balanced
import CubicPathwidth.Alg.Proofs2.R8Attach
import CubicPathwidth.Alg.Proofs2.SweepBound
import CubicPathwidth.Alg.Proofs2.T4LoopInit
import CubicPathwidth.Alg.Proofs2.T4LoopRun
import CubicPathwidth.Alg.Proofs2.T4LoopStep
import CubicPathwidth.Alg.Proofs2.TorsoBridge
import CubicPathwidth.Alg.Proofs2.TorsoLocal
import CubicPathwidth.Alg.Proofs2.U1PdTw2Width
import CubicPathwidth.Alg.Proofs2.U2PdTw2NoFallback
import CubicPathwidth.Alg.Proofs2.U3UndoNoFallback
import CubicPathwidth.Alg.Proofs2.U4UndoWidth
import CubicPathwidth.Alg.Proofs2.U5ThinWidth
import CubicPathwidth.Alg.Proofs2.X1Relabel
import CubicPathwidth.Alg.Proofs2.X2RelabelExists
import CubicPathwidth.Alg.Proofs2.X3DegreeTransfer
import CubicPathwidth.Alg.Proofs2.X4LabelTransfer

/-!
# Stage 2 targets: no fallbacks, widths, and the theorems realized by the port

Every Stage 2 proof file takes the Stage 2 results it uses as hypotheses; this file
instantiates them. The targets are the statements of
`Spec2.lean` §§2–5 and of `Spec.lean` §7, each proved below as a theorem without
hypotheses.
-/

namespace CubicPathwidth.Alg

/-! ## Plan interfaces (`Plan2.lean`, `Plan2Deletion.lean`) -/

theorem reduceConfluent : ReduceConfluent :=
  R6.reduceConfluent_of torsoSim (reduceRecordMaximal_of reduceRecordNoFallback) recordMono
    opsRecordCongr opsRecordAppend

theorem balancedElimBag : BalancedElimBag :=
  balancedElimBag_of torsoSim (reduceRecordMaximal_of reduceRecordNoFallback)
    componentsConnected opsRecordCongr opsRecordAppend

theorem attachInvariant : AttachInvariant :=
  attachInvariant_of torsoSim recordMono componentsConnected opsRecordCongr opsRecordAppend

theorem t4LoopInvInit : T4LoopInvInit :=
  t4LoopInvInit_of (reduceRecordMaximal_of reduceRecordNoFallback) componentsConnected
    opsRecordCongr

theorem t4LoopInvStep : T4LoopInvStep :=
  t4LoopInvStep_of (reduceRecordMaximal_of reduceRecordNoFallback) componentsConnected
    opsRecordCongr opsRecordAppend opsRecordFrame

theorem commitBound : CommitBound :=
  commitBound_of keyStepAt torsoSim torsoLocal torsoPotentialBridge
    (reduceRecordMaximal_of reduceRecordNoFallback) componentsConnected opsRecordCongr

theorem t4LoopRun : T4LoopRun := t4LoopRun_of t4LoopInvStep commitBound

theorem t4FinalFacts : T4FinalFacts := t4FinalFacts_of t4LoopRun t4LoopInvInit

/-! ## `Spec.lean` §7 and `Spec2.lean` §2: no fallbacks -/

-- `connectorNoFallback` and `reduceRecordNoFallback` are proved directly (N1, R1).

theorem reduceRecordMaximal : ReduceRecordMaximal := reduceRecordMaximal_of reduceRecordNoFallback

theorem pdTw2NoFallback : PdTw2NoFallback :=
  pdTw2NoFallback_of reduceRecordNoFallback reduceRecordMaximal opsRecordCongr recordMono
    reduceConfluent balancedElimBag

theorem undoNoFallback : UndoNoFallback :=
  undoNoFallback_of attachInvariant pdTw2NoFallback reduceConfluent opsRecordCongr

theorem t4LoopNoFallback : T4LoopNoFallback := t4LoopNoFallback_of reduceRecordNoFallback

theorem algoT1NoFallback : AlgoT1NoFallback := algoT1NoFallback_of connectorNoFallback

theorem algoMixedNoFallback : AlgoMixedNoFallback :=
  algoMixedNoFallback_of reduceRecordNoFallback reduceRecordMaximal opsRecordCongr undoNoFallback

theorem algoT4NoFallback : AlgoT4NoFallback :=
  algoT4NoFallback_of reduceRecordNoFallback t4LoopNoFallback undoNoFallback t4LoopRun
    t4LoopInvInit

/-! ## `Spec2.lean` §3: width bridges -/

theorem plainLayoutWidth : PlainLayoutWidth := plainLayoutWidth_of plainLayoutBags
-- `connectorLemma10` and `pdTw2Width` are proved directly (L4, U1).

theorem switchedLayoutWidth : SwitchedLayoutWidth :=
  switchedLayoutWidth_of connectorLemma10 connectorNoFallback

theorem undoWidth : UndoWidth := undoWidth_of pdTw2Width

theorem deletionProcessBound : DeletionProcessBound :=
  deletionProcessBound_of t4LoopRun t4LoopInvInit reduceRecordMaximal

/-! ## `Spec2.lean` §4: per algorithm -/

theorem algoT1Width : AlgoT1Width := algoT1Width_of switchedLayoutWidth

theorem algoT2aWidth : AlgoT2aWidth := algoT2aWidth_of plainLayoutWidth

theorem algoMixedWidth : AlgoMixedWidth := algoMixedWidth_of undoWidth

theorem algoT4Width : AlgoT4Width := algoT4Width_of undoWidth

theorem thinComponentWidth : ThinComponentWidth := thinComponentWidth_of undoWidth

/-! ## `Spec2.lean` §5: the theorems realized by the implementation -/

theorem algoT1RealizesTheorem1 : AlgoT1RealizesTheorem1 :=
  algoT1RealizesTheorem1_of algoT1Width algoT1NoFallback relabelOfSimpleGraph labelTransfer

theorem algoT2aRealizesTheorem2a : AlgoT2aRealizesTheorem2a :=
  algoT2aRealizesTheorem2a_of algoT2aWidth relabelOfSimpleGraph labelTransfer

theorem algoMixedRealizesTheorem2b : AlgoMixedRealizesTheorem2b :=
  algoMixedRealizesTheorem2b_of algoMixedWidth algoMixedNoFallback reduceRecordMaximal
    relabelExists degreeTransfer labelTransfer plainLayoutWidth

theorem algoMixedRealizesTheorem2c : AlgoMixedRealizesTheorem2c :=
  algoMixedRealizesTheorem2c_of algoMixedWidth algoMixedNoFallback reduceRecordMaximal
    relabelExists degreeTransfer labelTransfer plainLayoutWidth

theorem algoMixedRealizesTheorem3P : AlgoMixedRealizesTheorem3P :=
  algoMixedRealizesTheorem3P_of algoMixedWidth algoMixedNoFallback reduceRecordMaximal
    relabelExists degreeTransfer labelTransfer plainLayoutWidth

theorem algoMixedRealizesTheorem3R : AlgoMixedRealizesTheorem3R :=
  algoMixedRealizesTheorem3R_of algoMixedWidth algoMixedNoFallback reduceRecordMaximal
    relabelExists degreeTransfer labelTransfer plainLayoutWidth

theorem algoMixedRealizesTheorem3S : AlgoMixedRealizesTheorem3S :=
  algoMixedRealizesTheorem3S_of algoMixedWidth algoMixedNoFallback reduceRecordMaximal
    relabelExists degreeTransfer labelTransfer plainLayoutWidth

theorem algoT4InternalBound : AlgoT4InternalBound :=
  algoT4InternalBound_of
    (sweepComponentBound_of plainLayoutWidth relabelExists degreeTransfer labelTransfer)
    algoT4Width thinComponentWidth deletionProcessBound algoT4NoFallback t4FinalFacts
    psiPortFacts relabelOfSimpleGraph degreeTransfer

theorem algoT4RealizesTheorem4 : AlgoT4RealizesTheorem4 :=
  algoT4RealizesTheorem4_of algoT4InternalBound

theorem algoT4RealizesCorollary5 : AlgoT4RealizesCorollary5 :=
  algoT4RealizesCorollary5_of algoT4InternalBound

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.connectorNoFallback
#print axioms CubicPathwidth.Alg.reduceRecordNoFallback
#print axioms CubicPathwidth.Alg.pdTw2NoFallback
#print axioms CubicPathwidth.Alg.algoT1NoFallback
#print axioms CubicPathwidth.Alg.algoMixedNoFallback
#print axioms CubicPathwidth.Alg.algoT4NoFallback
#print axioms CubicPathwidth.Alg.reduceRecordMaximal
#print axioms CubicPathwidth.Alg.undoNoFallback
#print axioms CubicPathwidth.Alg.t4LoopNoFallback
#print axioms CubicPathwidth.Alg.plainLayoutWidth
#print axioms CubicPathwidth.Alg.connectorLemma10
#print axioms CubicPathwidth.Alg.switchedLayoutWidth
#print axioms CubicPathwidth.Alg.pdTw2Width
#print axioms CubicPathwidth.Alg.undoWidth
#print axioms CubicPathwidth.Alg.deletionProcessBound
#print axioms CubicPathwidth.Alg.algoT1Width
#print axioms CubicPathwidth.Alg.algoT2aWidth
#print axioms CubicPathwidth.Alg.algoMixedWidth
#print axioms CubicPathwidth.Alg.algoT4Width
#print axioms CubicPathwidth.Alg.thinComponentWidth
#print axioms CubicPathwidth.Alg.algoT1RealizesTheorem1
#print axioms CubicPathwidth.Alg.algoT2aRealizesTheorem2a
#print axioms CubicPathwidth.Alg.algoMixedRealizesTheorem2b
#print axioms CubicPathwidth.Alg.algoMixedRealizesTheorem2c
#print axioms CubicPathwidth.Alg.algoMixedRealizesTheorem3P
#print axioms CubicPathwidth.Alg.algoMixedRealizesTheorem3R
#print axioms CubicPathwidth.Alg.algoMixedRealizesTheorem3S
#print axioms CubicPathwidth.Alg.algoT4RealizesTheorem4
#print axioms CubicPathwidth.Alg.algoT4RealizesCorollary5
Back to top