You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
These tables map each definition and theorem in the paper to its mechanised counterpart in this development.
All file paths are relative to the PackageCalculus/ source directory.
Where the paper writes structured names like ⟨n, vs⟩ ∈ N or ⟨n, f⟩, the Lean uses dedicated inductive name/version types and Has*Names / Has*Versions typeclasses to inject them.
The paper states one standing condition on every dependency relation: Functional in Name (Def 3.1.2).
In Lean it appears as an explicit hypothesis (DepRel.FunctionalInName) on the theorems that consume it.
The paper's normalisation remark -- merging same-name entries per depender by intersecting their version sets -- is mechanised as DepRel.merge (merge_functionalInName, merge_resolution_iff), alongside DepRel.restrictReal (restrictReal_resolution_iff) for restricting version sets to real packages; both preserve the set of resolutions.
Lifting is mechanised per extension under Extensions/<Extension>/Lifting/ (and Versions/Lifting/): Definition.lean defines lift, Retraction.lean proves the round trip, and Soundness.lean/Completeness.lean carry core resolutions back to extension resolutions.
Extension
Round trip
Mechanised statement
Side conditions
Conflict
conflictLift_conflictReduce
lift ∘ reduce = id (packages, dependencies, conflicts)
--
Concurrent
concurrentLift_concurrentReduce
lift ∘ reduce = id (packages, dependencies)
DepRel.FunctionalInName
Peer
peerLift_peerReduce
lift ∘ reduce = id (packages, dependencies, peers)
NNF atom-set normal form (no formula retraction exists)
--
Variable formulae
liftAtoms_vfDeps, satisfies_iff_atoms
atom-set normal form, comparisons up to extension
--
Version formulae
vfReduce ∘ liftVFDeps = restrictReal
section direction only
--
Where the statement is weaker than lift ∘ reduce = id, the loss is syntactic rather than semantic: the lift recovers a normal form that is proven faithful.
Formulae are recovered as their NNF atom sets, and satisfies_iff_atoms shows a resolution satisfies a formula iff it satisfies its atoms; a variable comparison is recovered as its extension, which is all evaluation consults; virtual and version-formula dependencies are recovered up to restrictReal, which removes only versions no resolution can select.
The Virtual provides relation is likewise recovered as a normal form, its instantiation on Δ -- the admissible (provider, name, depender) triples -- and instantiate_resolution_congr shows resolutions consult it only through this instantiation; only the guards' behaviour on dependencies outside Δ is lost.
Each side condition's docstring in the Lean states why it is needed.
Appendix B -- DependencyResolution complexity
The paper's NP-completeness result (Thm 3.1.4) combines NP-hardness -- a polynomial-time reduction from 3SAT -- with NP-membership, which the paper establishes by direct polynomial-time verification of a candidate resolution (root inclusion, dependency closure, version uniqueness).
In Lean we mechanise the reduction's soundness and completeness (below); the polynomial-time bound and the membership verification are argued by inspection in the paper, not formalised.
The SAT encoding in Appendix C is a separate SAT-based solving method (formalised in SATEncoding.lean).
Defs C.5 and C.6 (resolution ordering, ordered SAT encoding) and Appendix E (build graph, optional dependencies) are definitional discussion with no accompanying theorems, and are not mechanised.