Something went wrong. Try again.
The Package Calculus
Something went wrong. Try again.
1.4 kB · 41 lines
at dev
123456789101112131415161718192021222324252627282930313233343536373839404142import PackageCalculus.Versions.Lifting.Definitionimport PackageCalculus.Versions.Reduction.Correctness
set_option linter.unusedSectionVars false
namespace PackageCalculus
variable {V : Type*} [DecidableEq V]variable {N : Type*} [DecidableEq N]
/-! ## Round-trip theorem -/
/-- `v` is a version of `m` in `R` iff the package `(m, v)` is real. -/private theorem mem_repoVersions {R : Real N V} {m : N} {v : V} : v ∈ repoVersions R m ↔ (m, v) ∈ R := by simp only [repoVersions, Finset.mem_image, Finset.mem_filter] constructor · rintro ⟨⟨a, b⟩, ⟨hR, ha⟩, hb⟩ dsimp only at ha hb subst ha; subst hb exact hR · exact fun h => ⟨(m, v), ⟨h, rfl⟩, rfl⟩
private theorem inter_repoVersions (R : Real N V) (m : N) (vs : Finset V) : vs ∩ repoVersions R m = vs.filter (fun v => (m, v) ∈ R) := by ext v simp only [Finset.mem_inter, Finset.mem_filter, mem_repoVersions]
/-- Reducing the lifted formulas gives back the original concrete deps, restricted to real versions. -/theorem liftVFDeps_vfReduce [LinearOrder V] (R : Real N V) (Δ : DepRel N V) : vfReduce R (liftVFDeps R Δ) = Δ.restrictReal R := by unfold vfReduce liftVFDeps DepRel.restrictReal rw [Finset.image_image] refine Finset.image_congr fun x _ => ?_ obtain ⟨p, m, vs⟩ := x simp only [Function.comp_apply] rw [finsetToFormula_eval, inter_repoVersions]
end PackageCalculus