Something went wrong. Try again.
The Package Calculus
Something went wrong. Try again.
1.0 kB · 26 lines
at dev
123456789101112131415161718192021222324252627import PackageCalculus.Extensions.PackageFormula.Lifting.Definition
namespace PackageCalculus.PkgFormula
set_option linter.unusedSectionVars false
variable {N : Type*} [DecidableEq N] {V : Type*} [DecidableEq V]variable {N' : Type*} [DecidableEq N'] {V' : Type*} [DecidableEq V']variable [hpn : HasPFNames N V N'] [hpv : Conflict.HasConflictVersions V V']
/-! ## Lifting soundness & completeness -/
theorem liftResolution_soundness (R_Ψ : Real N V) (Δ_Ψ : PFDepRel N V) (r : Package N V) (S' : Finset (Package N' V')) (hres : IsResolution (pfReal R_Ψ Δ_Ψ) (pfDeps Δ_Ψ) (embedPkg r) S') : IsPFResolution R_Ψ Δ_Ψ r (liftResolution S') := by have h := package_formula_soundness R_Ψ Δ_Ψ r S' hres suffices heq : liftResolution S' = S'.preimage embedPkg (Set.InjOn.mono (Set.subset_univ _) (Function.Injective.injOn embedPkgFn_injective)) by rw [heq]; exact h ext p; simp [← embedPkgFn_eq_embedPkg, mem_liftResolution, Finset.mem_preimage]
end PackageCalculus.PkgFormula