Something went wrong. Try again.
The Package Calculus
Something went wrong. Try again.
10 kB · 233 lines
at dev
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234import PackageCalculus.Extensions.Concurrent.Reduction.Definitionimport Mathlib.Data.Finset.Preimage
/-! # Concurrent extension: soundness
Any core resolution of the concurrent encoding projects back to a validconcurrent resolution of the original problem. -/
namespace PackageCalculus.Concurrent
open Classical
set_option linter.unusedSectionVars false
variable {N : Type*} {V : Type*} {G : Type*}variable {N' : Type*} {V' : Type*}variable [DecidableEq N] [DecidableEq V] [DecidableEq G] [DecidableEq N'] [DecidableEq V']variable [hcnm : HasConcurrentNames N V G N'] [hcvr : HasConcurrentVersions V G V']
theorem embedPkg_injective (g : V → G) : Function.Injective (embedPkg (N := N) (N' := N') (V' := V') g) := by intro ⟨n₁, v₁⟩ ⟨n₂, v₂⟩ h simp only [embedPkg, Prod.mk.injEq] at h obtain ⟨h1, h2⟩ := h have ⟨hn, _⟩ := hcnm.granularN_injective h1 have hv := hcvr.origV.injective h2 exact Prod.ext hn hv
private noncomputable def preimageS (g : V → G) (S : Finset (Package N' V')) : Finset (Package N V) := S.preimage (embedPkg g) (Set.InjOn.mono (Set.subset_univ _) (Function.Injective.injOn (embedPkg_injective g)))
theorem mem_preimageS {g : V → G} {S : Finset (Package N' V')} {p : Package N V} : p ∈ preimageS g S ↔ embedPkg g p ∈ S := by simp [preimageS, Finset.mem_preimage]
/-- Construct the parent-witness relation π as a Finset from Δ_C and S. -/def soundnessπ (Δ_C : DepRel N V) (g : V → G) (S : Finset (Package N' V')) : Finset (Package N V × Package N V) := Δ_C.biUnion (fun ⟨⟨n, v⟩, m, vs⟩ => vs.filter (fun u => (hcnm.granularN m (g u), hcvr.origV u) ∈ S ∧ (hcnm.granularN n (g v), hcvr.origV v) ∈ S ∧ (isSplit g vs → ∃ u₀ ∈ vs, (hcnm.intermediateN n v m, hcvr.granV (g u₀)) ∈ S ∧ g u = g u₀)) |>.image (fun u => ((m, u), (n, v))))
theorem mem_soundnessπ {Δ_C : DepRel N V} {g : V → G} {S : Finset (Package N' V')} {pair : Package N V × Package N V} : pair ∈ soundnessπ Δ_C g S ↔ ∃ n v m vs u, ((n, v), m, vs) ∈ Δ_C ∧ (hcnm.granularN n (g v), hcvr.origV v) ∈ S ∧ u ∈ vs ∧ (hcnm.granularN m (g u), hcvr.origV u) ∈ S ∧ (isSplit g vs → ∃ u₀ ∈ vs, (hcnm.intermediateN n v m, hcvr.granV (g u₀)) ∈ S ∧ g u = g u₀) ∧ pair = ((m, u), (n, v)) := by simp only [soundnessπ, Finset.mem_biUnion, Finset.mem_image, Finset.mem_filter] constructor · rintro ⟨⟨⟨n, v⟩, m, vs⟩, hdep, u, ⟨huv, huS, hvS, hspl⟩, rfl⟩ exact ⟨n, v, m, vs, u, hdep, hvS, huv, huS, hspl, rfl⟩ · rintro ⟨n, v, m, vs, u, hdep, hvS, huv, huS, hspl, rfl⟩ exact ⟨⟨⟨n, v⟩, m, vs⟩, hdep, u, ⟨huv, huS, hvS, hspl⟩, rfl⟩
theorem embedPkg_mem_concurrentReal {g : V → G} {p : Package N V} {R_C : Real N V} {Δ_C : DepRel N V} (h : embedPkg g p ∈ concurrentReal (N' := N') (V' := V') R_C Δ_C g) : p ∈ R_C := by simp only [concurrentReal, embedReal, Finset.mem_union, Finset.mem_image, Finset.mem_biUnion] at h rcases h with ⟨q, hqR, heq⟩ | ⟨a, haΔ, hmem⟩ · simp only [embedPkg, Prod.mk.injEq] at heq obtain ⟨h1, h2⟩ := heq have ⟨hn, _⟩ := hcnm.granularN_injective h1 have hv := hcvr.origV.injective h2 exact (Prod.ext hn hv : q = p) ▸ hqR · obtain ⟨⟨n, v⟩, m, vs⟩ := a simp only at hmem split at hmem · simp only [Finset.mem_image, embedPkg, Prod.mk.injEq] at hmem obtain ⟨_, _, ⟨heq, _⟩⟩ := hmem exact absurd heq.symm (hcnm.granularN_ne_intermediateN _ _ _ _ _) · exact (List.mem_nil_iff _).mp hmem |>.elim
theorem mem_concurrentDeps_direct {Δ_C : DepRel N V} {g : V → G} {n : N} {v : V} {m : N} {vs : Finset V} {u₀ : V} (hdep : ((n, v), m, vs) ∈ Δ_C) (hdir : isDirect g vs) (hu₀ : u₀ ∈ vs) : ((hcnm.granularN n (g v), hcvr.origV v), hcnm.granularN m (g u₀), vs.map hcvr.origV) ∈ concurrentDeps (N' := N') (V' := V') Δ_C g := by simp only [concurrentDeps, Finset.mem_union, Finset.mem_biUnion] left; left; left refine ⟨⟨⟨n, v⟩, m, vs⟩, hdep, ?_⟩ simp only rw [if_pos hdir] exact Finset.mem_image.mpr ⟨u₀, hu₀, rfl⟩
theorem mem_concurrentDeps_split1 {Δ_C : DepRel N V} {g : V → G} {n : N} {v : V} {m : N} {vs : Finset V} (hdep : ((n, v), m, vs) ∈ Δ_C) (hspl : isSplit g vs) : ((hcnm.granularN n (g v), hcvr.origV v), hcnm.intermediateN n v m, (vs.image (fun u => g u)).map hcvr.granV) ∈ concurrentDeps (N' := N') (V' := V') Δ_C g := by simp only [concurrentDeps, Finset.mem_union, Finset.mem_biUnion] left; left; right refine ⟨⟨⟨n, v⟩, m, vs⟩, hdep, ?_⟩ simp only rw [if_pos hspl] exact Finset.mem_singleton.mpr rfl
theorem mem_concurrentDeps_split2 {Δ_C : DepRel N V} {g : V → G} {n : N} {v : V} {m : N} {vs : Finset V} {u₀ : V} (hdep : ((n, v), m, vs) ∈ Δ_C) (hspl : isSplit g vs) (hu₀ : u₀ ∈ vs) : ((hcnm.intermediateN n v m, hcvr.granV (g u₀)), hcnm.granularN m (g u₀), (vs.filter (fun w => g w = g u₀)).map hcvr.origV) ∈ concurrentDeps (N' := N') (V' := V') Δ_C g := by simp only [concurrentDeps, Finset.mem_union, Finset.mem_biUnion] left; right refine ⟨⟨⟨n, v⟩, m, vs⟩, hdep, ?_⟩ simp only rw [if_pos hspl] exact Finset.mem_image.mpr ⟨u₀, hu₀, rfl⟩
theorem mem_concurrentDeps_empty {Δ_C : DepRel N V} {g : V → G} {n : N} {v : V} {m : N} (hdep : ((n, v), m, (∅ : Finset V)) ∈ Δ_C) : ((hcnm.granularN n (g v), hcvr.origV v), hcnm.intermediateN n v m, (∅ : Finset V')) ∈ concurrentDeps (N' := N') (V' := V') Δ_C g := by simp only [concurrentDeps, Finset.mem_union, Finset.mem_biUnion] right refine ⟨⟨⟨n, v⟩, m, ∅⟩, hdep, ?_⟩ exact Finset.mem_singleton.mpr rfl
theorem concurrent_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 (preimageS g S) (soundnessπ Δ_C g S) := by refine ⟨?_, ?_, ?_, ?_, ?_⟩ · -- subset intro p hp rw [mem_preimageS] at hp exact embedPkg_mem_concurrentReal (hres.subset hp) · -- root_mem rw [mem_preimageS] exact hres.root_mem · -- parent_closure intro ⟨pn, pv⟩ hp m vs hdep rw [mem_preimageS] at hp by_cases hemp : vs = ∅ · -- EMPTY case: the reduced instance forbids selecting the depender subst hemp have hd := mem_concurrentDeps_empty (N' := N') (V' := V') (g := g) hdep obtain ⟨cv, hcvv, _⟩ := hres.dep_closure _ hp _ _ hd exact absurd hcvv (Finset.notMem_empty cv) by_cases hdir : isDirect g vs · -- DIRECT case obtain ⟨u₀, hu₀⟩ := Finset.nonempty_iff_ne_empty.mpr hemp have hd := mem_concurrentDeps_direct hdep hdir hu₀ obtain ⟨cv, hcvv, hcvS⟩ := hres.dep_closure _ hp _ _ hd rw [Finset.mem_map] at hcvv obtain ⟨u, huv, rfl⟩ := hcvv have hgu : g u = g u₀ := hdir u u₀ huv hu₀ have huS : (hcnm.granularN m (g u), hcvr.origV u) ∈ S := by rwa [hgu] refine ⟨u, ?_, ?_⟩ · refine ⟨huv, mem_preimageS.mpr huS, ?_⟩ rw [mem_soundnessπ] exact ⟨pn, pv, m, vs, u, hdep, hp, huv, huS, fun ⟨a, b, ha, hb, hne⟩ => absurd (hdir a b ha hb) hne, rfl⟩ · intro u' ⟨hu'v, hu'S_pre, hpi'⟩ rw [mem_preimageS] at hu'S_pre rw [mem_soundnessπ] at hpi' obtain ⟨_, _, _, _, _, _, _, _, _, _, heq⟩ := hpi' simp only [Prod.mk.injEq] at heq obtain ⟨⟨rfl, rfl⟩, rfl, rfl⟩ := heq have hgu' : g u' = g u₀ := hdir u' u₀ hu'v hu₀ exact hcvr.origV.injective (hres.version_unique _ _ _ (hgu' ▸ hu'S_pre) hcvS) · -- SPLIT case have hspl : isSplit g vs := by unfold isDirect at hdir; push_neg at hdir obtain ⟨u₁, u₂, hu₁, hu₂, hne⟩ := hdir exact ⟨u₁, u₂, hu₁, hu₂, hne⟩ have hd1 := mem_concurrentDeps_split1 hdep hspl obtain ⟨cv₀, hcv₀v, hcv₀S⟩ := hres.dep_closure _ hp _ _ hd1 rw [Finset.mem_map] at hcv₀v obtain ⟨w₀, hw₀mem, rfl⟩ := hcv₀v rw [Finset.mem_image] at hw₀mem obtain ⟨u₀, hu₀v, rfl⟩ := hw₀mem have hd2 := mem_concurrentDeps_split2 hdep hspl hu₀v obtain ⟨cv, hcvv, hcvS⟩ := hres.dep_closure _ hcv₀S _ _ hd2 rw [Finset.mem_map] at hcvv obtain ⟨u, humem, rfl⟩ := hcvv rw [Finset.mem_filter] at humem obtain ⟨huv, hgu⟩ := humem have huS : (hcnm.granularN m (g u), hcvr.origV u) ∈ S := by rwa [hgu] refine ⟨u, ?_, ?_⟩ · refine ⟨huv, mem_preimageS.mpr huS, ?_⟩ rw [mem_soundnessπ] exact ⟨pn, pv, m, vs, u, hdep, hp, huv, huS, fun _ => ⟨u₀, hu₀v, hcv₀S, hgu⟩, rfl⟩ · intro u' ⟨hu'v, hu'S_pre, hpi'⟩ rw [mem_preimageS] at hu'S_pre rw [mem_soundnessπ] at hpi' obtain ⟨_, _, _, vs', _, hdep', _, _, _, hspl_cond', heq⟩ := hpi' simp only [Prod.mk.injEq] at heq obtain ⟨⟨rfl, rfl⟩, rfl, rfl⟩ := heq have hvs' := hfunc _ _ _ _ hdep' hdep; subst hvs' obtain ⟨u₀', hu₀'v, hu₀'S, hgu'⟩ := hspl_cond' hspl have huu := hcvr.granV.injective (hres.version_unique _ _ _ hu₀'S hcv₀S) rw [huu] at hgu' have hu'S₀ : (hcnm.granularN m (g u₀), hcvr.origV u') ∈ S := hgu' ▸ hu'S_pre exact hcvr.origV.injective (hres.version_unique _ _ _ hu'S₀ hcvS) · -- version_granularity intro n v v' hv hv' hne hge rw [mem_preimageS] at hv hv' exact hne (hcvr.origV.injective (hres.version_unique _ _ _ (hge ▸ hv) hv')) · -- parent_subset intro c p hcp rw [mem_soundnessπ] at hcp obtain ⟨n, v, m, vs, u, _, hvS, _, huS, _, heq⟩ := hcp simp only [Prod.mk.injEq] at heq obtain ⟨rfl, rfl⟩ := heq exact ⟨mem_preimageS.mpr huS, mem_preimageS.mpr hvS⟩
end PackageCalculus.Concurrent