diff --git a/CHANGELOG.md b/CHANGELOG.md index a6f66aa2f5..f547fc9790 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -152,6 +152,21 @@ New modules Additions to existing modules ----------------------------- +* In `Algebra.Consequences.Base`: + ```agda + module Congruence (_≈_ : Rel A ℓ) (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_) + where + ∙-congˡ : LeftCongruent _≈_ _∙_ + ∙-congʳ : RightCongruent _≈_ _∙_ + ``` + +* In `Algebra.Consequences.Setoid`: + ```agda + module Congruence (cong : Congruent₂ _≈_ _∙_) where + ∙-congˡ : LeftCongruent _≈_ _∙_ + ∙-congʳ : RightCongruent _≈_ _∙_ + ``` + * In `Algebra.Construct.Pointwise`: ```agda isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0# → @@ -232,6 +247,15 @@ Additions to existing modules filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys ``` +* In `Relation.Binary.Consequences`: + ```agda + mono₂⇒monoˡ : Reflexive ≤₁ → Monotonic₂ ≤₁ ≤₂ ≤₃ f → LeftMonotonic ≤₂ ≤₃ f + mono₂⇒monoˡ : Reflexive ≤₂ → Monotonic₂ ≤₁ ≤₂ ≤₃ f → RightMonotonic ≤₁ ≤₃ f + monoˡ∧monoʳ⇒mono₂ : Transitive ≤₃ → + LeftMonotonic ≤₂ ≤₃ f → RightMonotonic ≤₁ ≤₃ f → + Monotonic₂ ≤₁ ≤₂ ≤₃ f + ``` + * In `Relation.Binary.Construct.Add.Infimum.Strict`: ```agda <₋-accessible-⊥₋ : Acc _<₋_ ⊥₋ @@ -239,6 +263,12 @@ Additions to existing modules <₋-wellFounded : WellFounded _<_ → WellFounded _<₋_ ``` +* In `Relation.Binary.Definitions`: + ```agda + LeftMonotonic : Rel B ℓ₁ → Rel C ℓ₂ → (A → B → C) → Set _ + RightMonotonic : Rel A ℓ₁ → Rel C ℓ₂ → (A → B → C) → Set _ + ``` + * In `Relation.Nullary.Decidable.Core`: ```agda ⊤-dec : Dec {a} ⊤ diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda index 102fac3978..5df61df8ee 100644 --- a/src/Algebra/Consequences/Base.agda +++ b/src/Algebra/Consequences/Base.agda @@ -11,22 +11,35 @@ module Algebra.Consequences.Base {a} {A : Set a} where open import Algebra.Core using (Op₁; Op₂) -open import Algebra.Definitions - using (Selective; Idempotent; SelfInverse; Involutive) +import Algebra.Definitions as Definitions + using (Congruent₂; LeftCongruent; RightCongruent + ; Selective; Idempotent; SelfInverse; Involutive) open import Data.Sum.Base using (_⊎_; reduce) +open import Relation.Binary.Consequences + using (mono₂⇒monoˡ; mono₂⇒monoʳ) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Definitions using (Reflexive) -module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where +module Congruence {ℓ} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) (open Definitions _≈_) + (cong : Congruent₂ _∙_) (refl : Reflexive _≈_) + where - sel⇒idem : Selective _≈_ _•_ → Idempotent _≈_ _•_ + ∙-congˡ : LeftCongruent _∙_ + ∙-congˡ {x} = mono₂⇒monoˡ _ _≈_ _≈_ (refl {x = x}) cong x + + ∙-congʳ : RightCongruent _∙_ + ∙-congʳ {x} = mono₂⇒monoʳ _≈_ _ _≈_ (refl {x = x}) cong x + +module _ {ℓ} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) (open Definitions _≈_) where + + sel⇒idem : Selective _∙_ → Idempotent _∙_ sel⇒idem sel x = reduce (sel x x) -module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where +module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) (open Definitions _≈_) where reflexive∧selfInverse⇒involutive : Reflexive _≈_ → - SelfInverse _≈_ f → - Involutive _≈_ f + SelfInverse f → + Involutive f reflexive∧selfInverse⇒involutive refl inv _ = inv refl ------------------------------------------------------------------------ diff --git a/src/Algebra/Consequences/Propositional.agda b/src/Algebra/Consequences/Propositional.agda index cce01a56e3..42892f4aa9 100644 --- a/src/Algebra/Consequences/Propositional.agda +++ b/src/Algebra/Consequences/Propositional.agda @@ -10,6 +10,7 @@ module Algebra.Consequences.Propositional {a} {A : Set a} where +open import Algebra.Core using (Op₁; Op₂) open import Data.Sum.Base using (inj₁; inj₂) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Bundles using (Setoid) @@ -19,7 +20,6 @@ open import Relation.Binary.PropositionalEquality.Core open import Relation.Binary.PropositionalEquality.Properties using (setoid) open import Relation.Unary using (Pred) -open import Algebra.Core using (Op₁; Op₂) open import Algebra.Definitions {A = A} _≡_ import Algebra.Consequences.Setoid (setoid A) as Base diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda index a6c7d252a7..244470231c 100644 --- a/src/Algebra/Consequences/Setoid.agda +++ b/src/Algebra/Consequences/Setoid.agda @@ -13,47 +13,58 @@ open import Relation.Binary.Definitions module Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where -open Setoid S renaming (Carrier to A) +import Algebra.Consequences.Base as Base open import Algebra.Core -open import Algebra.Definitions _≈_ open import Data.Sum.Base using (inj₁; inj₂) open import Data.Product.Base using (_,_) open import Function.Base using (_$_; id; _∘_) open import Function.Definitions import Relation.Binary.Consequences as Bin open import Relation.Binary.Core using (Rel) -open import Relation.Binary.Reasoning.Setoid S open import Relation.Unary using (Pred) +open Setoid S renaming (Carrier to A) +open import Algebra.Definitions _≈_ +open import Relation.Binary.Reasoning.Setoid S + ------------------------------------------------------------------------ -- Re-exports -- Export base lemmas that don't require the setoid -open import Algebra.Consequences.Base public +open Base public + hiding (module Congruence) + +-- Export congruence lemmas using reflexivity + +module Congruence {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where + + open Base.Congruence _≈_ cong refl public ------------------------------------------------------------------------ -- MiddleFourExchange module _ {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where + open Congruence cong + comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ → _∙_ MiddleFourExchange _∙_ comm∧assoc⇒middleFour comm assoc w x y z = begin (w ∙ x) ∙ (y ∙ z) ≈⟨ assoc w x (y ∙ z) ⟩ - w ∙ (x ∙ (y ∙ z)) ≈⟨ cong refl (sym (assoc x y z)) ⟩ - w ∙ ((x ∙ y) ∙ z) ≈⟨ cong refl (cong (comm x y) refl) ⟩ - w ∙ ((y ∙ x) ∙ z) ≈⟨ cong refl (assoc y x z) ⟩ - w ∙ (y ∙ (x ∙ z)) ≈⟨ sym (assoc w y (x ∙ z)) ⟩ + w ∙ (x ∙ (y ∙ z)) ≈⟨ ∙-congˡ (assoc x y z) ⟨ + w ∙ ((x ∙ y) ∙ z) ≈⟨ ∙-congˡ (∙-congʳ (comm x y)) ⟩ + w ∙ ((y ∙ x) ∙ z) ≈⟨ ∙-congˡ (assoc y x z) ⟩ + w ∙ (y ∙ (x ∙ z)) ≈⟨ assoc w y (x ∙ z) ⟨ (w ∙ y) ∙ (x ∙ z) ∎ identity∧middleFour⇒assoc : {e : A} → Identity e _∙_ → _∙_ MiddleFourExchange _∙_ → Associative _∙_ identity∧middleFour⇒assoc {e} (identityˡ , identityʳ) middleFour x y z = begin - (x ∙ y) ∙ z ≈⟨ cong refl (sym (identityˡ z)) ⟩ + (x ∙ y) ∙ z ≈⟨ ∙-congˡ (identityˡ z) ⟨ (x ∙ y) ∙ (e ∙ z) ≈⟨ middleFour x y e z ⟩ - (x ∙ e) ∙ (y ∙ z) ≈⟨ cong (identityʳ x) refl ⟩ + (x ∙ e) ∙ (y ∙ z) ≈⟨ ∙-congʳ (identityʳ x) ⟩ x ∙ (y ∙ z) ∎ identity∧middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ → @@ -61,7 +72,7 @@ module _ {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where Commutative _∙_ identity∧middleFour⇒comm {_+_} {e} (identityˡ , identityʳ) middleFour x y = begin - x ∙ y ≈⟨ sym (cong (identityˡ x) (identityʳ y)) ⟩ + x ∙ y ≈⟨ cong (identityˡ x) (identityʳ y) ⟨ (e + x) ∙ (y + e) ≈⟨ middleFour e x y e ⟩ (e + y) ∙ (x + e) ≈⟨ cong (identityˡ y) (identityʳ x) ⟩ y ∙ x ∎ @@ -198,14 +209,16 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _∙_) whe module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) where + open Congruence cong + assoc∧id∧invʳ⇒invˡ-unique : Associative _∙_ → Identity e _∙_ → RightInverse e _⁻¹ _∙_ → ∀ x y → (x ∙ y) ≈ e → x ≈ (y ⁻¹) assoc∧id∧invʳ⇒invˡ-unique assoc (idˡ , idʳ) invʳ x y eq = begin - x ≈⟨ sym (idʳ x) ⟩ - x ∙ e ≈⟨ cong refl (sym (invʳ y)) ⟩ - x ∙ (y ∙ (y ⁻¹)) ≈⟨ sym (assoc x y (y ⁻¹)) ⟩ - (x ∙ y) ∙ (y ⁻¹) ≈⟨ cong eq refl ⟩ + x ≈⟨ idʳ x ⟨ + x ∙ e ≈⟨ ∙-congˡ (invʳ y) ⟨ + x ∙ (y ∙ (y ⁻¹)) ≈⟨ assoc x y (y ⁻¹) ⟨ + (x ∙ y) ∙ (y ⁻¹) ≈⟨ ∙-congʳ eq ⟩ e ∙ (y ⁻¹) ≈⟨ idˡ (y ⁻¹) ⟩ y ⁻¹ ∎ @@ -213,10 +226,10 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) wh Identity e _∙_ → LeftInverse e _⁻¹ _∙_ → ∀ x y → (x ∙ y) ≈ e → y ≈ (x ⁻¹) assoc∧id∧invˡ⇒invʳ-unique assoc (idˡ , idʳ) invˡ x y eq = begin - y ≈⟨ sym (idˡ y) ⟩ - e ∙ y ≈⟨ cong (sym (invˡ x)) refl ⟩ + y ≈⟨ idˡ y ⟨ + e ∙ y ≈⟨ ∙-congʳ (invˡ x) ⟨ ((x ⁻¹) ∙ x) ∙ y ≈⟨ assoc (x ⁻¹) x y ⟩ - (x ⁻¹) ∙ (x ∙ y) ≈⟨ cong refl eq ⟩ + (x ⁻¹) ∙ (x ∙ y) ≈⟨ ∙-congˡ eq ⟩ (x ⁻¹) ∙ e ≈⟨ idʳ (x ⁻¹) ⟩ x ⁻¹ ∎ @@ -228,6 +241,8 @@ module _ {_∙_ _◦_ : Op₂ A} (∙-comm : Commutative _∙_) where + open Congruence ◦-cong renaming (∙-congˡ to ◦-congˡ) + comm∧distrˡ⇒distrʳ : _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_ comm∧distrˡ⇒distrʳ distrˡ x y z = begin (y ◦ z) ∙ x ≈⟨ ∙-comm (y ◦ z) x ⟩ @@ -250,7 +265,7 @@ module _ {_∙_ _◦_ : Op₂ A} comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y ∙ z)) ≈ ((x ◦ y) ∙ (x ◦ z))) comm⇒sym[distribˡ] x {y} {z} prf = begin - x ◦ (z ∙ y) ≈⟨ ◦-cong refl (∙-comm z y) ⟩ + x ◦ (z ∙ y) ≈⟨ ◦-congˡ (∙-comm z y) ⟩ x ◦ (y ∙ z) ≈⟨ prf ⟩ (x ◦ y) ∙ (x ◦ z) ≈⟨ ∙-comm (x ◦ y) (x ◦ z) ⟩ (x ◦ z) ∙ (x ◦ y) ∎ @@ -262,16 +277,18 @@ module _ {_∙_ _◦_ : Op₂ A} (◦-comm : Commutative _◦_) where + open Congruence ∙-cong + distrib∧absorbs⇒distribˡ : _∙_ Absorbs _◦_ → _◦_ Absorbs _∙_ → _◦_ DistributesOver _∙_ → _∙_ DistributesOverˡ _◦_ distrib∧absorbs⇒distribˡ ∙-absorbs-◦ ◦-absorbs-∙ (◦-distribˡ-∙ , ◦-distribʳ-∙) x y z = begin - x ∙ (y ◦ z) ≈⟨ ∙-cong (∙-absorbs-◦ _ _) refl ⟨ - (x ∙ (x ◦ y)) ∙ (y ◦ z) ≈⟨ ∙-cong (∙-cong refl (◦-comm _ _)) refl ⟩ + x ∙ (y ◦ z) ≈⟨ ∙-congʳ (∙-absorbs-◦ _ _) ⟨ + (x ∙ (x ◦ y)) ∙ (y ◦ z) ≈⟨ ∙-congʳ (∙-congˡ (◦-comm _ _)) ⟩ (x ∙ (y ◦ x)) ∙ (y ◦ z) ≈⟨ ∙-assoc _ _ _ ⟩ - x ∙ ((y ◦ x) ∙ (y ◦ z)) ≈⟨ ∙-cong refl (◦-distribˡ-∙ _ _ _) ⟨ - x ∙ (y ◦ (x ∙ z)) ≈⟨ ∙-cong (◦-absorbs-∙ _ _) refl ⟨ + x ∙ ((y ◦ x) ∙ (y ◦ z)) ≈⟨ ∙-congˡ (◦-distribˡ-∙ _ _ _) ⟨ + x ∙ (y ◦ (x ∙ z)) ≈⟨ ∙-congʳ (◦-absorbs-∙ _ _) ⟨ (x ◦ (x ∙ z)) ∙ (y ◦ (x ∙ z)) ≈⟨ ◦-distribʳ-∙ _ _ _ ⟨ (x ∙ y) ◦ (x ∙ z) ∎ @@ -284,15 +301,19 @@ module _ {_+_ _*_ : Op₂ A} (*-cong : Congruent₂ _*_) where + open Congruence +-cong renaming (∙-congˡ to +-congˡ; ∙-congʳ to +-congʳ) + + open Congruence *-cong renaming (∙-congˡ to *-congˡ; ∙-congʳ to *-congʳ) + assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ → RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ → LeftZero 0# _*_ assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ +-assoc distribʳ idʳ invʳ x = begin - 0# * x ≈⟨ sym (idʳ _) ⟩ - (0# * x) + 0# ≈⟨ +-cong refl (sym (invʳ _)) ⟩ - (0# * x) + ((0# * x) + ((0# * x)⁻¹)) ≈⟨ sym (+-assoc _ _ _) ⟩ - ((0# * x) + (0# * x)) + ((0# * x)⁻¹) ≈⟨ +-cong (sym (distribʳ _ _ _)) refl ⟩ - ((0# + 0#) * x) + ((0# * x)⁻¹) ≈⟨ +-cong (*-cong (idʳ _) refl) refl ⟩ + 0# * x ≈⟨ idʳ _ ⟨ + (0# * x) + 0# ≈⟨ +-congˡ (invʳ _) ⟨ + (0# * x) + ((0# * x) + ((0# * x)⁻¹)) ≈⟨ +-assoc _ _ _ ⟨ + ((0# * x) + (0# * x)) + ((0# * x)⁻¹) ≈⟨ +-congʳ (distribʳ _ _ _) ⟨ + ((0# + 0#) * x) + ((0# * x)⁻¹) ≈⟨ +-congʳ (*-congʳ (idʳ _)) ⟩ (0# * x) + ((0# * x)⁻¹) ≈⟨ invʳ _ ⟩ 0# ∎ @@ -300,11 +321,11 @@ module _ {_+_ _*_ : Op₂ A} RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ → RightZero 0# _*_ assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ +-assoc distribˡ idʳ invʳ x = begin - x * 0# ≈⟨ sym (idʳ _) ⟩ - (x * 0#) + 0# ≈⟨ +-cong refl (sym (invʳ _)) ⟩ - (x * 0#) + ((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ sym (+-assoc _ _ _) ⟩ - ((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹) ≈⟨ +-cong (sym (distribˡ _ _ _)) refl ⟩ - (x * (0# + 0#)) + ((x * 0#)⁻¹) ≈⟨ +-cong (*-cong refl (idʳ _)) refl ⟩ + x * 0# ≈⟨ idʳ _ ⟨ + (x * 0#) + 0# ≈⟨ +-congˡ (invʳ _) ⟨ + (x * 0#) + ((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ +-assoc _ _ _ ⟨ + ((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹) ≈⟨ +-congʳ (distribˡ _ _ _) ⟨ + (x * (0# + 0#)) + ((x * 0#)⁻¹) ≈⟨ +-congʳ (*-congˡ (idʳ _)) ⟩ ((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ invʳ _ ⟩ 0# ∎ diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index 62528e5b70..eb64aa8e76 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -15,8 +15,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_) -open import Relation.Nullary.Negation.Core using (¬_) +open import Relation.Binary.Core using (Rel) module Algebra.Definitions {a ℓ} {A : Set a} -- The underlying set @@ -26,21 +25,24 @@ module Algebra.Definitions open import Algebra.Core using (Op₁; Op₂) open import Data.Product.Base using (_×_; ∃-syntax) open import Data.Sum.Base using (_⊎_) +open import Relation.Binary.Definitions using (Monotonic₁; Monotonic₂) +open import Relation.Nullary.Negation.Core using (¬_) + ------------------------------------------------------------------------ -- Properties of operations Congruent₁ : Op₁ A → Set _ -Congruent₁ f = f Preserves _≈_ ⟶ _≈_ +Congruent₁ = Monotonic₁ _≈_ _≈_ Congruent₂ : Op₂ A → Set _ -Congruent₂ ∙ = ∙ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_ +Congruent₂ = Monotonic₂ _≈_ _≈_ _≈_ LeftCongruent : Op₂ A → Set _ -LeftCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_ +LeftCongruent _∙_ = ∀ {x} → Congruent₁ (x ∙_) RightCongruent : Op₂ A → Set _ -RightCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_ +RightCongruent _∙_ = ∀ {x} → Congruent₁ (_∙ x) Associative : Op₂ A → Set _ Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z)) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index b15bad236f..6c24098ede 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -54,13 +54,14 @@ record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where setoid : Setoid a ℓ setoid = record { isEquivalence = isEquivalence } - +{- ∙-congˡ : LeftCongruent ∙ ∙-congˡ y≈z = ∙-cong refl y≈z ∙-congʳ : RightCongruent ∙ ∙-congʳ y≈z = ∙-cong y≈z refl - +-} + open Consequences.Congruence setoid ∙-cong public record IsCommutativeMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where field diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index e1f2d25d24..5a135726f0 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -902,7 +902,7 @@ pinch-surjective _ zero = zero , λ { refl → refl } pinch-surjective zero (suc j) = suc (suc j) , λ { refl → refl } pinch-surjective (suc i) (suc j) = map suc (λ {f refl → cong suc (f refl)}) (pinch-surjective i j) -pinch-mono-≤ : ∀ (i : Fin n) → (pinch i) Preserves _≤_ ⟶ _≤_ +pinch-mono-≤ : ∀ (i : Fin n) → Monotonic₁ _≤_ _≤_ (pinch i) pinch-mono-≤ 0F {0F} {k} 0≤n = z≤n pinch-mono-≤ 0F {suc j} {suc k} j≤k = ℕ.s≤s⁻¹ j≤k pinch-mono-≤ (suc i) {0F} {k} 0≤n = z≤n diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 8db99652a0..544f314983 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -27,6 +27,7 @@ import Data.Sign.Properties as Sign open import Function.Base using (_∘_; _$_; _$′_; id) open import Level using (0ℓ) open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_) +open import Relation.Binary.Definitions using (Monotonic₁; Monotonic₂; LeftMonotonic; RightMonotonic) open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder) open import Relation.Binary.Consequences using (wlog) @@ -415,7 +416,7 @@ neg-≤-pos : ∀ {m n} → - (+ m) ≤ + n neg-≤-pos {zero} = +≤+ z≤n neg-≤-pos {suc m} = -≤+ -neg-mono-≤ : -_ Preserves _≤_ ⟶ _≥_ +neg-mono-≤ : Monotonic₁ _≤_ _≥_ (-_) neg-mono-≤ -≤+ = neg-≤-pos neg-mono-≤ (-≤- n≤m) = +≤+ (s≤s n≤m) neg-mono-≤ (+≤+ z≤n) = neg-≤-pos @@ -430,7 +431,7 @@ neg-cancel-≤ { +0} { -[1+ n ]} _ = -≤+ neg-cancel-≤ { -[1+ m ]} { +0} (+≤+ ()) neg-cancel-≤ { -[1+ m ]} { -[1+ n ]} (+≤+ (s≤s m≤n)) = -≤- m≤n -neg-mono-< : -_ Preserves _<_ ⟶ _>_ +neg-mono-< : Monotonic₁ _<_ _>_ (-_) neg-mono-< { -[1+ _ ]} { -[1+ _ ]} (-<- n -⊖-monoʳ-≥-≤ : ∀ n → (n ⊖_) Preserves ℕ._≥_ ⟶ _≤_ +⊖-monoʳ-≥-≤ : LeftMonotonic ℕ._≥_ _≤_ _⊖_ ⊖-monoʳ-≥-≤ zero {m} z≤n = 0⊖m≤+ m ⊖-monoʳ-≥-≤ zero {_} (s≤s m≤n) = -≤- m≤n ⊖-monoʳ-≥-≤ (suc n) {zero} z≤n = ≤-refl @@ -624,7 +625,7 @@ sign-⊖-≰ = sign-⊖-< ∘ ℕ.≰⇒> n ⊖ o ≡⟨ [1+m]⊖[1+n]≡m⊖n n o ⟨ suc n ⊖ suc o ∎ where open ≤-Reasoning -⊖-monoˡ-≤ : ∀ n → (_⊖ n) Preserves ℕ._≤_ ⟶ _≤_ +⊖-monoˡ-≤ : RightMonotonic ℕ._≤_ _≤_ _⊖_ ⊖-monoˡ-≤ zero {_} {_} m≤o = +≤+ m≤o ⊖-monoˡ-≤ (suc n) {_} {0} z≤n = ≤-refl ⊖-monoˡ-≤ (suc n) {_} {suc o} z≤n = begin @@ -638,7 +639,7 @@ sign-⊖-≰ = sign-⊖-< ∘ ℕ.≰⇒> o ⊖ n ≡⟨ [1+m]⊖[1+n]≡m⊖n o n ⟨ suc o ⊖ suc n ∎ where open ≤-Reasoning -⊖-monoʳ->-< : ∀ p → (p ⊖_) Preserves ℕ._>_ ⟶ _<_ +⊖-monoʳ->-< : LeftMonotonic ℕ._>_ _<_ _⊖_ ⊖-monoʳ->-< zero {_} z-< zero {_} (s-< (suc p) {suc m} z p ⊖ n ≡⟨ [1+m]⊖[1+n]≡m⊖n p n ⟨ suc p ⊖ suc n ∎ where open ≤-Reasoning -⊖-monoˡ-< : ∀ n → (_⊖ n) Preserves ℕ._<_ ⟶ _<_ +⊖-monoˡ-< : RightMonotonic ℕ._<_ _<_ _⊖_ ⊖-monoˡ-< zero m-< n (s_ +*-monoˡ-<-neg : ∀ i .{{_ : Negative i}} → Monotonic₁ _<_ _>_ (i *_) *-monoˡ-<-neg i@(-[1+ _ ]) {j} {k} j_ +*-monoʳ-<-neg : ∀ i .{{_ : Negative i}} → Monotonic₁ _<_ _>_ (_* i) *-monoʳ-<-neg i {j} {k} rewrite *-comm k i | *-comm j i = *-monoˡ-<-neg i *-cancelˡ-<-nonPos : ∀ k .{{_ : NonPositive k}} → k * i < k * j → i > j @@ -1963,41 +1964,41 @@ open ⊓-⊔-latticeProperties public ------------------------------------------------------------------------ -- Other properties of _⊓_ and _⊔_ -mono-≤-distrib-⊔ : ∀ {f} → f Preserves _≤_ ⟶ _≤_ → +mono-≤-distrib-⊔ : ∀ {f} → Monotonic₁ _≤_ _≤_ f → ∀ i j → f (i ⊔ j) ≡ f i ⊔ f j mono-≤-distrib-⊔ {f} = ⊓-⊔-properties.mono-≤-distrib-⊔ (cong f) -mono-≤-distrib-⊓ : ∀ {f} → f Preserves _≤_ ⟶ _≤_ → +mono-≤-distrib-⊓ : ∀ {f} → Monotonic₁ _≤_ _≤_ f → ∀ i j → f (i ⊓ j) ≡ f i ⊓ f j mono-≤-distrib-⊓ {f} = ⊓-⊔-properties.mono-≤-distrib-⊓ (cong f) -antimono-≤-distrib-⊓ : ∀ {f} → f Preserves _≤_ ⟶ _≥_ → +antimono-≤-distrib-⊓ : ∀ {f} → Monotonic₁ _≤_ _≥_ f → ∀ i j → f (i ⊓ j) ≡ f i ⊔ f j antimono-≤-distrib-⊓ {f} = ⊓-⊔-properties.antimono-≤-distrib-⊓ (cong f) -antimono-≤-distrib-⊔ : ∀ {f} → f Preserves _≤_ ⟶ _≥_ → +antimono-≤-distrib-⊔ : ∀ {f} → Monotonic₁ _≤_ _≥_ f → ∀ i j → f (i ⊔ j) ≡ f i ⊓ f j antimono-≤-distrib-⊔ {f} = ⊓-⊔-properties.antimono-≤-distrib-⊔ (cong f) -mono-<-distrib-⊓ : ∀ f → f Preserves _<_ ⟶ _<_ → ∀ i j → f (i ⊓ j) ≡ f i ⊓ f j +mono-<-distrib-⊓ : ∀ f → Monotonic₁ _<_ _<_ f → ∀ i j → f (i ⊓ j) ≡ f i ⊓ f j mono-<-distrib-⊓ f f-mono-< i j with <-cmp i j ... | tri< i _ _ i>j = trans (cong f (i≥j⇒i⊓j≡j (<⇒≤ i>j))) (sym (i≥j⇒i⊓j≡j (<⇒≤ (f-mono-< i>j)))) -mono-<-distrib-⊔ : ∀ f → f Preserves _<_ ⟶ _<_ → ∀ i j → f (i ⊔ j) ≡ f i ⊔ f j +mono-<-distrib-⊔ : ∀ f → Monotonic₁ _<_ _<_ f → ∀ i j → f (i ⊔ j) ≡ f i ⊔ f j mono-<-distrib-⊔ f f-mono-< i j with <-cmp i j ... | tri< i _ _ i>j = trans (cong f (i≥j⇒i⊔j≡i (<⇒≤ i>j))) (sym (i≥j⇒i⊔j≡i (<⇒≤ (f-mono-< i>j)))) -antimono-<-distrib-⊔ : ∀ f → f Preserves _<_ ⟶ _>_ → ∀ i j → f (i ⊔ j) ≡ f i ⊓ f j +antimono-<-distrib-⊔ : ∀ f → Monotonic₁ _<_ _>_ f → ∀ i j → f (i ⊔ j) ≡ f i ⊓ f j antimono-<-distrib-⊔ f f-mono-< i j with <-cmp i j ... | tri< i _ _ i>j = trans (cong f (i≥j⇒i⊔j≡i (<⇒≤ i>j))) (sym (i≤j⇒i⊓j≡i (<⇒≤ (f-mono-< i>j)))) -antimono-<-distrib-⊓ : ∀ f → f Preserves _<_ ⟶ _>_ → ∀ i j → f (i ⊓ j) ≡ f i ⊔ f j +antimono-<-distrib-⊓ : ∀ f → Monotonic₁ _<_ _>_ f → ∀ i j → f (i ⊓ j) ≡ f i ⊔ f j antimono-<-distrib-⊓ f f-mono-< i j with <-cmp i j ... | tri< i1⇒m*n>1 m n rewrite *-comm m n = m≢0∧n>1⇒m*n>1 n m *-cancelˡ-≤ : ∀ o .{{_ : NonZero o}} → o * m ≤ o * n → m ≤ n *-cancelˡ-≤ {m} {n} o rewrite *-comm o m | *-comm o n = *-cancelʳ-≤ m n o -*-mono-≤ : _*_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_ -*-mono-≤ z≤n _ = z≤n +*-mono-≤ : Monotonic₂ _≤_ _≤_ _≤_ _*_ +*-mono-≤ z≤n u≤v = z≤n *-mono-≤ (s≤s m≤n) u≤v = +-mono-≤ u≤v (*-mono-≤ m≤n u≤v) -*-monoˡ-≤ : ∀ n → (_* n) Preserves _≤_ ⟶ _≤_ -*-monoˡ-≤ n m≤o = *-mono-≤ m≤o (≤-refl {n}) +*-monoˡ-≤ : RightMonotonic _≤_ _≤_ _*_ +*-monoˡ-≤ = mono₂⇒monoʳ _ _ _≤_ ≤-refl *-mono-≤ -*-monoʳ-≤ : ∀ n → (n *_) Preserves _≤_ ⟶ _≤_ -*-monoʳ-≤ n m≤o = *-mono-≤ (≤-refl {n}) m≤o +*-monoʳ-≤ : LeftMonotonic _≤_ _≤_ _*_ +*-monoʳ-≤ = mono₂⇒monoˡ _≤_ _≤_ _≤_ ≤-refl *-mono-≤ -*-mono-< : _*_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_ +*-mono-< : Monotonic₂ _<_ _<_ _<_ _*_ *-mono-< z0 : ∀ m .{{_ : NonZero m}} n → m ^ n > 0 m^n>0 m n = >-nonZero⁻¹ (m ^ n) {{m^n≢0 m n}} -^-monoˡ-≤ : ∀ n → (_^ n) Preserves _≤_ ⟶ _≤_ +^-monoˡ-≤ : RightMonotonic _≤_ _≤_ _^_ ^-monoˡ-≤ zero m≤o = s≤s z≤n ^-monoˡ-≤ (suc n) m≤o = *-mono-≤ m≤o (^-monoˡ-≤ n m≤o) -^-monoʳ-≤ : ∀ m .{{_ : NonZero m}} → (m ^_) Preserves _≤_ ⟶ _≤_ +^-monoʳ-≤ : ∀ m .{{_ : NonZero m}} → Monotonic₁ _≤_ _≤_ (m ^_) ^-monoʳ-≤ m {_} {o} z≤n = n≢0⇒n>0 (≢-nonZero⁻¹ (m ^ o) {{m^n≢0 m o}}) ^-monoʳ-≤ m (s≤s n≤o) = *-monoʳ-≤ m (^-monoʳ-≤ m n≤o) -^-monoˡ-< : ∀ n .{{_ : NonZero n}} → (_^ n) Preserves _<_ ⟶ _<_ +^-monoˡ-< : ∀ n .{{_ : NonZero n}} → Monotonic₁ _<_ _<_ (_^ n) ^-monoˡ-< (suc zero) m0 m o) ^-monoʳ-< m@(suc _) 1_ +*-monoˡ-<-neg : ∀ r .{{_ : Negative r}} → Monotonic₁ _<_ _>_ (_* r) *-monoˡ-<-neg r {p} {q} p_ +*-monoʳ-<-neg : ∀ r .{{_ : Negative r}} → Monotonic₁ _<_ _>_ (r *_) *-monoʳ-<-neg r {p} {q} rewrite *-comm r p | *-comm r q = *-monoˡ-<-neg r *-cancelˡ-<-nonPos : ∀ r .{{_ : NonPositive r}} → r * p < r * q → p > q @@ -1615,15 +1615,15 @@ open ⊓-⊔-latticeProperties public ------------------------------------------------------------------------ -- Other properties of _⊓_ and _⊔_ -mono-≤-distrib-⊔ : ∀ {f} → f Preserves _≤_ ⟶ _≤_ → +mono-≤-distrib-⊔ : ∀ {f} → Monotonic₁ _≤_ _≤_ f → ∀ p q → f (p ⊔ q) ≡ f p ⊔ f q mono-≤-distrib-⊔ {f} = ⊓-⊔-properties.mono-≤-distrib-⊔ (cong f) -mono-≤-distrib-⊓ : ∀ {f} → f Preserves _≤_ ⟶ _≤_ → +mono-≤-distrib-⊓ : ∀ {f} → Monotonic₁ _≤_ _≤_ f → ∀ p q → f (p ⊓ q) ≡ f p ⊓ f q mono-≤-distrib-⊓ {f} = ⊓-⊔-properties.mono-≤-distrib-⊓ (cong f) -mono-<-distrib-⊓ : ∀ {f} → f Preserves _<_ ⟶ _<_ → +mono-<-distrib-⊓ : ∀ {f} → Monotonic₁ _<_ _<_ f → ∀ p q → f (p ⊓ q) ≡ f p ⊓ f q mono-<-distrib-⊓ {f} f-mono-< p q with <-cmp p q ... | tri< p) + ; tri≈; tri<; tri>; Monotonic₁; LeftMonotonic; RightMonotonic; Monotonic₂) import Relation.Binary.Consequences as BC open import Relation.Binary.PropositionalEquality import Relation.Binary.Properties.Poset as PosetProperties @@ -211,7 +211,7 @@ neg-involutive p rewrite neg-involutive-≡ p = ≃-refl ↥(- q) ℤ.* ↧ p ∎) where open ≡-Reasoning -neg-mono-< : -_ Preserves _<_ ⟶ _>_ +neg-mono-< : Monotonic₁ _<_ _>_ (-_) neg-mono-< {p@record{}} {q@record{}} (*<* p_ +*-monoˡ-<-neg : ∀ r .{{_ : Negative r}} → Monotonic₁ _<_ _>_ (_* r) *-monoˡ-<-neg r {p} {q} p0 = positive (neg-mono-< (negative⁻¹ r)) -*-monoʳ-<-neg : ∀ r .{{_ : Negative r}} → (r *_) Preserves _<_ ⟶ _>_ +*-monoʳ-<-neg : ∀ r .{{_ : Negative r}} → Monotonic₁ _<_ _>_ (r *_) *-monoʳ-<-neg r {p} {q} rewrite *-comm-≡ r q | *-comm-≡ r p = *-monoˡ-<-neg r *-cancelˡ-<-nonPos : ∀ r .{{_ : NonPositive r}} → r * p < r * q → q < p @@ -1636,14 +1637,14 @@ open ⊓-⊔-properties public ; ⊔-triangulate -- : ∀ p q r → p ⊔ q ⊔ r ≃ (p ⊔ q) ⊔ (q ⊔ r) ; ⊓-glb -- : ∀ {p q r} → p ≥ r → q ≥ r → p ⊓ q ≥ r - ; ⊓-mono-≤ -- : _⊓_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_ - ; ⊓-monoˡ-≤ -- : ∀ p → (_⊓ p) Preserves _≤_ ⟶ _≤_ - ; ⊓-monoʳ-≤ -- : ∀ p → (p ⊓_) Preserves _≤_ ⟶ _≤_ + ; ⊓-mono-≤ -- : Monotonic₂ _≤_ _≤_ _≤_ _⊓_ + ; ⊓-monoˡ-≤ -- : ∀ p → Monotonic₁_≤_ _≤_ (_⊓ p) + ; ⊓-monoʳ-≤ -- : ∀ p → Monotonic₁_≤_ _≤_ (p ⊓_) ; ⊔-lub -- : ∀ {p q r} → p ≤ r → q ≤ r → p ⊔ q ≤ r - ; ⊔-mono-≤ -- : _⊔_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_ - ; ⊔-monoˡ-≤ -- : ∀ p → (_⊔ p) Preserves _≤_ ⟶ _≤_ - ; ⊔-monoʳ-≤ -- : ∀ p → (p ⊔_) Preserves _≤_ ⟶ _≤_ + ; ⊔-mono-≤ -- : Monotonic₂ _≤_ _≤_ _≤_ _⊔_ + ; ⊔-monoˡ-≤ -- : ∀ p → Monotonic₁_≤_ _≤_ (_⊔ p) + ; ⊔-monoʳ-≤ -- : ∀ p → Monotonic₁_≤_ _≤_ (p ⊔_) ) renaming ( x⊓y≈y⇒y≤x to p⊓q≃q⇒q≤p -- : ∀ {p q} → p ⊓ q ≃ q → q ≤ p @@ -1700,19 +1701,19 @@ open ⊓-⊔-latticeProperties public ------------------------------------------------------------------------ -- Monotonic or antimonotic functions distribute over _⊓_ and _⊔_ -mono-≤-distrib-⊔ : ∀ {f} → f Preserves _≤_ ⟶ _≤_ → +mono-≤-distrib-⊔ : ∀ {f} → Monotonic₁ _≤_ _≤_ f → ∀ m n → f (m ⊔ n) ≃ f m ⊔ f n mono-≤-distrib-⊔ pres = ⊓-⊔-properties.mono-≤-distrib-⊔ (mono⇒cong pres) pres -mono-≤-distrib-⊓ : ∀ {f} → f Preserves _≤_ ⟶ _≤_ → +mono-≤-distrib-⊓ : ∀ {f} → Monotonic₁ _≤_ _≤_ f → ∀ m n → f (m ⊓ n) ≃ f m ⊓ f n mono-≤-distrib-⊓ pres = ⊓-⊔-properties.mono-≤-distrib-⊓ (mono⇒cong pres) pres -antimono-≤-distrib-⊓ : ∀ {f} → f Preserves _≤_ ⟶ _≥_ → +antimono-≤-distrib-⊓ : ∀ {f} → Monotonic₁ _≤_ _≥_ f → ∀ m n → f (m ⊓ n) ≃ f m ⊔ f n antimono-≤-distrib-⊓ pres = ⊓-⊔-properties.antimono-≤-distrib-⊓ (antimono⇒cong pres) pres -antimono-≤-distrib-⊔ : ∀ {f} → f Preserves _≤_ ⟶ _≥_ → +antimono-≤-distrib-⊔ : ∀ {f} → Monotonic₁ _≤_ _≥_ f → ∀ m n → f (m ⊔ n) ≃ f m ⊓ f n antimono-≤-distrib-⊔ pres = ⊓-⊔-properties.antimono-≤-distrib-⊔ (antimono⇒cong pres) pres @@ -1758,12 +1759,12 @@ neg-distrib-⊓-⊔ = antimono-≤-distrib-⊓ neg-mono-≤ ------------------------------------------------------------------------ -- Properties of _⊓_, _⊔_ and _<_ -⊓-mono-< : _⊓_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_ +⊓-mono-< : Monotonic₂ _<_ _<_ _<_ _⊓_ ⊓-mono-< {p} {r} {q} {s} p