Something went wrong. Try again.
The Package Calculus
Something went wrong. Try again.
25 kB · 463 lines
at icfp
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464import PackageCalculus.Composition.FeatureConcurrent.Typesimport PackageCalculus.Composition.FeatureConcurrent.Definitionimport PackageCalculus.Extensions.Feature.Reduction.Definitionimport PackageCalculus.Extensions.Concurrent.Reduction.Definitionimport Mathlib
/-! # Feature-concurrent composition: reduction
`concurrentFeatureReal` and `concurrentFeatureDeps` encode the combined featureand concurrent problem into a core resolution problem. The encoding emits ashared intermediate plus per-feature secondaries linked by back-edges thatenforce version alignment. -/
namespace PackageCalculus.Composition
open Classical
variable {N : Type*} [DecidableEq N] {V : Type*} [DecidableEq V] {F : Type*} [DecidableEq F] {G : Type*} [DecidableEq G]variable {N_FC : Type*} [DecidableEq N_FC] {V_FC : Type*} [DecidableEq V_FC]variable [hcnm : Concurrent.HasConcurrentNames (Feature.FeatureName N F) V G N_FC]variable [hcvr : Concurrent.HasConcurrentVersions V G V_FC]variable [hcfi : HasConcurrentFeatureIntermediate N V F G N_FC]
set_option linter.unusedSectionVars false
/-- Resolve membership in a left-nested `Finset` union by backtracking search:`mem_unions t` closes `x ∈ s₁ ∪ ⋯ ∪ sₙ` given a proof `t` of membership in oneof the components. -/syntax "mem_unions " term : tacticmacro_rules | `(tactic| mem_unions $t) => `(tactic| first | exact $t | (apply Finset.mem_union_left; mem_unions $t) | (apply Finset.mem_union_right; mem_unions $t))
/-! ### Joint feature-concurrent reduction
For each base depender-dependee pair `((n, v), m)` arising in any `Δ_f` or`Δ_a` entry, a single shared intermediate `cfIntermediate n v m` isintroduced. The intermediate carries the full version `u` (peer-style) ratherthan the granularity bucket `g(u)`, so that version uniqueness on theintermediate pins `u` to a single element of the intersection of the sharingentries' version sets.
For each contributing entry with version set `vs` and feature set `fs`:* `(i, origV u) ∈ R` for each `u ∈ vs`;* `(granular ⟨n, v⟩, origV v) Δ (i, vs.map origV)` (depender → intermediate);* `(i, origV u) Δ (granular ⟨m, g u⟩, {origV u})` (intermediate → orig dependee) for each `u ∈ vs`;* `(i, origV u) Δ (granular ⟨⟨m, f⟩, g u⟩, {origV u})` (intermediate → feature dependee) for each `(u, f) ∈ vs × fs`.
The bare Concurrent reduction's `intermediateN` packages are not used by thisencoding. -/
def concurrentFeatureReal (R : Real N V) (support : Feature.Support N V F) (Δ_f : Feature.FeatDepRel N V F) (Δ_a : Feature.AddlDepRel N V F) (g : V → G) : Real N_FC V_FC := -- Granular packages: image of the feature-level real under the concurrent embedding. Concurrent.embedReal (Feature.featureReal R support) g ∪ -- Shared concurrent-feature intermediates from Δ_f: `(cfIntermediate n v m, origV u)` -- for each `u ∈ vs`. (Δ_f.biUnion (fun ⟨⟨n, v⟩, m, vs, _⟩ => vs.image (fun u => (hcfi.cfIntermediateN n v m, hcvr.origV u)))) ∪ -- Per-feature secondary intermediates from Δ_f: `(cfIntermediateN_f n v m f, origV u)` -- for each `(u, f) ∈ vs × fs`. (Δ_f.biUnion (fun ⟨⟨n, v⟩, m, vs, fs⟩ => vs.biUnion (fun u => fs.image (fun f => (hcfi.cfIntermediateN_f n v m f, hcvr.origV u))))) ∪ -- Shared concurrent-feature intermediates from Δ_a: same shape; the feature annotation `f` -- on the depender is irrelevant -- the shared intermediate keys only on `((n, v), m)`. (Δ_a.biUnion (fun ⟨⟨⟨n, v⟩, _⟩, m, vs, _⟩ => vs.image (fun u => (hcfi.cfIntermediateN n v m, hcvr.origV u)))) ∪ -- Per-feature secondary intermediates from Δ_a: -- `(cfIntermediateN_a n v f m f', origV u)` for each `(u, f') ∈ vs × fs`. (Δ_a.biUnion (fun ⟨⟨⟨n, v⟩, f⟩, m, vs, fs⟩ => vs.biUnion (fun u => fs.image (fun f' => (hcfi.cfIntermediateN_a n v f m f', hcvr.origV u)))))
def concurrentFeatureDeps (R : Real N V) (support : Feature.Support N V F) (Δ_f : Feature.FeatDepRel N V F) (Δ_a : Feature.AddlDepRel N V F) (g : V → G) : DepRel N_FC V_FC := -- Feature back-deps from support: -- `(granularN (featured n f) (g v), origV v) Δ (granularN (orig n) (g v), {origV v})`. (support.biUnion (fun ⟨⟨n, v⟩, f⟩ => if (n, v) ∈ R then {((hcnm.granularN (Feature.FeatureName.featured n f) (g v), hcvr.origV v), hcnm.granularN (Feature.FeatureName.orig n) (g v), (({v} : Finset V).map hcvr.origV))} else ∅)) ∪ -- Δ_f: depender → shared intermediate, one edge per `((n, v), m, vs)` entry. (Δ_f.biUnion (fun ⟨⟨n, v⟩, m, vs, _⟩ => {((hcnm.granularN (Feature.FeatureName.orig n) (g v), hcvr.origV v), hcfi.cfIntermediateN n v m, vs.map hcvr.origV)})) ∪ -- Δ_f: shared intermediate → orig dependee, one per `u ∈ vs`. (Δ_f.biUnion (fun ⟨⟨n, v⟩, m, vs, _⟩ => vs.image (fun u => ((hcfi.cfIntermediateN n v m, hcvr.origV u), hcnm.granularN (Feature.FeatureName.orig m) (g u), (({u} : Finset V).map hcvr.origV))))) ∪ -- Δ_f: depender → per-feature secondary intermediate, one per `f ∈ fs`. (Δ_f.biUnion (fun ⟨⟨n, v⟩, m, vs, fs⟩ => fs.image (fun f => ((hcnm.granularN (Feature.FeatureName.orig n) (g v), hcvr.origV v), hcfi.cfIntermediateN_f n v m f, vs.map hcvr.origV)))) ∪ -- Δ_f: per-feature secondary intermediate → feature dependee, one per `(u, f) ∈ vs × fs`. (Δ_f.biUnion (fun ⟨⟨n, v⟩, m, vs, fs⟩ => vs.biUnion (fun u => fs.image (fun f => ((hcfi.cfIntermediateN_f n v m f, hcvr.origV u), hcnm.granularN (Feature.FeatureName.featured m f) (g u), (({u} : Finset V).map hcvr.origV)))))) ∪ -- Δ_f: per-feature secondary intermediate → shared intermediate (back-edge for -- version alignment), one per `(u, f) ∈ vs × fs`. (Δ_f.biUnion (fun ⟨⟨n, v⟩, m, vs, fs⟩ => fs.biUnion (fun f => vs.image (fun u => ((hcfi.cfIntermediateN_f n v m f, hcvr.origV u), hcfi.cfIntermediateN n v m, (({u} : Finset V).map hcvr.origV)))))) ∪ -- Δ_a: depender → shared intermediate. (Δ_a.biUnion (fun ⟨⟨⟨n, v⟩, f⟩, m, vs, _⟩ => {((hcnm.granularN (Feature.FeatureName.featured n f) (g v), hcvr.origV v), hcfi.cfIntermediateN n v m, vs.map hcvr.origV)})) ∪ -- Δ_a: shared intermediate → orig dependee, one per `u ∈ vs`. (Δ_a.biUnion (fun ⟨⟨⟨n, v⟩, _⟩, m, vs, _⟩ => vs.image (fun u => ((hcfi.cfIntermediateN n v m, hcvr.origV u), hcnm.granularN (Feature.FeatureName.orig m) (g u), (({u} : Finset V).map hcvr.origV))))) ∪ -- Δ_a: depender's featured package → per-feature secondary intermediate, one per `f' ∈ fs`. (Δ_a.biUnion (fun ⟨⟨⟨n, v⟩, f⟩, m, vs, fs⟩ => fs.image (fun f' => ((hcnm.granularN (Feature.FeatureName.featured n f) (g v), hcvr.origV v), hcfi.cfIntermediateN_a n v f m f', vs.map hcvr.origV)))) ∪ -- Δ_a: per-feature secondary intermediate → feature dependee. (Δ_a.biUnion (fun ⟨⟨⟨n, v⟩, f⟩, m, vs, fs⟩ => vs.biUnion (fun u => fs.image (fun f' => ((hcfi.cfIntermediateN_a n v f m f', hcvr.origV u), hcnm.granularN (Feature.FeatureName.featured m f') (g u), (({u} : Finset V).map hcvr.origV)))))) ∪ -- Δ_a: per-feature secondary intermediate → shared intermediate (back-edge for -- version alignment), one per `(u, f') ∈ vs × fs`. (Δ_a.biUnion (fun ⟨⟨⟨n, v⟩, f⟩, m, vs, fs⟩ => fs.biUnion (fun f' => vs.image (fun u => ((hcfi.cfIntermediateN_a n v f m f', hcvr.origV u), hcfi.cfIntermediateN n v m, (({u} : Finset V).map hcvr.origV))))))
/-! ### Membership constructors for `concurrentFeatureDeps` -/
theorem mem_cfDeps_f_depToInter {R : Real N V} {support : Feature.Support N V F} {Δ_f : Feature.FeatDepRel N V F} {Δ_a : Feature.AddlDepRel N V F} {g : V → G} {n : N} {v : V} {m : N} {vs : Finset V} {fs : Finset F} (hdep : ((n, v), m, vs, fs) ∈ Δ_f) : ((hcnm.granularN (Feature.FeatureName.orig n) (g v), hcvr.origV v), hcfi.cfIntermediateN n v m, vs.map hcvr.origV) ∈ concurrentFeatureDeps R support Δ_f Δ_a g := by mem_unions Finset.mem_biUnion.mpr ⟨⟨(n, v), m, vs, fs⟩, hdep, Finset.mem_singleton.mpr rfl⟩
theorem mem_cfDeps_f_interToOrig {R : Real N V} {support : Feature.Support N V F} {Δ_f : Feature.FeatDepRel N V F} {Δ_a : Feature.AddlDepRel N V F} {g : V → G} {n : N} {v : V} {m : N} {vs : Finset V} {fs : Finset F} {u : V} (hdep : ((n, v), m, vs, fs) ∈ Δ_f) (hv : u ∈ vs) : ((hcfi.cfIntermediateN n v m, hcvr.origV u), hcnm.granularN (Feature.FeatureName.orig m) (g u), (({u} : Finset V).map hcvr.origV)) ∈ concurrentFeatureDeps R support Δ_f Δ_a g := by mem_unions Finset.mem_biUnion.mpr ⟨⟨(n, v), m, vs, fs⟩, hdep, Finset.mem_image.mpr ⟨u, hv, rfl⟩⟩
/-- Δ_f: depender's orig granular → per-feature secondary intermediate `cfIntermediateN_f n v m f` for each `f ∈ fs`. -/theorem mem_cfDeps_f_depToInterFeat {R : Real N V} {support : Feature.Support N V F} {Δ_f : Feature.FeatDepRel N V F} {Δ_a : Feature.AddlDepRel N V F} {g : V → G} {n : N} {v : V} {m : N} {vs : Finset V} {fs : Finset F} {f : F} (hdep : ((n, v), m, vs, fs) ∈ Δ_f) (hf : f ∈ fs) : ((hcnm.granularN (Feature.FeatureName.orig n) (g v), hcvr.origV v), hcfi.cfIntermediateN_f n v m f, vs.map hcvr.origV) ∈ concurrentFeatureDeps R support Δ_f Δ_a g := by mem_unions Finset.mem_biUnion.mpr ⟨⟨(n, v), m, vs, fs⟩, hdep, Finset.mem_image.mpr ⟨f, hf, rfl⟩⟩
/-- Δ_f: per-feature secondary intermediate `cfIntermediateN_f n v m f` at `origV u` → feature granular dependee `granularN (featured m f) (g u)`. -/theorem mem_cfDeps_f_interToFeat {R : Real N V} {support : Feature.Support N V F} {Δ_f : Feature.FeatDepRel N V F} {Δ_a : Feature.AddlDepRel N V F} {g : V → G} {n : N} {v : V} {m : N} {vs : Finset V} {fs : Finset F} {u : V} {f : F} (hdep : ((n, v), m, vs, fs) ∈ Δ_f) (hv : u ∈ vs) (hf : f ∈ fs) : ((hcfi.cfIntermediateN_f n v m f, hcvr.origV u), hcnm.granularN (Feature.FeatureName.featured m f) (g u), (({u} : Finset V).map hcvr.origV)) ∈ concurrentFeatureDeps R support Δ_f Δ_a g := by mem_unions Finset.mem_biUnion.mpr ⟨⟨(n, v), m, vs, fs⟩, hdep, Finset.mem_biUnion.mpr ⟨u, hv, Finset.mem_image.mpr ⟨f, hf, rfl⟩⟩⟩
/-- Δ_f: per-feature secondary intermediate `cfIntermediateN_f n v m f` at `origV u` → shared intermediate `cfIntermediateN n v m`. Back-edge enforcing version alignment between secondary and shared. -/theorem mem_cfDeps_f_interFeatToInter {R : Real N V} {support : Feature.Support N V F} {Δ_f : Feature.FeatDepRel N V F} {Δ_a : Feature.AddlDepRel N V F} {g : V → G} {n : N} {v : V} {m : N} {vs : Finset V} {fs : Finset F} {u : V} {f : F} (hdep : ((n, v), m, vs, fs) ∈ Δ_f) (hu : u ∈ vs) (hf : f ∈ fs) : ((hcfi.cfIntermediateN_f n v m f, hcvr.origV u), hcfi.cfIntermediateN n v m, (({u} : Finset V).map hcvr.origV)) ∈ concurrentFeatureDeps R support Δ_f Δ_a g := by mem_unions Finset.mem_biUnion.mpr ⟨⟨(n, v), m, vs, fs⟩, hdep, Finset.mem_biUnion.mpr ⟨f, hf, Finset.mem_image.mpr ⟨u, hu, rfl⟩⟩⟩
theorem mem_cfDeps_a_depToInter {R : Real N V} {support : Feature.Support N V F} {Δ_f : Feature.FeatDepRel N V F} {Δ_a : Feature.AddlDepRel N V F} {g : V → G} {n : N} {v : V} {f : F} {m : N} {vs : Finset V} {fs : Finset F} (hdep : (((n, v), f), m, vs, fs) ∈ Δ_a) : ((hcnm.granularN (Feature.FeatureName.featured n f) (g v), hcvr.origV v), hcfi.cfIntermediateN n v m, vs.map hcvr.origV) ∈ concurrentFeatureDeps R support Δ_f Δ_a g := by mem_unions Finset.mem_biUnion.mpr ⟨⟨((n, v), f), m, vs, fs⟩, hdep, Finset.mem_singleton.mpr rfl⟩
theorem mem_cfDeps_a_interToOrig {R : Real N V} {support : Feature.Support N V F} {Δ_f : Feature.FeatDepRel N V F} {Δ_a : Feature.AddlDepRel N V F} {g : V → G} {n : N} {v : V} {f : F} {m : N} {vs : Finset V} {fs : Finset F} {u : V} (hdep : (((n, v), f), m, vs, fs) ∈ Δ_a) (hv : u ∈ vs) : ((hcfi.cfIntermediateN n v m, hcvr.origV u), hcnm.granularN (Feature.FeatureName.orig m) (g u), (({u} : Finset V).map hcvr.origV)) ∈ concurrentFeatureDeps R support Δ_f Δ_a g := by mem_unions Finset.mem_biUnion.mpr ⟨⟨((n, v), f), m, vs, fs⟩, hdep, Finset.mem_image.mpr ⟨u, hv, rfl⟩⟩
/-- Δ_a: depender's featured granular `(featured n f, g v)` → per-feature secondary intermediate `cfIntermediateN_a n v f m f'` for each `f' ∈ fs`. -/theorem mem_cfDeps_a_depToInterFeat {R : Real N V} {support : Feature.Support N V F} {Δ_f : Feature.FeatDepRel N V F} {Δ_a : Feature.AddlDepRel N V F} {g : V → G} {n : N} {v : V} {f : F} {m : N} {vs : Finset V} {fs : Finset F} {f' : F} (hdep : (((n, v), f), m, vs, fs) ∈ Δ_a) (hf' : f' ∈ fs) : ((hcnm.granularN (Feature.FeatureName.featured n f) (g v), hcvr.origV v), hcfi.cfIntermediateN_a n v f m f', vs.map hcvr.origV) ∈ concurrentFeatureDeps R support Δ_f Δ_a g := by mem_unions Finset.mem_biUnion.mpr ⟨⟨((n, v), f), m, vs, fs⟩, hdep, Finset.mem_image.mpr ⟨f', hf', rfl⟩⟩
/-- Δ_a: per-feature secondary intermediate `cfIntermediateN_a n v f m f'` at `origV u` → feature granular dependee `granularN (featured m f') (g u)`. -/theorem mem_cfDeps_a_interToFeat {R : Real N V} {support : Feature.Support N V F} {Δ_f : Feature.FeatDepRel N V F} {Δ_a : Feature.AddlDepRel N V F} {g : V → G} {n : N} {v : V} {f : F} {m : N} {vs : Finset V} {fs : Finset F} {u : V} {f' : F} (hdep : (((n, v), f), m, vs, fs) ∈ Δ_a) (hv : u ∈ vs) (hf' : f' ∈ fs) : ((hcfi.cfIntermediateN_a n v f m f', hcvr.origV u), hcnm.granularN (Feature.FeatureName.featured m f') (g u), (({u} : Finset V).map hcvr.origV)) ∈ concurrentFeatureDeps R support Δ_f Δ_a g := by mem_unions Finset.mem_biUnion.mpr ⟨⟨((n, v), f), m, vs, fs⟩, hdep, Finset.mem_biUnion.mpr ⟨u, hv, Finset.mem_image.mpr ⟨f', hf', rfl⟩⟩⟩
/-- Δ_a: per-feature secondary intermediate `cfIntermediateN_a n v f m f'` at `origV u` → shared intermediate `cfIntermediateN n v m`. Back-edge enforcing version alignment between secondary and shared. -/theorem mem_cfDeps_a_interFeatToInter {R : Real N V} {support : Feature.Support N V F} {Δ_f : Feature.FeatDepRel N V F} {Δ_a : Feature.AddlDepRel N V F} {g : V → G} {n : N} {v : V} {f : F} {m : N} {vs : Finset V} {fs : Finset F} {u : V} {f' : F} (hdep : (((n, v), f), m, vs, fs) ∈ Δ_a) (hu : u ∈ vs) (hf' : f' ∈ fs) : ((hcfi.cfIntermediateN_a n v f m f', hcvr.origV u), hcfi.cfIntermediateN n v m, (({u} : Finset V).map hcvr.origV)) ∈ concurrentFeatureDeps R support Δ_f Δ_a g := by mem_unions Finset.mem_biUnion.mpr ⟨⟨((n, v), f), m, vs, fs⟩, hdep, Finset.mem_biUnion.mpr ⟨f', hf', Finset.mem_image.mpr ⟨u, hu, rfl⟩⟩⟩
/-! ### Membership constructors for `concurrentFeatureReal` -/
theorem mem_cfReal_inter_f {R : Real N V} {support : Feature.Support N V F} {Δ_f : Feature.FeatDepRel N V F} {Δ_a : Feature.AddlDepRel N V F} {g : V → G} {n : N} {v : V} {m : N} {vs : Finset V} {fs : Finset F} {u : V} (hdep : ((n, v), m, vs, fs) ∈ Δ_f) (hv : u ∈ vs) : (hcfi.cfIntermediateN n v m, hcvr.origV u) ∈ concurrentFeatureReal R support Δ_f Δ_a g := by mem_unions Finset.mem_biUnion.mpr ⟨⟨(n, v), m, vs, fs⟩, hdep, Finset.mem_image.mpr ⟨u, hv, rfl⟩⟩
/-- Per-feature secondary intermediate `cfIntermediateN_f n v m f` is in `R` for each `(u, f) ∈ vs × fs` of a Δ_f entry. -/theorem mem_cfReal_inter_f_feat {R : Real N V} {support : Feature.Support N V F} {Δ_f : Feature.FeatDepRel N V F} {Δ_a : Feature.AddlDepRel N V F} {g : V → G} {n : N} {v : V} {m : N} {vs : Finset V} {fs : Finset F} {u : V} {f : F} (hdep : ((n, v), m, vs, fs) ∈ Δ_f) (hv : u ∈ vs) (hf : f ∈ fs) : (hcfi.cfIntermediateN_f n v m f, hcvr.origV u) ∈ concurrentFeatureReal R support Δ_f Δ_a g := by mem_unions Finset.mem_biUnion.mpr ⟨⟨(n, v), m, vs, fs⟩, hdep, Finset.mem_biUnion.mpr ⟨u, hv, Finset.mem_image.mpr ⟨f, hf, rfl⟩⟩⟩
theorem mem_cfReal_inter_a {R : Real N V} {support : Feature.Support N V F} {Δ_f : Feature.FeatDepRel N V F} {Δ_a : Feature.AddlDepRel N V F} {g : V → G} {n : N} {v : V} {f : F} {m : N} {vs : Finset V} {fs : Finset F} {u : V} (hdep : (((n, v), f), m, vs, fs) ∈ Δ_a) (hv : u ∈ vs) : (hcfi.cfIntermediateN n v m, hcvr.origV u) ∈ concurrentFeatureReal R support Δ_f Δ_a g := by mem_unions Finset.mem_biUnion.mpr ⟨⟨((n, v), f), m, vs, fs⟩, hdep, Finset.mem_image.mpr ⟨u, hv, rfl⟩⟩
/-- Per-feature secondary intermediate `cfIntermediateN_a n v f m f'` is in `R` for each `(u, f') ∈ vs × fs` of a Δ_a entry. -/theorem mem_cfReal_inter_a_feat {R : Real N V} {support : Feature.Support N V F} {Δ_f : Feature.FeatDepRel N V F} {Δ_a : Feature.AddlDepRel N V F} {g : V → G} {n : N} {v : V} {f : F} {m : N} {vs : Finset V} {fs : Finset F} {u : V} {f' : F} (hdep : (((n, v), f), m, vs, fs) ∈ Δ_a) (hv : u ∈ vs) (hf' : f' ∈ fs) : (hcfi.cfIntermediateN_a n v f m f', hcvr.origV u) ∈ concurrentFeatureReal R support Δ_f Δ_a g := by mem_unions Finset.mem_biUnion.mpr ⟨⟨((n, v), f), m, vs, fs⟩, hdep, Finset.mem_biUnion.mpr ⟨u, hv, Finset.mem_image.mpr ⟨f', hf', rfl⟩⟩⟩
/-! ### Reverse membership for `concurrentFeatureDeps` -/
theorem concurrentFeatureDeps_mem_cases {R : Real N V} {support : Feature.Support N V F} {Δ_f : Feature.FeatDepRel N V F} {Δ_a : Feature.AddlDepRel N V F} {g : V → G} {p : Package N_FC V_FC} {m_fc : N_FC} {vs : Finset V_FC} (h : (p, m_fc, vs) ∈ concurrentFeatureDeps R support Δ_f Δ_a g) : -- supp_back (∃ n v f, (n, v) ∈ R ∧ ((n, v), f) ∈ support ∧ p = (hcnm.granularN (Feature.FeatureName.featured n f) (g v), hcvr.origV v) ∧ m_fc = hcnm.granularN (Feature.FeatureName.orig n) (g v) ∧ vs = ({v} : Finset V).map hcvr.origV) ∨ -- f_depToInter (∃ n v m vs_raw fs, ((n, v), m, vs_raw, fs) ∈ Δ_f ∧ p = (hcnm.granularN (Feature.FeatureName.orig n) (g v), hcvr.origV v) ∧ m_fc = hcfi.cfIntermediateN n v m ∧ vs = vs_raw.map hcvr.origV) ∨ -- f_interToOrig (∃ n v m vs_raw fs u, ((n, v), m, vs_raw, fs) ∈ Δ_f ∧ u ∈ vs_raw ∧ p = (hcfi.cfIntermediateN n v m, hcvr.origV u) ∧ m_fc = hcnm.granularN (Feature.FeatureName.orig m) (g u) ∧ vs = ({u} : Finset V).map hcvr.origV) ∨ -- f_depToInterFeat (∃ n v m vs_raw fs f, ((n, v), m, vs_raw, fs) ∈ Δ_f ∧ f ∈ fs ∧ p = (hcnm.granularN (Feature.FeatureName.orig n) (g v), hcvr.origV v) ∧ m_fc = hcfi.cfIntermediateN_f n v m f ∧ vs = vs_raw.map hcvr.origV) ∨ -- f_interToFeat (∃ n v m vs_raw fs u f, ((n, v), m, vs_raw, fs) ∈ Δ_f ∧ u ∈ vs_raw ∧ f ∈ fs ∧ p = (hcfi.cfIntermediateN_f n v m f, hcvr.origV u) ∧ m_fc = hcnm.granularN (Feature.FeatureName.featured m f) (g u) ∧ vs = ({u} : Finset V).map hcvr.origV) ∨ -- f_interFeatToInter (back-edge) (∃ n v m vs_raw fs u f, ((n, v), m, vs_raw, fs) ∈ Δ_f ∧ u ∈ vs_raw ∧ f ∈ fs ∧ p = (hcfi.cfIntermediateN_f n v m f, hcvr.origV u) ∧ m_fc = hcfi.cfIntermediateN n v m ∧ vs = ({u} : Finset V).map hcvr.origV) ∨ -- a_depToInter (∃ n v f m vs_raw fs, (((n, v), f), m, vs_raw, fs) ∈ Δ_a ∧ p = (hcnm.granularN (Feature.FeatureName.featured n f) (g v), hcvr.origV v) ∧ m_fc = hcfi.cfIntermediateN n v m ∧ vs = vs_raw.map hcvr.origV) ∨ -- a_interToOrig (∃ n v f_dep m vs_raw fs u, (((n, v), f_dep), m, vs_raw, fs) ∈ Δ_a ∧ u ∈ vs_raw ∧ p = (hcfi.cfIntermediateN n v m, hcvr.origV u) ∧ m_fc = hcnm.granularN (Feature.FeatureName.orig m) (g u) ∧ vs = ({u} : Finset V).map hcvr.origV) ∨ -- a_depToInterFeat (∃ n v f_dep m vs_raw fs f', (((n, v), f_dep), m, vs_raw, fs) ∈ Δ_a ∧ f' ∈ fs ∧ p = (hcnm.granularN (Feature.FeatureName.featured n f_dep) (g v), hcvr.origV v) ∧ m_fc = hcfi.cfIntermediateN_a n v f_dep m f' ∧ vs = vs_raw.map hcvr.origV) ∨ -- a_interToFeat (∃ n v f_dep m vs_raw fs u f', (((n, v), f_dep), m, vs_raw, fs) ∈ Δ_a ∧ u ∈ vs_raw ∧ f' ∈ fs ∧ p = (hcfi.cfIntermediateN_a n v f_dep m f', hcvr.origV u) ∧ m_fc = hcnm.granularN (Feature.FeatureName.featured m f') (g u) ∧ vs = ({u} : Finset V).map hcvr.origV) ∨ -- a_interFeatToInter (back-edge) (∃ n v f_dep m vs_raw fs u f', (((n, v), f_dep), m, vs_raw, fs) ∈ Δ_a ∧ u ∈ vs_raw ∧ f' ∈ fs ∧ p = (hcfi.cfIntermediateN_a n v f_dep m f', hcvr.origV u) ∧ m_fc = hcfi.cfIntermediateN n v m ∧ vs = ({u} : Finset V).map hcvr.origV) := by simp only [concurrentFeatureDeps, Finset.mem_union, Finset.mem_biUnion, Finset.mem_image, Finset.mem_singleton] at h rcases h with (((((((((h | h) | h) | h) | h) | h) | h) | h) | h) | h) | h · -- supp_back left obtain ⟨⟨⟨n, v⟩, f⟩, hsupp, hmem⟩ := h simp only at hmem split_ifs at hmem with hR · simp only [Finset.mem_singleton, Prod.mk.injEq] at hmem obtain ⟨rfl, rfl, rfl⟩ := hmem exact ⟨n, v, f, hR, hsupp, rfl, rfl, rfl⟩ · exact absurd hmem (Finset.notMem_empty _) · -- f_depToInter right; left obtain ⟨⟨⟨n, v⟩, m, vs_raw, fs⟩, hdep, heq⟩ := h simp only [Prod.mk.injEq] at heq obtain ⟨rfl, rfl, rfl⟩ := heq exact ⟨n, v, m, vs_raw, fs, hdep, rfl, rfl, rfl⟩ · -- f_interToOrig right; right; left obtain ⟨⟨⟨n, v⟩, m, vs_raw, fs⟩, hdep, u, hv, heq⟩ := h simp only at hv simp only [Prod.mk.injEq] at heq obtain ⟨rfl, rfl, rfl⟩ := heq exact ⟨n, v, m, vs_raw, fs, u, hdep, hv, rfl, rfl, rfl⟩ · -- f_depToInterFeat right; right; right; left obtain ⟨⟨⟨n, v⟩, m, vs_raw, fs⟩, hdep, f, hf, heq⟩ := h simp only at hf simp only [Prod.mk.injEq] at heq obtain ⟨rfl, rfl, rfl⟩ := heq exact ⟨n, v, m, vs_raw, fs, f, hdep, hf, rfl, rfl, rfl⟩ · -- f_interToFeat right; right; right; right; left obtain ⟨⟨⟨n, v⟩, m, vs_raw, fs⟩, hdep, u, hv, f, hf, heq⟩ := h simp only at hv hf simp only [Prod.mk.injEq] at heq obtain ⟨rfl, rfl, rfl⟩ := heq exact ⟨n, v, m, vs_raw, fs, u, f, hdep, hv, hf, rfl, rfl, rfl⟩ · -- f_interFeatToInter right; right; right; right; right; left obtain ⟨⟨⟨n, v⟩, m, vs_raw, fs⟩, hdep, f, hf, u, hu, heq⟩ := h simp only at hf hu simp only [Prod.mk.injEq] at heq obtain ⟨rfl, rfl, rfl⟩ := heq exact ⟨n, v, m, vs_raw, fs, u, f, hdep, hu, hf, rfl, rfl, rfl⟩ · -- a_depToInter right; right; right; right; right; right; left obtain ⟨⟨⟨⟨n, v⟩, f⟩, m, vs_raw, fs⟩, hdep, heq⟩ := h simp only [Prod.mk.injEq] at heq obtain ⟨rfl, rfl, rfl⟩ := heq exact ⟨n, v, f, m, vs_raw, fs, hdep, rfl, rfl, rfl⟩ · -- a_interToOrig right; right; right; right; right; right; right; left obtain ⟨⟨⟨⟨n, v⟩, f⟩, m, vs_raw, fs⟩, hdep, u, hv, heq⟩ := h simp only at hv simp only [Prod.mk.injEq] at heq obtain ⟨rfl, rfl, rfl⟩ := heq exact ⟨n, v, f, m, vs_raw, fs, u, hdep, hv, rfl, rfl, rfl⟩ · -- a_depToInterFeat right; right; right; right; right; right; right; right; left obtain ⟨⟨⟨⟨n, v⟩, f⟩, m, vs_raw, fs⟩, hdep, f', hf', heq⟩ := h simp only at hf' simp only [Prod.mk.injEq] at heq obtain ⟨rfl, rfl, rfl⟩ := heq exact ⟨n, v, f, m, vs_raw, fs, f', hdep, hf', rfl, rfl, rfl⟩ · -- a_interToFeat right; right; right; right; right; right; right; right; right; left obtain ⟨⟨⟨⟨n, v⟩, f⟩, m, vs_raw, fs⟩, hdep, u, hv, f', hf', heq⟩ := h simp only at hv hf' simp only [Prod.mk.injEq] at heq obtain ⟨rfl, rfl, rfl⟩ := heq exact ⟨n, v, f, m, vs_raw, fs, u, f', hdep, hv, hf', rfl, rfl, rfl⟩ · -- a_interFeatToInter right; right; right; right; right; right; right; right; right; right obtain ⟨⟨⟨⟨n, v⟩, f⟩, m, vs_raw, fs⟩, hdep, f', hf', u, hu, heq⟩ := h simp only at hf' hu simp only [Prod.mk.injEq] at heq obtain ⟨rfl, rfl, rfl⟩ := heq exact ⟨n, v, f, m, vs_raw, fs, u, f', hdep, hu, hf', rfl, rfl, rfl⟩
end PackageCalculus.Composition