import PackageCalculus.Extensions.Conflict.Reduction.Definition import PackageCalculus.Extensions.Concurrent.Lifting.Retraction import PackageCalculus.Extensions.PeerDependency.Lifting.Retraction import PackageCalculus.Extensions.Feature.Lifting.Retraction import PackageCalculus.Extensions.Virtual.Lifting.Retraction import PackageCalculus.Extensions.Visibility.Reduction.Definition /-! # Lookup locality of the reductions For each encoded-source constructor, `Lookup` computes its out-edges from local inputs, and `Deps_lookup` proves it agrees with the monolithic encoding; the filters in the theorems state which inputs are local. The formula extensions are future work: their fibres need an occurrence relation over the NNF-atom closure for the guard edges on original packages. -/ set_option linter.unusedSectionVars false namespace PackageCalculus /-! ### Conflicts -/ section Conflict open Conflict variable {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 ConflictNoDeps open Conflict variable {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 Concurrent open Concurrent 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'] /-- 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 Peer open PeerDep Concurrent 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'] /-- 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) whose target 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 Feature open Feature variable {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 the additional-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 Virtual open Virtual variable {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 Visibility open Visibility variable {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 carried dependency. -/ 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