Prove that constant functions are monotonic

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

Isomorphism.agda

@@ -1,7 +1,7 @@
 module Isomorphism where
 
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
-open import Function.Definitions using (Inverseˡ; Inverseʳ; Injective)
+open import Function.Definitions using (Injective)
 open import Lattice
 open import Equivalence
 open import Relation.Binary.Core using (_Preserves_⟶_ )
@@ -9,6 +9,16 @@ open import Data.Nat using (ℕ)
 open import Data.Product using (_,_)
 open import Relation.Nullary using (¬_)
 
+IsInverseˡ : ∀ {a b} {A : Set a} {B : Set b}
+               (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b)
+               (f : A → B) (g : B → A) → Set b
+IsInverseˡ {A = A} {B = B} _≈₁_ _≈₂_ f g = ∀ (x : B) → f (g x) ≈₂ x
+
+IsInverseʳ : ∀ {a b} {A : Set a} {B : Set b}
+               (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b)
+               (f : A → B) (g : B → A) → Set a
+IsInverseʳ {A = A} {B = B} _≈₁_ _≈₂_ f g = ∀ (x : A) → g (f x) ≈₁ x
+
 module TransportFiniteHeight
          {a b : Level} {A : Set a} {B : Set b}
          {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b}
@@ -20,7 +30,7 @@ module TransportFiniteHeight
          (f-preserves-≈₁ : f Preserves _≈₁_ ⟶  _≈₂_) (g-preserves-≈₂ : g Preserves _≈₂_ ⟶  _≈₁_)
          (f-⊔-distr : ∀ (a₁ a₂ : A) → f (a₁ ⊔₁ a₂) ≈₂ ((f a₁) ⊔₂ (f a₂)))
          (g-⊔-distr : ∀ (b₁ b₂ : B) → g (b₁ ⊔₂ b₂) ≈₁ ((g b₁) ⊔₁ (g b₂)))
-         (inverseˡ : Inverseˡ _≈₁_ _≈₂_ f g) (inverseʳ : Inverseʳ _≈₁_ _≈₂_ f g) where
+         (inverseˡ : IsInverseˡ _≈₁_ _≈₂_ f g) (inverseʳ : IsInverseʳ _≈₁_ _≈₂_ f g) where
 
     open IsFiniteHeightLattice fhlA using () renaming (_≺_ to _≺₁_; ≺-cong to ≺₁-cong; ≈-equiv to ≈₁-equiv)
     open IsLattice lB               using () renaming (_≺_ to _≺₂_; ≺-cong to ≺₂-cong; ≈-equiv to ≈₂-equiv)

Lattice.agda

@@ -62,6 +62,26 @@ record IsSemilattice {a} (A : Set a)
                     (a ⊔ a₁) ⊔ (a ⊔ a₂)
                 ∎
 
+    ⊔-Monotonicʳ : ∀ (a₂ : A) → Monotonic _≼_ _≼_ (λ a₁ → a₁ ⊔ a₂)
+    ⊔-Monotonicʳ a {a₁} {a₂} a₁≼a₂ = ≈-trans (≈-sym lhs) (≈-⊔-cong a₁≼a₂ (≈-refl {a}))
+        where
+            lhs =
+                begin
+                    (a₁ ⊔ a₂) ⊔ a
+                ∼⟨ ≈-⊔-cong ≈-refl (≈-sym (⊔-idemp _)) ⟩
+                    (a₁ ⊔ a₂) ⊔ (a ⊔ a)
+                ∼⟨ ≈-sym (⊔-assoc _ _ _) ⟩
+                    ((a₁ ⊔ a₂) ⊔ a) ⊔ a
+                ∼⟨ ≈-⊔-cong (⊔-assoc _ _ _) ≈-refl ⟩
+                    (a₁ ⊔ (a₂ ⊔ a)) ⊔ a
+                ∼⟨ ≈-⊔-cong (≈-⊔-cong ≈-refl (⊔-comm _ _)) ≈-refl ⟩
+                    (a₁ ⊔ (a ⊔ a₂)) ⊔ a
+                ∼⟨ ≈-⊔-cong (≈-sym (⊔-assoc _ _ _)) ≈-refl ⟩
+                    ((a₁ ⊔ a) ⊔ a₂) ⊔ a
+                ∼⟨ ⊔-assoc _ _ _ ⟩
+                    (a₁ ⊔ a) ⊔ (a₂ ⊔ a)
+                ∎
+
     ≼-refl : ∀ (a : A) → a ≼ a
     ≼-refl a = ⊔-idemp a
 
