Something went wrong. Try again.
The Package Calculus
Something went wrong. Try again.
1.3 kB · 32 lines
at dev
123456789101112131415161718192021222324252627282930313233import PackageCalculus.Extensions.Feature.Lifting.Definition
namespace PackageCalculus.Feature
variable {N : Type*} [DecidableEq N] {V : Type*} [DecidableEq V] {F : Type*} [DecidableEq F] [Fintype F]variable {N' : Type*} [DecidableEq N'] [hfn : HasFeatureNames N F N']
/-! ## Lifting soundness & completeness -/
theorem liftResolution_soundness (R_f : Real N V) (support : Support N V F) (Δ_f : FeatDepRel N V F) (Δ_a : AddlDepRel N V F) (r : Package N V) (S' : Finset (Package N' V)) (hres : IsResolution (featureReal R_f support) (featureDeps R_f support Δ_f Δ_a) (embedPkg F r) S') (hroot_no_support : ∀ f, (r, f) ∉ support) : IsFeatureResolution R_f support Δ_f Δ_a r (liftResolution S') := by have h := feature_soundness R_f support Δ_f Δ_a r S' hres hroot_no_support -- soundnessWitness and liftResolution agree extensionally suffices heq : liftResolution S' = soundnessWitness S' by rw [heq]; exact h simp only [liftResolution, soundnessWitness] congr 1 ext ⟨n, v⟩ simp only [Finset.mem_filterMap, Finset.mem_preimage, embedPkg] constructor · rintro ⟨_, hp', hinv⟩ have := tryInvPkg_some hinv; simp only [embedPkg] at this; exact this ▸ hp' · exact fun hp => ⟨_, hp, by simp [tryInvPkg, hfn.tryOrigN_origN]⟩
end PackageCalculus.Feature