Something went wrong. Try again.
The Package Calculus
Something went wrong. Try again.
22 kB · 472 lines
at dev
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473import PackageCalculus.Extensions.Feature.Lifting.Definition
namespace PackageCalculus.Feature
variable {N : Type*} [DecidableEq N] {V : Type*} [DecidableEq V] {F : Type*} [DecidableEq F] [Fintype F]variable {N' : Type*} [DecidableEq N'] [hfn : HasFeatureNames N F N']
/-! ## Round-trip theorem -/
omit [Fintype F] intheorem liftReal_featureReal (R : Real N V) (support : Support N V F) : liftReal (hfn := hfn) (featureReal R support) = R := by ext p rw [mem_liftReal] simp only [featureReal, embedSet, embedPkg, Finset.mem_union, Finset.mem_image, Finset.mem_biUnion] constructor · intro h rcases h with ⟨⟨qn, qv⟩, hqR, heq⟩ | ⟨a, _, hmem_ite⟩ · simp only [Prod.mk.injEq] at heq obtain ⟨h1, h2⟩ := heq have := hfn.origN.injective h1; subst this; subst h2 exact hqR · split at hmem_ite · simp only [Finset.mem_singleton, Prod.mk.injEq] at hmem_ite exact absurd hmem_ite.1 (hfn.origN_ne_featuredN _ _ _) · simp at hmem_ite · intro hp exact Or.inl ⟨p, hp, rfl⟩
/-! ## Support, dependency- and additional-dependency-relation retraction -/
set_option linter.unusedSectionVars false
/-- `tryOrigN` rejects featured names. -/private theorem tryOrigN_featuredN (n : N) (f : F) : hfn.tryOrigN (hfn.featuredN n f) = none := by cases h : hfn.tryOrigN (hfn.featuredN n f) with | none => rfl | some m => exact (hfn.origN_ne_featuredN _ _ _ (hfn.tryOrigN_some _ _ h)).elim
/-- `tryFeaturedN` rejects origin names. -/private theorem tryFeaturedN_origN (n : N) : hfn.tryFeaturedN (hfn.origN n) = none := by cases h : hfn.tryFeaturedN (hfn.origN n) with | none => rfl | some p => exact (hfn.featuredN_ne_origN _ _ _ (hfn.tryFeaturedN_some _ _ h)).elim
/-- Membership in `featureDeps`, decomposed into its five edge families. -/theorem mem_featureDeps_iff {R : Real N V} {support : Support N V F} {Δ_f : FeatDepRel N V F} {Δ_a : AddlDepRel N V F} {e : Package N' V × N' × Finset V} : e ∈ featureDeps R support Δ_f Δ_a ↔ (∃ n v f, ((n, v), f) ∈ support ∧ (n, v) ∈ R ∧ e = ((hfn.featuredN n f, v), hfn.origN n, {v})) ∨ (∃ p n vs, (p, n, vs, (∅ : Finset F)) ∈ Δ_f ∧ e = (embedPkg F p, hfn.origN n, vs)) ∨ (∃ p n vs fs, (p, n, vs, fs) ∈ Δ_f ∧ fs.Nonempty ∧ ∃ f ∈ fs, e = (embedPkg F p, hfn.featuredN n f, vs)) ∨ (∃ n v f m vs, (((n, v), f), m, vs, (∅ : Finset F)) ∈ Δ_a ∧ e = ((hfn.featuredN n f, v), hfn.origN m, vs)) ∨ (∃ n v f m vs fs, (((n, v), f), m, vs, fs) ∈ Δ_a ∧ fs.Nonempty ∧ ∃ f' ∈ fs, e = ((hfn.featuredN n f, v), hfn.featuredN m f', vs)) := by simp only [featureDeps, Finset.mem_union, Finset.mem_image, Finset.mem_biUnion, Finset.mem_filter, Prod.exists] constructor · rintro ((((⟨n, v, f, hmem, hif⟩ | ⟨p₁, p₂, n, vs, fs, ⟨hmem, hfs⟩, heq⟩) | ⟨p₁, p₂, n, vs, fs, ⟨hmem, hfs⟩, f, hf, heq⟩) | ⟨n, v, f, m, vs, fs, ⟨hmem, hfs⟩, heq⟩) | ⟨n, v, f, m, vs, fs, ⟨hmem, hfs⟩, f', hf', heq⟩) · split at hif · rw [Finset.mem_singleton] at hif exact Or.inl ⟨n, v, f, hmem, ‹_›, hif⟩ · exact absurd hif (Finset.notMem_empty e) · subst hfs exact Or.inr (Or.inl ⟨p₁, p₂, n, vs, hmem, heq.symm⟩) · exact Or.inr (Or.inr (Or.inl ⟨p₁, p₂, n, vs, fs, hmem, hfs, f, hf, heq.symm⟩)) · subst hfs exact Or.inr (Or.inr (Or.inr (Or.inl ⟨n, v, f, m, vs, hmem, heq.symm⟩))) · exact Or.inr (Or.inr (Or.inr (Or.inr ⟨n, v, f, m, vs, fs, hmem, hfs, f', hf', heq.symm⟩))) · rintro (⟨n, v, f, hmem, hR, rfl⟩ | ⟨p₁, p₂, n, vs, hmem, rfl⟩ | ⟨p₁, p₂, n, vs, fs, hmem, hfs, f, hf, rfl⟩ | ⟨n, v, f, m, vs, hmem, rfl⟩ | ⟨n, v, f, m, vs, fs, hmem, hfs, f', hf', rfl⟩) · refine Or.inl (Or.inl (Or.inl (Or.inl ⟨n, v, f, hmem, ?_⟩))) rw [if_pos hR] exact Finset.mem_singleton.mpr rfl · exact Or.inl (Or.inl (Or.inl (Or.inr ⟨p₁, p₂, n, vs, ∅, ⟨hmem, rfl⟩, rfl⟩))) · exact Or.inl (Or.inl (Or.inr ⟨p₁, p₂, n, vs, fs, ⟨hmem, hfs⟩, f, hf, rfl⟩)) · exact Or.inl (Or.inr ⟨n, v, f, m, vs, ∅, ⟨hmem, rfl⟩, rfl⟩) · exact Or.inr ⟨n, v, f, m, vs, fs, ⟨hmem, hfs⟩, f', hf', rfl⟩
/-! ### Evaluation of the edge decoders on canonical edges -/
private theorem embedPkg_injective {p q : Package N V} (h : embedPkg F (hfn := hfn) p = embedPkg F (hfn := hfn) q) : p = q := by simp only [embedPkg, Prod.mk.injEq] at h exact Prod.ext (hfn.origN.injective h.1) h.2
private theorem tryInvDepF0_eval {p : Package N V} {n : N} {vs : Finset V} : tryInvDepF0 (hfn := hfn) (embedPkg F p, hfn.origN n, vs) = some (p, n, vs, ∅) := by simp only [tryInvDepF0, embedPkg, hfn.tryOrigN_origN]
private theorem tryInvDepF1_eval {Δ' : DepRel N' V} {p : Package N V} {n : N} {f : F} {vs : Finset V} : tryInvDepF1 Δ' (embedPkg F p, hfn.featuredN n f, vs) = some (p, n, vs, gatherFs (F := F) Δ' p n vs) := by simp only [tryInvDepF1, embedPkg, hfn.tryOrigN_origN, hfn.tryFeaturedN_featuredN]
private theorem tryInvDepA0_eval {n : N} {v : V} {f : F} {m : N} {vs : Finset V} : tryInvDepA0 (hfn := hfn) ((hfn.featuredN n f, v), hfn.origN m, vs) = some (((n, v), f), m, vs, ∅) := by simp only [tryInvDepA0, hfn.tryFeaturedN_featuredN, hfn.tryOrigN_origN]
private theorem tryInvDepA1_eval {Δ' : DepRel N' V} {n : N} {v : V} {f : F} {m : N} {f' : F} {vs : Finset V} : tryInvDepA1 Δ' ((hfn.featuredN n f, v), hfn.featuredN m f', vs) = some (((n, v), f), m, vs, gatherAFs Δ' n v f m vs) := by simp only [tryInvDepA1, hfn.tryFeaturedN_featuredN]
theorem mem_baseDeps {R : Real N V} {support : Support N V F} {d : (Package N V × F) × N × Finset V × Finset F} : d ∈ baseDeps R support ↔ ∃ n v f, ((n, v), f) ∈ support ∧ (n, v) ∈ R ∧ d = (((n, v), f), n, {v}, ∅) := by simp only [baseDeps, Finset.mem_biUnion] constructor · rintro ⟨s, hs, hd⟩ split at hd · rw [Finset.mem_singleton] at hd obtain ⟨⟨n, v⟩, f⟩ := s exact ⟨n, v, f, hs, ‹_›, hd⟩ · exact absurd hd (Finset.notMem_empty d) · rintro ⟨n, v, f, hs, hR, rfl⟩ exact ⟨((n, v), f), hs, by rw [if_pos hR]; exact Finset.mem_singleton.mpr rfl⟩
/-! ### Gather lemmas -/
/-- For an entry of a `FunctionalInName` relation, `gatherFs` over the reductionrecovers exactly its required-feature set. -/private theorem gatherFs_eq_of_mem {R : Real N V} {support : Support N V F} {Δ_f : FeatDepRel N V F} {Δ_a : AddlDepRel N V F} {p : Package N V} {n : N} {vs : Finset V} {fs : Finset F} (hmem : (p, n, vs, fs) ∈ Δ_f) (hfunc : Δ_f.FunctionalInName) : gatherFs (featureDeps R support Δ_f Δ_a) p n vs = fs := by ext f simp only [gatherFs, Finset.mem_filter, Finset.mem_univ, true_and] constructor · intro hf rw [mem_featureDeps_iff] at hf rcases hf with ⟨n', v', f', _, _, heq⟩ | ⟨p', n', vs', _, heq⟩ | ⟨p', n', vs', fs', hmem', _, f₀, hf₀, heq⟩ | ⟨n', v', f', m', vs', _, heq⟩ | ⟨n', v', f', m', vs', fs', _, _, f₁, _, heq⟩ · simp [embedPkg] at heq · simp [embedPkg] at heq · simp only [embedPkg, Prod.mk.injEq] at heq obtain ⟨⟨hp1, hp2⟩, hn, hv⟩ := heq obtain rfl : p = p' := Prod.ext (hfn.origN.injective hp1) hp2 obtain ⟨rfl, rfl⟩ := hfn.featuredN_injective hn subst hv obtain ⟨_, rfl⟩ := hfunc p n vs fs vs fs' hmem hmem' exact hf₀ · simp [embedPkg] at heq · simp [embedPkg] at heq · intro hf rw [mem_featureDeps_iff] exact Or.inr (Or.inr (Or.inl ⟨p, n, vs, fs, hmem, ⟨f, hf⟩, f, hf, rfl⟩))
/-- For an entry of a `FunctionalInName` additional-dependency relation,`gatherAFs` over the reduction recovers exactly its required-feature set. -/private theorem gatherAFs_eq_of_mem {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} {m : N} {vs : Finset V} {fs : Finset F} (hmem : (((n, v), f), m, vs, fs) ∈ Δ_a) (hfunc : Δ_a.FunctionalInName) : gatherAFs (featureDeps R support Δ_f Δ_a) n v f m vs = fs := by ext f₂ simp only [gatherAFs, Finset.mem_filter, Finset.mem_univ, true_and] constructor · intro hf rw [mem_featureDeps_iff] at hf rcases hf with ⟨n', v', f', _, _, heq⟩ | ⟨p', n', vs', _, heq⟩ | ⟨p', n', vs', fs', _, _, f₀, _, heq⟩ | ⟨n', v', f', m', vs', _, heq⟩ | ⟨n', v', f', m', vs', fs', hmem', _, f₁, hf₁, heq⟩ · simp at heq · simp [embedPkg] at heq · simp [embedPkg] at heq · simp at heq · simp only [Prod.mk.injEq] at heq obtain ⟨⟨hn, hv⟩, hm, hvs⟩ := heq obtain ⟨rfl, rfl⟩ := hfn.featuredN_injective hn obtain ⟨rfl, rfl⟩ := hfn.featuredN_injective hm subst hv subst hvs obtain ⟨_, rfl⟩ := hfunc ((n, v), f) m vs fs vs fs' hmem hmem' exact hf₁ · intro hf rw [mem_featureDeps_iff] exact Or.inr (Or.inr (Or.inr (Or.inr ⟨n, v, f, m, vs, fs, hmem, ⟨f₂, hf⟩, f₂, hf, rfl⟩)))
/-! ### Soundness of the decoders on reduced dependency relations -/
/-- Membership in `featureReal`, decomposed into its two package families. -/theorem mem_featureReal_iff {R : Real N V} {support : Support N V F} {q : Package N' V} : q ∈ featureReal R support ↔ (∃ p ∈ R, q = embedPkg F p) ∨ (∃ n v f, ((n, v), f) ∈ support ∧ (n, v) ∈ R ∧ q = (hfn.featuredN n f, v)) := by simp only [featureReal, embedSet, Finset.mem_union, Finset.mem_image, Finset.mem_biUnion, Prod.exists] constructor · rintro (⟨p₁, p₂, hp, heq⟩ | ⟨n, v, f, hs, hif⟩) · exact Or.inl ⟨p₁, p₂, hp, heq.symm⟩ · split at hif · rw [Finset.mem_singleton] at hif exact Or.inr ⟨n, v, f, hs, ‹_›, hif⟩ · exact absurd hif (Finset.notMem_empty q) · rintro (⟨p₁, p₂, hp, rfl⟩ | ⟨n, v, f, hs, hR, rfl⟩) · exact Or.inl ⟨p₁, p₂, hp, rfl⟩ · refine Or.inr ⟨n, v, f, hs, ?_⟩ rw [if_pos hR] exact Finset.mem_singleton.mpr rfl
theorem mem_liftSupport {R' : Real N' V} {n : N} {v : V} {f : F} : ((n, v), f) ∈ liftSupport (hfn := hfn) R' ↔ (hfn.featuredN n f, v) ∈ R' := by simp only [liftSupport, Finset.mem_biUnion, Option.mem_toFinset, Option.mem_def] constructor · rintro ⟨p, hp, hinv⟩ rw [tryInvSupp, Option.map_eq_some_iff] at hinv obtain ⟨⟨n₀, f₀⟩, htry, heq⟩ := hinv simp only [Prod.mk.injEq] at heq obtain ⟨⟨hn, hp2⟩, hf0⟩ := heq rw [hn, hf0] at htry have hp1 := hfn.tryFeaturedN_some _ _ htry have hpe : ((hfn.featuredN n f, v) : Package N' V) = p := Prod.ext hp1 hp2.symm rwa [hpe] · intro hp refine ⟨(hfn.featuredN n f, v), hp, ?_⟩ rw [tryInvSupp] simp [hfn.tryFeaturedN_featuredN]
/-- Only no-feature parameterised edges are inverted by `tryInvDepF0`, togenuine entries of `Δ_f`. -/private theorem sound_depF0 {R : Real N V} {support : Support N V F} {Δ_f : FeatDepRel N V F} {Δ_a : AddlDepRel N V F} {e : Package N' V × N' × Finset V} {d : Package N V × N × Finset V × Finset F} (hmem : e ∈ featureDeps R support Δ_f Δ_a) (h : tryInvDepF0 (hfn := hfn) e = some d) : d ∈ Δ_f := by rw [mem_featureDeps_iff] at hmem rcases hmem with ⟨n, v, f, _, _, rfl⟩ | ⟨p, n, vs, hmem, rfl⟩ | ⟨p, n, vs, fs, _, _, f, _, rfl⟩ | ⟨n, v, f, m, vs, _, rfl⟩ | ⟨n, v, f, m, vs, fs, _, _, f', _, rfl⟩ · simp only [tryInvDepF0, tryOrigN_featuredN] at h exact absurd h (by simp) · rw [tryInvDepF0_eval] at h obtain rfl := Option.some.inj h exact hmem · simp only [tryInvDepF0, embedPkg, hfn.tryOrigN_origN, tryOrigN_featuredN] at h exact absurd h (by simp) · simp only [tryInvDepF0, tryOrigN_featuredN] at h exact absurd h (by simp) · simp only [tryInvDepF0, tryOrigN_featuredN] at h exact absurd h (by simp)
/-- Only featured parameterised edges are inverted by `tryInvDepF1`, to genuineentries of `Δ_f` (via `gatherFs`). -/private theorem sound_depF1 {R : Real N V} {support : Support N V F} {Δ_f : FeatDepRel N V F} {Δ_a : AddlDepRel N V F} {e : Package N' V × N' × Finset V} {d : Package N V × N × Finset V × Finset F} (hfunc : Δ_f.FunctionalInName) (hmem : e ∈ featureDeps R support Δ_f Δ_a) (h : tryInvDepF1 (featureDeps R support Δ_f Δ_a) e = some d) : d ∈ Δ_f := by rw [mem_featureDeps_iff] at hmem rcases hmem with ⟨n, v, f, _, _, rfl⟩ | ⟨p, n, vs, hmem, rfl⟩ | ⟨p, n, vs, fs, hmem, _, f, _, rfl⟩ | ⟨n, v, f, m, vs, _, rfl⟩ | ⟨n, v, f, m, vs, fs, _, _, f', _, rfl⟩ · simp only [tryInvDepF1, tryOrigN_featuredN] at h exact absurd h (by simp) · simp only [tryInvDepF1, embedPkg, hfn.tryOrigN_origN, tryFeaturedN_origN] at h exact absurd h (by simp) · rw [tryInvDepF1_eval] at h obtain rfl := Option.some.inj h rw [gatherFs_eq_of_mem hmem hfunc] exact hmem · simp only [tryInvDepF1, tryOrigN_featuredN] at h exact absurd h (by simp) · simp only [tryInvDepF1, tryOrigN_featuredN] at h exact absurd h (by simp)
/-- No-feature additional edges are inverted by `tryInvDepA0` to genuine entriesof `Δ_a` — or to automatic base requirements, with which they alias. -/private theorem sound_depA0 {R : Real N V} {support : Support N V F} {Δ_f : FeatDepRel N V F} {Δ_a : AddlDepRel N V F} {e : Package N' V × N' × Finset V} {d : (Package N V × F) × N × Finset V × Finset F} (hmem : e ∈ featureDeps R support Δ_f Δ_a) (h : tryInvDepA0 (hfn := hfn) e = some d) : d ∈ Δ_a ∪ baseDeps R support := by rw [mem_featureDeps_iff] at hmem rcases hmem with ⟨n, v, f, hs, hR, rfl⟩ | ⟨p, n, vs, _, rfl⟩ | ⟨p, n, vs, fs, _, _, f, _, rfl⟩ | ⟨n, v, f, m, vs, hmem, rfl⟩ | ⟨n, v, f, m, vs, fs, _, _, f', _, rfl⟩ · rw [tryInvDepA0_eval] at h obtain rfl := Option.some.inj h exact Finset.mem_union_right _ (mem_baseDeps.mpr ⟨n, v, f, hs, hR, rfl⟩) · simp only [tryInvDepA0, embedPkg, tryFeaturedN_origN] at h exact absurd h (by simp) · simp only [tryInvDepA0, embedPkg, tryFeaturedN_origN] at h exact absurd h (by simp) · rw [tryInvDepA0_eval] at h obtain rfl := Option.some.inj h exact Finset.mem_union_left _ hmem · simp only [tryInvDepA0, hfn.tryFeaturedN_featuredN, tryOrigN_featuredN] at h exact absurd h (by simp)
/-- Featured additional edges are inverted by `tryInvDepA1` to genuine entriesof `Δ_a` (via `gatherAFs`). -/private theorem sound_depA1 {R : Real N V} {support : Support N V F} {Δ_f : FeatDepRel N V F} {Δ_a : AddlDepRel N V F} {e : Package N' V × N' × Finset V} {d : (Package N V × F) × N × Finset V × Finset F} (hfunc : Δ_a.FunctionalInName) (hmem : e ∈ featureDeps R support Δ_f Δ_a) (h : tryInvDepA1 (featureDeps R support Δ_f Δ_a) e = some d) : d ∈ Δ_a := by rw [mem_featureDeps_iff] at hmem rcases hmem with ⟨n, v, f, _, _, rfl⟩ | ⟨p, n, vs, _, rfl⟩ | ⟨p, n, vs, fs, _, _, f, _, rfl⟩ | ⟨n, v, f, m, vs, _, rfl⟩ | ⟨n, v, f, m, vs, fs, hmem, _, f', _, rfl⟩ · simp only [tryInvDepA1, hfn.tryFeaturedN_featuredN, tryFeaturedN_origN] at h exact absurd h (by simp) · simp only [tryInvDepA1, embedPkg, tryFeaturedN_origN] at h exact absurd h (by simp) · simp only [tryInvDepA1, embedPkg, tryFeaturedN_origN] at h exact absurd h (by simp) · simp only [tryInvDepA1, hfn.tryFeaturedN_featuredN, tryFeaturedN_origN] at h exact absurd h (by simp) · rw [tryInvDepA1_eval] at h obtain rfl := Option.some.inj h rw [gatherAFs_eq_of_mem hmem hfunc] exact hmem
/-! ### Retraction theorems -/
/-- **Retraction of the support relation.** The reduced repository determinesthe grounded part of the support relation. -/theorem liftSupport_featureReal (R : Real N V) (support : Support N V F) : liftSupport (hfn := hfn) (featureReal R support) = support.filter (fun s => s.1 ∈ R) := by ext s obtain ⟨⟨n, v⟩, f⟩ := s rw [mem_liftSupport, mem_featureReal_iff, Finset.mem_filter] constructor · rintro (⟨p, _, heq⟩ | ⟨n', v', f', hs, hR, heq⟩) · simp [embedPkg] at heq · simp only [Prod.mk.injEq] at heq obtain ⟨hn, rfl⟩ := heq obtain ⟨rfl, rfl⟩ := hfn.featuredN_injective hn exact ⟨hs, hR⟩ · rintro ⟨hs, hR⟩ exact Or.inr ⟨n, v, f, hs, hR, rfl⟩
/-- For a `GroundedIn` support relation, the retraction is exact. -/theorem liftSupport_featureReal_of_grounded (R : Real N V) (support : Support N V F) (hg : support.GroundedIn R) : liftSupport (hfn := hfn) (featureReal R support) = support := by rw [liftSupport_featureReal] exact Finset.filter_true_of_mem (fun s hs => hg s.1 s.2 hs)
/-- `baseDeps` only sees the grounded part of the support relation. -/theorem baseDeps_filter (R : Real N V) (support : Support N V F) : baseDeps R (support.filter (fun s => s.1 ∈ R)) = baseDeps R support := by ext d rw [mem_baseDeps, mem_baseDeps] constructor · rintro ⟨n, v, f, hs, hR, rfl⟩ exact ⟨n, v, f, (Finset.mem_filter.mp hs).1, hR, rfl⟩ · rintro ⟨n, v, f, hs, hR, rfl⟩ exact ⟨n, v, f, Finset.mem_filter.mpr ⟨hs, hR⟩, hR, rfl⟩
/-- **Retraction of the feature dependency relation.** No side-condition beyondthe standing Functional-in-Name normalisation. -/theorem liftDepsF_featureDeps (R : Real N V) (support : Support N V F) (Δ_f : FeatDepRel N V F) (Δ_a : AddlDepRel N V F) (hfunc : Δ_f.FunctionalInName) : liftDepsF (featureDeps (hfn := hfn) R support Δ_f Δ_a) = Δ_f := by ext d simp only [liftDepsF, Finset.mem_biUnion, Finset.mem_union, Option.mem_toFinset, Option.mem_def] constructor · rintro ⟨e, he, hF | hF⟩ · exact sound_depF0 he hF · exact sound_depF1 hfunc he hF · intro hd obtain ⟨p, n, vs, fs⟩ := d rcases Finset.eq_empty_or_nonempty fs with rfl | ⟨f, hf⟩ · exact ⟨(embedPkg F p, hfn.origN n, vs), mem_featureDeps_iff.mpr (Or.inr (Or.inl ⟨p, n, vs, hd, rfl⟩)), Or.inl tryInvDepF0_eval⟩ · refine ⟨(embedPkg F p, hfn.featuredN n f, vs), mem_featureDeps_iff.mpr (Or.inr (Or.inr (Or.inl ⟨p, n, vs, fs, hd, ⟨f, hf⟩, f, hf, rfl⟩))), Or.inr ?_⟩ rw [tryInvDepF1_eval, gatherFs_eq_of_mem hd hfunc]
/-- **Normal-form retraction of the additional-dependency relation.** Withoutany irredundancy hypothesis, the raw lift recovers `Δ_a` *up to thebase-requirement closure*: exactly the automatic base requirements of groundedsupport facts are added, and nothing else. -/theorem liftDepsARaw_featureDeps (R : Real N V) (support : Support N V F) (Δ_f : FeatDepRel N V F) (Δ_a : AddlDepRel N V F) (hfunc : Δ_a.FunctionalInName) : liftDepsARaw (featureDeps (hfn := hfn) R support Δ_f Δ_a) = Δ_a ∪ baseDeps R support := by ext d simp only [liftDepsARaw, Finset.mem_biUnion, Finset.mem_union, Option.mem_toFinset, Option.mem_def] constructor · rintro ⟨e, he, hA | hA⟩ · have := sound_depA0 he hA rwa [Finset.mem_union] at this · exact Or.inl (sound_depA1 hfunc he hA) · rintro (hd | hd) · obtain ⟨⟨⟨n, v⟩, f⟩, m, vs, fs⟩ := d rcases Finset.eq_empty_or_nonempty fs with rfl | ⟨f', hf'⟩ · exact ⟨((hfn.featuredN n f, v), hfn.origN m, vs), mem_featureDeps_iff.mpr (Or.inr (Or.inr (Or.inr (Or.inl ⟨n, v, f, m, vs, hd, rfl⟩)))), Or.inl tryInvDepA0_eval⟩ · refine ⟨((hfn.featuredN n f, v), hfn.featuredN m f', vs), mem_featureDeps_iff.mpr (Or.inr (Or.inr (Or.inr (Or.inr ⟨n, v, f, m, vs, fs, hd, ⟨f', hf'⟩, f', hf', rfl⟩)))), Or.inr ?_⟩ rw [tryInvDepA1_eval, gatherAFs_eq_of_mem hd hfunc] · rw [mem_baseDeps] at hd obtain ⟨n, v, f, hs, hR, rfl⟩ := hd exact ⟨((hfn.featuredN n f, v), hfn.origN n, {v}), mem_featureDeps_iff.mpr (Or.inl ⟨n, v, f, hs, hR, rfl⟩), Or.inl tryInvDepA0_eval⟩
/-- **Retraction of the additional-dependency relation.** For a`BaseIrredundant` relation, subtracting the recomputed base requirementsrecovers `Δ_a` on the nose. -/theorem liftDepsA_featureDeps (R : Real N V) (support : Support N V F) (Δ_f : FeatDepRel N V F) (Δ_a : AddlDepRel N V F) (hfunc : Δ_a.FunctionalInName) (hirr : Δ_a.BaseIrredundant R support) : liftDepsA (featureReal (hfn := hfn) R support) (featureDeps R support Δ_f Δ_a) = Δ_a := by rw [liftDepsA, liftDepsARaw_featureDeps R support Δ_f Δ_a hfunc, liftReal_featureReal, liftSupport_featureReal, baseDeps_filter] ext d simp only [Finset.mem_sdiff, Finset.mem_union] constructor · rintro ⟨hd | hd, hnb⟩ · exact hd · exact absurd hd hnb · intro hd refine ⟨Or.inl hd, fun hb => ?_⟩ rw [mem_baseDeps] at hb obtain ⟨n, v, f, hs, hR, rfl⟩ := hb exact hirr n v f hs hR hd
/-- **Full instance-level retraction for the feature extension.** For agrounded support relation and Functional-in-Name, base-irredundant dependencyrelations, lifting the reduced package universe and dependency relationrecovers the original quadruple `(R_f, support, Δ_f, Δ_a)`. -/theorem featureLift_featureReduce (R : Real N V) (support : Support N V F) (Δ_f : FeatDepRel N V F) (Δ_a : AddlDepRel N V F) (hg : support.GroundedIn R) (hf : Δ_f.FunctionalInName) (ha : Δ_a.FunctionalInName) (hirr : Δ_a.BaseIrredundant R support) : (liftReal (hfn := hfn) (featureReal R support), liftSupport (hfn := hfn) (featureReal R support), liftDepsF (featureDeps (hfn := hfn) R support Δ_f Δ_a), liftDepsA (featureReal (hfn := hfn) R support) (featureDeps R support Δ_f Δ_a)) = (R, support, Δ_f, Δ_a) := by rw [liftReal_featureReal, liftSupport_featureReal_of_grounded R support hg, liftDepsF_featureDeps R support Δ_f Δ_a hf, liftDepsA_featureDeps R support Δ_f Δ_a ha hirr]
end PackageCalculus.Feature