@@ -83,6 +103,17 @@ record IsSemilattice {a} (A : Set a)
         , λ a₂≈a₄ → a₁̷≈a₃ (≈-trans a₁≈a₂ (≈-trans a₂≈a₄ (≈-sym a₃≈a₄)))
         )
 
+module _ {a b} {A : Set a} {B : Set b}
+         {_≈₁_ : A → A → Set a} {_⊔₁_ : A → A → A}
+         {_≈₂_ : B → B → Set b} {_⊔₂_ : B → B → B}
+         (lA : IsSemilattice A _≈₁_ _⊔₁_) (lB : IsSemilattice B _≈₂_ _⊔₂_) where
+
+    open IsSemilattice lA using () renaming (_≼_ to _≼₁_)
+    open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp)
+
+    const-Mono : ∀ (x : B) → Monotonic _≼₁_ _≼₂_ (λ _ → x)
+    const-Mono x _ = ⊔₂-idemp x
+
 record IsLattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
     (_⊔_ : A → A → A)
@@ -100,6 +131,8 @@ record IsLattice {a} (A : Set a)
         ( ⊔-assoc to ⊓-assoc
         ; ⊔-comm to ⊓-comm
         ; ⊔-idemp to ⊓-idemp
+        ; ⊔-Monotonicˡ to ⊓-Monotonicˡ
+        ; ⊔-Monotonicʳ to ⊓-Monotonicʳ
         ; ≈-⊔-cong to ≈-⊓-cong
         ; _≼_ to _≽_
         ; _≺_ to _≻_

Lattice/FiniteValueMap.agda

@@ -27,6 +27,7 @@ open import Data.List.Properties using (∷-injectiveʳ)
 open import Data.List.Relation.Unary.All using (All)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Relation.Nullary using (¬_)
+open import Isomorphism using (IsInverseˡ; IsInverseʳ)
 
 open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB
     using
@@ -105,8 +106,8 @@ module IterProdIsomorphism where
 
     -- The left inverse is: from (to x) = x
     from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) →
-                      Inverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks})
+                      IsInverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks})
-                               (from {ks}) (to {ks} uks)
+                                 (from {ks}) (to {ks} uks)
     from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv 0)
     from-to-inverseˡ {k ∷ ks'} (push k≢ks' uks') (v , rest)
         with ((fm' , ufm') , refl) ← to uks' rest in p rewrite sym p =
@@ -121,8 +122,8 @@ module IterProdIsomorphism where
     --
     -- The right inverse is: to (from x) = x
     from-to-inverseʳ : ∀ {ks : List A} (uks : Unique ks) →
-                       Inverseʳ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks})
+                       IsInverseʳ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks})
-                                (from {ks}) (to {ks} uks)
+                                  (from {ks}) (to {ks} uks)
     from-to-inverseʳ {[]} _ (([] , empty) , kvs≡ks) rewrite kvs≡ks =
         ( (λ k v ())
         , (λ k v ())

Lattice/Prod.agda

@@ -168,7 +168,7 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
                                  ))
         ...   | no a₁̷≈a  | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
                 ((suc n₁ , suc n₂) , ( (step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
-                                     , ≤-stepsˡ 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂))
+                                     , m≤n⇒m≤o+n 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂))
                                      ))
 
     fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)