From 6a3e2e55e1d58c36ad713460dcbfb78df16b6486 Mon Sep 17 00:00:00 2001 From: Github Actions Date: Fri, 18 Oct 2024 16:21:26 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20agda/agd?= =?UTF-8?q?a-stdlib@c3c9f4f62f5022f4dad0918ca365fefce0775965=20?= =?UTF-8?q?=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- master/Data.Rational.Properties.html | 1590 ++++++++++++++------------ master/Data.Rational.Solver.html | 4 +- 2 files changed, 837 insertions(+), 757 deletions(-) diff --git a/master/Data.Rational.Properties.html b/master/Data.Rational.Properties.html index 609ae88ec7..b50ed3a245 100644 --- a/master/Data.Rational.Properties.html +++ b/master/Data.Rational.Properties.html @@ -1013,778 +1013,858 @@ +-monoʳ-≤ : ∀ r → (_+_ r) Preserves _≤_ ⟶ _≤_ +-monoʳ-≤ r p≤q = +-mono-≤ (≤-refl {r}) p≤q ------------------------------------------------------------------------- --- Properties of _+_ and _<_ - -+-mono-<-≤ : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_ -+-mono-<-≤ {p} {q} {r} {s} p<q r≤s = toℚᵘ-cancel-< (begin-strict - toℚᵘ(p + r) ≃⟨ toℚᵘ-homo-+ p r ⟩ - toℚᵘ(p) ℚᵘ.+ toℚᵘ(r) <⟨ ℚᵘ.+-mono-<-≤ (toℚᵘ-mono-< p<q) (toℚᵘ-mono-≤ r≤s) ⟩ - toℚᵘ(q) ℚᵘ.+ toℚᵘ(s) ≃⟨ ℚᵘ.≃-sym (toℚᵘ-homo-+ q s) ⟩ - toℚᵘ(q + s) ∎) - where open ℚᵘ.≤-Reasoning - -+-mono-≤-< : _+_ Preserves₂ _≤_ ⟶ _<_ ⟶ _<_ -+-mono-≤-< {p} {q} {r} {s} p≤q r<s rewrite +-comm p r | +-comm q s = +-mono-<-≤ r<s p≤q - -+-mono-< : _+_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_ -+-mono-< {p} {q} {r} {s} p<q r<s = <-trans (+-mono-<-≤ p<q (≤-refl {r})) (+-mono-≤-< (≤-refl {q}) r<s) - -+-monoˡ-< : ∀ r → (_+ r) Preserves _<_ ⟶ _<_ -+-monoˡ-< r p<q = +-mono-<-≤ p<q (≤-refl {r}) - -+-monoʳ-< : ∀ r → (_+_ r) Preserves _<_ ⟶ _<_ -+-monoʳ-< r p<q = +-mono-≤-< (≤-refl {r}) p<q - ------------------------------------------------------------------------- --- Properties of _*_ ------------------------------------------------------------------------- - -private - *-nf : ℚ → ℚ → ℤ - *-nf p q = gcd (↥ p ℤ.* ↥ q) (↧ p ℤ.* ↧ q) - -↥-* : ∀ p q → ↥ (p * q) ℤ.* *-nf p q ≡ ↥ p ℤ.* ↥ q -↥-* p@record{} q@record{} = ↥-/ (↥ p ℤ.* ↥ q) (↧ₙ p ℕ.* ↧ₙ q) - -↧-* : ∀ p q → ↧ (p * q) ℤ.* *-nf p q ≡ ↧ p ℤ.* ↧ q -↧-* p@record{} q@record{} = ↧-/ (↥ p ℤ.* ↥ q) (↧ₙ p ℕ.* ↧ₙ q) - ------------------------------------------------------------------------- --- Monomorphic to unnormalised _*_ - -toℚᵘ-homo-* : Homomorphic₂ toℚᵘ _*_ ℚᵘ._*_ -toℚᵘ-homo-* p@record{} q@record{} with *-nf p q ℤ.≟ 0ℤ -... | yes nf[p,q]≡0 = *≡* $ begin - ↥ᵘ (toℚᵘ (p * q)) ℤ.* (↧ p ℤ.* ↧ q) ≡⟨ cong (ℤ._* (↧ p ℤ.* ↧ q)) (↥ᵘ-toℚᵘ (p * q)) ⟩ - ↥ (p * q) ℤ.* (↧ p ℤ.* ↧ q) ≡⟨ cong (ℤ._* (↧ p ℤ.* ↧ q)) eq ⟩ - 0ℤ ℤ.* (↧ p ℤ.* ↧ q) ≡⟨⟩ - 0ℤ ℤ.* ↧ (p * q) ≡⟨ cong (ℤ._* ↧ (p * q)) (sym eq2) ⟩ - (↥ p ℤ.* ↥ q) ℤ.* ↧ (p * q) ≡⟨ cong ((↥ p ℤ.* ↥ q) ℤ.*_) (sym (↧ᵘ-toℚᵘ (p * q))) ⟩ - (↥ p ℤ.* ↥ q) ℤ.* ↧ᵘ (toℚᵘ (p * q)) ∎ - where - open ≡-Reasoning - eq2 : ↥ p ℤ.* ↥ q ≡ 0ℤ - eq2 = gcd[i,j]≡0⇒i≡0 (↥ p ℤ.* ↥ q) (↧ p ℤ.* ↧ q) nf[p,q]≡0 - - eq : ↥ (p * q) ≡ 0ℤ - eq rewrite eq2 = cong ↥_ (0/n≡0 (↧ₙ p ℕ.* ↧ₙ q)) -... | no nf[p,q]≢0 = *≡* (ℤ.*-cancelʳ-≡ _ _ (*-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} $ begin - ↥ᵘ (toℚᵘ (p * q)) ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q ≡⟨ cong (λ v → v ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q) (↥ᵘ-toℚᵘ (p * q)) ⟩ - ↥ (p * q) ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q ≡⟨ xy∙z≈xz∙y (↥ (p * q)) _ _ ⟩ - ↥ (p * q) ℤ.* *-nf p q ℤ.* (↧ p ℤ.* ↧ q) ≡⟨ cong (ℤ._* (↧ p ℤ.* ↧ q)) (↥-* p q) ⟩ - (↥ p ℤ.* ↥ q) ℤ.* (↧ p ℤ.* ↧ q) ≡⟨ cong ((↥ p ℤ.* ↥ q) ℤ.*_) (sym (↧-* p q)) ⟩ - (↥ p ℤ.* ↥ q) ℤ.* (↧ (p * q) ℤ.* *-nf p q) ≡⟨ x∙yz≈xy∙z (↥ p ℤ.* ↥ q) _ _ ⟩ - (↥ p ℤ.* ↥ q) ℤ.* ↧ (p * q) ℤ.* *-nf p q ≡⟨ cong (λ v → (↥ p ℤ.* ↥ q) ℤ.* v ℤ.* *-nf p q) (↧ᵘ-toℚᵘ (p * q)) ⟨ - (↥ p ℤ.* ↥ q) ℤ.* ↧ᵘ (toℚᵘ (p * q)) ℤ.* *-nf p q ∎) - where open ≡-Reasoning; open CommSemigroupProperties ℤ.*-commutativeSemigroup - -toℚᵘ-homo-1/ : ∀ p .{{_ : NonZero p}} → toℚᵘ (1/ p) ℚᵘ.≃ (ℚᵘ.1/ toℚᵘ p) -toℚᵘ-homo-1/ (mkℚ +[1+ _ ] _ _) = ℚᵘ.≃-refl -toℚᵘ-homo-1/ (mkℚ -[1+ _ ] _ _) = ℚᵘ.≃-refl - -toℚᵘ-isMagmaHomomorphism-* : IsMagmaHomomorphism *-rawMagma ℚᵘ.*-rawMagma toℚᵘ -toℚᵘ-isMagmaHomomorphism-* = record - { isRelHomomorphism = toℚᵘ-isRelHomomorphism - ; homo = toℚᵘ-homo-* - } - -toℚᵘ-isMonoidHomomorphism-* : IsMonoidHomomorphism *-1-rawMonoid ℚᵘ.*-1-rawMonoid toℚᵘ -toℚᵘ-isMonoidHomomorphism-* = record - { isMagmaHomomorphism = toℚᵘ-isMagmaHomomorphism-* - ; ε-homo = ℚᵘ.≃-refl - } - -toℚᵘ-isMonoidMonomorphism-* : IsMonoidMonomorphism *-1-rawMonoid ℚᵘ.*-1-rawMonoid toℚᵘ -toℚᵘ-isMonoidMonomorphism-* = record - { isMonoidHomomorphism = toℚᵘ-isMonoidHomomorphism-* - ; injective = toℚᵘ-injective - } - -toℚᵘ-isNearSemiringHomomorphism-+-* : IsNearSemiringHomomorphism +-*-rawNearSemiring ℚᵘ.+-*-rawNearSemiring toℚᵘ -toℚᵘ-isNearSemiringHomomorphism-+-* = record - { +-isMonoidHomomorphism = toℚᵘ-isMonoidHomomorphism-+ - ; *-homo = toℚᵘ-homo-* - } - -toℚᵘ-isNearSemiringMonomorphism-+-* : IsNearSemiringMonomorphism +-*-rawNearSemiring ℚᵘ.+-*-rawNearSemiring toℚᵘ -toℚᵘ-isNearSemiringMonomorphism-+-* = record - { isNearSemiringHomomorphism = toℚᵘ-isNearSemiringHomomorphism-+-* - ; injective = toℚᵘ-injective - } - -toℚᵘ-isSemiringHomomorphism-+-* : IsSemiringHomomorphism +-*-rawSemiring ℚᵘ.+-*-rawSemiring toℚᵘ -toℚᵘ-isSemiringHomomorphism-+-* = record - { isNearSemiringHomomorphism = toℚᵘ-isNearSemiringHomomorphism-+-* - ; 1#-homo = ℚᵘ.≃-refl - } - -toℚᵘ-isSemiringMonomorphism-+-* : IsSemiringMonomorphism +-*-rawSemiring ℚᵘ.+-*-rawSemiring toℚᵘ -toℚᵘ-isSemiringMonomorphism-+-* = record - { isSemiringHomomorphism = toℚᵘ-isSemiringHomomorphism-+-* - ; injective = toℚᵘ-injective - } - -toℚᵘ-isRingHomomorphism-+-* : IsRingHomomorphism +-*-rawRing ℚᵘ.+-*-rawRing toℚᵘ -toℚᵘ-isRingHomomorphism-+-* = record - { isSemiringHomomorphism = toℚᵘ-isSemiringHomomorphism-+-* - ; -‿homo = toℚᵘ-homo‿- - } - -toℚᵘ-isRingMonomorphism-+-* : IsRingMonomorphism +-*-rawRing ℚᵘ.+-*-rawRing toℚᵘ -toℚᵘ-isRingMonomorphism-+-* = record - { isRingHomomorphism = toℚᵘ-isRingHomomorphism-+-* - ; injective = toℚᵘ-injective - } - ------------------------------------------------------------------------- --- Algebraic properties - -private - module +-*-Monomorphism = RingMonomorphisms toℚᵘ-isRingMonomorphism-+-* - -*-assoc : Associative _*_ -*-assoc = +-*-Monomorphism.*-assoc ℚᵘ.*-isMagma ℚᵘ.*-assoc - -*-comm : Commutative _*_ -*-comm = +-*-Monomorphism.*-comm ℚᵘ.*-isMagma ℚᵘ.*-comm - -*-identityˡ : LeftIdentity 1ℚ _*_ -*-identityˡ = +-*-Monomorphism.*-identityˡ ℚᵘ.*-isMagma ℚᵘ.*-identityˡ - -*-identityʳ : RightIdentity 1ℚ _*_ -*-identityʳ = +-*-Monomorphism.*-identityʳ ℚᵘ.*-isMagma ℚᵘ.*-identityʳ - -*-identity : Identity 1ℚ _*_ -*-identity = *-identityˡ , *-identityʳ - -*-zeroˡ : LeftZero 0ℚ _*_ -*-zeroˡ = +-*-Monomorphism.zeroˡ ℚᵘ.+-0-isGroup ℚᵘ.*-isMagma ℚᵘ.*-zeroˡ - -*-zeroʳ : RightZero 0ℚ _*_ -*-zeroʳ = +-*-Monomorphism.zeroʳ ℚᵘ.+-0-isGroup ℚᵘ.*-isMagma ℚᵘ.*-zeroʳ - -*-zero : Zero 0ℚ _*_ -*-zero = *-zeroˡ , *-zeroʳ - -*-distribˡ-+ : _*_ DistributesOverˡ _+_ -*-distribˡ-+ = +-*-Monomorphism.distribˡ ℚᵘ.+-0-isGroup ℚᵘ.*-isMagma ℚᵘ.*-distribˡ-+ - -*-distribʳ-+ : _*_ DistributesOverʳ _+_ -*-distribʳ-+ = +-*-Monomorphism.distribʳ ℚᵘ.+-0-isGroup ℚᵘ.*-isMagma ℚᵘ.*-distribʳ-+ - -*-distrib-+ : _*_ DistributesOver _+_ -*-distrib-+ = *-distribˡ-+ , *-distribʳ-+ - -*-inverseˡ : ∀ p .{{_ : NonZero p}} → (1/ p) * p ≡ 1ℚ -*-inverseˡ p = toℚᵘ-injective (begin-equality - toℚᵘ (1/ p * p) ≃⟨ toℚᵘ-homo-* (1/ p) p ⟩ - toℚᵘ (1/ p) ℚᵘ.* toℚᵘ p ≃⟨ ℚᵘ.*-congʳ (toℚᵘ-homo-1/ p) ⟩ - ℚᵘ.1/ (toℚᵘ p) ℚᵘ.* toℚᵘ p ≃⟨ ℚᵘ.*-inverseˡ (toℚᵘ p) ⟩ - ℚᵘ.1ℚᵘ ∎) - where open ℚᵘ.≤-Reasoning - -*-inverseʳ : ∀ p .{{_ : NonZero p}} → p * (1/ p) ≡ 1ℚ -*-inverseʳ p = trans (*-comm p (1/ p)) (*-inverseˡ p) - -neg-distribˡ-* : ∀ p q → - (p * q) ≡ - p * q -neg-distribˡ-* = +-*-Monomorphism.neg-distribˡ-* ℚᵘ.+-0-isGroup ℚᵘ.*-isMagma ℚᵘ.neg-distribˡ-* - -neg-distribʳ-* : ∀ p q → - (p * q) ≡ p * - q -neg-distribʳ-* = +-*-Monomorphism.neg-distribʳ-* ℚᵘ.+-0-isGroup ℚᵘ.*-isMagma ℚᵘ.neg-distribʳ-* - ------------------------------------------------------------------------- --- Structures - -*-isMagma : IsMagma _*_ -*-isMagma = +-*-Monomorphism.*-isMagma ℚᵘ.*-isMagma +nonNeg+nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p + q) +nonNeg+nonNeg⇒nonNeg p q = nonNegative $ +-mono-≤ (nonNegative⁻¹ p) (nonNegative⁻¹ q) + +nonPos+nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonPositive (p + q) +nonPos+nonPos⇒nonPos p q = nonPositive $ +-mono-≤ (nonPositive⁻¹ p) (nonPositive⁻¹ q) + +------------------------------------------------------------------------ +-- Properties of _+_ and _<_ + ++-mono-<-≤ : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_ ++-mono-<-≤ {p} {q} {r} {s} p<q r≤s = toℚᵘ-cancel-< (begin-strict + toℚᵘ(p + r) ≃⟨ toℚᵘ-homo-+ p r ⟩ + toℚᵘ(p) ℚᵘ.+ toℚᵘ(r) <⟨ ℚᵘ.+-mono-<-≤ (toℚᵘ-mono-< p<q) (toℚᵘ-mono-≤ r≤s) ⟩ + toℚᵘ(q) ℚᵘ.+ toℚᵘ(s) ≃⟨ ℚᵘ.≃-sym (toℚᵘ-homo-+ q s) ⟩ + toℚᵘ(q + s) ∎) + where open ℚᵘ.≤-Reasoning + ++-mono-≤-< : _+_ Preserves₂ _≤_ ⟶ _<_ ⟶ _<_ ++-mono-≤-< {p} {q} {r} {s} p≤q r<s rewrite +-comm p r | +-comm q s = +-mono-<-≤ r<s p≤q + ++-mono-< : _+_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_ ++-mono-< {p} {q} {r} {s} p<q r<s = <-trans (+-mono-<-≤ p<q (≤-refl {r})) (+-mono-≤-< (≤-refl {q}) r<s) + ++-monoˡ-< : ∀ r → (_+ r) Preserves _<_ ⟶ _<_ ++-monoˡ-< r p<q = +-mono-<-≤ p<q (≤-refl {r}) + ++-monoʳ-< : ∀ r → (_+_ r) Preserves _<_ ⟶ _<_ ++-monoʳ-< r p<q = +-mono-≤-< (≤-refl {r}) p<q + +pos+nonNeg⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : NonNegative q}} → Positive (p + q) +pos+nonNeg⇒pos p q = positive $ +-mono-<-≤ (positive⁻¹ p) (nonNegative⁻¹ q) + +nonNeg+pos⇒pos : ∀ p .{{_ : NonNegative p}} q .{{_ : Positive q}} → Positive (p + q) +nonNeg+pos⇒pos p q = positive $ +-mono-≤-< (nonNegative⁻¹ p) (positive⁻¹ q) + +pos+pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p + q) +pos+pos⇒pos p q = positive $ +-mono-< (positive⁻¹ p) (positive⁻¹ q) + +neg+nonPos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : NonPositive q}} → Negative (p + q) +neg+nonPos⇒neg p q = negative $ +-mono-<-≤ (negative⁻¹ p) (nonPositive⁻¹ q) + +nonPos+neg⇒neg : ∀ p .{{_ : NonPositive p}} q .{{_ : Negative q}} → Negative (p + q) +nonPos+neg⇒neg p q = negative $ +-mono-≤-< (nonPositive⁻¹ p) (negative⁻¹ q) + +neg+neg⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Negative (p + q) +neg+neg⇒neg p q = negative $ +-mono-< (negative⁻¹ p) (negative⁻¹ q) + +------------------------------------------------------------------------ +-- Properties of _*_ +------------------------------------------------------------------------ + +private + *-nf : ℚ → ℚ → ℤ + *-nf p q = gcd (↥ p ℤ.* ↥ q) (↧ p ℤ.* ↧ q) + +↥-* : ∀ p q → ↥ (p * q) ℤ.* *-nf p q ≡ ↥ p ℤ.* ↥ q +↥-* p@record{} q@record{} = ↥-/ (↥ p ℤ.* ↥ q) (↧ₙ p ℕ.* ↧ₙ q) + +↧-* : ∀ p q → ↧ (p * q) ℤ.* *-nf p q ≡ ↧ p ℤ.* ↧ q +↧-* p@record{} q@record{} = ↧-/ (↥ p ℤ.* ↥ q) (↧ₙ p ℕ.* ↧ₙ q) + +------------------------------------------------------------------------ +-- Monomorphic to unnormalised _*_ + +toℚᵘ-homo-* : Homomorphic₂ toℚᵘ _*_ ℚᵘ._*_ +toℚᵘ-homo-* p@record{} q@record{} with *-nf p q ℤ.≟ 0ℤ +... | yes nf[p,q]≡0 = *≡* $ begin + ↥ᵘ (toℚᵘ (p * q)) ℤ.* (↧ p ℤ.* ↧ q) ≡⟨ cong (ℤ._* (↧ p ℤ.* ↧ q)) (↥ᵘ-toℚᵘ (p * q)) ⟩ + ↥ (p * q) ℤ.* (↧ p ℤ.* ↧ q) ≡⟨ cong (ℤ._* (↧ p ℤ.* ↧ q)) eq ⟩ + 0ℤ ℤ.* (↧ p ℤ.* ↧ q) ≡⟨⟩ + 0ℤ ℤ.* ↧ (p * q) ≡⟨ cong (ℤ._* ↧ (p * q)) (sym eq2) ⟩ + (↥ p ℤ.* ↥ q) ℤ.* ↧ (p * q) ≡⟨ cong ((↥ p ℤ.* ↥ q) ℤ.*_) (sym (↧ᵘ-toℚᵘ (p * q))) ⟩ + (↥ p ℤ.* ↥ q) ℤ.* ↧ᵘ (toℚᵘ (p * q)) ∎ + where + open ≡-Reasoning + eq2 : ↥ p ℤ.* ↥ q ≡ 0ℤ + eq2 = gcd[i,j]≡0⇒i≡0 (↥ p ℤ.* ↥ q) (↧ p ℤ.* ↧ q) nf[p,q]≡0 + + eq : ↥ (p * q) ≡ 0ℤ + eq rewrite eq2 = cong ↥_ (0/n≡0 (↧ₙ p ℕ.* ↧ₙ q)) +... | no nf[p,q]≢0 = *≡* (ℤ.*-cancelʳ-≡ _ _ (*-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} $ begin + ↥ᵘ (toℚᵘ (p * q)) ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q ≡⟨ cong (λ v → v ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q) (↥ᵘ-toℚᵘ (p * q)) ⟩ + ↥ (p * q) ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q ≡⟨ xy∙z≈xz∙y (↥ (p * q)) _ _ ⟩ + ↥ (p * q) ℤ.* *-nf p q ℤ.* (↧ p ℤ.* ↧ q) ≡⟨ cong (ℤ._* (↧ p ℤ.* ↧ q)) (↥-* p q) ⟩ + (↥ p ℤ.* ↥ q) ℤ.* (↧ p ℤ.* ↧ q) ≡⟨ cong ((↥ p ℤ.* ↥ q) ℤ.*_) (sym (↧-* p q)) ⟩ + (↥ p ℤ.* ↥ q) ℤ.* (↧ (p * q) ℤ.* *-nf p q) ≡⟨ x∙yz≈xy∙z (↥ p ℤ.* ↥ q) _ _ ⟩ + (↥ p ℤ.* ↥ q) ℤ.* ↧ (p * q) ℤ.* *-nf p q ≡⟨ cong (λ v → (↥ p ℤ.* ↥ q) ℤ.* v ℤ.* *-nf p q) (↧ᵘ-toℚᵘ (p * q)) ⟨ + (↥ p ℤ.* ↥ q) ℤ.* ↧ᵘ (toℚᵘ (p * q)) ℤ.* *-nf p q ∎) + where open ≡-Reasoning; open CommSemigroupProperties ℤ.*-commutativeSemigroup + +toℚᵘ-homo-1/ : ∀ p .{{_ : NonZero p}} → toℚᵘ (1/ p) ℚᵘ.≃ (ℚᵘ.1/ toℚᵘ p) +toℚᵘ-homo-1/ (mkℚ +[1+ _ ] _ _) = ℚᵘ.≃-refl +toℚᵘ-homo-1/ (mkℚ -[1+ _ ] _ _) = ℚᵘ.≃-refl + +toℚᵘ-isMagmaHomomorphism-* : IsMagmaHomomorphism *-rawMagma ℚᵘ.*-rawMagma toℚᵘ +toℚᵘ-isMagmaHomomorphism-* = record + { isRelHomomorphism = toℚᵘ-isRelHomomorphism + ; homo = toℚᵘ-homo-* + } + +toℚᵘ-isMonoidHomomorphism-* : IsMonoidHomomorphism *-1-rawMonoid ℚᵘ.*-1-rawMonoid toℚᵘ +toℚᵘ-isMonoidHomomorphism-* = record + { isMagmaHomomorphism = toℚᵘ-isMagmaHomomorphism-* + ; ε-homo = ℚᵘ.≃-refl + } + +toℚᵘ-isMonoidMonomorphism-* : IsMonoidMonomorphism *-1-rawMonoid ℚᵘ.*-1-rawMonoid toℚᵘ +toℚᵘ-isMonoidMonomorphism-* = record + { isMonoidHomomorphism = toℚᵘ-isMonoidHomomorphism-* + ; injective = toℚᵘ-injective + } + +toℚᵘ-isNearSemiringHomomorphism-+-* : IsNearSemiringHomomorphism +-*-rawNearSemiring ℚᵘ.+-*-rawNearSemiring toℚᵘ +toℚᵘ-isNearSemiringHomomorphism-+-* = record + { +-isMonoidHomomorphism = toℚᵘ-isMonoidHomomorphism-+ + ; *-homo = toℚᵘ-homo-* + } + +toℚᵘ-isNearSemiringMonomorphism-+-* : IsNearSemiringMonomorphism +-*-rawNearSemiring ℚᵘ.+-*-rawNearSemiring toℚᵘ +toℚᵘ-isNearSemiringMonomorphism-+-* = record + { isNearSemiringHomomorphism = toℚᵘ-isNearSemiringHomomorphism-+-* + ; injective = toℚᵘ-injective + } + +toℚᵘ-isSemiringHomomorphism-+-* : IsSemiringHomomorphism +-*-rawSemiring ℚᵘ.+-*-rawSemiring toℚᵘ +toℚᵘ-isSemiringHomomorphism-+-* = record + { isNearSemiringHomomorphism = toℚᵘ-isNearSemiringHomomorphism-+-* + ; 1#-homo = ℚᵘ.≃-refl + } + +toℚᵘ-isSemiringMonomorphism-+-* : IsSemiringMonomorphism +-*-rawSemiring ℚᵘ.+-*-rawSemiring toℚᵘ +toℚᵘ-isSemiringMonomorphism-+-* = record + { isSemiringHomomorphism = toℚᵘ-isSemiringHomomorphism-+-* + ; injective = toℚᵘ-injective + } + +toℚᵘ-isRingHomomorphism-+-* : IsRingHomomorphism +-*-rawRing ℚᵘ.+-*-rawRing toℚᵘ +toℚᵘ-isRingHomomorphism-+-* = record + { isSemiringHomomorphism = toℚᵘ-isSemiringHomomorphism-+-* + ; -‿homo = toℚᵘ-homo‿- + } + +toℚᵘ-isRingMonomorphism-+-* : IsRingMonomorphism +-*-rawRing ℚᵘ.+-*-rawRing toℚᵘ +toℚᵘ-isRingMonomorphism-+-* = record + { isRingHomomorphism = toℚᵘ-isRingHomomorphism-+-* + ; injective = toℚᵘ-injective + } + +------------------------------------------------------------------------ +-- Algebraic properties + +private + module +-*-Monomorphism = RingMonomorphisms toℚᵘ-isRingMonomorphism-+-* + +*-assoc : Associative _*_ +*-assoc = +-*-Monomorphism.*-assoc ℚᵘ.*-isMagma ℚᵘ.*-assoc + +*-comm : Commutative _*_ +*-comm = +-*-Monomorphism.*-comm ℚᵘ.*-isMagma ℚᵘ.*-comm + +*-identityˡ : LeftIdentity 1ℚ _*_ +*-identityˡ = +-*-Monomorphism.*-identityˡ ℚᵘ.*-isMagma ℚᵘ.*-identityˡ + +*-identityʳ : RightIdentity 1ℚ _*_ +*-identityʳ = +-*-Monomorphism.*-identityʳ ℚᵘ.*-isMagma ℚᵘ.*-identityʳ + +*-identity : Identity 1ℚ _*_ +*-identity = *-identityˡ , *-identityʳ + +*-zeroˡ : LeftZero 0ℚ _*_ +*-zeroˡ = +-*-Monomorphism.zeroˡ ℚᵘ.+-0-isGroup ℚᵘ.*-isMagma ℚᵘ.*-zeroˡ + +*-zeroʳ : RightZero 0ℚ _*_ +*-zeroʳ = +-*-Monomorphism.zeroʳ ℚᵘ.+-0-isGroup ℚᵘ.*-isMagma ℚᵘ.*-zeroʳ + +*-zero : Zero 0ℚ _*_ +*-zero = *-zeroˡ , *-zeroʳ + +*-distribˡ-+ : _*_ DistributesOverˡ _+_ +*-distribˡ-+ = +-*-Monomorphism.distribˡ ℚᵘ.+-0-isGroup ℚᵘ.*-isMagma ℚᵘ.*-distribˡ-+ + +*-distribʳ-+ : _*_ DistributesOverʳ _+_ +*-distribʳ-+ = +-*-Monomorphism.distribʳ ℚᵘ.+-0-isGroup ℚᵘ.*-isMagma ℚᵘ.*-distribʳ-+ + +*-distrib-+ : _*_ DistributesOver _+_ +*-distrib-+ = *-distribˡ-+ , *-distribʳ-+ + +*-inverseˡ : ∀ p .{{_ : NonZero p}} → (1/ p) * p ≡ 1ℚ +*-inverseˡ p = toℚᵘ-injective (begin-equality + toℚᵘ (1/ p * p) ≃⟨ toℚᵘ-homo-* (1/ p) p ⟩ + toℚᵘ (1/ p) ℚᵘ.* toℚᵘ p ≃⟨ ℚᵘ.*-congʳ (toℚᵘ-homo-1/ p) ⟩ + ℚᵘ.1/ (toℚᵘ p) ℚᵘ.* toℚᵘ p ≃⟨ ℚᵘ.*-inverseˡ (toℚᵘ p) ⟩ + ℚᵘ.1ℚᵘ ∎) + where open ℚᵘ.≤-Reasoning + +*-inverseʳ : ∀ p .{{_ : NonZero p}} → p * (1/ p) ≡ 1ℚ +*-inverseʳ p = trans (*-comm p (1/ p)) (*-inverseˡ p) + +neg-distribˡ-* : ∀ p q → - (p * q) ≡ - p * q +neg-distribˡ-* = +-*-Monomorphism.neg-distribˡ-* ℚᵘ.+-0-isGroup ℚᵘ.*-isMagma ℚᵘ.neg-distribˡ-* + +neg-distribʳ-* : ∀ p q → - (p * q) ≡ p * - q +neg-distribʳ-* = +-*-Monomorphism.neg-distribʳ-* ℚᵘ.+-0-isGroup ℚᵘ.*-isMagma ℚᵘ.neg-distribʳ-* + +------------------------------------------------------------------------ +-- Structures + +*-isMagma : IsMagma _*_ +*-isMagma = +-*-Monomorphism.*-isMagma ℚᵘ.*-isMagma -*-isSemigroup : IsSemigroup _*_ -*-isSemigroup = +-*-Monomorphism.*-isSemigroup ℚᵘ.*-isSemigroup - -*-1-isMonoid : IsMonoid _*_ 1ℚ -*-1-isMonoid = +-*-Monomorphism.*-isMonoid ℚᵘ.*-1-isMonoid +*-isSemigroup : IsSemigroup _*_ +*-isSemigroup = +-*-Monomorphism.*-isSemigroup ℚᵘ.*-isSemigroup + +*-1-isMonoid : IsMonoid _*_ 1ℚ +*-1-isMonoid = +-*-Monomorphism.*-isMonoid ℚᵘ.*-1-isMonoid -*-1-isCommutativeMonoid : IsCommutativeMonoid _*_ 1ℚ -*-1-isCommutativeMonoid = +-*-Monomorphism.*-isCommutativeMonoid ℚᵘ.*-1-isCommutativeMonoid +*-1-isCommutativeMonoid : IsCommutativeMonoid _*_ 1ℚ +*-1-isCommutativeMonoid = +-*-Monomorphism.*-isCommutativeMonoid ℚᵘ.*-1-isCommutativeMonoid -+-*-isRing : IsRing _+_ _*_ -_ 0ℚ 1ℚ -+-*-isRing = +-*-Monomorphism.isRing ℚᵘ.+-*-isRing ++-*-isRing : IsRing _+_ _*_ -_ 0ℚ 1ℚ ++-*-isRing = +-*-Monomorphism.isRing ℚᵘ.+-*-isRing -+-*-isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0ℚ 1ℚ -+-*-isCommutativeRing = +-*-Monomorphism.isCommutativeRing ℚᵘ.+-*-isCommutativeRing - ------------------------------------------------------------------------- --- Packages ++-*-isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0ℚ 1ℚ ++-*-isCommutativeRing = +-*-Monomorphism.isCommutativeRing ℚᵘ.+-*-isCommutativeRing + +------------------------------------------------------------------------ +-- Packages -*-magma : Magma 0ℓ 0ℓ -*-magma = record - { isMagma = *-isMagma - } +*-magma : Magma 0ℓ 0ℓ +*-magma = record + { isMagma = *-isMagma + } -*-semigroup : Semigroup 0ℓ 0ℓ -*-semigroup = record - { isSemigroup = *-isSemigroup - } +*-semigroup : Semigroup 0ℓ 0ℓ +*-semigroup = record + { isSemigroup = *-isSemigroup + } -*-1-monoid : Monoid 0ℓ 0ℓ -*-1-monoid = record - { isMonoid = *-1-isMonoid - } +*-1-monoid : Monoid 0ℓ 0ℓ +*-1-monoid = record + { isMonoid = *-1-isMonoid + } -*-1-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ -*-1-commutativeMonoid = record - { isCommutativeMonoid = *-1-isCommutativeMonoid - } +*-1-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ +*-1-commutativeMonoid = record + { isCommutativeMonoid = *-1-isCommutativeMonoid + } -+-*-ring : Ring 0ℓ 0ℓ -+-*-ring = record - { isRing = +-*-isRing - } ++-*-ring : Ring 0ℓ 0ℓ ++-*-ring = record + { isRing = +-*-isRing + } -+-*-commutativeRing : CommutativeRing 0ℓ 0ℓ -+-*-commutativeRing = record - { isCommutativeRing = +-*-isCommutativeRing - } - - ------------------------------------------------------------------------- --- HeytingField structures and bundles - -module _ where - open CommutativeRing +-*-commutativeRing - using (+-group; zeroˡ; *-congʳ; isCommutativeRing) - - open GroupProperties +-group - open DecSetoidProperties ≡-decSetoid - - #⇒invertible : p ≢ q → Invertible 1ℚ _*_ (p - q) - #⇒invertible {p} {q} p≢q = let r = p - q in 1/ r , *-inverseˡ r , *-inverseʳ r - where instance _ = ≢-nonZero (p≢q ∘ (x∙y⁻¹≈ε⇒x≈y p q)) - - invertible⇒# : Invertible 1ℚ _*_ (p - q) → p ≢ q - invertible⇒# {p} {q} (1/[p-q] , _ , [p-q]/[p-q]≡1) p≡q = contradiction 1≡0 1≢0 - where - open ≈-Reasoning ≡-setoid - 1≡0 : 1ℚ ≡ 0ℚ - 1≡0 = begin - 1ℚ ≈⟨ [p-q]/[p-q]≡1 ⟨ - (p - q) * 1/[p-q] ≈⟨ *-congʳ (x≈y⇒x∙y⁻¹≈ε p≡q) ⟩ - 0ℚ * 1/[p-q] ≈⟨ zeroˡ 1/[p-q] ⟩ - 0ℚ ∎ - - isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ - isHeytingCommutativeRing = record - { isCommutativeRing = isCommutativeRing - ; isApartnessRelation = ≉-isApartnessRelation - ; #⇒invertible = #⇒invertible - ; invertible⇒# = invertible⇒# - } - - isHeytingField : IsHeytingField _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ - isHeytingField = record - { isHeytingCommutativeRing = isHeytingCommutativeRing - ; tight = ≉-tight - } - - heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ - heytingCommutativeRing = record { isHeytingCommutativeRing = isHeytingCommutativeRing } - - heytingField : HeytingField 0ℓ 0ℓ 0ℓ - heytingField = record { isHeytingField = isHeytingField } - - ------------------------------------------------------------------------- --- Properties of _*_ and _≤_ - -*-cancelʳ-≤-pos : ∀ r .{{_ : Positive r}} → p * r ≤ q * r → p ≤ q -*-cancelʳ-≤-pos {p} {q} r pr≤qr = toℚᵘ-cancel-≤ (ℚᵘ.*-cancelʳ-≤-pos (toℚᵘ r) (begin - toℚᵘ p ℚᵘ.* toℚᵘ r ≃⟨ toℚᵘ-homo-* p r ⟨ - toℚᵘ (p * r) ≤⟨ toℚᵘ-mono-≤ pr≤qr ⟩ - toℚᵘ (q * r) ≃⟨ toℚᵘ-homo-* q r ⟩ - toℚᵘ q ℚᵘ.* toℚᵘ r ∎)) - where open ℚᵘ.≤-Reasoning - -*-cancelˡ-≤-pos : ∀ r .{{_ : Positive r}} → r * p ≤ r * q → p ≤ q -*-cancelˡ-≤-pos {p} {q} r rewrite *-comm r p | *-comm r q = *-cancelʳ-≤-pos r - -*-monoʳ-≤-nonNeg : ∀ r .{{_ : NonNegative r}} → (_* r) Preserves _≤_ ⟶ _≤_ -*-monoʳ-≤-nonNeg r {p} {q} p≤q = toℚᵘ-cancel-≤ (begin - toℚᵘ (p * r) ≃⟨ toℚᵘ-homo-* p r ⟩ - toℚᵘ p ℚᵘ.* toℚᵘ r ≤⟨ ℚᵘ.*-monoˡ-≤-nonNeg (toℚᵘ r) (toℚᵘ-mono-≤ p≤q) ⟩ - toℚᵘ q ℚᵘ.* toℚᵘ r ≃⟨ toℚᵘ-homo-* q r ⟨ - toℚᵘ (q * r) ∎) - where open ℚᵘ.≤-Reasoning - -*-monoˡ-≤-nonNeg : ∀ r .{{_ : NonNegative r}} → (r *_) Preserves _≤_ ⟶ _≤_ -*-monoˡ-≤-nonNeg r {p} {q} rewrite *-comm r p | *-comm r q = *-monoʳ-≤-nonNeg r - -*-monoʳ-≤-nonPos : ∀ r .{{_ : NonPositive r}} → (_* r) Preserves _≤_ ⟶ _≥_ -*-monoʳ-≤-nonPos r {p} {q} p≤q = toℚᵘ-cancel-≤ (begin - toℚᵘ (q * r) ≃⟨ toℚᵘ-homo-* q r ⟩ - toℚᵘ q ℚᵘ.* toℚᵘ r ≤⟨ ℚᵘ.*-monoˡ-≤-nonPos (toℚᵘ r) (toℚᵘ-mono-≤ p≤q) ⟩ - toℚᵘ p ℚᵘ.* toℚᵘ r ≃⟨ toℚᵘ-homo-* p r ⟨ - toℚᵘ (p * r) ∎) - where open ℚᵘ.≤-Reasoning - -*-monoˡ-≤-nonPos : ∀ r .{{_ : NonPositive r}} → (r *_) Preserves _≤_ ⟶ _≥_ -*-monoˡ-≤-nonPos r {p} {q} rewrite *-comm r p | *-comm r q = *-monoʳ-≤-nonPos r - -*-cancelʳ-≤-neg : ∀ r .{{_ : Negative r}} → p * r ≤ q * r → p ≥ q -*-cancelʳ-≤-neg {p} {q} r pr≤qr = toℚᵘ-cancel-≤ (ℚᵘ.*-cancelʳ-≤-neg _ (begin - toℚᵘ p ℚᵘ.* toℚᵘ r ≃⟨ toℚᵘ-homo-* p r ⟨ - toℚᵘ (p * r) ≤⟨ toℚᵘ-mono-≤ pr≤qr ⟩ - toℚᵘ (q * r) ≃⟨ toℚᵘ-homo-* q r ⟩ - toℚᵘ q ℚᵘ.* toℚᵘ r ∎)) - where open ℚᵘ.≤-Reasoning - -*-cancelˡ-≤-neg : ∀ r .{{_ : Negative r}} → r * p ≤ r * q → p ≥ q -*-cancelˡ-≤-neg {p} {q} r rewrite *-comm r p | *-comm r q = *-cancelʳ-≤-neg r - ------------------------------------------------------------------------- --- Properties of _*_ and _<_ - -*-monoˡ-<-pos : ∀ r .{{_ : Positive r}} → (_* r) Preserves _<_ ⟶ _<_ -*-monoˡ-<-pos r {p} {q} p<q = toℚᵘ-cancel-< (begin-strict - toℚᵘ (p * r) ≃⟨ toℚᵘ-homo-* p r ⟩ - toℚᵘ p ℚᵘ.* toℚᵘ r <⟨ ℚᵘ.*-monoˡ-<-pos (toℚᵘ r) (toℚᵘ-mono-< p<q) ⟩ - toℚᵘ q ℚᵘ.* toℚᵘ r ≃⟨ toℚᵘ-homo-* q r ⟨ - toℚᵘ (q * r) ∎) - where open ℚᵘ.≤-Reasoning - -*-monoʳ-<-pos : ∀ r .{{_ : Positive r}} → (r *_) Preserves _<_ ⟶ _<_ -*-monoʳ-<-pos r {p} {q} rewrite *-comm r p | *-comm r q = *-monoˡ-<-pos r - -*-cancelˡ-<-nonNeg : ∀ r .{{_ : NonNegative r}} → ∀ {p q} → r * p < r * q → p < q -*-cancelˡ-<-nonNeg r {p} {q} rp<rq = toℚᵘ-cancel-< (ℚᵘ.*-cancelˡ-<-nonNeg (toℚᵘ r) (begin-strict - toℚᵘ r ℚᵘ.* toℚᵘ p ≃⟨ toℚᵘ-homo-* r p ⟨ - toℚᵘ (r * p) <⟨ toℚᵘ-mono-< rp<rq ⟩ - toℚᵘ (r * q) ≃⟨ toℚᵘ-homo-* r q ⟩ - toℚᵘ r ℚᵘ.* toℚᵘ q ∎)) - where open ℚᵘ.≤-Reasoning - -*-cancelʳ-<-nonNeg : ∀ r .{{_ : NonNegative r}} → ∀ {p q} → p * r < q * r → p < q -*-cancelʳ-<-nonNeg r {p} {q} rewrite *-comm p r | *-comm q r = *-cancelˡ-<-nonNeg r - -*-monoˡ-<-neg : ∀ r .{{_ : Negative r}} → (_* r) Preserves _<_ ⟶ _>_ -*-monoˡ-<-neg r {p} {q} p<q = toℚᵘ-cancel-< (begin-strict - toℚᵘ (q * r) ≃⟨ toℚᵘ-homo-* q r ⟩ - toℚᵘ q ℚᵘ.* toℚᵘ r <⟨ ℚᵘ.*-monoˡ-<-neg (toℚᵘ r) (toℚᵘ-mono-< p<q) ⟩ - toℚᵘ p ℚᵘ.* toℚᵘ r ≃⟨ toℚᵘ-homo-* p r ⟨ - toℚᵘ (p * r) ∎) - where open ℚᵘ.≤-Reasoning - -*-monoʳ-<-neg : ∀ r .{{_ : Negative r}} → (r *_) Preserves _<_ ⟶ _>_ -*-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 -*-cancelˡ-<-nonPos {p} {q} r rp<rq = toℚᵘ-cancel-< (ℚᵘ.*-cancelˡ-<-nonPos (toℚᵘ r) (begin-strict - toℚᵘ r ℚᵘ.* toℚᵘ p ≃⟨ toℚᵘ-homo-* r p ⟨ - toℚᵘ (r * p) <⟨ toℚᵘ-mono-< rp<rq ⟩ - toℚᵘ (r * q) ≃⟨ toℚᵘ-homo-* r q ⟩ - toℚᵘ r ℚᵘ.* toℚᵘ q ∎)) - where open ℚᵘ.≤-Reasoning - -*-cancelʳ-<-nonPos : ∀ r .{{_ : NonPositive r}} → p * r < q * r → p > q -*-cancelʳ-<-nonPos {p} {q} r rewrite *-comm p r | *-comm q r = *-cancelˡ-<-nonPos r - ------------------------------------------------------------------------- --- Properties of _⊓_ ------------------------------------------------------------------------- - -p≤q⇒p⊔q≡q : p ≤ q → p ⊔ q ≡ q -p≤q⇒p⊔q≡q {p@record{}} {q@record{}} p≤q with p ≤ᵇ q in p≰q -... | true = refl -... | false = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym p≰q) λ()) - -p≥q⇒p⊔q≡p : p ≥ q → p ⊔ q ≡ p -p≥q⇒p⊔q≡p {p@record{}} {q@record{}} p≥q with p ≤ᵇ q in p≤q -... | true = ≤-antisym p≥q (≤ᵇ⇒≤ (subst T (sym p≤q) _)) -... | false = refl - -p≤q⇒p⊓q≡p : p ≤ q → p ⊓ q ≡ p -p≤q⇒p⊓q≡p {p@record{}} {q@record{}} p≤q with p ≤ᵇ q in p≰q -... | true = refl -... | false = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym p≰q) λ()) - -p≥q⇒p⊓q≡q : p ≥ q → p ⊓ q ≡ q -p≥q⇒p⊓q≡q {p@record{}} {q@record{}} p≥q with p ≤ᵇ q in p≤q -... | true = ≤-antisym (≤ᵇ⇒≤ (subst T (sym p≤q) _)) p≥q -... | false = refl - -⊓-operator : MinOperator ≤-totalPreorder -⊓-operator = record - { x≤y⇒x⊓y≈x = p≤q⇒p⊓q≡p - ; x≥y⇒x⊓y≈y = p≥q⇒p⊓q≡q - } - -⊔-operator : MaxOperator ≤-totalPreorder -⊔-operator = record - { x≤y⇒x⊔y≈y = p≤q⇒p⊔q≡q - ; x≥y⇒x⊔y≈x = p≥q⇒p⊔q≡p - } - ------------------------------------------------------------------------- --- Automatically derived properties of _⊓_ and _⊔_ - -private - module ⊓-⊔-properties = MinMaxOp ⊓-operator ⊔-operator - module ⊓-⊔-latticeProperties = LatticeMinMaxOp ⊓-operator ⊔-operator - -open ⊓-⊔-properties public - using - ( ⊓-idem -- : Idempotent _⊓_ - ; ⊓-sel -- : Selective _⊓_ - ; ⊓-assoc -- : Associative _⊓_ - ; ⊓-comm -- : Commutative _⊓_ - - ; ⊔-idem -- : Idempotent _⊔_ - ; ⊔-sel -- : Selective _⊔_ - ; ⊔-assoc -- : Associative _⊔_ - ; ⊔-comm -- : Commutative _⊔_ - - ; ⊓-distribˡ-⊔ -- : _⊓_ DistributesOverˡ _⊔_ - ; ⊓-distribʳ-⊔ -- : _⊓_ DistributesOverʳ _⊔_ - ; ⊓-distrib-⊔ -- : _⊓_ DistributesOver _⊔_ - ; ⊔-distribˡ-⊓ -- : _⊔_ DistributesOverˡ _⊓_ - ; ⊔-distribʳ-⊓ -- : _⊔_ DistributesOverʳ _⊓_ - ; ⊔-distrib-⊓ -- : _⊔_ DistributesOver _⊓_ - ; ⊓-absorbs-⊔ -- : _⊓_ Absorbs _⊔_ - ; ⊔-absorbs-⊓ -- : _⊔_ Absorbs _⊓_ - ; ⊔-⊓-absorptive -- : Absorptive _⊔_ _⊓_ - ; ⊓-⊔-absorptive -- : Absorptive _⊓_ _⊔_ - - ; ⊓-isMagma -- : IsMagma _⊓_ - ; ⊓-isSemigroup -- : IsSemigroup _⊓_ - ; ⊓-isCommutativeSemigroup -- : IsCommutativeSemigroup _⊓_ - ; ⊓-isBand -- : IsBand _⊓_ - ; ⊓-isSelectiveMagma -- : IsSelectiveMagma _⊓_ - - ; ⊔-isMagma -- : IsMagma _⊔_ - ; ⊔-isSemigroup -- : IsSemigroup _⊔_ - ; ⊔-isCommutativeSemigroup -- : IsCommutativeSemigroup _⊔_ - ; ⊔-isBand -- : IsBand _⊔_ - ; ⊔-isSelectiveMagma -- : IsSelectiveMagma _⊔_ - - ; ⊓-magma -- : Magma _ _ - ; ⊓-semigroup -- : Semigroup _ _ - ; ⊓-band -- : Band _ _ - ; ⊓-commutativeSemigroup -- : CommutativeSemigroup _ _ - ; ⊓-selectiveMagma -- : SelectiveMagma _ _ - - ; ⊔-magma -- : Magma _ _ - ; ⊔-semigroup -- : Semigroup _ _ - ; ⊔-band -- : Band _ _ - ; ⊔-commutativeSemigroup -- : CommutativeSemigroup _ _ - ; ⊔-selectiveMagma -- : SelectiveMagma _ _ - - ; ⊓-glb -- : ∀ {p q r} → p ≥ r → q ≥ r → p ⊓ q ≥ r - ; ⊓-triangulate -- : ∀ p q r → p ⊓ q ⊓ r ≡ (p ⊓ q) ⊓ (q ⊓ r) - ; ⊓-mono-≤ -- : _⊓_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_ - ; ⊓-monoˡ-≤ -- : ∀ p → (_⊓ p) Preserves _≤_ ⟶ _≤_ - ; ⊓-monoʳ-≤ -- : ∀ p → (p ⊓_) Preserves _≤_ ⟶ _≤_ - - ; ⊔-lub -- : ∀ {p q r} → p ≤ r → q ≤ r → p ⊔ q ≤ r - ; ⊔-triangulate -- : ∀ p q r → p ⊔ q ⊔ r ≡ (p ⊔ q) ⊔ (q ⊔ r) - ; ⊔-mono-≤ -- : _⊔_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_ - ; ⊔-monoˡ-≤ -- : ∀ p → (_⊔ p) Preserves _≤_ ⟶ _≤_ - ; ⊔-monoʳ-≤ -- : ∀ p → (p ⊔_) Preserves _≤_ ⟶ _≤_ - ) - renaming - ( x⊓y≈y⇒y≤x to p⊓q≡q⇒q≤p -- : ∀ {p q} → p ⊓ q ≡ q → q ≤ p - ; x⊓y≈x⇒x≤y to p⊓q≡p⇒p≤q -- : ∀ {p q} → p ⊓ q ≡ p → p ≤ q - ; x⊓y≤x to p⊓q≤p -- : ∀ p q → p ⊓ q ≤ p - ; x⊓y≤y to p⊓q≤q -- : ∀ p q → p ⊓ q ≤ q - ; x≤y⇒x⊓z≤y to p≤q⇒p⊓r≤q -- : ∀ {p q} r → p ≤ q → p ⊓ r ≤ q - ; x≤y⇒z⊓x≤y to p≤q⇒r⊓p≤q -- : ∀ {p q} r → p ≤ q → r ⊓ p ≤ q - ; x≤y⊓z⇒x≤y to p≤q⊓r⇒p≤q -- : ∀ {p} q r → p ≤ q ⊓ r → p ≤ q - ; x≤y⊓z⇒x≤z to p≤q⊓r⇒p≤r -- : ∀ {p} q r → p ≤ q ⊓ r → p ≤ r - - ; x⊔y≈y⇒x≤y to p⊔q≡q⇒p≤q -- : ∀ {p q} → p ⊔ q ≡ q → p ≤ q - ; x⊔y≈x⇒y≤x to p⊔q≡p⇒q≤p -- : ∀ {p q} → p ⊔ q ≡ p → q ≤ p - ; x≤x⊔y to p≤p⊔q -- : ∀ p q → p ≤ p ⊔ q - ; x≤y⊔x to p≤q⊔p -- : ∀ p q → p ≤ q ⊔ p - ; x≤y⇒x≤y⊔z to p≤q⇒p≤q⊔r -- : ∀ {p q} r → p ≤ q → p ≤ q ⊔ r - ; x≤y⇒x≤z⊔y to p≤q⇒p≤r⊔q -- : ∀ {p q} r → p ≤ q → p ≤ r ⊔ q - ; x⊔y≤z⇒x≤z to p⊔q≤r⇒p≤r -- : ∀ p q {r} → p ⊔ q ≤ r → p ≤ r - ; x⊔y≤z⇒y≤z to p⊔q≤r⇒q≤r -- : ∀ p q {r} → p ⊔ q ≤ r → q ≤ r - - ; x⊓y≤x⊔y to p⊓q≤p⊔q -- : ∀ p q → p ⊓ q ≤ p ⊔ q - ) - -open ⊓-⊔-latticeProperties public - using - ( ⊓-isSemilattice -- : IsSemilattice _⊓_ - ; ⊔-isSemilattice -- : IsSemilattice _⊔_ - ; ⊔-⊓-isLattice -- : IsLattice _⊔_ _⊓_ - ; ⊓-⊔-isLattice -- : IsLattice _⊓_ _⊔_ - ; ⊔-⊓-isDistributiveLattice -- : IsDistributiveLattice _⊔_ _⊓_ - ; ⊓-⊔-isDistributiveLattice -- : IsDistributiveLattice _⊓_ _⊔_ - - ; ⊓-semilattice -- : Semilattice _ _ - ; ⊔-semilattice -- : Semilattice _ _ - ; ⊔-⊓-lattice -- : Lattice _ _ - ; ⊓-⊔-lattice -- : Lattice _ _ - ; ⊔-⊓-distributiveLattice -- : DistributiveLattice _ _ - ; ⊓-⊔-distributiveLattice -- : DistributiveLattice _ _ - ) - ------------------------------------------------------------------------- --- Other properties of _⊓_ and _⊔_ - -mono-≤-distrib-⊔ : ∀ {f} → f Preserves _≤_ ⟶ _≤_ → - ∀ p q → f (p ⊔ q) ≡ f p ⊔ f q -mono-≤-distrib-⊔ {f} = ⊓-⊔-properties.mono-≤-distrib-⊔ (cong f) - -mono-≤-distrib-⊓ : ∀ {f} → f Preserves _≤_ ⟶ _≤_ → - ∀ p q → f (p ⊓ q) ≡ f p ⊓ f q -mono-≤-distrib-⊓ {f} = ⊓-⊔-properties.mono-≤-distrib-⊓ (cong f) - -mono-<-distrib-⊓ : ∀ {f} → f Preserves _<_ ⟶ _<_ → - ∀ p q → f (p ⊓ q) ≡ f p ⊓ f q -mono-<-distrib-⊓ {f} f-mono-< p q with <-cmp p q -... | tri< p<q p≢r p≯q = begin - f (p ⊓ q) ≡⟨ cong f (p≤q⇒p⊓q≡p (<⇒≤ p<q)) ⟩ - f p ≡⟨ p≤q⇒p⊓q≡p (<⇒≤ (f-mono-< p<q)) ⟨ - f p ⊓ f q ∎ - where open ≡-Reasoning -... | tri≈ p≮q refl p≯q = begin - f (p ⊓ q) ≡⟨ cong f (⊓-idem p) ⟩ - f p ≡⟨ ⊓-idem (f p) ⟨ - f p ⊓ f q ∎ - where open ≡-Reasoning -... | tri> p≮q p≡r p>q = begin - f (p ⊓ q) ≡⟨ cong f (p≥q⇒p⊓q≡q (<⇒≤ p>q)) ⟩ - f q ≡⟨ p≥q⇒p⊓q≡q (<⇒≤ (f-mono-< p>q)) ⟨ - f p ⊓ f q ∎ - where open ≡-Reasoning - -mono-<-distrib-⊔ : ∀ {f} → f Preserves _<_ ⟶ _<_ → - ∀ p q → f (p ⊔ q) ≡ f p ⊔ f q -mono-<-distrib-⊔ {f} f-mono-< p q with <-cmp p q -... | tri< p<q p≢r p≯q = begin - f (p ⊔ q) ≡⟨ cong f (p≤q⇒p⊔q≡q (<⇒≤ p<q)) ⟩ - f q ≡⟨ p≤q⇒p⊔q≡q (<⇒≤ (f-mono-< p<q)) ⟨ - f p ⊔ f q ∎ - where open ≡-Reasoning -... | tri≈ p≮q refl p≯q = begin - f (p ⊔ q) ≡⟨ cong f (⊔-idem p) ⟩ - f q ≡⟨ ⊔-idem (f p) ⟨ - f p ⊔ f q ∎ - where open ≡-Reasoning -... | tri> p≮q p≡r p>q = begin - f (p ⊔ q) ≡⟨ cong f (p≥q⇒p⊔q≡p (<⇒≤ p>q)) ⟩ - f p ≡⟨ p≥q⇒p⊔q≡p (<⇒≤ (f-mono-< p>q)) ⟨ - f p ⊔ f q ∎ - where open ≡-Reasoning - -antimono-≤-distrib-⊓ : ∀ {f} → f Preserves _≤_ ⟶ _≥_ → - ∀ p q → f (p ⊓ q) ≡ f p ⊔ f q -antimono-≤-distrib-⊓ {f} = ⊓-⊔-properties.antimono-≤-distrib-⊓ (cong f) - -antimono-≤-distrib-⊔ : ∀ {f} → f Preserves _≤_ ⟶ _≥_ → - ∀ p q → f (p ⊔ q) ≡ f p ⊓ f q -antimono-≤-distrib-⊔ {f} = ⊓-⊔-properties.antimono-≤-distrib-⊔ (cong f) - ------------------------------------------------------------------------- --- Properties of _⊓_ and _*_ - -*-distribˡ-⊓-nonNeg : ∀ p .{{_ : NonNegative p}} → ∀ q r → p * (q ⊓ r) ≡ (p * q) ⊓ (p * r) -*-distribˡ-⊓-nonNeg p = mono-≤-distrib-⊓ (*-monoˡ-≤-nonNeg p) - -*-distribʳ-⊓-nonNeg : ∀ p .{{_ : NonNegative p}} → ∀ q r → (q ⊓ r) * p ≡ (q * p) ⊓ (r * p) -*-distribʳ-⊓-nonNeg p = mono-≤-distrib-⊓ (*-monoʳ-≤-nonNeg p) - -*-distribˡ-⊔-nonNeg : ∀ p .{{_ : NonNegative p}} → ∀ q r → p * (q ⊔ r) ≡ (p * q) ⊔ (p * r) -*-distribˡ-⊔-nonNeg p = mono-≤-distrib-⊔ (*-monoˡ-≤-nonNeg p) - -*-distribʳ-⊔-nonNeg : ∀ p .{{_ : NonNegative p}} → ∀ q r → (q ⊔ r) * p ≡ (q * p) ⊔ (r * p) -*-distribʳ-⊔-nonNeg p = mono-≤-distrib-⊔ (*-monoʳ-≤-nonNeg p) - ------------------------------------------------------------------------- --- Properties of _⊓_, _⊔_ and _*_ - -*-distribˡ-⊔-nonPos : ∀ p .{{_ : NonPositive p}} → ∀ q r → p * (q ⊔ r) ≡ (p * q) ⊓ (p * r) -*-distribˡ-⊔-nonPos p = antimono-≤-distrib-⊔ (*-monoˡ-≤-nonPos p) - -*-distribʳ-⊔-nonPos : ∀ p .{{_ : NonPositive p}} → ∀ q r → (q ⊔ r) * p ≡ (q * p) ⊓ (r * p) -*-distribʳ-⊔-nonPos p = antimono-≤-distrib-⊔ (*-monoʳ-≤-nonPos p) - -*-distribˡ-⊓-nonPos : ∀ p .{{_ : NonPositive p}} → ∀ q r → p * (q ⊓ r) ≡ (p * q) ⊔ (p * r) -*-distribˡ-⊓-nonPos p = antimono-≤-distrib-⊓ (*-monoˡ-≤-nonPos p) - -*-distribʳ-⊓-nonPos : ∀ p .{{_ : NonPositive p}} → ∀ q r → (q ⊓ r) * p ≡ (q * p) ⊔ (r * p) -*-distribʳ-⊓-nonPos p = antimono-≤-distrib-⊓ (*-monoʳ-≤-nonPos p) - ------------------------------------------------------------------------- --- Properties of 1/_ ------------------------------------------------------------------------- - -nonZero⇒1/nonZero : ∀ p .{{_ : NonZero p}} → NonZero (1/ p) -nonZero⇒1/nonZero (mkℚ +[1+ _ ] _ _) = _ -nonZero⇒1/nonZero (mkℚ -[1+ _ ] _ _) = _ - -1/-involutive : ∀ p .{{_ : NonZero p}} → (1/ (1/ p)) {{nonZero⇒1/nonZero p}} ≡ p -1/-involutive (mkℚ +[1+ n ] d-1 _) = refl -1/-involutive (mkℚ -[1+ n ] d-1 _) = refl - -1/pos⇒pos : ∀ p .{{_ : Positive p}} → Positive ((1/ p) {{pos⇒nonZero p}}) -1/pos⇒pos (mkℚ +[1+ _ ] _ _) = _ - -1/neg⇒neg : ∀ p .{{_ : Negative p}} → Negative ((1/ p) {{neg⇒nonZero p}}) -1/neg⇒neg (mkℚ -[1+ _ ] _ _) = _ - -pos⇒1/pos : ∀ p .{{_ : NonZero p}} .{{_ : Positive (1/ p)}} → Positive p -pos⇒1/pos p = subst Positive (1/-involutive p) (1/pos⇒pos (1/ p)) - -neg⇒1/neg : ∀ p .{{_ : NonZero p}} .{{_ : Negative (1/ p)}} → Negative p -neg⇒1/neg p = subst Negative (1/-involutive p) (1/neg⇒neg (1/ p)) - ------------------------------------------------------------------------- --- Properties of ∣_∣ ------------------------------------------------------------------------- - ------------------------------------------------------------------------- --- Monomorphic to unnormalised -_ - -toℚᵘ-homo-∣-∣ : Homomorphic₁ toℚᵘ ∣_∣ ℚᵘ.∣_∣ -toℚᵘ-homo-∣-∣ (mkℚ +[1+ _ ] _ _) = *≡* refl -toℚᵘ-homo-∣-∣ (mkℚ +0 _ _) = *≡* refl -toℚᵘ-homo-∣-∣ (mkℚ -[1+ _ ] _ _) = *≡* refl - ------------------------------------------------------------------------- --- Properties - -∣p∣≡0⇒p≡0 : ∀ p → ∣ p ∣ ≡ 0ℚ → p ≡ 0ℚ -∣p∣≡0⇒p≡0 (mkℚ +0 zero _) ∣p∣≡0 = refl - -0≤∣p∣ : ∀ p → 0ℚ ≤ ∣ p ∣ -0≤∣p∣ p@record{} = *≤* (begin - (↥ 0ℚ) ℤ.* (↧ ∣ p ∣) ≡⟨ ℤ.*-zeroˡ (↧ ∣ p ∣) ⟩ - 0ℤ ≤⟨ ℤ.+≤+ ℕ.z≤n ⟩ - ↥ ∣ p ∣ ≡⟨ ℤ.*-identityʳ (↥ ∣ p ∣) ⟨ - ↥ ∣ p ∣ ℤ.* 1ℤ ∎) - where open ℤ.≤-Reasoning - -0≤p⇒∣p∣≡p : 0ℚ ≤ p → ∣ p ∣ ≡ p -0≤p⇒∣p∣≡p {p@record{}} 0≤p = toℚᵘ-injective (ℚᵘ.0≤p⇒∣p∣≃p (toℚᵘ-mono-≤ 0≤p)) - -∣-p∣≡∣p∣ : ∀ p → ∣ - p ∣ ≡ ∣ p ∣ -∣-p∣≡∣p∣ (mkℚ +[1+ n ] d-1 _) = refl -∣-p∣≡∣p∣ (mkℚ +0 d-1 _) = refl -∣-p∣≡∣p∣ (mkℚ -[1+ n ] d-1 _) = refl - -∣p∣≡p⇒0≤p : ∀ {p} → ∣ p ∣ ≡ p → 0ℚ ≤ p -∣p∣≡p⇒0≤p {p} ∣p∣≡p = toℚᵘ-cancel-≤ (ℚᵘ.∣p∣≃p⇒0≤p (begin-equality - ℚᵘ.∣ toℚᵘ p ∣ ≃⟨ ℚᵘ.≃-sym (toℚᵘ-homo-∣-∣ p) ⟩ - toℚᵘ ∣ p ∣ ≡⟨ cong toℚᵘ ∣p∣≡p ⟩ - toℚᵘ p ∎)) - where open ℚᵘ.≤-Reasoning - -∣p∣≡p∨∣p∣≡-p : ∀ p → ∣ p ∣ ≡ p ⊎ ∣ p ∣ ≡ - p -∣p∣≡p∨∣p∣≡-p (mkℚ (+ n) d-1 _) = inj₁ refl -∣p∣≡p∨∣p∣≡-p (mkℚ (-[1+ n ]) d-1 _) = inj₂ refl - -∣p+q∣≤∣p∣+∣q∣ : ∀ p q → ∣ p + q ∣ ≤ ∣ p ∣ + ∣ q ∣ -∣p+q∣≤∣p∣+∣q∣ p q = toℚᵘ-cancel-≤ (begin - toℚᵘ ∣ p + q ∣ ≃⟨ toℚᵘ-homo-∣-∣ (p + q) ⟩ - ℚᵘ.∣ toℚᵘ (p + q) ∣ ≃⟨ ℚᵘ.∣-∣-cong (toℚᵘ-homo-+ p q) ⟩ - ℚᵘ.∣ toℚᵘ p ℚᵘ.+ toℚᵘ q ∣ ≤⟨ ℚᵘ.∣p+q∣≤∣p∣+∣q∣ (toℚᵘ p) (toℚᵘ q) ⟩ - ℚᵘ.∣ toℚᵘ p ∣ ℚᵘ.+ ℚᵘ.∣ toℚᵘ q ∣ ≃⟨ ℚᵘ.+-cong (toℚᵘ-homo-∣-∣ p) (toℚᵘ-homo-∣-∣ q) ⟨ - toℚᵘ ∣ p ∣ ℚᵘ.+ toℚᵘ ∣ q ∣ ≃⟨ toℚᵘ-homo-+ ∣ p ∣ ∣ q ∣ ⟨ - toℚᵘ (∣ p ∣ + ∣ q ∣) ∎) - where open ℚᵘ.≤-Reasoning - -∣p-q∣≤∣p∣+∣q∣ : ∀ p q → ∣ p - q ∣ ≤ ∣ p ∣ + ∣ q ∣ -∣p-q∣≤∣p∣+∣q∣ p@record{} q@record{} = begin - ∣ p - q ∣ ≤⟨ ∣p+q∣≤∣p∣+∣q∣ p (- q) ⟩ - ∣ p ∣ + ∣ - q ∣ ≡⟨ cong (λ h → ∣ p ∣ + h) (∣-p∣≡∣p∣ q) ⟩ - ∣ p ∣ + ∣ q ∣ ∎ - where open ≤-Reasoning - -∣p*q∣≡∣p∣*∣q∣ : ∀ p q → ∣ p * q ∣ ≡ ∣ p ∣ * ∣ q ∣ -∣p*q∣≡∣p∣*∣q∣ p q = toℚᵘ-injective (begin-equality - toℚᵘ ∣ p * q ∣ ≃⟨ toℚᵘ-homo-∣-∣ (p * q) ⟩ - ℚᵘ.∣ toℚᵘ (p * q) ∣ ≃⟨ ℚᵘ.∣-∣-cong (toℚᵘ-homo-* p q) ⟩ - ℚᵘ.∣ toℚᵘ p ℚᵘ.* toℚᵘ q ∣ ≃⟨ ℚᵘ.∣p*q∣≃∣p∣*∣q∣ (toℚᵘ p) (toℚᵘ q) ⟩ - ℚᵘ.∣ toℚᵘ p ∣ ℚᵘ.* ℚᵘ.∣ toℚᵘ q ∣ ≃⟨ ℚᵘ.*-cong (toℚᵘ-homo-∣-∣ p) (toℚᵘ-homo-∣-∣ q) ⟨ - toℚᵘ ∣ p ∣ ℚᵘ.* toℚᵘ ∣ q ∣ ≃⟨ toℚᵘ-homo-* ∣ p ∣ ∣ q ∣ ⟨ - toℚᵘ (∣ p ∣ * ∣ q ∣) ∎) - where open ℚᵘ.≤-Reasoning - -∣-∣-nonNeg : ∀ p → NonNegative ∣ p ∣ -∣-∣-nonNeg (mkℚ +[1+ _ ] _ _) = _ -∣-∣-nonNeg (mkℚ +0 _ _) = _ -∣-∣-nonNeg (mkℚ -[1+ _ ] _ _) = _ - -∣∣p∣∣≡∣p∣ : ∀ p → ∣ ∣ p ∣ ∣ ≡ ∣ p ∣ -∣∣p∣∣≡∣p∣ p = 0≤p⇒∣p∣≡p (0≤∣p∣ p) - - ------------------------------------------------------------------------- --- DEPRECATED NAMES ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- Version 2.0 - -*-monoʳ-≤-neg : ∀ r → Negative r → (_* r) Preserves _≤_ ⟶ _≥_ -*-monoʳ-≤-neg r@(mkℚ -[1+ _ ] _ _) _ = *-monoʳ-≤-nonPos r -{-# WARNING_ON_USAGE *-monoʳ-≤-neg -"Warning: *-monoʳ-≤-neg was deprecated in v2.0. ++-*-commutativeRing : CommutativeRing 0ℓ 0ℓ ++-*-commutativeRing = record + { isCommutativeRing = +-*-isCommutativeRing + } + + +------------------------------------------------------------------------ +-- HeytingField structures and bundles + +module _ where + open CommutativeRing +-*-commutativeRing + using (+-group; zeroˡ; *-congʳ; isCommutativeRing) + + open GroupProperties +-group + open DecSetoidProperties ≡-decSetoid + + #⇒invertible : p ≢ q → Invertible 1ℚ _*_ (p - q) + #⇒invertible {p} {q} p≢q = let r = p - q in 1/ r , *-inverseˡ r , *-inverseʳ r + where instance _ = ≢-nonZero (p≢q ∘ (x∙y⁻¹≈ε⇒x≈y p q)) + + invertible⇒# : Invertible 1ℚ _*_ (p - q) → p ≢ q + invertible⇒# {p} {q} (1/[p-q] , _ , [p-q]/[p-q]≡1) p≡q = contradiction 1≡0 1≢0 + where + open ≈-Reasoning ≡-setoid + 1≡0 : 1ℚ ≡ 0ℚ + 1≡0 = begin + 1ℚ ≈⟨ [p-q]/[p-q]≡1 ⟨ + (p - q) * 1/[p-q] ≈⟨ *-congʳ (x≈y⇒x∙y⁻¹≈ε p≡q) ⟩ + 0ℚ * 1/[p-q] ≈⟨ zeroˡ 1/[p-q] ⟩ + 0ℚ ∎ + + isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ + isHeytingCommutativeRing = record + { isCommutativeRing = isCommutativeRing + ; isApartnessRelation = ≉-isApartnessRelation + ; #⇒invertible = #⇒invertible + ; invertible⇒# = invertible⇒# + } + + isHeytingField : IsHeytingField _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ + isHeytingField = record + { isHeytingCommutativeRing = isHeytingCommutativeRing + ; tight = ≉-tight + } + + heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ + heytingCommutativeRing = record { isHeytingCommutativeRing = isHeytingCommutativeRing } + + heytingField : HeytingField 0ℓ 0ℓ 0ℓ + heytingField = record { isHeytingField = isHeytingField } + + +------------------------------------------------------------------------ +-- Properties of _*_ and _≤_ + +*-cancelʳ-≤-pos : ∀ r .{{_ : Positive r}} → p * r ≤ q * r → p ≤ q +*-cancelʳ-≤-pos {p} {q} r pr≤qr = toℚᵘ-cancel-≤ (ℚᵘ.*-cancelʳ-≤-pos (toℚᵘ r) (begin + toℚᵘ p ℚᵘ.* toℚᵘ r ≃⟨ toℚᵘ-homo-* p r ⟨ + toℚᵘ (p * r) ≤⟨ toℚᵘ-mono-≤ pr≤qr ⟩ + toℚᵘ (q * r) ≃⟨ toℚᵘ-homo-* q r ⟩ + toℚᵘ q ℚᵘ.* toℚᵘ r ∎)) + where open ℚᵘ.≤-Reasoning + +*-cancelˡ-≤-pos : ∀ r .{{_ : Positive r}} → r * p ≤ r * q → p ≤ q +*-cancelˡ-≤-pos {p} {q} r rewrite *-comm r p | *-comm r q = *-cancelʳ-≤-pos r + +*-monoʳ-≤-nonNeg : ∀ r .{{_ : NonNegative r}} → (_* r) Preserves _≤_ ⟶ _≤_ +*-monoʳ-≤-nonNeg r {p} {q} p≤q = toℚᵘ-cancel-≤ (begin + toℚᵘ (p * r) ≃⟨ toℚᵘ-homo-* p r ⟩ + toℚᵘ p ℚᵘ.* toℚᵘ r ≤⟨ ℚᵘ.*-monoˡ-≤-nonNeg (toℚᵘ r) (toℚᵘ-mono-≤ p≤q) ⟩ + toℚᵘ q ℚᵘ.* toℚᵘ r ≃⟨ toℚᵘ-homo-* q r ⟨ + toℚᵘ (q * r) ∎) + where open ℚᵘ.≤-Reasoning + +*-monoˡ-≤-nonNeg : ∀ r .{{_ : NonNegative r}} → (r *_) Preserves _≤_ ⟶ _≤_ +*-monoˡ-≤-nonNeg r {p} {q} rewrite *-comm r p | *-comm r q = *-monoʳ-≤-nonNeg r + +*-monoʳ-≤-nonPos : ∀ r .{{_ : NonPositive r}} → (_* r) Preserves _≤_ ⟶ _≥_ +*-monoʳ-≤-nonPos r {p} {q} p≤q = toℚᵘ-cancel-≤ (begin + toℚᵘ (q * r) ≃⟨ toℚᵘ-homo-* q r ⟩ + toℚᵘ q ℚᵘ.* toℚᵘ r ≤⟨ ℚᵘ.*-monoˡ-≤-nonPos (toℚᵘ r) (toℚᵘ-mono-≤ p≤q) ⟩ + toℚᵘ p ℚᵘ.* toℚᵘ r ≃⟨ toℚᵘ-homo-* p r ⟨ + toℚᵘ (p * r) ∎) + where open ℚᵘ.≤-Reasoning + +*-monoˡ-≤-nonPos : ∀ r .{{_ : NonPositive r}} → (r *_) Preserves _≤_ ⟶ _≥_ +*-monoˡ-≤-nonPos r {p} {q} rewrite *-comm r p | *-comm r q = *-monoʳ-≤-nonPos r + +*-cancelʳ-≤-neg : ∀ r .{{_ : Negative r}} → p * r ≤ q * r → p ≥ q +*-cancelʳ-≤-neg {p} {q} r pr≤qr = toℚᵘ-cancel-≤ (ℚᵘ.*-cancelʳ-≤-neg _ (begin + toℚᵘ p ℚᵘ.* toℚᵘ r ≃⟨ toℚᵘ-homo-* p r ⟨ + toℚᵘ (p * r) ≤⟨ toℚᵘ-mono-≤ pr≤qr ⟩ + toℚᵘ (q * r) ≃⟨ toℚᵘ-homo-* q r ⟩ + toℚᵘ q ℚᵘ.* toℚᵘ r ∎)) + where open ℚᵘ.≤-Reasoning + +*-cancelˡ-≤-neg : ∀ r .{{_ : Negative r}} → r * p ≤ r * q → p ≥ q +*-cancelˡ-≤-neg {p} {q} r rewrite *-comm r p | *-comm r q = *-cancelʳ-≤-neg r + +nonNeg*nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p * q) +nonNeg*nonNeg⇒nonNeg p q = nonNegative $ begin + 0ℚ ≡⟨ *-zeroʳ p ⟨ + p * 0ℚ ≤⟨ *-monoˡ-≤-nonNeg p (nonNegative⁻¹ q) ⟩ + p * q ∎ + where open ≤-Reasoning + +nonPos*nonNeg⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonNegative q}} → NonPositive (p * q) +nonPos*nonNeg⇒nonPos p q = nonPositive $ begin + p * q ≤⟨ *-monoˡ-≤-nonPos p (nonNegative⁻¹ q) ⟩ + p * 0ℚ ≡⟨ *-zeroʳ p ⟩ + 0ℚ ∎ + where open ≤-Reasoning + +nonNeg*nonPos⇒nonPos : ∀ p .{{_ : NonNegative p}} q .{{_ : NonPositive q}} → NonPositive (p * q) +nonNeg*nonPos⇒nonPos p q = nonPositive $ begin + p * q ≤⟨ *-monoˡ-≤-nonNeg p (nonPositive⁻¹ q) ⟩ + p * 0ℚ ≡⟨ *-zeroʳ p ⟩ + 0ℚ ∎ + where open ≤-Reasoning + +nonPos*nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonNegative (p * q) +nonPos*nonPos⇒nonPos p q = nonNegative $ begin + 0ℚ ≡⟨ *-zeroʳ p ⟨ + p * 0ℚ ≤⟨ *-monoˡ-≤-nonPos p (nonPositive⁻¹ q) ⟩ + p * q ∎ + where open ≤-Reasoning + +------------------------------------------------------------------------ +-- Properties of _*_ and _<_ + +*-monoˡ-<-pos : ∀ r .{{_ : Positive r}} → (_* r) Preserves _<_ ⟶ _<_ +*-monoˡ-<-pos r {p} {q} p<q = toℚᵘ-cancel-< (begin-strict + toℚᵘ (p * r) ≃⟨ toℚᵘ-homo-* p r ⟩ + toℚᵘ p ℚᵘ.* toℚᵘ r <⟨ ℚᵘ.*-monoˡ-<-pos (toℚᵘ r) (toℚᵘ-mono-< p<q) ⟩ + toℚᵘ q ℚᵘ.* toℚᵘ r ≃⟨ toℚᵘ-homo-* q r ⟨ + toℚᵘ (q * r) ∎) + where open ℚᵘ.≤-Reasoning + +*-monoʳ-<-pos : ∀ r .{{_ : Positive r}} → (r *_) Preserves _<_ ⟶ _<_ +*-monoʳ-<-pos r {p} {q} rewrite *-comm r p | *-comm r q = *-monoˡ-<-pos r + +*-cancelˡ-<-nonNeg : ∀ r .{{_ : NonNegative r}} → ∀ {p q} → r * p < r * q → p < q +*-cancelˡ-<-nonNeg r {p} {q} rp<rq = toℚᵘ-cancel-< (ℚᵘ.*-cancelˡ-<-nonNeg (toℚᵘ r) (begin-strict + toℚᵘ r ℚᵘ.* toℚᵘ p ≃⟨ toℚᵘ-homo-* r p ⟨ + toℚᵘ (r * p) <⟨ toℚᵘ-mono-< rp<rq ⟩ + toℚᵘ (r * q) ≃⟨ toℚᵘ-homo-* r q ⟩ + toℚᵘ r ℚᵘ.* toℚᵘ q ∎)) + where open ℚᵘ.≤-Reasoning + +*-cancelʳ-<-nonNeg : ∀ r .{{_ : NonNegative r}} → ∀ {p q} → p * r < q * r → p < q +*-cancelʳ-<-nonNeg r {p} {q} rewrite *-comm p r | *-comm q r = *-cancelˡ-<-nonNeg r + +*-monoˡ-<-neg : ∀ r .{{_ : Negative r}} → (_* r) Preserves _<_ ⟶ _>_ +*-monoˡ-<-neg r {p} {q} p<q = toℚᵘ-cancel-< (begin-strict + toℚᵘ (q * r) ≃⟨ toℚᵘ-homo-* q r ⟩ + toℚᵘ q ℚᵘ.* toℚᵘ r <⟨ ℚᵘ.*-monoˡ-<-neg (toℚᵘ r) (toℚᵘ-mono-< p<q) ⟩ + toℚᵘ p ℚᵘ.* toℚᵘ r ≃⟨ toℚᵘ-homo-* p r ⟨ + toℚᵘ (p * r) ∎) + where open ℚᵘ.≤-Reasoning + +*-monoʳ-<-neg : ∀ r .{{_ : Negative r}} → (r *_) Preserves _<_ ⟶ _>_ +*-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 +*-cancelˡ-<-nonPos {p} {q} r rp<rq = toℚᵘ-cancel-< (ℚᵘ.*-cancelˡ-<-nonPos (toℚᵘ r) (begin-strict + toℚᵘ r ℚᵘ.* toℚᵘ p ≃⟨ toℚᵘ-homo-* r p ⟨ + toℚᵘ (r * p) <⟨ toℚᵘ-mono-< rp<rq ⟩ + toℚᵘ (r * q) ≃⟨ toℚᵘ-homo-* r q ⟩ + toℚᵘ r ℚᵘ.* toℚᵘ q ∎)) + where open ℚᵘ.≤-Reasoning + +*-cancelʳ-<-nonPos : ∀ r .{{_ : NonPositive r}} → p * r < q * r → p > q +*-cancelʳ-<-nonPos {p} {q} r rewrite *-comm p r | *-comm q r = *-cancelˡ-<-nonPos r + +pos*pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p * q) +pos*pos⇒pos p q = positive $ begin-strict + 0ℚ ≡⟨ *-zeroʳ p ⟨ + p * 0ℚ <⟨ *-monoʳ-<-pos p (positive⁻¹ q) ⟩ + p * q ∎ + where open ≤-Reasoning + +neg*pos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Positive q}} → Negative (p * q) +neg*pos⇒neg p q = negative $ begin-strict + p * q <⟨ *-monoʳ-<-neg p (positive⁻¹ q) ⟩ + p * 0ℚ ≡⟨ *-zeroʳ p ⟩ + 0ℚ ∎ + where open ≤-Reasoning + +pos*neg⇒neg : ∀ p .{{_ : Positive p}} q .{{_ : Negative q}} → Negative (p * q) +pos*neg⇒neg p q = negative $ begin-strict + p * q <⟨ *-monoʳ-<-pos p (negative⁻¹ q) ⟩ + p * 0ℚ ≡⟨ *-zeroʳ p ⟩ + 0ℚ ∎ + where open ≤-Reasoning + +neg*neg⇒pos : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Positive (p * q) +neg*neg⇒pos p q = positive $ begin-strict + 0ℚ ≡⟨ *-zeroʳ p ⟨ + p * 0ℚ <⟨ *-monoʳ-<-neg p (negative⁻¹ q) ⟩ + p * q ∎ + where open ≤-Reasoning + +------------------------------------------------------------------------ +-- Properties of _⊓_ +------------------------------------------------------------------------ + +p≤q⇒p⊔q≡q : p ≤ q → p ⊔ q ≡ q +p≤q⇒p⊔q≡q {p@record{}} {q@record{}} p≤q with p ≤ᵇ q in p≰q +... | true = refl +... | false = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym p≰q) λ()) + +p≥q⇒p⊔q≡p : p ≥ q → p ⊔ q ≡ p +p≥q⇒p⊔q≡p {p@record{}} {q@record{}} p≥q with p ≤ᵇ q in p≤q +... | true = ≤-antisym p≥q (≤ᵇ⇒≤ (subst T (sym p≤q) _)) +... | false = refl + +p≤q⇒p⊓q≡p : p ≤ q → p ⊓ q ≡ p +p≤q⇒p⊓q≡p {p@record{}} {q@record{}} p≤q with p ≤ᵇ q in p≰q +... | true = refl +... | false = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym p≰q) λ()) + +p≥q⇒p⊓q≡q : p ≥ q → p ⊓ q ≡ q +p≥q⇒p⊓q≡q {p@record{}} {q@record{}} p≥q with p ≤ᵇ q in p≤q +... | true = ≤-antisym (≤ᵇ⇒≤ (subst T (sym p≤q) _)) p≥q +... | false = refl + +⊓-operator : MinOperator ≤-totalPreorder +⊓-operator = record + { x≤y⇒x⊓y≈x = p≤q⇒p⊓q≡p + ; x≥y⇒x⊓y≈y = p≥q⇒p⊓q≡q + } + +⊔-operator : MaxOperator ≤-totalPreorder +⊔-operator = record + { x≤y⇒x⊔y≈y = p≤q⇒p⊔q≡q + ; x≥y⇒x⊔y≈x = p≥q⇒p⊔q≡p + } + +------------------------------------------------------------------------ +-- Automatically derived properties of _⊓_ and _⊔_ + +private + module ⊓-⊔-properties = MinMaxOp ⊓-operator ⊔-operator + module ⊓-⊔-latticeProperties = LatticeMinMaxOp ⊓-operator ⊔-operator + +open ⊓-⊔-properties public + using + ( ⊓-idem -- : Idempotent _⊓_ + ; ⊓-sel -- : Selective _⊓_ + ; ⊓-assoc -- : Associative _⊓_ + ; ⊓-comm -- : Commutative _⊓_ + + ; ⊔-idem -- : Idempotent _⊔_ + ; ⊔-sel -- : Selective _⊔_ + ; ⊔-assoc -- : Associative _⊔_ + ; ⊔-comm -- : Commutative _⊔_ + + ; ⊓-distribˡ-⊔ -- : _⊓_ DistributesOverˡ _⊔_ + ; ⊓-distribʳ-⊔ -- : _⊓_ DistributesOverʳ _⊔_ + ; ⊓-distrib-⊔ -- : _⊓_ DistributesOver _⊔_ + ; ⊔-distribˡ-⊓ -- : _⊔_ DistributesOverˡ _⊓_ + ; ⊔-distribʳ-⊓ -- : _⊔_ DistributesOverʳ _⊓_ + ; ⊔-distrib-⊓ -- : _⊔_ DistributesOver _⊓_ + ; ⊓-absorbs-⊔ -- : _⊓_ Absorbs _⊔_ + ; ⊔-absorbs-⊓ -- : _⊔_ Absorbs _⊓_ + ; ⊔-⊓-absorptive -- : Absorptive _⊔_ _⊓_ + ; ⊓-⊔-absorptive -- : Absorptive _⊓_ _⊔_ + + ; ⊓-isMagma -- : IsMagma _⊓_ + ; ⊓-isSemigroup -- : IsSemigroup _⊓_ + ; ⊓-isCommutativeSemigroup -- : IsCommutativeSemigroup _⊓_ + ; ⊓-isBand -- : IsBand _⊓_ + ; ⊓-isSelectiveMagma -- : IsSelectiveMagma _⊓_ + + ; ⊔-isMagma -- : IsMagma _⊔_ + ; ⊔-isSemigroup -- : IsSemigroup _⊔_ + ; ⊔-isCommutativeSemigroup -- : IsCommutativeSemigroup _⊔_ + ; ⊔-isBand -- : IsBand _⊔_ + ; ⊔-isSelectiveMagma -- : IsSelectiveMagma _⊔_ + + ; ⊓-magma -- : Magma _ _ + ; ⊓-semigroup -- : Semigroup _ _ + ; ⊓-band -- : Band _ _ + ; ⊓-commutativeSemigroup -- : CommutativeSemigroup _ _ + ; ⊓-selectiveMagma -- : SelectiveMagma _ _ + + ; ⊔-magma -- : Magma _ _ + ; ⊔-semigroup -- : Semigroup _ _ + ; ⊔-band -- : Band _ _ + ; ⊔-commutativeSemigroup -- : CommutativeSemigroup _ _ + ; ⊔-selectiveMagma -- : SelectiveMagma _ _ + + ; ⊓-glb -- : ∀ {p q r} → p ≥ r → q ≥ r → p ⊓ q ≥ r + ; ⊓-triangulate -- : ∀ p q r → p ⊓ q ⊓ r ≡ (p ⊓ q) ⊓ (q ⊓ r) + ; ⊓-mono-≤ -- : _⊓_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_ + ; ⊓-monoˡ-≤ -- : ∀ p → (_⊓ p) Preserves _≤_ ⟶ _≤_ + ; ⊓-monoʳ-≤ -- : ∀ p → (p ⊓_) Preserves _≤_ ⟶ _≤_ + + ; ⊔-lub -- : ∀ {p q r} → p ≤ r → q ≤ r → p ⊔ q ≤ r + ; ⊔-triangulate -- : ∀ p q r → p ⊔ q ⊔ r ≡ (p ⊔ q) ⊔ (q ⊔ r) + ; ⊔-mono-≤ -- : _⊔_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_ + ; ⊔-monoˡ-≤ -- : ∀ p → (_⊔ p) Preserves _≤_ ⟶ _≤_ + ; ⊔-monoʳ-≤ -- : ∀ p → (p ⊔_) Preserves _≤_ ⟶ _≤_ + ) + renaming + ( x⊓y≈y⇒y≤x to p⊓q≡q⇒q≤p -- : ∀ {p q} → p ⊓ q ≡ q → q ≤ p + ; x⊓y≈x⇒x≤y to p⊓q≡p⇒p≤q -- : ∀ {p q} → p ⊓ q ≡ p → p ≤ q + ; x⊓y≤x to p⊓q≤p -- : ∀ p q → p ⊓ q ≤ p + ; x⊓y≤y to p⊓q≤q -- : ∀ p q → p ⊓ q ≤ q + ; x≤y⇒x⊓z≤y to p≤q⇒p⊓r≤q -- : ∀ {p q} r → p ≤ q → p ⊓ r ≤ q + ; x≤y⇒z⊓x≤y to p≤q⇒r⊓p≤q -- : ∀ {p q} r → p ≤ q → r ⊓ p ≤ q + ; x≤y⊓z⇒x≤y to p≤q⊓r⇒p≤q -- : ∀ {p} q r → p ≤ q ⊓ r → p ≤ q + ; x≤y⊓z⇒x≤z to p≤q⊓r⇒p≤r -- : ∀ {p} q r → p ≤ q ⊓ r → p ≤ r + + ; x⊔y≈y⇒x≤y to p⊔q≡q⇒p≤q -- : ∀ {p q} → p ⊔ q ≡ q → p ≤ q + ; x⊔y≈x⇒y≤x to p⊔q≡p⇒q≤p -- : ∀ {p q} → p ⊔ q ≡ p → q ≤ p + ; x≤x⊔y to p≤p⊔q -- : ∀ p q → p ≤ p ⊔ q + ; x≤y⊔x to p≤q⊔p -- : ∀ p q → p ≤ q ⊔ p + ; x≤y⇒x≤y⊔z to p≤q⇒p≤q⊔r -- : ∀ {p q} r → p ≤ q → p ≤ q ⊔ r + ; x≤y⇒x≤z⊔y to p≤q⇒p≤r⊔q -- : ∀ {p q} r → p ≤ q → p ≤ r ⊔ q + ; x⊔y≤z⇒x≤z to p⊔q≤r⇒p≤r -- : ∀ p q {r} → p ⊔ q ≤ r → p ≤ r + ; x⊔y≤z⇒y≤z to p⊔q≤r⇒q≤r -- : ∀ p q {r} → p ⊔ q ≤ r → q ≤ r + + ; x⊓y≤x⊔y to p⊓q≤p⊔q -- : ∀ p q → p ⊓ q ≤ p ⊔ q + ) + +open ⊓-⊔-latticeProperties public + using + ( ⊓-isSemilattice -- : IsSemilattice _⊓_ + ; ⊔-isSemilattice -- : IsSemilattice _⊔_ + ; ⊔-⊓-isLattice -- : IsLattice _⊔_ _⊓_ + ; ⊓-⊔-isLattice -- : IsLattice _⊓_ _⊔_ + ; ⊔-⊓-isDistributiveLattice -- : IsDistributiveLattice _⊔_ _⊓_ + ; ⊓-⊔-isDistributiveLattice -- : IsDistributiveLattice _⊓_ _⊔_ + + ; ⊓-semilattice -- : Semilattice _ _ + ; ⊔-semilattice -- : Semilattice _ _ + ; ⊔-⊓-lattice -- : Lattice _ _ + ; ⊓-⊔-lattice -- : Lattice _ _ + ; ⊔-⊓-distributiveLattice -- : DistributiveLattice _ _ + ; ⊓-⊔-distributiveLattice -- : DistributiveLattice _ _ + ) + +------------------------------------------------------------------------ +-- Other properties of _⊓_ and _⊔_ + +mono-≤-distrib-⊔ : ∀ {f} → f Preserves _≤_ ⟶ _≤_ → + ∀ p q → f (p ⊔ q) ≡ f p ⊔ f q +mono-≤-distrib-⊔ {f} = ⊓-⊔-properties.mono-≤-distrib-⊔ (cong f) + +mono-≤-distrib-⊓ : ∀ {f} → f Preserves _≤_ ⟶ _≤_ → + ∀ p q → f (p ⊓ q) ≡ f p ⊓ f q +mono-≤-distrib-⊓ {f} = ⊓-⊔-properties.mono-≤-distrib-⊓ (cong f) + +mono-<-distrib-⊓ : ∀ {f} → f Preserves _<_ ⟶ _<_ → + ∀ p q → f (p ⊓ q) ≡ f p ⊓ f q +mono-<-distrib-⊓ {f} f-mono-< p q with <-cmp p q +... | tri< p<q p≢r p≯q = begin + f (p ⊓ q) ≡⟨ cong f (p≤q⇒p⊓q≡p (<⇒≤ p<q)) ⟩ + f p ≡⟨ p≤q⇒p⊓q≡p (<⇒≤ (f-mono-< p<q)) ⟨ + f p ⊓ f q ∎ + where open ≡-Reasoning +... | tri≈ p≮q refl p≯q = begin + f (p ⊓ q) ≡⟨ cong f (⊓-idem p) ⟩ + f p ≡⟨ ⊓-idem (f p) ⟨ + f p ⊓ f q ∎ + where open ≡-Reasoning +... | tri> p≮q p≡r p>q = begin + f (p ⊓ q) ≡⟨ cong f (p≥q⇒p⊓q≡q (<⇒≤ p>q)) ⟩ + f q ≡⟨ p≥q⇒p⊓q≡q (<⇒≤ (f-mono-< p>q)) ⟨ + f p ⊓ f q ∎ + where open ≡-Reasoning + +mono-<-distrib-⊔ : ∀ {f} → f Preserves _<_ ⟶ _<_ → + ∀ p q → f (p ⊔ q) ≡ f p ⊔ f q +mono-<-distrib-⊔ {f} f-mono-< p q with <-cmp p q +... | tri< p<q p≢r p≯q = begin + f (p ⊔ q) ≡⟨ cong f (p≤q⇒p⊔q≡q (<⇒≤ p<q)) ⟩ + f q ≡⟨ p≤q⇒p⊔q≡q (<⇒≤ (f-mono-< p<q)) ⟨ + f p ⊔ f q ∎ + where open ≡-Reasoning +... | tri≈ p≮q refl p≯q = begin + f (p ⊔ q) ≡⟨ cong f (⊔-idem p) ⟩ + f q ≡⟨ ⊔-idem (f p) ⟨ + f p ⊔ f q ∎ + where open ≡-Reasoning +... | tri> p≮q p≡r p>q = begin + f (p ⊔ q) ≡⟨ cong f (p≥q⇒p⊔q≡p (<⇒≤ p>q)) ⟩ + f p ≡⟨ p≥q⇒p⊔q≡p (<⇒≤ (f-mono-< p>q)) ⟨ + f p ⊔ f q ∎ + where open ≡-Reasoning + +antimono-≤-distrib-⊓ : ∀ {f} → f Preserves _≤_ ⟶ _≥_ → + ∀ p q → f (p ⊓ q) ≡ f p ⊔ f q +antimono-≤-distrib-⊓ {f} = ⊓-⊔-properties.antimono-≤-distrib-⊓ (cong f) + +antimono-≤-distrib-⊔ : ∀ {f} → f Preserves _≤_ ⟶ _≥_ → + ∀ p q → f (p ⊔ q) ≡ f p ⊓ f q +antimono-≤-distrib-⊔ {f} = ⊓-⊔-properties.antimono-≤-distrib-⊔ (cong f) + +------------------------------------------------------------------------ +-- Properties of _⊓_ and _*_ + +*-distribˡ-⊓-nonNeg : ∀ p .{{_ : NonNegative p}} → ∀ q r → p * (q ⊓ r) ≡ (p * q) ⊓ (p * r) +*-distribˡ-⊓-nonNeg p = mono-≤-distrib-⊓ (*-monoˡ-≤-nonNeg p) + +*-distribʳ-⊓-nonNeg : ∀ p .{{_ : NonNegative p}} → ∀ q r → (q ⊓ r) * p ≡ (q * p) ⊓ (r * p) +*-distribʳ-⊓-nonNeg p = mono-≤-distrib-⊓ (*-monoʳ-≤-nonNeg p) + +*-distribˡ-⊔-nonNeg : ∀ p .{{_ : NonNegative p}} → ∀ q r → p * (q ⊔ r) ≡ (p * q) ⊔ (p * r) +*-distribˡ-⊔-nonNeg p = mono-≤-distrib-⊔ (*-monoˡ-≤-nonNeg p) + +*-distribʳ-⊔-nonNeg : ∀ p .{{_ : NonNegative p}} → ∀ q r → (q ⊔ r) * p ≡ (q * p) ⊔ (r * p) +*-distribʳ-⊔-nonNeg p = mono-≤-distrib-⊔ (*-monoʳ-≤-nonNeg p) + +------------------------------------------------------------------------ +-- Properties of _⊓_, _⊔_ and _*_ + +*-distribˡ-⊔-nonPos : ∀ p .{{_ : NonPositive p}} → ∀ q r → p * (q ⊔ r) ≡ (p * q) ⊓ (p * r) +*-distribˡ-⊔-nonPos p = antimono-≤-distrib-⊔ (*-monoˡ-≤-nonPos p) + +*-distribʳ-⊔-nonPos : ∀ p .{{_ : NonPositive p}} → ∀ q r → (q ⊔ r) * p ≡ (q * p) ⊓ (r * p) +*-distribʳ-⊔-nonPos p = antimono-≤-distrib-⊔ (*-monoʳ-≤-nonPos p) + +*-distribˡ-⊓-nonPos : ∀ p .{{_ : NonPositive p}} → ∀ q r → p * (q ⊓ r) ≡ (p * q) ⊔ (p * r) +*-distribˡ-⊓-nonPos p = antimono-≤-distrib-⊓ (*-monoˡ-≤-nonPos p) + +*-distribʳ-⊓-nonPos : ∀ p .{{_ : NonPositive p}} → ∀ q r → (q ⊓ r) * p ≡ (q * p) ⊔ (r * p) +*-distribʳ-⊓-nonPos p = antimono-≤-distrib-⊓ (*-monoʳ-≤-nonPos p) + +------------------------------------------------------------------------ +-- Properties of 1/_ +------------------------------------------------------------------------ + +nonZero⇒1/nonZero : ∀ p .{{_ : NonZero p}} → NonZero (1/ p) +nonZero⇒1/nonZero (mkℚ +[1+ _ ] _ _) = _ +nonZero⇒1/nonZero (mkℚ -[1+ _ ] _ _) = _ + +1/-involutive : ∀ p .{{_ : NonZero p}} → (1/ (1/ p)) {{nonZero⇒1/nonZero p}} ≡ p +1/-involutive (mkℚ +[1+ n ] d-1 _) = refl +1/-involutive (mkℚ -[1+ n ] d-1 _) = refl + +1/pos⇒pos : ∀ p .{{_ : Positive p}} → Positive ((1/ p) {{pos⇒nonZero p}}) +1/pos⇒pos (mkℚ +[1+ _ ] _ _) = _ + +1/neg⇒neg : ∀ p .{{_ : Negative p}} → Negative ((1/ p) {{neg⇒nonZero p}}) +1/neg⇒neg (mkℚ -[1+ _ ] _ _) = _ + +pos⇒1/pos : ∀ p .{{_ : NonZero p}} .{{_ : Positive (1/ p)}} → Positive p +pos⇒1/pos p = subst Positive (1/-involutive p) (1/pos⇒pos (1/ p)) + +neg⇒1/neg : ∀ p .{{_ : NonZero p}} .{{_ : Negative (1/ p)}} → Negative p +neg⇒1/neg p = subst Negative (1/-involutive p) (1/neg⇒neg (1/ p)) + +------------------------------------------------------------------------ +-- Properties of ∣_∣ +------------------------------------------------------------------------ + +------------------------------------------------------------------------ +-- Monomorphic to unnormalised -_ + +toℚᵘ-homo-∣-∣ : Homomorphic₁ toℚᵘ ∣_∣ ℚᵘ.∣_∣ +toℚᵘ-homo-∣-∣ (mkℚ +[1+ _ ] _ _) = *≡* refl +toℚᵘ-homo-∣-∣ (mkℚ +0 _ _) = *≡* refl +toℚᵘ-homo-∣-∣ (mkℚ -[1+ _ ] _ _) = *≡* refl + +------------------------------------------------------------------------ +-- Properties + +∣p∣≡0⇒p≡0 : ∀ p → ∣ p ∣ ≡ 0ℚ → p ≡ 0ℚ +∣p∣≡0⇒p≡0 (mkℚ +0 zero _) ∣p∣≡0 = refl + +0≤∣p∣ : ∀ p → 0ℚ ≤ ∣ p ∣ +0≤∣p∣ p@record{} = *≤* (begin + (↥ 0ℚ) ℤ.* (↧ ∣ p ∣) ≡⟨ ℤ.*-zeroˡ (↧ ∣ p ∣) ⟩ + 0ℤ ≤⟨ ℤ.+≤+ ℕ.z≤n ⟩ + ↥ ∣ p ∣ ≡⟨ ℤ.*-identityʳ (↥ ∣ p ∣) ⟨ + ↥ ∣ p ∣ ℤ.* 1ℤ ∎) + where open ℤ.≤-Reasoning + +0≤p⇒∣p∣≡p : 0ℚ ≤ p → ∣ p ∣ ≡ p +0≤p⇒∣p∣≡p {p@record{}} 0≤p = toℚᵘ-injective (ℚᵘ.0≤p⇒∣p∣≃p (toℚᵘ-mono-≤ 0≤p)) + +∣-p∣≡∣p∣ : ∀ p → ∣ - p ∣ ≡ ∣ p ∣ +∣-p∣≡∣p∣ (mkℚ +[1+ n ] d-1 _) = refl +∣-p∣≡∣p∣ (mkℚ +0 d-1 _) = refl +∣-p∣≡∣p∣ (mkℚ -[1+ n ] d-1 _) = refl + +∣p∣≡p⇒0≤p : ∀ {p} → ∣ p ∣ ≡ p → 0ℚ ≤ p +∣p∣≡p⇒0≤p {p} ∣p∣≡p = toℚᵘ-cancel-≤ (ℚᵘ.∣p∣≃p⇒0≤p (begin-equality + ℚᵘ.∣ toℚᵘ p ∣ ≃⟨ ℚᵘ.≃-sym (toℚᵘ-homo-∣-∣ p) ⟩ + toℚᵘ ∣ p ∣ ≡⟨ cong toℚᵘ ∣p∣≡p ⟩ + toℚᵘ p ∎)) + where open ℚᵘ.≤-Reasoning + +∣p∣≡p∨∣p∣≡-p : ∀ p → ∣ p ∣ ≡ p ⊎ ∣ p ∣ ≡ - p +∣p∣≡p∨∣p∣≡-p (mkℚ (+ n) d-1 _) = inj₁ refl +∣p∣≡p∨∣p∣≡-p (mkℚ (-[1+ n ]) d-1 _) = inj₂ refl + +∣p+q∣≤∣p∣+∣q∣ : ∀ p q → ∣ p + q ∣ ≤ ∣ p ∣ + ∣ q ∣ +∣p+q∣≤∣p∣+∣q∣ p q = toℚᵘ-cancel-≤ (begin + toℚᵘ ∣ p + q ∣ ≃⟨ toℚᵘ-homo-∣-∣ (p + q) ⟩ + ℚᵘ.∣ toℚᵘ (p + q) ∣ ≃⟨ ℚᵘ.∣-∣-cong (toℚᵘ-homo-+ p q) ⟩ + ℚᵘ.∣ toℚᵘ p ℚᵘ.+ toℚᵘ q ∣ ≤⟨ ℚᵘ.∣p+q∣≤∣p∣+∣q∣ (toℚᵘ p) (toℚᵘ q) ⟩ + ℚᵘ.∣ toℚᵘ p ∣ ℚᵘ.+ ℚᵘ.∣ toℚᵘ q ∣ ≃⟨ ℚᵘ.+-cong (toℚᵘ-homo-∣-∣ p) (toℚᵘ-homo-∣-∣ q) ⟨ + toℚᵘ ∣ p ∣ ℚᵘ.+ toℚᵘ ∣ q ∣ ≃⟨ toℚᵘ-homo-+ ∣ p ∣ ∣ q ∣ ⟨ + toℚᵘ (∣ p ∣ + ∣ q ∣) ∎) + where open ℚᵘ.≤-Reasoning + +∣p-q∣≤∣p∣+∣q∣ : ∀ p q → ∣ p - q ∣ ≤ ∣ p ∣ + ∣ q ∣ +∣p-q∣≤∣p∣+∣q∣ p@record{} q@record{} = begin + ∣ p - q ∣ ≤⟨ ∣p+q∣≤∣p∣+∣q∣ p (- q) ⟩ + ∣ p ∣ + ∣ - q ∣ ≡⟨ cong (λ h → ∣ p ∣ + h) (∣-p∣≡∣p∣ q) ⟩ + ∣ p ∣ + ∣ q ∣ ∎ + where open ≤-Reasoning + +∣p*q∣≡∣p∣*∣q∣ : ∀ p q → ∣ p * q ∣ ≡ ∣ p ∣ * ∣ q ∣ +∣p*q∣≡∣p∣*∣q∣ p q = toℚᵘ-injective (begin-equality + toℚᵘ ∣ p * q ∣ ≃⟨ toℚᵘ-homo-∣-∣ (p * q) ⟩ + ℚᵘ.∣ toℚᵘ (p * q) ∣ ≃⟨ ℚᵘ.∣-∣-cong (toℚᵘ-homo-* p q) ⟩ + ℚᵘ.∣ toℚᵘ p ℚᵘ.* toℚᵘ q ∣ ≃⟨ ℚᵘ.∣p*q∣≃∣p∣*∣q∣ (toℚᵘ p) (toℚᵘ q) ⟩ + ℚᵘ.∣ toℚᵘ p ∣ ℚᵘ.* ℚᵘ.∣ toℚᵘ q ∣ ≃⟨ ℚᵘ.*-cong (toℚᵘ-homo-∣-∣ p) (toℚᵘ-homo-∣-∣ q) ⟨ + toℚᵘ ∣ p ∣ ℚᵘ.* toℚᵘ ∣ q ∣ ≃⟨ toℚᵘ-homo-* ∣ p ∣ ∣ q ∣ ⟨ + toℚᵘ (∣ p ∣ * ∣ q ∣) ∎) + where open ℚᵘ.≤-Reasoning + +∣-∣-nonNeg : ∀ p → NonNegative ∣ p ∣ +∣-∣-nonNeg (mkℚ +[1+ _ ] _ _) = _ +∣-∣-nonNeg (mkℚ +0 _ _) = _ +∣-∣-nonNeg (mkℚ -[1+ _ ] _ _) = _ + +∣∣p∣∣≡∣p∣ : ∀ p → ∣ ∣ p ∣ ∣ ≡ ∣ p ∣ +∣∣p∣∣≡∣p∣ p = 0≤p⇒∣p∣≡p (0≤∣p∣ p) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +*-monoʳ-≤-neg : ∀ r → Negative r → (_* r) Preserves _≤_ ⟶ _≥_ +*-monoʳ-≤-neg r@(mkℚ -[1+ _ ] _ _) _ = *-monoʳ-≤-nonPos r +{-# WARNING_ON_USAGE *-monoʳ-≤-neg +"Warning: *-monoʳ-≤-neg was deprecated in v2.0. Please use *-monoʳ-≤-nonPos instead." -#-} -*-monoˡ-≤-neg : ∀ r → Negative r → (r *_) Preserves _≤_ ⟶ _≥_ -*-monoˡ-≤-neg r@(mkℚ -[1+ _ ] _ _) _ = *-monoˡ-≤-nonPos r -{-# WARNING_ON_USAGE *-monoˡ-≤-neg -"Warning: *-monoˡ-≤-neg was deprecated in v2.0. +#-} +*-monoˡ-≤-neg : ∀ r → Negative r → (r *_) Preserves _≤_ ⟶ _≥_ +*-monoˡ-≤-neg r@(mkℚ -[1+ _ ] _ _) _ = *-monoˡ-≤-nonPos r +{-# WARNING_ON_USAGE *-monoˡ-≤-neg +"Warning: *-monoˡ-≤-neg was deprecated in v2.0. Please use *-monoˡ-≤-nonPos instead." -#-} -*-monoʳ-≤-pos : ∀ r → Positive r → (_* r) Preserves _≤_ ⟶ _≤_ -*-monoʳ-≤-pos r@(mkℚ +[1+ _ ] _ _) _ = *-monoʳ-≤-nonNeg r -{-# WARNING_ON_USAGE *-monoʳ-≤-pos -"Warning: *-monoʳ-≤-pos was deprecated in v2.0. +#-} +*-monoʳ-≤-pos : ∀ r → Positive r → (_* r) Preserves _≤_ ⟶ _≤_ +*-monoʳ-≤-pos r@(mkℚ +[1+ _ ] _ _) _ = *-monoʳ-≤-nonNeg r +{-# WARNING_ON_USAGE *-monoʳ-≤-pos +"Warning: *-monoʳ-≤-pos was deprecated in v2.0. Please use *-monoʳ-≤-nonNeg instead." -#-} -*-monoˡ-≤-pos : ∀ r → Positive r → (r *_) Preserves _≤_ ⟶ _≤_ -*-monoˡ-≤-pos r@(mkℚ +[1+ _ ] _ _) _ = *-monoˡ-≤-nonNeg r -{-# WARNING_ON_USAGE *-monoˡ-≤-pos -"Warning: *-monoˡ-≤-pos was deprecated in v2.0. +#-} +*-monoˡ-≤-pos : ∀ r → Positive r → (r *_) Preserves _≤_ ⟶ _≤_ +*-monoˡ-≤-pos r@(mkℚ +[1+ _ ] _ _) _ = *-monoˡ-≤-nonNeg r +{-# WARNING_ON_USAGE *-monoˡ-≤-pos +"Warning: *-monoˡ-≤-pos was deprecated in v2.0. Please use *-monoˡ-≤-nonNeg instead." -#-} -*-cancelˡ-<-pos : ∀ r → Positive r → ∀ {p q} → r * p < r * q → p < q -*-cancelˡ-<-pos r@(mkℚ +[1+ _ ] _ _) _ = *-cancelˡ-<-nonNeg r -{-# WARNING_ON_USAGE *-cancelˡ-<-pos -"Warning: *-cancelˡ-<-pos was deprecated in v2.0. +#-} +*-cancelˡ-<-pos : ∀ r → Positive r → ∀ {p q} → r * p < r * q → p < q +*-cancelˡ-<-pos r@(mkℚ +[1+ _ ] _ _) _ = *-cancelˡ-<-nonNeg r +{-# WARNING_ON_USAGE *-cancelˡ-<-pos +"Warning: *-cancelˡ-<-pos was deprecated in v2.0. Please use *-cancelˡ-<-nonNeg instead." -#-} -*-cancelʳ-<-pos : ∀ r → Positive r → ∀ {p q} → p * r < q * r → p < q -*-cancelʳ-<-pos r@(mkℚ +[1+ _ ] _ _) _ = *-cancelʳ-<-nonNeg r -{-# WARNING_ON_USAGE *-cancelʳ-<-pos -"Warning: *-cancelʳ-<-pos was deprecated in v2.0. +#-} +*-cancelʳ-<-pos : ∀ r → Positive r → ∀ {p q} → p * r < q * r → p < q +*-cancelʳ-<-pos r@(mkℚ +[1+ _ ] _ _) _ = *-cancelʳ-<-nonNeg r +{-# WARNING_ON_USAGE *-cancelʳ-<-pos +"Warning: *-cancelʳ-<-pos was deprecated in v2.0. Please use *-cancelʳ-<-nonNeg instead." -#-} -*-cancelˡ-<-neg : ∀ r → Negative r → ∀ {p q} → r * p < r * q → p > q -*-cancelˡ-<-neg r@(mkℚ -[1+ _ ] _ _) _ = *-cancelˡ-<-nonPos r -{-# WARNING_ON_USAGE *-cancelˡ-<-neg -"Warning: *-cancelˡ-<-neg was deprecated in v2.0. +#-} +*-cancelˡ-<-neg : ∀ r → Negative r → ∀ {p q} → r * p < r * q → p > q +*-cancelˡ-<-neg r@(mkℚ -[1+ _ ] _ _) _ = *-cancelˡ-<-nonPos r +{-# WARNING_ON_USAGE *-cancelˡ-<-neg +"Warning: *-cancelˡ-<-neg was deprecated in v2.0. Please use *-cancelˡ-<-nonPos instead." -#-} -*-cancelʳ-<-neg : ∀ r → Negative r → ∀ {p q} → p * r < q * r → p > q -*-cancelʳ-<-neg r@(mkℚ -[1+ _ ] _ _) _ = *-cancelʳ-<-nonPos r -{-# WARNING_ON_USAGE *-cancelʳ-<-neg -"Warning: *-cancelʳ-<-neg was deprecated in v2.0. +#-} +*-cancelʳ-<-neg : ∀ r → Negative r → ∀ {p q} → p * r < q * r → p > q +*-cancelʳ-<-neg r@(mkℚ -[1+ _ ] _ _) _ = *-cancelʳ-<-nonPos r +{-# WARNING_ON_USAGE *-cancelʳ-<-neg +"Warning: *-cancelʳ-<-neg was deprecated in v2.0. Please use *-cancelʳ-<-nonPos instead." -#-} -negative<positive : Negative p → Positive q → p < q -negative<positive {p} {q} p<0 q>0 = neg<pos p q {{p<0}} {{q>0}} -{-# WARNING_ON_USAGE negative<positive -"Warning: negative<positive was deprecated in v2.0. +#-} +negative<positive : Negative p → Positive q → p < q +negative<positive {p} {q} p<0 q>0 = neg<pos p q {{p<0}} {{q>0}} +{-# WARNING_ON_USAGE negative<positive +"Warning: negative<positive was deprecated in v2.0. Please use neg<pos instead." -#-} -{- issue1865/issue1755: raw bundles have moved to `Data.X.Base` -} -open Data.Rational.Base public - using (+-rawMagma; +-0-rawGroup; *-rawMagma; +-*-rawNearSemiring; +-*-rawSemiring; +-*-rawRing) - renaming (+-0-rawMonoid to +-rawMonoid; *-1-rawMonoid to *-rawMonoid) +#-} +{- issue1865/issue1755: raw bundles have moved to `Data.X.Base` -} +open Data.Rational.Base public + using (+-rawMagma; +-0-rawGroup; *-rawMagma; +-*-rawNearSemiring; +-*-rawSemiring; +-*-rawRing) + renaming (+-0-rawMonoid to +-rawMonoid; *-1-rawMonoid to *-rawMonoid) \ No newline at end of file diff --git a/master/Data.Rational.Solver.html b/master/Data.Rational.Solver.html index b12d0247a8..6886c302fc 100644 --- a/master/Data.Rational.Solver.html +++ b/master/Data.Rational.Solver.html @@ -11,12 +11,12 @@ import Algebra.Solver.Ring.Simple as Solver import Algebra.Solver.Ring.AlmostCommutativeRing as ACR -open import Data.Rational.Properties using (_≟_; +-*-commutativeRing) +open import Data.Rational.Properties using (_≟_; +-*-commutativeRing) ------------------------------------------------------------------------ -- A module for automatically solving propositional equivalences -- containing _+_ and _*_ module +-*-Solver = - Solver (ACR.fromCommutativeRing +-*-commutativeRing) _≟_ + Solver (ACR.fromCommutativeRing +-*-commutativeRing) _≟_ \ No newline at end of file