ryan.freumh.org
The Package Calculus
1.9 kB
44 lines
1import PackageCalculus.Extensions.Virtual.Lifting.Definition
2
3namespace PackageCalculus.Virtual
4
5variable {N : Type*} [DecidableEq N] {V : Type*} [DecidableEq V]
6variable {N' : Type*} [DecidableEq N'] {V' : Type*} [DecidableEq V']
7variable [hvn : HasVirtualNames N V N'] [hvv : HasVirtualVersions N V V']
8
9theorem liftResolution_completenessWitness
10 (Delta_v : DepRel N V) (prov : ProvidesRel N V)
11 (S_v : Finset (Package N V))
12 (rho : Finset (Package N V × N × Package N V)) :
13 liftResolution (completenessWitness Delta_v prov S_v rho) = S_v := by
14 ext p
15 simp only [mem_liftResolution, completenessWitness, embedSet, Finset.mem_union,
16 Finset.mem_image, Finset.mem_biUnion, Finset.mem_filter, embedPkg]
17 constructor
18 · intro h
19 rcases h with ⟨q, hqS, heq⟩ | ⟨⟨p', n, vs⟩, ⟨_, _⟩, hmem⟩
20 · simp only [Prod.mk.injEq] at heq
21 exact (Prod.ext (hvn.origN.injective heq.1) (hvv.origV.injective heq.2) : q = p) ▸ hqS
22 · split at hmem
23 · rw [Finset.mem_singleton] at hmem
24 simp only [Prod.mk.injEq] at hmem
25 exact absurd hmem.1 (hvn.origN_ne_selectorN _ _ _)
26 · simp at hmem
27 · intro hp
28 exact Or.inl ⟨p, hp, rfl⟩
29
30theorem liftResolution_completeness
31 (R_v : Real N V) (Delta_v : DepRel N V)
32 (prov : ProvidesRel N V) (r : Package N V)
33 (S_v : Finset (Package N V))
34 (rho : Finset (Package N V × N × Package N V))
35 (hres : IsVirtualResolution R_v Delta_v prov r S_v rho)
36 (hfunc : ∀ p n vs₁ vs₂, (p, n, vs₁) ∈ Delta_v → (p, n, vs₂) ∈ Delta_v → vs₁ = vs₂) :
37 ∃ S', IsResolution (virtualReal R_v Delta_v prov) (virtualDeps Delta_v R_v prov)
38 (embedPkg r) S' ∧ liftResolution S' = S_v :=
39 ⟨completenessWitness Delta_v prov S_v rho,
40 virtual_completeness R_v Delta_v prov r S_v rho hres hfunc,
41 liftResolution_completenessWitness Delta_v prov S_v rho⟩
42
43
44end PackageCalculus.Virtual