Something went wrong. Try again.
The Package Calculus
Something went wrong. Try again.
1.1 kB · 26 lines
at dev
123456789101112131415161718192021222324252627import PackageCalculus.Extensions.Virtual.Lifting.Definition
namespace PackageCalculus.Virtual
variable {N : Type*} [DecidableEq N] {V : Type*} [DecidableEq V]variable {N' : Type*} [DecidableEq N'] {V' : Type*} [DecidableEq V']variable [hvn : HasVirtualNames N V N'] [hvv : HasVirtualVersions N V V']
/-! ## Lifting soundness -/
theorem liftResolution_soundness (R_v : Real N V) (Delta_v : DepRel N V) (prov : ProvidesRel N V) (r : Package N V) (S' : Finset (Package N' V')) (hres : IsResolution (virtualReal R_v Delta_v prov) (virtualDeps Delta_v R_v prov) (embedPkg r) S') : ∃ rho, IsVirtualResolution R_v Delta_v prov r (liftResolution S') rho := by have hsound := virtual_soundness R_v Delta_v prov 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 ⟨_, hsound⟩ ext p; simp [← embedPkgFn_eq_embedPkg, mem_liftResolution, Finset.mem_preimage]
end PackageCalculus.Virtual