Something went wrong. Try again.
The Package Calculus
Something went wrong. Try again.
3.7 kB · 80 lines
at dev
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081import PackageCalculus.Core.Definitionimport Mathlib.Logic.Embedding.Basicimport Mathlib.Data.Finset.Image
/-! # Conflict extension: definitions
A `ConflictRel` records pairs `(p, n, vs)` where package `p` excludes name `n`at versions `vs`. `IsConflictResolution` extends `IsResolution` with theconstraint that no excluded package may be present. -/
namespace PackageCalculus.Conflict
open Function
variable {N : Type*} [DecidableEq N] {V : Type*} [DecidableEq V]
/-- p Γ (n, vs) means package p conflicts with name n at versions vs. -/abbrev ConflictRel (N V : Type*) := Finset (Package N V × N × Finset V)
structure IsConflictResolution (R : Real N V) (Δ : DepRel N V) (Γ : ConflictRel N V) (r : Package N V) (S : Finset (Package N V)) : Prop where core : IsResolution R Δ r S conflict_avoidance : ∀ p ∈ S, ∀ n : N, ∀ vs : Finset V, (p, n, vs) ∈ Γ → ¬∃ v ∈ vs, (n, v) ∈ S
/-! ## Extended type interfaces
Each reduction encodes extension-specific constraints by extending the name andversion types with synthetic constructors. These typeclasses abstract over theextended types so that lifting functions (`liftReal`, `liftDeps`, etc.) only seetheir own constructors and are agnostic to constructors added by otherextensions. This makes lifting modular under reduction composition: composingmultiple reductions produces a type with constructors from all of them, but eachextension's lift still works unchanged.
Crucially, this allows lifting a single extension out of a composed type withoutunwrapping the others. A solver producing a core resolution over thefully-composed type can be lifted directly by any extension whose constraintsthe consumer cares about, ignoring unsupported extensions entirely. -/
class HasConflictNames (N V : Type*) (N' : outParam Type*) where origN : N ↪ N' /-- Synthetic conflict-witness name for a (name, version-set) pair. -/ syntheticN : N → Finset V → N' syntheticN_injective : Injective2 syntheticN origN_ne_syntheticN : ∀ n₁ n₂ (vs : Finset V), origN n₁ ≠ syntheticN n₂ vs syntheticN_ne_origN : ∀ n₁ (vs : Finset V) n₂, syntheticN n₁ vs ≠ origN n₂ /-- Decidable partial inverse of `origN`. -/ tryOrigN : N' → Option N tryOrigN_origN : ∀ n, tryOrigN (origN n) = some n tryOrigN_some : ∀ n' n, tryOrigN n' = some n → origN n = n' /-- Decidable partial inverse of `syntheticN`. -/ trySyntheticN : N' → Option (N × Finset V) trySyntheticN_syntheticN : ∀ n vs, trySyntheticN (syntheticN n vs) = some (n, vs) trySyntheticN_some : ∀ n' p, trySyntheticN n' = some p → syntheticN p.1 p.2 = n'
attribute [simp] HasConflictNames.origN_ne_syntheticN HasConflictNames.syntheticN_ne_origN
class HasConflictVersions (V : Type*) (V' : outParam Type*) where origV : V ↪ V' /-- Synthetic zero version for conflict witnesses. -/ zeroV : V' /-- Synthetic one version for conflict witnesses. -/ oneV : V' origV_ne_zeroV : ∀ v, origV v ≠ zeroV zeroV_ne_origV : ∀ v, zeroV ≠ origV v origV_ne_oneV : ∀ v, origV v ≠ oneV oneV_ne_origV : ∀ v, oneV ≠ origV v zeroV_ne_oneV : zeroV ≠ oneV oneV_ne_zeroV : oneV ≠ zeroV /-- Decidable partial inverse of `origV`. -/ tryOrigV : V' → Option V tryOrigV_origV : ∀ v, tryOrigV (origV v) = some v tryOrigV_some : ∀ v' v, tryOrigV v' = some v → origV v = v'
attribute [simp] HasConflictVersions.origV_ne_zeroV HasConflictVersions.zeroV_ne_origV HasConflictVersions.origV_ne_oneV HasConflictVersions.oneV_ne_origV HasConflictVersions.zeroV_ne_oneV HasConflictVersions.oneV_ne_zeroV
end PackageCalculus.Conflict