Something went wrong. Try again.
The Package Calculus
Something went wrong. Try again.
36 kB · 761 lines
at dev
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762import PackageCalculus.Extensions.Conflict.Reduction.Definitionimport PackageCalculus.Extensions.Concurrent.Lifting.Retractionimport PackageCalculus.Extensions.PeerDependency.Lifting.Retractionimport PackageCalculus.Extensions.Feature.Lifting.Retractionimport PackageCalculus.Extensions.Virtual.Lifting.Retractionimport PackageCalculus.Extensions.Visibility.Reduction.Definition
/-! # Lookup locality of the reductions
For each encoded-source constructor, `<ext>Lookup<Source>` computes itsout-edges from local inputs, and `<ext>Deps_lookup<Source>` proves it agreeswith the monolithic encoding; the filters in the theorems state which inputsare local. The formula extensions are future work: their fibres need anoccurrence relation over the NNF-atom closure for the guard edges onoriginal packages. -/
set_option linter.unusedSectionVars false
namespace PackageCalculus
/-! ### Conflicts -/
section Conflictopen Conflictvariable {N : Type*} [DecidableEq N] {V : Type*} [DecidableEq V]variable {N' : Type*} [DecidableEq N'] {V' : Type*} [DecidableEq V']variable [hcn : HasConflictNames N V N'] [hcv : HasConflictVersions V V']
/-- Own block, `one` per declared conflict, `zero` per conflict against it. -/def conflictLookupOrig (Δp : DepRel N V) (Γp Γrev : ConflictRel N V) : Finset (N' × Finset V') := (Δp.image fun e => (hcn.origN e.2.1, embedVS (V' := V') e.2.2)) ∪ (Γp.image fun e => (hcn.syntheticN e.2.1 e.2.2, {hcv.oneV})) ∪ (Γrev.image fun e => (hcn.syntheticN e.2.1 e.2.2, {hcv.zeroV}))
theorem conflictDeps_lookupOrig (Δ : DepRel N V) (Γ : ConflictRel N V) (p : Package N V) (tn : N') (tvs : Finset V') : (embedPkg p, tn, tvs) ∈ conflictDeps (N' := N') (V' := V') Δ Γ ↔ (tn, tvs) ∈ conflictLookupOrig (Δ.filter fun e => e.1 = p) (Γ.filter fun e => e.1 = p) (Γ.filter fun e => e.2.1 = p.1 ∧ p.2 ∈ e.2.2) := by simp only [conflictDeps, conflictLookupOrig, embedPkg, Finset.mem_union, Finset.mem_image, Finset.mem_biUnion, Finset.mem_filter] constructor · rintro ((⟨⟨q, m, vs⟩, he, heq⟩ | ⟨⟨q, m, vs⟩, he, heq⟩) | ⟨⟨q, m, vs⟩, he, u, hu, heq⟩) · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq refine Or.inl (Or.inl ⟨(q, m, vs), ⟨he, Prod.ext (hcn.origN.injective h1) (hcv.origV.injective h2)⟩, ?_⟩) rw [h3, h4] · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq refine Or.inl (Or.inr ⟨(q, m, vs), ⟨he, Prod.ext (hcn.origN.injective h1) (hcv.origV.injective h2)⟩, ?_⟩) rw [h3, h4] · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq have hm : m = p.1 := hcn.origN.injective h1 have hu' : u = p.2 := hcv.origV.injective h2 refine Or.inr ⟨(q, m, vs), ⟨he, hm, hu' ▸ hu⟩, ?_⟩ rw [h3, h4] · rintro ((⟨e, ⟨he, he1⟩, heq⟩ | ⟨e, ⟨he, he1⟩, heq⟩) | ⟨e, ⟨he, he1, he2⟩, heq⟩) · refine Or.inl (Or.inl ⟨e, he, ?_⟩) obtain ⟨q, m, vs⟩ := e simp only at he1 rw [he1, heq] · refine Or.inl (Or.inr ⟨e, he, ?_⟩) obtain ⟨q, m, vs⟩ := e simp only at he1 rw [he1, heq] · obtain ⟨q, m, vs⟩ := e simp only at he1 he2 refine Or.inr ⟨(q, m, vs), he, p.2, he2, ?_⟩ rw [heq, he1]end Conflict
section ConflictNoDepsopen Conflictvariable {N : Type*} [DecidableEq N] {V : Type*} [DecidableEq V]variable {N' : Type*} [DecidableEq N'] {V' : Type*} [DecidableEq V']variable [hcn : HasConflictNames N V N'] [hcv : HasConflictVersions V V']
theorem conflictDeps_synthetic_src {Δ : DepRel N V} {Γ : ConflictRel N V} {n : N} {vs : Finset V} {w : V'} {tn : N'} {tvs : Finset V'} (h : ((hcn.syntheticN n vs, w), tn, tvs) ∈ conflictDeps (N' := N') (V' := V') Δ Γ) : False := by simp only [conflictDeps, embedPkg, Finset.mem_union, Finset.mem_image, Finset.mem_biUnion] at h rcases h with ((⟨⟨q, m, vs'⟩, -, heq⟩ | ⟨⟨q, m, vs'⟩, -, heq⟩) | ⟨⟨q, m, vs'⟩, -, u, -, heq⟩) <;> simp only [Prod.mk.injEq] at heq <;> exact absurd heq.1.1 (hcn.origN_ne_syntheticN _ _ _)end ConflictNoDeps
/-! ### Concurrent Versions -/
section Concurrentopen Concurrentvariable {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']
/-- Direct granular targets, or the split/empty intermediate. -/def concurrentLookupGranular (Δp : DepRel N V) (g : V → G) (n : N) (v : V) : Finset (N' × Finset V') := Δp.biUnion fun e => (if isDirect g e.2.2 then e.2.2.image fun u => (hcnm.granularN e.2.1 (g u), e.2.2.map hcvr.origV) else ∅) ∪ (if isSplit g e.2.2 then {(hcnm.intermediateN n v e.2.1, (e.2.2.image g).map hcvr.granV)} else ∅) ∪ (if e.2.2 = ∅ then {(hcnm.intermediateN n v e.2.1, (∅ : Finset V'))} else ∅)
theorem concurrentDeps_lookupGranular (Δ : DepRel N V) (g : V → G) (n : N) (v : V) (tn : N') (tvs : Finset V') : ((hcnm.granularN n (g v), hcvr.origV v), tn, tvs) ∈ concurrentDeps (N' := N') (V' := V') Δ g ↔ (tn, tvs) ∈ concurrentLookupGranular (Δ.filter fun e => e.1 = (n, v)) g n v := by rw [mem_concurrentDeps_iff] simp only [concurrentLookupGranular, Finset.mem_biUnion, Finset.mem_filter, Finset.mem_union] constructor · rintro (⟨n₁, v₁, m, vs, hmem, hdir, u, hu, heq⟩ | ⟨n₁, v₁, m, vs, hmem, hs, heq⟩ | ⟨n₁, v₁, m, vs, hmem, hs, u, hu, heq⟩ | ⟨n₁, v₁, m, vs, hmem, hemp, heq⟩) · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq obtain ⟨hn, -⟩ := hcnm.granularN_injective h1 have hv := hcvr.origV.injective h2 refine ⟨((n₁, v₁), m, vs), ⟨hmem, Prod.ext hn.symm hv.symm⟩, Or.inl (Or.inl ?_)⟩ rw [if_pos hdir] exact Finset.mem_image.mpr ⟨u, hu, by rw [h3, h4]⟩ · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq obtain ⟨hn, -⟩ := hcnm.granularN_injective h1 have hv := hcvr.origV.injective h2 subst hn; subst hv refine ⟨((n, v), m, vs), ⟨hmem, rfl⟩, Or.inl (Or.inr ?_)⟩ rw [if_pos hs, Finset.mem_singleton, h3, h4] · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hcnm.granularN_ne_intermediateN _ _ _ _ _) · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq obtain ⟨hn, -⟩ := hcnm.granularN_injective h1 have hv := hcvr.origV.injective h2 subst hn; subst hv refine ⟨((n, v), m, vs), ⟨hmem, rfl⟩, Or.inr ?_⟩ rw [if_pos hemp, Finset.mem_singleton, h3, h4] · rintro ⟨⟨⟨n₁, v₁⟩, m, vs⟩, ⟨hmem, he1⟩, hbr⟩ simp only [Prod.mk.injEq] at he1 obtain ⟨hn, hv⟩ := he1 subst hn; subst hv rcases hbr with (h | h) | h · split at h · obtain ⟨u, hu, heq⟩ := Finset.mem_image.mp h exact Or.inl ⟨n₁, v₁, m, vs, hmem, ‹_›, u, hu, by rw [← heq]⟩ · exact absurd h (Finset.notMem_empty _) · split at h · rw [Finset.mem_singleton] at h exact Or.inr (Or.inl ⟨n₁, v₁, m, vs, hmem, ‹_›, by rw [← h]⟩) · exact absurd h (Finset.notMem_empty _) · split at h · rw [Finset.mem_singleton] at h exact Or.inr (Or.inr (Or.inr ⟨n₁, v₁, m, vs, hmem, ‹_›, by rw [← h]⟩)) · exact absurd h (Finset.notMem_empty _)
/-- The granularity-w group of each split dependency on m. -/def concurrentLookupIntermediate (Δp : DepRel N V) (g : V → G) (m : N) (w : G) : Finset (N' × Finset V') := Δp.biUnion fun e => if e.2.1 = m ∧ isSplit g e.2.2 ∧ ∃ u ∈ e.2.2, g u = w then {(hcnm.granularN m w, (e.2.2.filter fun u => g u = w).map hcvr.origV)} else ∅
theorem concurrentDeps_lookupIntermediate (Δ : DepRel N V) (g : V → G) (n : N) (v : V) (m : N) (w : G) (tn : N') (tvs : Finset V') : ((hcnm.intermediateN n v m, hcvr.granV w), tn, tvs) ∈ concurrentDeps (N' := N') (V' := V') Δ g ↔ (tn, tvs) ∈ concurrentLookupIntermediate (Δ.filter fun e => e.1 = (n, v)) g m w := by rw [mem_concurrentDeps_iff] simp only [concurrentLookupIntermediate, Finset.mem_biUnion, Finset.mem_filter] constructor · rintro (⟨n₁, v₁, m₁, vs, hmem, hdir, u, hu, heq⟩ | ⟨n₁, v₁, m₁, vs, hmem, hs, heq⟩ | ⟨n₁, v₁, m₁, vs, hmem, hs, u, hu, heq⟩ | ⟨n₁, v₁, m₁, vs, hmem, hemp, heq⟩) · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hcnm.intermediateN_ne_granularN _ _ _ _ _) · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hcnm.intermediateN_ne_granularN _ _ _ _ _) · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq obtain ⟨hn, hv, hm⟩ := hcnm.intermediateN_injective _ _ _ _ _ _ h1 have hw := hcvr.granV.injective h2 subst hn; subst hv; subst hm; subst hw refine ⟨((n, v), m, vs), ⟨hmem, rfl⟩, ?_⟩ rw [if_pos ⟨rfl, hs, u, hu, rfl⟩, Finset.mem_singleton, h3, h4] · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hcnm.intermediateN_ne_granularN _ _ _ _ _) · rintro ⟨⟨⟨n₁, v₁⟩, m₁, vs⟩, ⟨hmem, he1⟩, hbr⟩ simp only [Prod.mk.injEq] at he1 obtain ⟨hn, hv⟩ := he1 subst hn; subst hv split at hbr · rename_i hcond obtain ⟨hm, hs, u, hu, hw⟩ := hcond subst hm; subst hw rw [Finset.mem_singleton] at hbr exact Or.inr (Or.inr (Or.inl ⟨n₁, v₁, m₁, vs, hmem, hs, u, hu, by rw [← hbr]⟩)) · exact absurd hbr (Finset.notMem_empty _)
end Concurrent
/-! ### Peer Dependencies -/
section Peeropen PeerDep Concurrentvariable {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']
/-- One intermediate per dependency. -/def peerLookupGranular (Δp : DepRel N V) (_g : V → G) (n : N) (v : V) : Finset (N' × Finset V') := Δp.image fun e => (hcnm.intermediateN n v e.2.1, e.2.2.map hcvr.origV)
theorem peerDeps_lookupGranular (Δ : DepRel N V) (Θ : PeerRel N V) (g : V → G) (n : N) (v : V) (tn : N') (tvs : Finset V') : ((hcnm.granularN n (g v), hcvr.origV v), tn, tvs) ∈ peerDeps (N' := N') (V' := V') Δ Θ g ↔ (tn, tvs) ∈ peerLookupGranular (Δ.filter fun e => e.1 = (n, v)) g n v := by rw [mem_peerDeps_iff] simp only [peerLookupGranular, Finset.mem_image, Finset.mem_filter] constructor · rintro (⟨n₁, v₁, m, vs, hmem, heq⟩ | ⟨n₁, v₁, m, vs, hmem, u, hu, heq⟩ | ⟨n₁, v₁, o, us, hmem, u, hu, m, ws, hΘ, hg, heq⟩) · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq obtain ⟨hn, -⟩ := hcnm.granularN_injective h1 have hv := hcvr.origV.injective h2 subst hn; subst hv exact ⟨((n, v), m, vs), ⟨hmem, rfl⟩, by rw [h3, h4]⟩ · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hcnm.granularN_ne_intermediateN _ _ _ _ _) · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hcnm.granularN_ne_intermediateN _ _ _ _ _) · rintro ⟨⟨⟨n₁, v₁⟩, m, vs⟩, ⟨hmem, he1⟩, heq⟩ simp only [Prod.mk.injEq] at he1 obtain ⟨hn, hv⟩ := he1 subst hn; subst hv exact Or.inl ⟨n₁, v₁, m, vs, hmem, by rw [← heq]⟩
/-- The dependee, and one intermediate per peer declaration of (o, u) whosetarget the depender also depends on. -/def peerLookupIntermediate (Δp : DepRel N V) (Θu : PeerRel N V) (g : V → G) (n : N) (v : V) (o : N) (u : V) : Finset (N' × Finset V') := (Δp.biUnion fun e => if e.2.1 = o ∧ u ∈ e.2.2 then {(hcnm.granularN o (g u), ({hcvr.origV u} : Finset V'))} else ∅) ∪ (Θu.biUnion fun t => if (∃ e ∈ Δp, e.2.1 = o ∧ u ∈ e.2.2) ∧ ∃ e ∈ Δp, e.2.1 = t.2.1 then {(hcnm.intermediateN n v t.2.1, t.2.2.map hcvr.origV)} else ∅)
theorem peerDeps_lookupIntermediate (Δ : DepRel N V) (Θ : PeerRel N V) (g : V → G) (n : N) (v : V) (o : N) (u : V) (tn : N') (tvs : Finset V') : ((hcnm.intermediateN n v o, hcvr.origV u), tn, tvs) ∈ peerDeps (N' := N') (V' := V') Δ Θ g ↔ (tn, tvs) ∈ peerLookupIntermediate (Δ.filter fun e => e.1 = (n, v)) (Θ.filter fun t => t.1 = (o, u)) g n v o u := by rw [mem_peerDeps_iff] simp only [peerLookupIntermediate, Finset.mem_union, Finset.mem_biUnion] constructor · rintro (⟨n₁, v₁, m, vs, hmem, heq⟩ | ⟨n₁, v₁, m, vs, hmem, u₁, hu₁, heq⟩ | ⟨n₁, v₁, o₁, us, hmem, u₁, hu₁, m, ws, hΘ, ⟨ws', hws'⟩, heq⟩) · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hcnm.intermediateN_ne_granularN _ _ _ _ _) · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq obtain ⟨hn, hv, hm⟩ := hcnm.intermediateN_injective _ _ _ _ _ _ h1 have hu := hcvr.origV.injective h2 subst hn; subst hv; subst hm; subst hu refine Or.inl ⟨((n, v), o, vs), Finset.mem_filter.mpr ⟨hmem, rfl⟩, ?_⟩ rw [if_pos ⟨rfl, hu₁⟩, Finset.mem_singleton, h3, h4] · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq obtain ⟨hn, hv, ho⟩ := hcnm.intermediateN_injective _ _ _ _ _ _ h1 have hu := hcvr.origV.injective h2 subst hn; subst hv; subst ho; subst hu refine Or.inr ⟨((o, u), m, ws), Finset.mem_filter.mpr ⟨hΘ, rfl⟩, ?_⟩ rw [if_pos ⟨⟨((n, v), o, us), Finset.mem_filter.mpr ⟨hmem, rfl⟩, rfl, hu₁⟩, ((n, v), m, ws'), Finset.mem_filter.mpr ⟨hws', rfl⟩, rfl⟩, Finset.mem_singleton, h3, h4] · rintro (⟨⟨⟨n₁, v₁⟩, m, vs⟩, hef, hbr⟩ | ⟨⟨⟨o₁, u₁⟩, m, ws⟩, htf, hbr⟩) · rw [Finset.mem_filter] at hef obtain ⟨hmem, he1⟩ := hef simp only [Prod.mk.injEq] at he1 obtain ⟨hn, hv⟩ := he1 subst hn; subst hv split at hbr · rename_i hcond obtain ⟨hm, hu⟩ := hcond subst hm rw [Finset.mem_singleton] at hbr exact Or.inr (Or.inl ⟨n₁, v₁, m, vs, hmem, u, hu, by rw [← hbr]⟩) · exact absurd hbr (Finset.notMem_empty _) · rw [Finset.mem_filter] at htf obtain ⟨hΘ, ht1⟩ := htf simp only [Prod.mk.injEq] at ht1 obtain ⟨ho, hu⟩ := ht1 subst ho; subst hu split at hbr · rename_i hcond obtain ⟨⟨e₁, he₁f, ho₁, hu₁⟩, e₂, he₂f, hm₂⟩ := hcond rw [Finset.mem_singleton] at hbr obtain ⟨⟨a, b⟩, c, ds⟩ := e₁ rw [Finset.mem_filter] at he₁f obtain ⟨he₁, he₁1⟩ := he₁f simp only at he₁1 ho₁ hu₁ rw [he₁1, ho₁] at he₁ obtain ⟨⟨a₂, b₂⟩, c₂, ds₂⟩ := e₂ rw [Finset.mem_filter] at he₂f obtain ⟨he₂, he₂1⟩ := he₂f simp only at he₂1 hm₂ rw [he₂1, hm₂] at he₂ exact Or.inr (Or.inr ⟨n, v, o₁, ds, he₁, u₁, hu₁, m, ws, hΘ, ⟨ds₂, he₂⟩, by rw [← hbr]⟩) · exact absurd hbr (Finset.notMem_empty _)
end Peer
/-! ### Features -/
section Featureopen Featurevariable {N : Type*} [DecidableEq N] {V : Type*} [DecidableEq V]variable {F : Type*} [DecidableEq F] [Fintype F]variable {N' : Type*} [DecidableEq N'] [hfn : HasFeatureNames N F N']
/-- The featured-dependency block, one edge per required feature. -/def featureLookupOrig (Δfp : FeatDepRel N V F) : Finset (N' × Finset V) := Δfp.biUnion fun e => if e.2.2.2 = ∅ then {(hfn.origN e.2.1, e.2.2.1)} else e.2.2.2.image fun f => (hfn.featuredN e.2.1 f, e.2.2.1)
theorem featureDeps_lookupOrig (R : Real N V) (support : Support N V F) (Δ_f : FeatDepRel N V F) (Δ_a : AddlDepRel N V F) (p : Package N V) (tn : N') (tvs : Finset V) : ((hfn.origN p.1, p.2), tn, tvs) ∈ featureDeps (N' := N') R support Δ_f Δ_a ↔ (tn, tvs) ∈ featureLookupOrig (Δ_f.filter fun e => e.1 = p) := by rw [mem_featureDeps_iff] simp only [featureLookupOrig, embedPkg, Finset.mem_biUnion, Finset.mem_filter] constructor · rintro (⟨n₁, v₁, f, hsupp, hR, heq⟩ | ⟨q, m, vs, hmem, heq⟩ | ⟨q, m, vs, fs, hmem, hfs, f, hf, heq⟩ | ⟨n₁, v₁, f, m, vs, hmem, heq⟩ | ⟨n₁, v₁, f, m, vs, fs, hmem, hfs, f', hf', heq⟩) · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hfn.origN_ne_featuredN _ _ _) · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq have hq : q = p := Prod.ext (hfn.origN.injective h1).symm h2.symm refine ⟨(q, m, vs, ∅), ⟨hmem, hq⟩, ?_⟩ rw [if_pos rfl, Finset.mem_singleton, h3, h4] · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq have hq : q = p := Prod.ext (hfn.origN.injective h1).symm h2.symm refine ⟨(q, m, vs, fs), ⟨hmem, hq⟩, ?_⟩ rw [if_neg (Finset.nonempty_iff_ne_empty.mp hfs)] exact Finset.mem_image.mpr ⟨f, hf, by rw [h3, h4]⟩ · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hfn.origN_ne_featuredN _ _ _) · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hfn.origN_ne_featuredN _ _ _) · rintro ⟨⟨q, m, vs, fs⟩, ⟨hmem, he1⟩, hbr⟩ simp only at he1 subst he1 split at hbr · rename_i hfs subst hfs rw [Finset.mem_singleton] at hbr exact Or.inr (Or.inl ⟨q, m, vs, hmem, by rw [← hbr]⟩) · rename_i hfs obtain ⟨f, hf, heq⟩ := Finset.mem_image.mp hbr exact Or.inr (Or.inr (Or.inl ⟨q, m, vs, fs, hmem, Finset.nonempty_iff_ne_empty.mpr hfs, f, hf, by rw [← heq]⟩))
/-- The base requirement (when supported and real) and theadditional-dependency block. -/def featureLookupFeatured (suppv : Support N V F) (Rv : Real N V) (Δap : AddlDepRel N V F) (n : N) (v : V) (f : F) : Finset (N' × Finset V) := (if ((n, v), f) ∈ suppv ∧ (n, v) ∈ Rv then {(hfn.origN n, ({v} : Finset V))} else ∅) ∪ (Δap.biUnion fun e => if e.2.2.2 = ∅ then {(hfn.origN e.2.1, e.2.2.1)} else e.2.2.2.image fun f' => (hfn.featuredN e.2.1 f', e.2.2.1))
theorem featureDeps_lookupFeatured (R : Real N V) (support : Support N V F) (Δ_f : FeatDepRel N V F) (Δ_a : AddlDepRel N V F) (n : N) (v : V) (f : F) (tn : N') (tvs : Finset V) : ((hfn.featuredN n f, v), tn, tvs) ∈ featureDeps (N' := N') R support Δ_f Δ_a ↔ (tn, tvs) ∈ featureLookupFeatured (support.filter fun s => s.1 = (n, v)) (R.filter fun q => q = (n, v)) (Δ_a.filter fun e => e.1 = ((n, v), f)) n v f := by rw [mem_featureDeps_iff] simp only [featureLookupFeatured, embedPkg, Finset.mem_union, Finset.mem_biUnion] constructor · rintro (⟨n₁, v₁, f₁, hsupp, hR, heq⟩ | ⟨q, m, vs, hmem, heq⟩ | ⟨q, m, vs, fs, hmem, hfs, f₁, hf₁, heq⟩ | ⟨n₁, v₁, f₁, m, vs, hmem, heq⟩ | ⟨n₁, v₁, f₁, m, vs, fs, hmem, hfs, f', hf', heq⟩) · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq obtain ⟨hn, hf⟩ := hfn.featuredN_injective h1 subst hn; subst hf; subst h2 refine Or.inl ?_ rw [if_pos ⟨Finset.mem_filter.mpr ⟨hsupp, rfl⟩, Finset.mem_filter.mpr ⟨hR, rfl⟩⟩, Finset.mem_singleton, h3, h4] · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hfn.featuredN_ne_origN _ _ _) · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hfn.featuredN_ne_origN _ _ _) · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq obtain ⟨hn, hf⟩ := hfn.featuredN_injective h1 subst hn; subst hf; subst h2 refine Or.inr ⟨(((n, v), f), m, vs, ∅), Finset.mem_filter.mpr ⟨hmem, rfl⟩, ?_⟩ rw [if_pos rfl, Finset.mem_singleton, h3, h4] · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq obtain ⟨hn, hf⟩ := hfn.featuredN_injective h1 subst hn; subst hf; subst h2 refine Or.inr ⟨(((n, v), f), m, vs, fs), Finset.mem_filter.mpr ⟨hmem, rfl⟩, ?_⟩ rw [if_neg (Finset.nonempty_iff_ne_empty.mp hfs)] exact Finset.mem_image.mpr ⟨f', hf', by rw [h3, h4]⟩ · rintro (hbr | ⟨⟨⟨⟨a, b⟩, f₀⟩, m, vs, fs⟩, hef, hbr⟩) · split at hbr · rename_i hcond obtain ⟨hs, hr⟩ := hcond rw [Finset.mem_filter] at hs hr rw [Finset.mem_singleton] at hbr exact Or.inl ⟨n, v, f, hs.1, hr.1, by rw [← hbr]⟩ · exact absurd hbr (Finset.notMem_empty _) · rw [Finset.mem_filter] at hef obtain ⟨hmem, he1⟩ := hef simp only [Prod.mk.injEq] at he1 obtain ⟨⟨ha, hb⟩, hf₀⟩ := he1 subst ha; subst hb; subst hf₀ split at hbr · rename_i hfs subst hfs rw [Finset.mem_singleton] at hbr exact Or.inr (Or.inr (Or.inr (Or.inl ⟨a, b, f₀, m, vs, hmem, by rw [← hbr]⟩))) · rename_i hfs obtain ⟨f', hf', heq⟩ := Finset.mem_image.mp hbr exact Or.inr (Or.inr (Or.inr (Or.inr ⟨a, b, f₀, m, vs, fs, hmem, Finset.nonempty_iff_ne_empty.mpr hfs, f', hf', by rw [← heq]⟩)))
end Feature
/-! ### Virtual Packages -/
section Virtualopen Virtualvariable {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']
theorem hasProvider_filter_name (prov : ProvidesRel N V) (n : N) (vs : Finset V) : hasProvider (prov.filter fun x => x.2.1 = n) n vs ↔ hasProvider prov n vs := by constructor · rintro ⟨q, v, hqv, hm⟩ exact ⟨q, v, (Finset.mem_filter.mp hqv).1, hm⟩ · rintro ⟨q, v, hqv, hm⟩ exact ⟨q, v, Finset.mem_filter.mpr ⟨hqv, rfl⟩, hm⟩
theorem selectorVersions_filter_name (R : Real N V) (prov : ProvidesRel N V) (n : N) (vs : Finset V) : selectorVersions (V' := V') (R.filter fun q => q.1 = n) (prov.filter fun x => x.2.1 = n) n vs = selectorVersions R prov n vs := by unfold selectorVersions congr 1 · ext w simp only [Finset.mem_biUnion, Finset.mem_filter] constructor · rintro ⟨⟨⟨m, u⟩, n', v⟩, ⟨hqv, -⟩, hw⟩ exact ⟨((m, u), n', v), hqv, hw⟩ · rintro ⟨⟨⟨m, u⟩, n', v⟩, hqv, hw⟩ by_cases hn : n' = n · exact ⟨((m, u), n', v), ⟨hqv, hn⟩, hw⟩ · rw [if_neg (fun hc => hn hc.1)] at hw exact absurd hw (Finset.notMem_empty _) · congr 1 exact Finset.filter_congr fun u _ => by simp [Finset.mem_filter]
/-- Per dependency, the dependee directly (no provider) or its selector. -/def virtualLookupOrig (Δp : DepRel N V) (R : Real N V) (prov : ProvidesRel N V) (p : Package N V) : Finset (N' × Finset V') := Δp.image fun e => if hasProvider prov e.2.1 e.2.2 then (hvn.selectorN p e.2.1, selectorVersions R prov e.2.1 e.2.2) else (hvn.origN e.2.1, e.2.2.map hvv.origV)
theorem virtualDeps_lookupOrig (Δ : DepRel N V) (R : Real N V) (prov : ProvidesRel N V) (p : Package N V) (tn : N') (tvs : Finset V') : (embedPkg p, tn, tvs) ∈ virtualDeps (N' := N') (V' := V') Δ R prov ↔ (tn, tvs) ∈ virtualLookupOrig (Δ.filter fun e => e.1 = p) R prov p := by rw [mem_virtualDeps_iff] simp only [virtualLookupOrig, embedPkg, Finset.mem_image, Finset.mem_filter] constructor · rintro (⟨q, m, vs, hmem, hnp, heq⟩ | ⟨q, m, vs, hmem, hp, heq⟩ | ⟨q, m, vs, hmem, m₁, w, v₁, hpv, hmt, heq⟩ | ⟨q, m, vs, hmem, hp, u, hu, hR, heq⟩) · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq have hq : q = p := Prod.ext (hvn.origN.injective h1).symm (hvv.origV.injective h2).symm refine ⟨(q, m, vs), ⟨hmem, hq⟩, ?_⟩ rw [if_neg hnp, h3, h4] · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq have hq : q = p := Prod.ext (hvn.origN.injective h1).symm (hvv.origV.injective h2).symm subst hq refine ⟨(q, m, vs), ⟨hmem, rfl⟩, ?_⟩ rw [if_pos hp, h3, h4] · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hvn.origN_ne_selectorN _ _ _) · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hvn.origN_ne_selectorN _ _ _) · rintro ⟨⟨q, m, vs⟩, ⟨hmem, he1⟩, hbr⟩ simp only at he1 subst he1 simp only at hbr split at hbr · rename_i hp exact Or.inr (Or.inl ⟨q, m, vs, hmem, hp, by rw [← hbr]⟩) · rename_i hnp exact Or.inl ⟨q, m, vs, hmem, hnp, by rw [← hbr]⟩
/-- The concrete package the version stands for. -/def virtualLookupSelector (Δp : DepRel N V) (provn : ProvidesRel N V) (Rn : Real N V) (n m : N) (w : V) : Finset (N' × Finset V') := Δp.biUnion fun e => if e.2.1 = n then (provn.biUnion fun x => if x.1 = (m, w) ∧ x.2.1 = n ∧ memTop x.2.2 e.2.2 then {(hvn.origN m, ({hvv.origV w} : Finset V'))} else ∅) ∪ (if m = n ∧ hasProvider provn n e.2.2 ∧ w ∈ e.2.2 ∧ (n, w) ∈ Rn then {(hvn.origN n, ({hvv.origV w} : Finset V'))} else ∅) else ∅
theorem virtualDeps_lookupSelector (Δ : DepRel N V) (R : Real N V) (prov : ProvidesRel N V) (p : Package N V) (n m : N) (w : V) (tn : N') (tvs : Finset V') : ((hvn.selectorN p n, hvv.providerV m w), tn, tvs) ∈ virtualDeps (N' := N') (V' := V') Δ R prov ↔ (tn, tvs) ∈ virtualLookupSelector (Δ.filter fun e => e.1 = p) (prov.filter fun x => x.2.1 = n) (R.filter fun q => q.1 = n) n m w := by rw [mem_virtualDeps_iff] simp only [virtualLookupSelector, embedPkg, Finset.mem_biUnion] constructor · rintro (⟨q, m₁, vs, hmem, hnp, heq⟩ | ⟨q, m₁, vs, hmem, hp, heq⟩ | ⟨q, n₁, vs, hmem, m₁, w₁, v₁, hpv, hmt, heq⟩ | ⟨q, n₁, vs, hmem, hp, u, hu, hR, heq⟩) · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hvn.selectorN_ne_origN _ _ _) · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hvn.selectorN_ne_origN _ _ _) · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq obtain ⟨hq, hn⟩ := hvn.selectorN_injective h1 obtain ⟨hm, hw⟩ := hvv.providerV_injective h2 subst hq; subst hn; subst hm; subst hw refine ⟨(p, n, vs), Finset.mem_filter.mpr ⟨hmem, rfl⟩, ?_⟩ rw [if_pos rfl] refine Finset.mem_union_left _ ?_ refine Finset.mem_biUnion.mpr ⟨((m, w), n, v₁), Finset.mem_filter.mpr ⟨hpv, rfl⟩, ?_⟩ rw [if_pos ⟨rfl, rfl, hmt⟩, Finset.mem_singleton, h3, h4] · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq obtain ⟨hq, hn⟩ := hvn.selectorN_injective h1 obtain ⟨hm, hw⟩ := hvv.providerV_injective h2 subst hq; subst hn; subst hm; subst hw refine ⟨(p, m, vs), Finset.mem_filter.mpr ⟨hmem, rfl⟩, ?_⟩ rw [if_pos rfl] refine Finset.mem_union_right _ ?_ rw [if_pos ⟨rfl, (hasProvider_filter_name prov m vs).mpr hp, hu, Finset.mem_filter.mpr ⟨hR, rfl⟩⟩, Finset.mem_singleton, h3, h4] · rintro ⟨⟨q, n₁, vs⟩, hef, hbr⟩ rw [Finset.mem_filter] at hef obtain ⟨hmem, he1⟩ := hef simp only at he1 subst he1 simp only at hbr split at hbr · rename_i hn₁ rw [hn₁] at hmem rcases Finset.mem_union.mp hbr with hpr | hdir · obtain ⟨⟨⟨m₁, u₁⟩, n₂, v₂⟩, hx, hin⟩ := Finset.mem_biUnion.mp hpr rw [Finset.mem_filter] at hx obtain ⟨hpv, hn₂⟩ := hx simp only at hn₂ split at hin · rename_i hc obtain ⟨hmw, -, hmt⟩ := hc simp only at hmw hmt rw [hmw, hn₂] at hpv rw [Finset.mem_singleton] at hin exact Or.inr (Or.inr (Or.inl ⟨q, n, vs, hmem, m, w, v₂, hpv, hmt, by rw [hin]⟩)) · exact absurd hin (Finset.notMem_empty _) · split at hdir · rename_i hc obtain ⟨hmn, hp, hw, hR⟩ := hc rw [Finset.mem_filter] at hR rw [Finset.mem_singleton] at hdir subst hmn exact Or.inr (Or.inr (Or.inr ⟨q, m, vs, hmem, (hasProvider_filter_name prov m vs).mp hp, w, hw, hR.1, by rw [hdir]⟩)) · exact absurd hdir (Finset.notMem_empty _) · exact absurd hbr (Finset.notMem_empty _)
end Virtual
/-! ### Public and Private Dependencies -/
section Visibilityopen Visibilityvariable {N : Type*} [DecidableEq N] {V : Type*} [DecidableEq V]variable {N' : Type*} [DecidableEq N'] [hvn : HasVisibilityNames N V N']
theorem Priv_block {Δ : DepRel N V} {pub : PubRel N V} {p : Package N V} : Priv (Δ.filter fun e => e.1 = p) pub p ↔ Priv Δ pub p := by constructor · rintro ⟨n, vs, he, hn⟩ exact ⟨n, vs, (Finset.mem_filter.mp he).1, hn⟩ · rintro ⟨n, vs, he, hn⟩ exact ⟨n, vs, Finset.mem_filter.mpr ⟨he, rfl⟩, hn⟩
/-- The self-driving edge away from home, one intermediate per carrieddependency. -/def visLookupOccurrence (Δp : DepRel N V) (pub : PubRel N V) (n : N) (v : V) (q : Package N V) : Finset (N' × Finset V) := (if Priv Δp pub (n, v) ∧ q ≠ (n, v) then {(hvn.occurrenceN n (n, v), ({v} : Finset V))} else ∅) ∪ (Δp.biUnion fun e => if carried pub (n, v) e.2.1 q then {(hvn.intermediateN n v e.2.1 q, e.2.2)} else ∅)
theorem visDeps_lookupOccurrence (R_C : Real N V) (Δ : DepRel N V) (pub : PubRel N V) (r : Package N V) {n : N} {v : V} {q : Package N V} (hR : (n, v) ∈ R_C) (hq : q ∈ potentialOrigins R_C Δ pub r) (tn : N') (tvs : Finset V) : ((hvn.occurrenceN n q, v), tn, tvs) ∈ visDeps R_C Δ pub r ↔ (tn, tvs) ∈ visLookupOccurrence (Δ.filter fun e => e.1 = (n, v)) pub n v q := by rw [mem_visDeps_iff] simp only [visLookupOccurrence, Finset.mem_union, Finset.mem_biUnion, Finset.mem_filter] constructor · rintro (⟨⟨pn, pv⟩, q', hp, hq', hpriv, hne, heq⟩ | ⟨n₁, v₁, m, vs, q', hdep, hq', hc, heq⟩ | ⟨n₁, v₁, m, vs, q', u, hdep, hq', hc, hu, heq⟩ | ⟨n₁, v₁, m, vs, q', u, hdep, hq', hc, hu, heq⟩) · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq obtain ⟨rfl, rfl⟩ := hvn.occurrenceN_injective _ _ _ _ h1 subst h2 refine Or.inl ?_ rw [if_pos ⟨Priv_block.mpr hpriv, hne⟩, Finset.mem_singleton, h3, h4] · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq obtain ⟨rfl, rfl⟩ := hvn.occurrenceN_injective _ _ _ _ h1 subst h2 refine Or.inr ⟨((n, v), m, vs), ⟨hdep, rfl⟩, ?_⟩ rw [if_pos hc, Finset.mem_singleton, h3, h4] · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hvn.occurrenceN_ne_intermediateN _ _ _ _ _ _) · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hvn.occurrenceN_ne_intermediateN _ _ _ _ _ _) · rintro (hself | ⟨⟨⟨a, b⟩, m, vs⟩, ⟨hdep, he1⟩, hin⟩) · split at hself · rename_i hcond rw [Finset.mem_singleton] at hself exact Or.inl ⟨(n, v), q, hR, hq, Priv_block.mp hcond.1, hcond.2, by rw [hself]⟩ · exact absurd hself (Finset.notMem_empty _) · simp only at he1 rw [he1] at hdep split at hin · rename_i hc rw [Finset.mem_singleton] at hin exact Or.inr (Or.inl ⟨n, v, m, vs, q, hdep, hq, hc, by rw [hin]⟩) · exact absurd hin (Finset.notMem_empty _)
/-- The dependee's occurrence at the same origin, and the agreement. -/def visLookupIntermediate (Δp : DepRel N V) (pub : PubRel N V) (n : N) (v : V) (m : N) (q : Package N V) (u : V) : Finset (N' × Finset V) := Δp.biUnion fun e => if e.2.1 = m ∧ u ∈ e.2.2 ∧ carried pub (n, v) m q then {(hvn.occurrenceN m q, ({u} : Finset V)), (hvn.agreementN n v m, ({u} : Finset V))} else ∅
theorem visDeps_lookupIntermediate (R_C : Real N V) (Δ : DepRel N V) (pub : PubRel N V) (r : Package N V) {n : N} {v : V} {m : N} {q : Package N V} {u : V} (hq : q ∈ potentialOrigins R_C Δ pub r) (tn : N') (tvs : Finset V) : ((hvn.intermediateN n v m q, u), tn, tvs) ∈ visDeps R_C Δ pub r ↔ (tn, tvs) ∈ visLookupIntermediate (Δ.filter fun e => e.1 = (n, v)) pub n v m q u := by rw [mem_visDeps_iff] simp only [visLookupIntermediate, Finset.mem_biUnion, Finset.mem_filter] constructor · rintro (⟨⟨pn, pv⟩, q', hp, hq', hpriv, hne, heq⟩ | ⟨n₁, v₁, m₁, vs, q', hdep, hq', hc, heq⟩ | ⟨n₁, v₁, m₁, vs, q', u₁, hdep, hq', hc, hu, heq⟩ | ⟨n₁, v₁, m₁, vs, q', u₁, hdep, hq', hc, hu, heq⟩) · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hvn.intermediateN_ne_occurrenceN _ _ _ _ _ _) · simp only [Prod.mk.injEq] at heq exact absurd heq.1.1 (hvn.intermediateN_ne_occurrenceN _ _ _ _ _ _) · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq obtain ⟨rfl, rfl, rfl, rfl⟩ := hvn.intermediateN_injective _ _ _ _ _ _ _ _ h1 subst h2 refine ⟨((n, v), m, vs), ⟨hdep, rfl⟩, ?_⟩ rw [if_pos ⟨rfl, hu, hc⟩] exact Finset.mem_insert.mpr (Or.inl (by rw [h3, h4])) · simp only [Prod.mk.injEq] at heq obtain ⟨⟨h1, h2⟩, h3, h4⟩ := heq obtain ⟨rfl, rfl, rfl, rfl⟩ := hvn.intermediateN_injective _ _ _ _ _ _ _ _ h1 subst h2 refine ⟨((n, v), m, vs), ⟨hdep, rfl⟩, ?_⟩ rw [if_pos ⟨rfl, hu, hc⟩] exact Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton.mpr (by rw [h3, h4]))) · rintro ⟨⟨⟨a, b⟩, m₁, vs⟩, ⟨hdep, he1⟩, hin⟩ simp only at he1 rw [he1] at hdep split at hin · rename_i hc obtain ⟨hm₁, hu, hcarr⟩ := hc simp only at hm₁ hu rw [hm₁] at hdep rcases Finset.mem_insert.mp hin with heq | heq · exact Or.inr (Or.inr (Or.inl ⟨n, v, m, vs, q, u, hdep, hq, hcarr, hu, by rw [heq]⟩)) · rw [Finset.mem_singleton] at heq exact Or.inr (Or.inr (Or.inr ⟨n, v, m, vs, q, u, hdep, hq, hcarr, hu, by rw [heq]⟩)) · exact absurd hin (Finset.notMem_empty _)
theorem visDeps_agreement_src {R_C : Real N V} {Δ : DepRel N V} {pub : PubRel N V} {r : Package N V} {n : N} {v : V} {m : N} {u : V} {tn : N'} {tvs : Finset V} (h : ((hvn.agreementN n v m, u), tn, tvs) ∈ visDeps R_C Δ pub r) : False := by rcases mem_visDeps_iff.mp h with ⟨p, q, -, -, -, -, heq⟩ | ⟨n₁, v₁, m₁, vs, q, -, -, -, heq⟩ | ⟨n₁, v₁, m₁, vs, q, u₁, -, -, -, -, heq⟩ | ⟨n₁, v₁, m₁, vs, q, u₁, -, -, -, -, heq⟩ <;> simp only [Prod.mk.injEq] at heq · exact absurd heq.1.1 (hvn.agreementN_ne_occurrenceN _ _ _ _ _) · exact absurd heq.1.1 (hvn.agreementN_ne_occurrenceN _ _ _ _ _) · exact absurd heq.1.1 (hvn.agreementN_ne_intermediateN _ _ _ _ _ _ _) · exact absurd heq.1.1 (hvn.agreementN_ne_intermediateN _ _ _ _ _ _ _)
end Visibility
end PackageCalculus