Prove that foldr is monotonic when input lists are pairwise monotonic

This should help prove that "join" is monotonic

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

Lattice.agda

@@ -85,6 +85,20 @@ record IsSemilattice {a} (A : Set a)
     ≼-refl : ∀ (a : A) → a ≼ a
     ≼-refl a = ⊔-idemp a
 
+    ≼-trans : ∀ {a₁ a₂ a₃ : A} → a₁ ≼ a₂ → a₂ ≼ a₃ → a₁ ≼ a₃
+    ≼-trans {a₁} {a₂} {a₃} a₁≼a₂ a₂≼a₃ =
+        begin
+            a₁ ⊔ a₃
+        ∼⟨ ≈-⊔-cong ≈-refl (≈-sym a₂≼a₃) ⟩
+            a₁ ⊔ (a₂ ⊔ a₃)
+        ∼⟨ ≈-sym (⊔-assoc _ _ _) ⟩
+            (a₁ ⊔ a₂) ⊔ a₃
+        ∼⟨ ≈-⊔-cong a₁≼a₂ ≈-refl ⟩
+            a₂ ⊔ a₃
+        ∼⟨ a₂≼a₃ ⟩
+            a₃
+        ∎
+
     ≼-cong : ∀ {a₁ a₂ a₃ a₄ : A} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≼ a₃ → a₂ ≼ a₄
     ≼-cong {a₁} {a₂} {a₃} {a₄} a₁≈a₂ a₃≈a₄ a₁⊔a₃≈a₃ =
         begin
@@ -118,11 +132,24 @@ module _ {a b} {A : Set a} {B : Set b}
          (lA : IsSemilattice A _≈₁_ _⊔₁_) (lB : IsSemilattice B _≈₂_ _⊔₂_) where
 
     open IsSemilattice lA using () renaming (_≼_ to _≼₁_)
-    open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp)
+    open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp; ≼-trans to ≼₂-trans)
 
     const-Mono : ∀ (x : B) → Monotonic _≼₁_ _≼₂_ (λ _ → x)
     const-Mono x _ = ⊔₂-idemp x
 
+    open import Data.List as List using (List; foldr; _∷_)
+    open import Utils using (Pairwise; _∷_)
+
+    foldr-Mono : ∀ (l₁ l₂ : List A) (f : A → B → B) (b₁ b₂ : B) →
+                 Pairwise _≼₁_ l₁ l₂ → b₁ ≼₂ b₂ →
+                 (∀ b → Monotonic _≼₁_ _≼₂_ (λ a → f a b)) →
+                 (∀ a → Monotonic _≼₂_ _≼₂_ (f a)) →
+                 foldr f b₁ l₁ ≼₂ foldr f b₂ l₂
+    foldr-Mono List.[] List.[] f b₁ b₂ _ b₁≼b₂ _ _ = b₁≼b₂
+    foldr-Mono (x ∷ xs) (y ∷ ys) f b₁ b₂ (x≼y ∷ xs≼ys) b₁≼b₂ f-Mono₁ f-Mono₂ =
+        ≼₂-trans (f-Mono₁ (foldr f b₁ xs) x≼y)
+                 (f-Mono₂ y (foldr-Mono xs ys f b₁ b₂ xs≼ys b₁≼b₂ f-Mono₁ f-Mono₂))
+
 record IsLattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
     (_⊔_ : A → A → A)
@@ -146,6 +173,7 @@ record IsLattice {a} (A : Set a)
         ; _≼_ to _≽_
         ; _≺_ to _≻_
         ; ≼-refl to ≽-refl
+        ; ≼-trans to ≽-trans
         )
 
     FixedHeight : ∀ (h : ℕ) → Set a

Utils.agda

@@ -1,5 +1,6 @@
 module Utils where
 
+open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_)
 open import Data.Nat using (ℕ; suc)
 open import Data.List using (List; []; _∷_; _++_)
 open import Data.List.Membership.Propositional using (_∈_)
@@ -43,3 +44,9 @@ All-x∈xs (x ∷ xs') = here refl ∷ map there (All-x∈xs xs')
 iterate : ∀ {a} {A : Set a} (n : ℕ) → (f : A → A) → A → A
 iterate 0 _ a = a
 iterate (suc n) f a = f (iterate n f a)
+
+data Pairwise {a} {b} {c} {A : Set a} {B : Set b} (P : A → B → Set c) : List A → List B → Set (a ⊔ℓ b ⊔ℓ c)  where
+    [] : Pairwise P [] []
+    _∷_ : ∀ {x : A} {y : B} {xs : List A} {ys : List B} →
+          P x y → Pairwise P xs ys →
+          Pairwise P (x ∷ xs) (y ∷ ys)