From 794c04eee93ba5bbb8ac0e512b185029d33efb65 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 9 May 2024 18:37:50 -0700 Subject: [PATCH] Prove the foldr-implies lemma Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 28 +++++++++++++++++++++++--- Lattice/FiniteValueMap.agda | 40 ++++++++++++++++++------------------- 2 files changed, 45 insertions(+), 23 deletions(-) diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index 6b612cd..8565dae 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -11,6 +11,7 @@ open import Data.Empty using (⊥-elim) open import Data.String using (String) renaming (_≟_ to _≟ˢ_) open import Data.Nat using (suc) open import Data.Product using (_×_; proj₁; proj₂; _,_) +open import Data.Sum using (inj₁; inj₂) open import Data.List using (List; _∷_; []; foldr; foldl; cartesianProduct; cartesianProductWith) open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_) open import Data.List.Relation.Unary.Any as Any using () @@ -19,7 +20,7 @@ open import Relation.Nullary using (¬_; Dec; yes; no) open import Data.Unit using (⊤) open import Function using (_∘_; flip) -open import Utils using (Pairwise; _⇒_) +open import Utils using (Pairwise; _⇒_; _∨_) import Lattice.FiniteValueMap open IsFiniteHeightLattice isFiniteHeightLatticeˡ @@ -62,6 +63,11 @@ module WithProg (prog : Program) where ; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ ; ⊔-idemp to ⊔ᵛ-idemp ) + open Lattice.FiniteValueMap.IterProdIsomorphism _≟ˢ_ isLatticeˡ + using () + renaming + ( Provenance-union to Provenance-unionᵐ + ) open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟ˢ_ isLatticeˡ vars-Unique ≈ˡ-dec _ fixedHeightˡ using () renaming @@ -236,7 +242,11 @@ module WithProg (prog : Program) where module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where open LatticeInterpretation latticeInterpretationˡ using () - renaming (⟦_⟧ to ⟦_⟧ˡ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ) + renaming + ( ⟦_⟧ to ⟦_⟧ˡ + ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ + ; ⟦⟧-⊔-∨ to ⟦⟧ˡ-⊔ˡ-∨ + ) ⟦_⟧ᵛ : VariableValues → Env → Set ⟦_⟧ᵛ vs ρ = ∀ {k l} → (k , l) ∈ᵛ vs → ∀ {v} → (k , v) Language.∈ ρ → ⟦ l ⟧ˡ v @@ -251,9 +261,21 @@ module WithProg (prog : Program) where in ⟦⟧ˡ-respects-≈ˡ (≈ˡ-sym l≈l') v ⟦l'⟧v + ⟦⟧ᵛ-⊔ᵛ-∨ : ∀ {vs₁ vs₂ : VariableValues} → (⟦ vs₁ ⟧ᵛ ∨ ⟦ vs₂ ⟧ᵛ) ⇒ ⟦ vs₁ ⊔ᵛ vs₂ ⟧ᵛ + ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁} {vs₂} ρ ⟦vs₁⟧ρ∨⟦vs₂⟧ρ {k} {l} k,l∈vs₁₂ {v} k,v∈ρ + with ((l₁ , l₂) , (refl , (k,l₁∈vs₁ , k,l₂∈vs₂))) + ← Provenance-unionᵐ vs₁ vs₂ k,l∈vs₁₂ + with ⟦vs₁⟧ρ∨⟦vs₂⟧ρ + ... | inj₁ ⟦vs₁⟧ρ = ⟦⟧ˡ-⊔ˡ-∨ {l₁} {l₂} v (inj₁ (⟦vs₁⟧ρ k,l₁∈vs₁ k,v∈ρ)) + ... | inj₂ ⟦vs₂⟧ρ = ⟦⟧ˡ-⊔ˡ-∨ {l₁} {l₂} v (inj₂ (⟦vs₂⟧ρ k,l₂∈vs₂ k,v∈ρ)) + ⟦⟧ᵛ-foldr : ∀ {vs : VariableValues} {vss : List VariableValues} {ρ : Env} → ⟦ vs ⟧ᵛ ρ → vs ∈ˡ vss → ⟦ foldr _⊔ᵛ_ ⊥ᵛ vss ⟧ᵛ ρ - ⟦⟧ᵛ-foldr = {!!} + ⟦⟧ᵛ-foldr {vs} {vs ∷ vss'} {ρ = ρ} ⟦vs⟧ρ (Any.here refl) = + ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ (inj₁ ⟦vs⟧ρ) + ⟦⟧ᵛ-foldr {vs} {vs' ∷ vss'} {ρ = ρ} ⟦vs⟧ρ (Any.there vs∈vss') = + ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs'} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ + (inj₂ (⟦⟧ᵛ-foldr ⟦vs⟧ρ vs∈vss')) InterpretationValid : Set InterpretationValid = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v diff --git a/Lattice/FiniteValueMap.agda b/Lattice/FiniteValueMap.agda index 47c6104..1c60ac9 100644 --- a/Lattice/FiniteValueMap.agda +++ b/Lattice/FiniteValueMap.agda @@ -153,6 +153,26 @@ module IterProdIsomorphism where fm'₂⊆fm'₁ k' v' k',v'∈fm'₂ in (v'' , (v'≈v'' , there k',v''∈fm'₁)) + FromBothMaps : ∀ (k : A) (v : B) {ks : List A} (fm₁ fm₂ : FiniteMap ks) → Set + FromBothMaps k v fm₁ fm₂ = + Σ (B × B) + (λ (v₁ , v₂) → ( (v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂))) + + Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B} → + (k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) → FromBothMaps k v fm₁ fm₂ + Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂ + with Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) k,v∈fm₁fm₂ + ... | in₁ (single k,v∈m₁) k∉km₂ + with k∈km₁ ← (forget k,v∈m₁) + rewrite trans ks₁≡ks (sym ks₂≡ks) = + ⊥-elim (k∉km₂ k∈km₁) + ... | in₂ k∉km₁ (single k,v∈m₂) + with k∈km₂ ← (forget k,v∈m₂) + rewrite trans ks₁≡ks (sym ks₂≡ks) = + ⊥-elim (k∉km₁ k∈km₂) + ... | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) = + ((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂))) + private first-key-in-map : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → Σ B (λ v → (k , v) ∈ᵐ fm) @@ -204,26 +224,6 @@ module IterProdIsomorphism where k,v∈⇒k,v∈pop (m@(_ ∷ _ , push k≢ks _) , refl) k≢k' (here refl) = ⊥-elim (k≢k' refl) k,v∈⇒k,v∈pop (m@(_ ∷ _ , push k≢ks _) , refl) k≢k' (there k,v'∈fm') = k,v'∈fm' - FromBothMaps : ∀ (k : A) (v : B) {ks : List A} (fm₁ fm₂ : FiniteMap ks) → Set - FromBothMaps k v fm₁ fm₂ = - Σ (B × B) - (λ (v₁ , v₂) → ( (v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂))) - - Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B} → - (k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) → FromBothMaps k v fm₁ fm₂ - Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂ - with Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) k,v∈fm₁fm₂ - ... | in₁ (single k,v∈m₁) k∉km₂ - with k∈km₁ ← (forget k,v∈m₁) - rewrite trans ks₁≡ks (sym ks₂≡ks) = - ⊥-elim (k∉km₂ k∈km₁) - ... | in₂ k∉km₁ (single k,v∈m₂) - with k∈km₂ ← (forget k,v∈m₂) - rewrite trans ks₁≡ks (sym ks₂≡ks) = - ⊥-elim (k∉km₁ k∈km₂) - ... | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) = - ((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂))) - pop-⊔-distr : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) → pop (fm₁ ⊔ᵐ fm₂) ≈ᵐ (pop fm₁ ⊔ᵐ pop fm₂) pop-⊔-distr {k} {ks} fm₁@(m₁ , _) fm₂@(m₂ , _) =