Something went wrong. Try again.
The Package Calculus
Something went wrong. Try again.
1.2 kB · 30 lines
at dev
12345678910111213141516171819202122232425262728293031import PackageCalculus.Extensions.Concurrent.Lifting.Definition
namespace PackageCalculus.Concurrent
set_option linter.unusedSectionVars false
variable {N : Type*} [DecidableEq N] {V : Type*} [DecidableEq V] {G : Type*} [DecidableEq G]variable {N' : Type*} [DecidableEq N'] {V' : Type*} [DecidableEq V']variable [hcnm : HasConcurrentNames N V G N'] [hcvr : HasConcurrentVersions V G V']
/-! ## Lifting soundness & completeness -/
theorem liftResolution_soundness (R_C : Real N V) (Δ_C : DepRel N V) (g : V → G) (r : Package N V) (S' : Finset (Package N' V')) (hres : IsResolution (concurrentReal R_C Δ_C g) (concurrentDeps Δ_C g) (embedPkg g r) S') (hfunc : Δ_C.FunctionalInName) : ∃ π, IsConcurrentResolution R_C Δ_C g r (liftResolution g S') π := by have hsound := concurrent_soundness R_C Δ_C g r S' hres hfunc -- The preimageS used internally equals our liftResolution extensionally suffices heq : liftResolution g S' = S'.preimage (embedPkg g) (Set.InjOn.mono (Set.subset_univ _) (Function.Injective.injOn (embedPkgFn_injective g))) by rw [heq]; exact ⟨_, hsound⟩ ext p; simp [mem_liftResolution, Finset.mem_preimage]
end PackageCalculus.Concurrent