Prove the foldr-implies lemma

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

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

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₂ , _) =