{-# OPTIONS --cubical-compatible --safe #-}
module Data.Nat.Properties where
open import Axiom.UniquenessOfIdentityProofs
open import Algebra.Bundles
open import Algebra.Morphism
open import Algebra.Consequences.Propositional
open import Algebra.Construct.NaturalChoice.Base
import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp
import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
import Algebra.Properties.CommutativeSemigroup as CommSemigroupProperties
open import Data.Bool.Base using (Bool; false; true; T)
open import Data.Bool.Properties using (T?)
open import Data.Empty using (⊥)
open import Data.Nat.Base
open import Data.Product.Base using (∃; _×_; _,_)
open import Data.Sum.Base as Sum
open import Data.Unit using (tt)
open import Function.Base
open import Function.Bundles using (_↣_)
open import Function.Metric.Nat
open import Level using (0ℓ)
open import Relation.Unary as U using (Pred)
open import Relation.Binary
open import Relation.Binary.Consequences using (flip-Connex)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary hiding (Irrelevant)
open import Relation.Nullary.Decidable using (True; via-injection; map′)
open import Relation.Nullary.Negation using (contradiction; contradiction₂)
open import Relation.Nullary.Reflects using (fromEquivalence)
open import Algebra.Definitions {A = ℕ} _≡_
hiding (LeftCancellative; RightCancellative; Cancellative)
open import Algebra.Definitions
using (LeftCancellative; RightCancellative; Cancellative)
open import Algebra.Structures {A = ℕ} _≡_
nonZero? : U.Decidable NonZero
nonZero? zero = no NonZero.nonZero
nonZero? (suc n) = yes _
suc-injective : ∀ {m n} → suc m ≡ suc n → m ≡ n
suc-injective refl = refl
≡ᵇ⇒≡ : ∀ m n → T (m ≡ᵇ n) → m ≡ n
≡ᵇ⇒≡ zero zero _ = refl
≡ᵇ⇒≡ (suc m) (suc n) eq = cong suc (≡ᵇ⇒≡ m n eq)
≡⇒≡ᵇ : ∀ m n → m ≡ n → T (m ≡ᵇ n)
≡⇒≡ᵇ zero zero eq = _
≡⇒≡ᵇ (suc m) (suc n) eq = ≡⇒≡ᵇ m n (suc-injective eq)
infix 4 _≟_
_≟_ : DecidableEquality ℕ
m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
≡-irrelevant : Irrelevant {A = ℕ} _≡_
≡-irrelevant = Decidable⇒UIP.≡-irrelevant _≟_
≟-diag : ∀ {m n} (eq : m ≡ n) → (m ≟ n) ≡ yes eq
≟-diag = ≡-≟-identity _≟_
≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ})
≡-isDecEquivalence = record
{ isEquivalence = isEquivalence
; _≟_ = _≟_
}
≡-decSetoid : DecSetoid 0ℓ 0ℓ
≡-decSetoid = record
{ Carrier = ℕ
; _≈_ = _≡_
; isDecEquivalence = ≡-isDecEquivalence
}
0≢1+n : ∀ {n} → 0 ≢ suc n
0≢1+n ()
1+n≢0 : ∀ {n} → suc n ≢ 0
1+n≢0 ()
1+n≢n : ∀ {n} → suc n ≢ n
1+n≢n {suc n} = 1+n≢n ∘ suc-injective
<ᵇ⇒< : ∀ m n → T (m <ᵇ n) → m < n
<ᵇ⇒< zero (suc n) m<n = z<s
<ᵇ⇒< (suc m) (suc n) m<n = s<s (<ᵇ⇒< m n m<n)
<⇒<ᵇ : ∀ {m n} → m < n → T (m <ᵇ n)
<⇒<ᵇ z<s = tt
<⇒<ᵇ (s<s m<n@(s≤s _)) = <⇒<ᵇ m<n
<ᵇ-reflects-< : ∀ m n → Reflects (m < n) (m <ᵇ n)
<ᵇ-reflects-< m n = fromEquivalence (<ᵇ⇒< m n) <⇒<ᵇ
≤ᵇ⇒≤ : ∀ m n → T (m ≤ᵇ n) → m ≤ n
≤ᵇ⇒≤ zero n m≤n = z≤n
≤ᵇ⇒≤ (suc m) n m≤n = <ᵇ⇒< m n m≤n
≤⇒≤ᵇ : ∀ {m n} → m ≤ n → T (m ≤ᵇ n)
≤⇒≤ᵇ z≤n = tt
≤⇒≤ᵇ m≤n@(s≤s _) = <⇒<ᵇ m≤n
≤ᵇ-reflects-≤ : ∀ m n → Reflects (m ≤ n) (m ≤ᵇ n)
≤ᵇ-reflects-≤ m n = fromEquivalence (≤ᵇ⇒≤ m n) ≤⇒≤ᵇ
≤-reflexive : _≡_ ⇒ _≤_
≤-reflexive {zero} refl = z≤n
≤-reflexive {suc m} refl = s≤s (≤-reflexive refl)
≤-refl : Reflexive _≤_
≤-refl = ≤-reflexive refl
≤-antisym : Antisymmetric _≡_ _≤_
≤-antisym z≤n z≤n = refl
≤-antisym (s≤s m≤n) (s≤s n≤m) = cong suc (≤-antisym m≤n n≤m)
≤-trans : Transitive _≤_
≤-trans z≤n _ = z≤n
≤-trans (s≤s m≤n) (s≤s n≤o) = s≤s (≤-trans m≤n n≤o)
≤-total : Total _≤_
≤-total zero _ = inj₁ z≤n
≤-total _ zero = inj₂ z≤n
≤-total (suc m) (suc n) with ≤-total m n
... | inj₁ m≤n = inj₁ (s≤s m≤n)
... | inj₂ n≤m = inj₂ (s≤s n≤m)
≤-irrelevant : Irrelevant _≤_
≤-irrelevant z≤n z≤n = refl
≤-irrelevant (s≤s m≤n₁) (s≤s m≤n₂) = cong s≤s (≤-irrelevant m≤n₁ m≤n₂)
infix 4 _≤?_ _≥?_
_≤?_ : Decidable _≤_
m ≤? n = map′ (≤ᵇ⇒≤ m n) ≤⇒≤ᵇ (T? (m ≤ᵇ n))
_≥?_ : Decidable _≥_
_≥?_ = flip _≤?_
≤-isPreorder : IsPreorder _≡_ _≤_
≤-isPreorder = record
{ isEquivalence = isEquivalence
; reflexive = ≤-reflexive
; trans = ≤-trans
}
≤-isTotalPreorder : IsTotalPreorder _≡_ _≤_
≤-isTotalPreorder = record
{ isPreorder = ≤-isPreorder
; total = ≤-total
}
≤-isPartialOrder : IsPartialOrder _≡_ _≤_
≤-isPartialOrder = record
{ isPreorder = ≤-isPreorder
; antisym = ≤-antisym
}
≤-isTotalOrder : IsTotalOrder _≡_ _≤_
≤-isTotalOrder = record
{ isPartialOrder = ≤-isPartialOrder
; total = ≤-total
}
≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
≤-isDecTotalOrder = record
{ isTotalOrder = ≤-isTotalOrder
; _≟_ = _≟_
; _≤?_ = _≤?_
}
≤-preorder : Preorder 0ℓ 0ℓ 0ℓ
≤-preorder = record
{ isPreorder = ≤-isPreorder
}
≤-totalPreorder : TotalPreorder 0ℓ 0ℓ 0ℓ
≤-totalPreorder = record
{ isTotalPreorder = ≤-isTotalPreorder
}
≤-poset : Poset 0ℓ 0ℓ 0ℓ
≤-poset = record
{ isPartialOrder = ≤-isPartialOrder
}
≤-totalOrder : TotalOrder 0ℓ 0ℓ 0ℓ
≤-totalOrder = record
{ isTotalOrder = ≤-isTotalOrder
}
≤-decTotalOrder : DecTotalOrder 0ℓ 0ℓ 0ℓ
≤-decTotalOrder = record
{ isDecTotalOrder = ≤-isDecTotalOrder
}
s≤s-injective : ∀ {m n} {p q : m ≤ n} → s≤s p ≡ s≤s q → p ≡ q
s≤s-injective refl = refl
≤-pred : ∀ {m n} → suc m ≤ suc n → m ≤ n
≤-pred (s≤s m≤n) = m≤n
m≤n⇒m≤1+n : ∀ {m n} → m ≤ n → m ≤ 1 + n
m≤n⇒m≤1+n z≤n = z≤n
m≤n⇒m≤1+n (s≤s m≤n) = s≤s (m≤n⇒m≤1+n m≤n)
n≤1+n : ∀ n → n ≤ 1 + n
n≤1+n _ = m≤n⇒m≤1+n ≤-refl
1+n≰n : ∀ {n} → 1 + n ≰ n
1+n≰n (s≤s 1+n≤n) = 1+n≰n 1+n≤n
n≤0⇒n≡0 : ∀ {n} → n ≤ 0 → n ≡ 0
n≤0⇒n≡0 z≤n = refl
n≤1⇒n≡0∨n≡1 : ∀ {n : ℕ} → n ≤ 1 → n ≡ 0 ⊎ n ≡ 1
n≤1⇒n≡0∨n≡1 z≤n = inj₁ refl
n≤1⇒n≡0∨n≡1 (s≤s z≤n) = inj₂ refl
<⇒≤ : _<_ ⇒ _≤_
<⇒≤ z<s = z≤n
<⇒≤ (s<s m<n@(s≤s _)) = s≤s (<⇒≤ m<n)
<⇒≢ : _<_ ⇒ _≢_
<⇒≢ m<n refl = 1+n≰n m<n
>⇒≢ : _>_ ⇒ _≢_
>⇒≢ = ≢-sym ∘ <⇒≢
≤⇒≯ : _≤_ ⇒ _≯_
≤⇒≯ (s≤s m≤n) (s≤s n≤m) = ≤⇒≯ m≤n n≤m
<⇒≱ : _<_ ⇒ _≱_
<⇒≱ (s≤s m+1≤n) (s≤s n≤m) = <⇒≱ m+1≤n n≤m
<⇒≯ : _<_ ⇒ _≯_
<⇒≯ (s≤s m<n) (s≤s n<m) = <⇒≯ m<n n<m
≰⇒≮ : _≰_ ⇒ _≮_
≰⇒≮ m≰n 1+m≤n = m≰n (<⇒≤ 1+m≤n)
≰⇒> : _≰_ ⇒ _>_
≰⇒> {zero} z≰n = contradiction z≤n z≰n
≰⇒> {suc m} {zero} _ = z<s
≰⇒> {suc m} {suc n} m≰n = s<s (≰⇒> (m≰n ∘ s≤s))
≰⇒≥ : _≰_ ⇒ _≥_
≰⇒≥ = <⇒≤ ∘ ≰⇒>
≮⇒≥ : _≮_ ⇒ _≥_
≮⇒≥ {_} {zero} _ = z≤n
≮⇒≥ {zero} {suc j} 1≮j+1 = contradiction z<s 1≮j+1
≮⇒≥ {suc i} {suc j} i+1≮j+1 = s≤s (≮⇒≥ (i+1≮j+1 ∘ s<s))
≤∧≢⇒< : ∀ {m n} → m ≤ n → m ≢ n → m < n
≤∧≢⇒< {_} {zero} z≤n m≢n = contradiction refl m≢n
≤∧≢⇒< {_} {suc n} z≤n m≢n = z<s
≤∧≢⇒< {_} {suc n} (s≤s m≤n) 1+m≢1+n =
s<s (≤∧≢⇒< m≤n (1+m≢1+n ∘ cong suc))
≤∧≮⇒≡ : ∀ {m n} → m ≤ n → m ≮ n → m ≡ n
≤∧≮⇒≡ m≤n m≮n = ≤-antisym m≤n (≮⇒≥ m≮n)
≤-<-connex : Connex _≤_ _<_
≤-<-connex m n with m ≤? n
... | yes m≤n = inj₁ m≤n
... | no ¬m≤n = inj₂ (≰⇒> ¬m≤n)
≥->-connex : Connex _≥_ _>_
≥->-connex = flip ≤-<-connex
<-≤-connex : Connex _<_ _≤_
<-≤-connex = flip-Connex ≤-<-connex
>-≥-connex : Connex _>_ _≥_
>-≥-connex = flip-Connex ≥->-connex
<-irrefl : Irreflexive _≡_ _<_
<-irrefl refl (s<s n<n) = <-irrefl refl n<n
<-asym : Asymmetric _<_
<-asym (s<s n<m) (s<s m<n) = <-asym n<m m<n
<-trans : Transitive _<_
<-trans (s≤s i≤j) (s≤s j<k) = s≤s (≤-trans i≤j (≤-trans (n≤1+n _) j<k))
<-transʳ : Trans _≤_ _<_ _<_
<-transʳ m≤n (s<s n≤o) = s≤s (≤-trans m≤n n≤o)
<-transˡ : Trans _<_ _≤_ _<_
<-transˡ (s<s m≤n) (s≤s n≤o) = s≤s (≤-trans m≤n n≤o)
<-cmp : Trichotomous _≡_ _<_
<-cmp m n with m ≟ n | T? (m <ᵇ n)
... | yes m≡n | _ = tri≈ (<-irrefl m≡n) m≡n (<-irrefl (sym m≡n))
... | no m≢n | yes m<n = tri< (<ᵇ⇒< m n m<n) m≢n (<⇒≯ (<ᵇ⇒< m n m<n))
... | no m≢n | no m≮n = tri> (m≮n ∘ <⇒<ᵇ) m≢n (≤∧≢⇒< (≮⇒≥ (m≮n ∘ <⇒<ᵇ)) (m≢n ∘ sym))
infix 4 _<?_ _>?_
_<?_ : Decidable _<_
m <? n = suc m ≤? n
_>?_ : Decidable _>_
_>?_ = flip _<?_
<-irrelevant : Irrelevant _<_
<-irrelevant = ≤-irrelevant
<-resp₂-≡ : _<_ Respects₂ _≡_
<-resp₂-≡ = subst (_ <_) , subst (_< _)
<-isStrictPartialOrder : IsStrictPartialOrder _≡_ _<_
<-isStrictPartialOrder = record
{ isEquivalence = isEquivalence
; irrefl = <-irrefl
; trans = <-trans
; <-resp-≈ = <-resp₂-≡
}
<-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
<-isStrictTotalOrder = record
{ isEquivalence = isEquivalence
; trans = <-trans
; compare = <-cmp
}
<-strictPartialOrder : StrictPartialOrder 0ℓ 0ℓ 0ℓ
<-strictPartialOrder = record
{ isStrictPartialOrder = <-isStrictPartialOrder
}
<-strictTotalOrder : StrictTotalOrder 0ℓ 0ℓ 0ℓ
<-strictTotalOrder = record
{ isStrictTotalOrder = <-isStrictTotalOrder
}
s<s-injective : ∀ {m n} {p q : m < n} → s<s p ≡ s<s q → p ≡ q
s<s-injective refl = refl
<-pred : ∀ {m n} → suc m < suc n → m < n
<-pred (s<s m<n) = m<n
m<n⇒m<1+n : ∀ {m n} → m < n → m < 1 + n
m<n⇒m<1+n z<s = z<s
m<n⇒m<1+n (s<s m<n@(s≤s _)) = s<s (m<n⇒m<1+n m<n)
n≮0 : ∀ {n} → n ≮ 0
n≮0 ()
n≮n : ∀ n → n ≮ n
n≮n n = <-irrefl (refl {x = n})
0<1+n : ∀ {n} → 0 < suc n
0<1+n = z<s
n<1+n : ∀ n → n < suc n
n<1+n n = ≤-refl
n<1⇒n≡0 : ∀ {n} → n < 1 → n ≡ 0
n<1⇒n≡0 (s≤s n≤0) = n≤0⇒n≡0 n≤0
n>0⇒n≢0 : ∀ {n} → n > 0 → n ≢ 0
n>0⇒n≢0 {suc n} _ ()
n≢0⇒n>0 : ∀ {n} → n ≢ 0 → n > 0
n≢0⇒n>0 {zero} 0≢0 = contradiction refl 0≢0
n≢0⇒n>0 {suc n} _ = 0<1+n
m<n⇒0<n : ∀ {m n} → m < n → 0 < n
m<n⇒0<n = ≤-trans 0<1+n
m<n⇒n≢0 : ∀ {m n} → m < n → n ≢ 0
m<n⇒n≢0 (s≤s m≤n) ()
m<n⇒m≤1+n : ∀ {m n} → m < n → m ≤ suc n
m<n⇒m≤1+n = m≤n⇒m≤1+n ∘ <⇒≤
m<1+n⇒m<n∨m≡n : ∀ {m n} → m < suc n → m < n ⊎ m ≡ n
m<1+n⇒m<n∨m≡n {0} {0} _ = inj₂ refl
m<1+n⇒m<n∨m≡n {0} {suc n} _ = inj₁ 0<1+n
m<1+n⇒m<n∨m≡n {suc m} {suc n} (s<s m<1+n) with m<1+n⇒m<n∨m≡n m<1+n
... | inj₂ m≡n = inj₂ (cong suc m≡n)
... | inj₁ m<n = inj₁ (s<s m<n)
m≤n⇒m<n∨m≡n : ∀ {m n} → m ≤ n → m < n ⊎ m ≡ n
m≤n⇒m<n∨m≡n m≤n = m<1+n⇒m<n∨m≡n (s≤s m≤n)
m<1+n⇒m≤n : ∀ {m n} → m < suc n → m ≤ n
m<1+n⇒m≤n (s≤s m≤n) = m≤n
∀[m≤n⇒m≢o]⇒n<o : ∀ n o → (∀ {m} → m ≤ n → m ≢ o) → n < o
∀[m≤n⇒m≢o]⇒n<o _ zero m≤n⇒n≢0 = contradiction refl (m≤n⇒n≢0 z≤n)
∀[m≤n⇒m≢o]⇒n<o zero (suc o) _ = 0<1+n
∀[m≤n⇒m≢o]⇒n<o (suc n) (suc o) m≤n⇒n≢o = s≤s (∀[m≤n⇒m≢o]⇒n<o n o rec)
where
rec : ∀ {m} → m ≤ n → m ≢ o
rec m≤n refl = m≤n⇒n≢o (s≤s m≤n) refl
∀[m<n⇒m≢o]⇒n≤o : ∀ n o → (∀ {m} → m < n → m ≢ o) → n ≤ o
∀[m<n⇒m≢o]⇒n≤o zero n _ = z≤n
∀[m<n⇒m≢o]⇒n≤o (suc n) zero m<n⇒m≢0 = contradiction refl (m<n⇒m≢0 0<1+n)
∀[m<n⇒m≢o]⇒n≤o (suc n) (suc o) m<n⇒m≢o = s≤s (∀[m<n⇒m≢o]⇒n≤o n o rec)
where
rec : ∀ {m} → m < n → m ≢ o
rec x<m refl = m<n⇒m≢o (s≤s x<m) refl
module ≤-Reasoning where
open import Relation.Binary.Reasoning.Base.Triple
≤-isPreorder
<-trans
(resp₂ _<_)
<⇒≤
<-transˡ
<-transʳ
public
hiding (step-≈; step-≈˘)
open ≤-Reasoning
+-suc : ∀ m n → m + suc n ≡ suc (m + n)
+-suc zero n = refl
+-suc (suc m) n = cong suc (+-suc m n)
+-assoc : Associative _+_
+-assoc zero _ _ = refl
+-assoc (suc m) n o = cong suc (+-assoc m n o)
+-identityˡ : LeftIdentity 0 _+_
+-identityˡ _ = refl
+-identityʳ : RightIdentity 0 _+_
+-identityʳ zero = refl
+-identityʳ (suc n) = cong suc (+-identityʳ n)
+-identity : Identity 0 _+_
+-identity = +-identityˡ , +-identityʳ
+-comm : Commutative _+_
+-comm zero n = sym (+-identityʳ n)
+-comm (suc m) n = begin-equality
suc m + n ≡⟨⟩
suc (m + n) ≡⟨ cong suc (+-comm m n) ⟩
suc (n + m) ≡⟨ sym (+-suc n m) ⟩
n + suc m ∎
+-cancelˡ-≡ : LeftCancellative _≡_ _+_
+-cancelˡ-≡ zero _ _ eq = eq
+-cancelˡ-≡ (suc m) _ _ eq = +-cancelˡ-≡ m _ _ (cong pred eq)
+-cancelʳ-≡ : RightCancellative _≡_ _+_
+-cancelʳ-≡ = comm+cancelˡ⇒cancelʳ +-comm +-cancelˡ-≡
+-cancel-≡ : Cancellative _≡_ _+_
+-cancel-≡ = +-cancelˡ-≡ , +-cancelʳ-≡
+-isMagma : IsMagma _+_
+-isMagma = record
{ isEquivalence = isEquivalence
; ∙-cong = cong₂ _+_
}
+-isSemigroup : IsSemigroup _+_
+-isSemigroup = record
{ isMagma = +-isMagma
; assoc = +-assoc
}
+-isCommutativeSemigroup : IsCommutativeSemigroup _+_
+-isCommutativeSemigroup = record
{ isSemigroup = +-isSemigroup
; comm = +-comm
}
+-0-isMonoid : IsMonoid _+_ 0
+-0-isMonoid = record
{ isSemigroup = +-isSemigroup
; identity = +-identity
}
+-0-isCommutativeMonoid : IsCommutativeMonoid _+_ 0
+-0-isCommutativeMonoid = record
{ isMonoid = +-0-isMonoid
; comm = +-comm
}
+-magma : Magma 0ℓ 0ℓ
+-magma = record
{ isMagma = +-isMagma
}
+-semigroup : Semigroup 0ℓ 0ℓ
+-semigroup = record
{ isSemigroup = +-isSemigroup
}
+-commutativeSemigroup : CommutativeSemigroup 0ℓ 0ℓ
+-commutativeSemigroup = record
{ isCommutativeSemigroup = +-isCommutativeSemigroup
}
+-0-monoid : Monoid 0ℓ 0ℓ
+-0-monoid = record
{ isMonoid = +-0-isMonoid
}
+-0-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
+-0-commutativeMonoid = record
{ isCommutativeMonoid = +-0-isCommutativeMonoid
}
∸-magma : Magma 0ℓ 0ℓ
∸-magma = magma _∸_
m≢1+m+n : ∀ m {n} → m ≢ suc (m + n)
m≢1+m+n (suc m) eq = m≢1+m+n m (cong pred eq)
m≢1+n+m : ∀ m {n} → m ≢ suc (n + m)
m≢1+n+m m m≡1+n+m = m≢1+m+n m (trans m≡1+n+m (cong suc (+-comm _ m)))
m+1+n≢m : ∀ m {n} → m + suc n ≢ m
m+1+n≢m (suc m) = (m+1+n≢m m) ∘ suc-injective
m+1+n≢n : ∀ m {n} → m + suc n ≢ n
m+1+n≢n m {n} rewrite +-suc m n = ≢-sym (m≢1+n+m n)
m+1+n≢0 : ∀ m {n} → m + suc n ≢ 0
m+1+n≢0 m {n} rewrite +-suc m n = λ()
m+n≡0⇒m≡0 : ∀ m {n} → m + n ≡ 0 → m ≡ 0
m+n≡0⇒m≡0 zero eq = refl
m+n≡0⇒n≡0 : ∀ m {n} → m + n ≡ 0 → n ≡ 0
m+n≡0⇒n≡0 m {n} m+n≡0 = m+n≡0⇒m≡0 n (trans (+-comm n m) (m+n≡0))
+-cancelˡ-≤ : LeftCancellative _≤_ _+_
+-cancelˡ-≤ zero _ _ le = le
+-cancelˡ-≤ (suc m) _ _ (s≤s le) = +-cancelˡ-≤ m _ _ le
+-cancelʳ-≤ : RightCancellative _≤_ _+_
+-cancelʳ-≤ m n o le =
+-cancelˡ-≤ m _ _ (subst₂ _≤_ (+-comm n m) (+-comm o m) le)
+-cancel-≤ : Cancellative _≤_ _+_
+-cancel-≤ = +-cancelˡ-≤ , +-cancelʳ-≤
+-cancelˡ-< : LeftCancellative _<_ _+_
+-cancelˡ-< m n o = +-cancelˡ-≤ m (suc n) o ∘ subst (_≤ m + o) (sym (+-suc m n))
+-cancelʳ-< : RightCancellative _<_ _+_
+-cancelʳ-< m n o n+m<o+m = +-cancelʳ-≤ m (suc n) o n+m<o+m
+-cancel-< : Cancellative _<_ _+_
+-cancel-< = +-cancelˡ-< , +-cancelʳ-<
m≤n⇒m≤o+n : ∀ {m n} o → m ≤ n → m ≤ o + n
m≤n⇒m≤o+n zero m≤n = m≤n
m≤n⇒m≤o+n (suc o) m≤n = m≤n⇒m≤1+n (m≤n⇒m≤o+n o m≤n)
m≤n⇒m≤n+o : ∀ {m n} o → m ≤ n → m ≤ n + o
m≤n⇒m≤n+o {m} o m≤n = subst (m ≤_) (+-comm o _) (m≤n⇒m≤o+n o m≤n)
m≤m+n : ∀ m n → m ≤ m + n
m≤m+n zero n = z≤n
m≤m+n (suc m) n = s≤s (m≤m+n m n)
m≤n+m : ∀ m n → m ≤ n + m
m≤n+m m n = subst (m ≤_) (+-comm m n) (m≤m+n m n)
m+n≤o⇒m≤o : ∀ m {n o} → m + n ≤ o → m ≤ o
m+n≤o⇒m≤o zero m+n≤o = z≤n
m+n≤o⇒m≤o (suc m) (s≤s m+n≤o) = s≤s (m+n≤o⇒m≤o m m+n≤o)
m+n≤o⇒n≤o : ∀ m {n o} → m + n ≤ o → n ≤ o
m+n≤o⇒n≤o zero n≤o = n≤o
m+n≤o⇒n≤o (suc m) m+n<o = m+n≤o⇒n≤o m (<⇒≤ m+n<o)
+-mono-≤ : _+_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
+-mono-≤ {_} {m} z≤n o≤p = ≤-trans o≤p (m≤n+m _ m)
+-mono-≤ {_} {_} (s≤s m≤n) o≤p = s≤s (+-mono-≤ m≤n o≤p)
+-monoˡ-≤ : ∀ n → (_+ n) Preserves _≤_ ⟶ _≤_
+-monoˡ-≤ n m≤o = +-mono-≤ m≤o (≤-refl {n})
+-monoʳ-≤ : ∀ n → (n +_) Preserves _≤_ ⟶ _≤_
+-monoʳ-≤ n m≤o = +-mono-≤ (≤-refl {n}) m≤o
+-mono-<-≤ : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_
+-mono-<-≤ {_} {suc n} z<s o≤p = s≤s (m≤n⇒m≤o+n n o≤p)
+-mono-<-≤ {_} {_} (s<s m<n@(s≤s _)) o≤p = s≤s (+-mono-<-≤ m<n o≤p)
+-mono-≤-< : _+_ Preserves₂ _≤_ ⟶ _<_ ⟶ _<_
+-mono-≤-< {_} {n} z≤n o<p = ≤-trans o<p (m≤n+m _ n)
+-mono-≤-< {_} {_} (s≤s m≤n) o<p = s≤s (+-mono-≤-< m≤n o<p)
+-mono-< : _+_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
+-mono-< m≤n = +-mono-≤-< (<⇒≤ m≤n)
+-monoˡ-< : ∀ n → (_+ n) Preserves _<_ ⟶ _<_
+-monoˡ-< n = +-monoˡ-≤ n
+-monoʳ-< : ∀ n → (n +_) Preserves _<_ ⟶ _<_
+-monoʳ-< zero m≤o = m≤o
+-monoʳ-< (suc n) m≤o = s≤s (+-monoʳ-< n m≤o)
m+1+n≰m : ∀ m {n} → m + suc n ≰ m
m+1+n≰m (suc m) (s≤s m+1+n≤m) = m+1+n≰m m m+1+n≤m
m<m+n : ∀ m {n} → n > 0 → m < m + n
m<m+n zero n>0 = n>0
m<m+n (suc m) n>0 = s<s (m<m+n m n>0)
m<n+m : ∀ m {n} → n > 0 → m < n + m
m<n+m m {n} n>0 rewrite +-comm n m = m<m+n m n>0
m+n≮n : ∀ m n → m + n ≮ n
m+n≮n zero n = n≮n n
m+n≮n (suc m) (suc n) (s<s m+n<n) = m+n≮n m (suc n) (m<n⇒m<1+n m+n<n)
m+n≮m : ∀ m n → m + n ≮ m
m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)
*-suc : ∀ m n → m * suc n ≡ m + m * n
*-suc zero n = refl
*-suc (suc m) n = begin-equality
suc m * suc n ≡⟨⟩
suc n + m * suc n ≡⟨ cong (suc n +_) (*-suc m n) ⟩
suc n + (m + m * n) ≡⟨⟩
suc (n + (m + m * n)) ≡⟨ cong suc (sym (+-assoc n m (m * n))) ⟩
suc (n + m + m * n) ≡⟨ cong (λ x → suc (x + m * n)) (+-comm n m) ⟩
suc (m + n + m * n) ≡⟨ cong suc (+-assoc m n (m * n)) ⟩
suc (m + (n + m * n)) ≡⟨⟩
suc m + suc m * n ∎
*-identityˡ : LeftIdentity 1 _*_
*-identityˡ n = +-identityʳ n
*-identityʳ : RightIdentity 1 _*_
*-identityʳ zero = refl
*-identityʳ (suc n) = cong suc (*-identityʳ n)
*-identity : Identity 1 _*_
*-identity = *-identityˡ , *-identityʳ
*-zeroˡ : LeftZero 0 _*_
*-zeroˡ _ = refl
*-zeroʳ : RightZero 0 _*_
*-zeroʳ zero = refl
*-zeroʳ (suc n) = *-zeroʳ n
*-zero : Zero 0 _*_
*-zero = *-zeroˡ , *-zeroʳ
*-comm : Commutative _*_
*-comm zero n = sym (*-zeroʳ n)
*-comm (suc m) n = begin-equality
suc m * n ≡⟨⟩
n + m * n ≡⟨ cong (n +_) (*-comm m n) ⟩
n + n * m ≡⟨ sym (*-suc n m) ⟩
n * suc m ∎
*-distribʳ-+ : _*_ DistributesOverʳ _+_
*-distribʳ-+ m zero o = refl
*-distribʳ-+ m (suc n) o = begin-equality
(suc n + o) * m ≡⟨⟩
m + (n + o) * m ≡⟨ cong (m +_) (*-distribʳ-+ m n o) ⟩
m + (n * m + o * m) ≡⟨ sym (+-assoc m (n * m) (o * m)) ⟩
m + n * m + o * m ≡⟨⟩
suc n * m + o * m ∎
*-distribˡ-+ : _*_ DistributesOverˡ _+_
*-distribˡ-+ = comm+distrʳ⇒distrˡ *-comm *-distribʳ-+
*-distrib-+ : _*_ DistributesOver _+_
*-distrib-+ = *-distribˡ-+ , *-distribʳ-+
*-assoc : Associative _*_
*-assoc zero n o = refl
*-assoc (suc m) n o = begin-equality
(suc m * n) * o ≡⟨⟩
(n + m * n) * o ≡⟨ *-distribʳ-+ o n (m * n) ⟩
n * o + (m * n) * o ≡⟨ cong (n * o +_) (*-assoc m n o) ⟩
n * o + m * (n * o) ≡⟨⟩
suc m * (n * o) ∎
*-isMagma : IsMagma _*_
*-isMagma = record
{ isEquivalence = isEquivalence
; ∙-cong = cong₂ _*_
}
*-isSemigroup : IsSemigroup _*_
*-isSemigroup = record
{ isMagma = *-isMagma
; assoc = *-assoc
}
*-isCommutativeSemigroup : IsCommutativeSemigroup _*_
*-isCommutativeSemigroup = record
{ isSemigroup = *-isSemigroup
; comm = *-comm
}
*-1-isMonoid : IsMonoid _*_ 1
*-1-isMonoid = record
{ isSemigroup = *-isSemigroup
; identity = *-identity
}
*-1-isCommutativeMonoid : IsCommutativeMonoid _*_ 1
*-1-isCommutativeMonoid = record
{ isMonoid = *-1-isMonoid
; comm = *-comm
}
+-*-isSemiring : IsSemiring _+_ _*_ 0 1
+-*-isSemiring = record
{ isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = +-0-isCommutativeMonoid
; *-cong = cong₂ _*_
; *-assoc = *-assoc
; *-identity = *-identity
; distrib = *-distrib-+
}
; zero = *-zero
}
+-*-isCommutativeSemiring : IsCommutativeSemiring _+_ _*_ 0 1
+-*-isCommutativeSemiring = record
{ isSemiring = +-*-isSemiring
; *-comm = *-comm
}
*-magma : Magma 0ℓ 0ℓ
*-magma = record
{ isMagma = *-isMagma
}
*-semigroup : Semigroup 0ℓ 0ℓ
*-semigroup = record
{ isSemigroup = *-isSemigroup
}
*-commutativeSemigroup : CommutativeSemigroup 0ℓ 0ℓ
*-commutativeSemigroup = record
{ isCommutativeSemigroup = *-isCommutativeSemigroup
}
*-1-monoid : Monoid 0ℓ 0ℓ
*-1-monoid = record
{ isMonoid = *-1-isMonoid
}
*-1-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
*-1-commutativeMonoid = record
{ isCommutativeMonoid = *-1-isCommutativeMonoid
}
+-*-semiring : Semiring 0ℓ 0ℓ
+-*-semiring = record
{ isSemiring = +-*-isSemiring
}
+-*-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ
+-*-commutativeSemiring = record
{ isCommutativeSemiring = +-*-isCommutativeSemiring
}
*-cancelʳ-≡ : ∀ m n o .{{_ : NonZero o}} → m * o ≡ n * o → m ≡ n
*-cancelʳ-≡ zero zero (suc o) eq = refl
*-cancelʳ-≡ (suc m) (suc n) (suc o) eq =
cong suc (*-cancelʳ-≡ m n (suc o) (+-cancelˡ-≡ (suc o) (m * suc o) (n * suc o) eq))
*-cancelˡ-≡ : ∀ m n o .{{_ : NonZero o}} → o * m ≡ o * n → m ≡ n
*-cancelˡ-≡ m n o rewrite *-comm o m | *-comm o n = *-cancelʳ-≡ m n o
m*n≡0⇒m≡0∨n≡0 : ∀ m {n} → m * n ≡ 0 → m ≡ 0 ⊎ n ≡ 0
m*n≡0⇒m≡0∨n≡0 zero {n} eq = inj₁ refl
m*n≡0⇒m≡0∨n≡0 (suc m) {zero} eq = inj₂ refl
m*n≢0 : ∀ m n → .{{_ : NonZero m}} .{{_ : NonZero n}} → NonZero (m * n)
m*n≢0 (suc m) (suc n) = _
m*n≡0⇒m≡0 : ∀ m n .{{_ : NonZero n}} → m * n ≡ 0 → m ≡ 0
m*n≡0⇒m≡0 zero (suc _) eq = refl
m*n≡1⇒m≡1 : ∀ m n → m * n ≡ 1 → m ≡ 1
m*n≡1⇒m≡1 (suc zero) n _ = refl
m*n≡1⇒m≡1 (suc (suc m)) (suc zero) ()
m*n≡1⇒m≡1 (suc (suc m)) zero eq =
contradiction (trans (sym $ *-zeroʳ m) eq) λ()
m*n≡1⇒n≡1 : ∀ m n → m * n ≡ 1 → n ≡ 1
m*n≡1⇒n≡1 m n eq = m*n≡1⇒m≡1 n m (trans (*-comm n m) eq)
[m*n]*[o*p]≡[m*o]*[n*p] : ∀ m n o p → (m * n) * (o * p) ≡ (m * o) * (n * p)
[m*n]*[o*p]≡[m*o]*[n*p] m n o p = begin-equality
(m * n) * (o * p) ≡⟨ *-assoc m n (o * p) ⟩
m * (n * (o * p)) ≡⟨ cong (m *_) (x∙yz≈y∙xz n o p) ⟩
m * (o * (n * p)) ≡˘⟨ *-assoc m o (n * p) ⟩
(m * o) * (n * p) ∎
where open CommSemigroupProperties *-commutativeSemigroup
*-cancelʳ-≤ : ∀ m n o .{{_ : NonZero o}} → m * o ≤ n * o → m ≤ n
*-cancelʳ-≤ zero _ (suc o) _ = z≤n
*-cancelʳ-≤ (suc m) (suc n) (suc o) le =
s≤s (*-cancelʳ-≤ m n (suc o) (+-cancelˡ-≤ _ _ _ le))
*-cancelˡ-≤ : ∀ {m n} 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-≤ (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ʳ-≤ : ∀ n → (n *_) Preserves _≤_ ⟶ _≤_
*-monoʳ-≤ n m≤o = *-mono-≤ (≤-refl {n}) m≤o
*-mono-< : _*_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
*-mono-< z<s u<v@(s≤s _) = 0<1+n
*-mono-< (s<s m<n@(s≤s _)) u<v@(s≤s _) = +-mono-< u<v (*-mono-< m<n u<v)
*-monoˡ-< : ∀ n .{{_ : NonZero n}} → (_* n) Preserves _<_ ⟶ _<_
*-monoˡ-< (suc n) z<s = 0<1+n
*-monoˡ-< (suc n) (s<s m<o@(s≤s _)) =
+-mono-≤-< (≤-refl {suc n}) (*-monoˡ-< (suc n) m<o)
*-monoʳ-< : ∀ n .{{_ : NonZero n}} → (n *_) Preserves _<_ ⟶ _<_
*-monoʳ-< (suc zero) m<o@(s≤s _) = +-mono-≤ m<o z≤n
*-monoʳ-< (suc n@(suc _)) m<o@(s≤s _) =
+-mono-≤ m<o (<⇒≤ (*-monoʳ-< n m<o))
m≤m*n : ∀ m n .{{_ : NonZero n}} → m ≤ m * n
m≤m*n m n@(suc _) = begin
m ≡⟨ sym (*-identityʳ m) ⟩
m * 1 ≤⟨ *-monoʳ-≤ m 0<1+n ⟩
m * n ∎
m≤n*m : ∀ m n .{{_ : NonZero n}} → m ≤ n * m
m≤n*m m n@(suc _) = begin
m ≤⟨ m≤m*n m n ⟩
m * n ≡⟨ *-comm m n ⟩
n * m ∎
m<m*n : ∀ m n .{{_ : NonZero m}} → 1 < n → m < m * n
m<m*n m@(suc m-1) n@(suc (suc n-2)) (s≤s (s≤s _)) = begin-strict
m <⟨ s≤s (s≤s (m≤n+m m-1 n-2)) ⟩
n + m-1 ≤⟨ +-monoʳ-≤ n (m≤m*n m-1 n) ⟩
n + m-1 * n ≡⟨⟩
m * n ∎
m<n⇒m<n*o : ∀ {m n} o .{{_ : NonZero o}} → m < n → m < n * o
m<n⇒m<n*o {m} {n} o m<n = <-transˡ m<n (m≤m*n n o)
m<n⇒m<o*n : ∀ {m n} o .{{_ : NonZero o}} → m < n → m < o * n
m<n⇒m<o*n {m} {n} o m<n = begin-strict
m <⟨ m<n⇒m<n*o o m<n ⟩
n * o ≡⟨ *-comm n o ⟩
o * n ∎
*-cancelʳ-< : RightCancellative _<_ _*_
*-cancelʳ-< zero zero (suc o) _ = 0<1+n
*-cancelʳ-< (suc m) zero (suc o) _ = 0<1+n
*-cancelʳ-< m (suc n) (suc o) nm<om =
s≤s (*-cancelʳ-< m n o (+-cancelˡ-< m _ _ nm<om))
*-cancelˡ-< : LeftCancellative _<_ _*_
*-cancelˡ-< x y z rewrite *-comm x y | *-comm x z = *-cancelʳ-< x y z
*-cancel-< : Cancellative _<_ _*_
*-cancel-< = *-cancelˡ-< , *-cancelʳ-<
^-identityʳ : RightIdentity 1 _^_
^-identityʳ zero = refl
^-identityʳ (suc n) = cong suc (^-identityʳ n)
^-zeroˡ : LeftZero 1 _^_
^-zeroˡ zero = refl
^-zeroˡ (suc n) = begin-equality
1 ^ suc n ≡⟨⟩
1 * (1 ^ n) ≡⟨ *-identityˡ (1 ^ n) ⟩
1 ^ n ≡⟨ ^-zeroˡ n ⟩
1 ∎
^-distribˡ-+-* : ∀ m n o → m ^ (n + o) ≡ m ^ n * m ^ o
^-distribˡ-+-* m zero o = sym (+-identityʳ (m ^ o))
^-distribˡ-+-* m (suc n) o = begin-equality
m * (m ^ (n + o)) ≡⟨ cong (m *_) (^-distribˡ-+-* m n o) ⟩
m * ((m ^ n) * (m ^ o)) ≡⟨ sym (*-assoc m _ _) ⟩
(m * (m ^ n)) * (m ^ o) ∎
^-semigroup-morphism : ∀ {n} → (n ^_) Is +-semigroup -Semigroup⟶ *-semigroup
^-semigroup-morphism = record
{ ⟦⟧-cong = cong (_ ^_)
; ∙-homo = ^-distribˡ-+-* _
}
^-monoid-morphism : ∀ {n} → (n ^_) Is +-0-monoid -Monoid⟶ *-1-monoid
^-monoid-morphism = record
{ sm-homo = ^-semigroup-morphism
; ε-homo = refl
}
^-*-assoc : ∀ m n o → (m ^ n) ^ o ≡ m ^ (n * o)
^-*-assoc m n zero = cong (m ^_) (sym $ *-zeroʳ n)
^-*-assoc m n (suc o) = begin-equality
(m ^ n) * ((m ^ n) ^ o) ≡⟨ cong ((m ^ n) *_) (^-*-assoc m n o) ⟩
(m ^ n) * (m ^ (n * o)) ≡⟨ sym (^-distribˡ-+-* m n (n * o)) ⟩
m ^ (n + n * o) ≡⟨ cong (m ^_) (sym (*-suc n o)) ⟩
m ^ (n * (suc o)) ∎
m^n≡0⇒m≡0 : ∀ m n → m ^ n ≡ 0 → m ≡ 0
m^n≡0⇒m≡0 m (suc n) eq = [ id , m^n≡0⇒m≡0 m n ]′ (m*n≡0⇒m≡0∨n≡0 m eq)
m^n≡1⇒n≡0∨m≡1 : ∀ m n → m ^ n ≡ 1 → n ≡ 0 ⊎ m ≡ 1
m^n≡1⇒n≡0∨m≡1 m zero _ = inj₁ refl
m^n≡1⇒n≡0∨m≡1 m (suc n) eq = inj₂ (m*n≡1⇒m≡1 m (m ^ n) eq)
m^n≢0 : ∀ m n .{{_ : NonZero m}} → NonZero (m ^ n)
m^n≢0 m n = ≢-nonZero (≢-nonZero⁻¹ m ∘′ m^n≡0⇒m≡0 m n)
m^n>0 : ∀ 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ˡ-≤ 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 {_} {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ˡ-< (suc zero) m<o = *-monoˡ-< 1 m<o
^-monoˡ-< (suc n@(suc _)) m<o = *-mono-< m<o (^-monoˡ-< n m<o)
^-monoʳ-< : ∀ m → 1 < m → (m ^_) Preserves _<_ ⟶ _<_
^-monoʳ-< m@(suc _) 1<m {zero} {suc o} z<s = *-mono-≤ 1<m (m^n>0 m o)
^-monoʳ-< m@(suc _) 1<m {suc n} {suc o} (s<s n<o) = *-monoʳ-< m (^-monoʳ-< m 1<m n<o)
m≤n⇒m⊔n≡n : ∀ {m n} → m ≤ n → m ⊔ n ≡ n
m≤n⇒m⊔n≡n {zero} _ = refl
m≤n⇒m⊔n≡n {suc m} (s≤s m≤n) = cong suc (m≤n⇒m⊔n≡n m≤n)
m≥n⇒m⊔n≡m : ∀ {m n} → m ≥ n → m ⊔ n ≡ m
m≥n⇒m⊔n≡m {zero} {zero} z≤n = refl
m≥n⇒m⊔n≡m {suc m} {zero} z≤n = refl
m≥n⇒m⊔n≡m {suc m} {suc n} (s≤s m≥n) = cong suc (m≥n⇒m⊔n≡m m≥n)
m≤n⇒m⊓n≡m : ∀ {m n} → m ≤ n → m ⊓ n ≡ m
m≤n⇒m⊓n≡m {zero} z≤n = refl
m≤n⇒m⊓n≡m {suc m} (s≤s m≤n) = cong suc (m≤n⇒m⊓n≡m m≤n)
m≥n⇒m⊓n≡n : ∀ {m n} → m ≥ n → m ⊓ n ≡ n
m≥n⇒m⊓n≡n {zero} {zero} z≤n = refl
m≥n⇒m⊓n≡n {suc m} {zero} z≤n = refl
m≥n⇒m⊓n≡n {suc m} {suc n} (s≤s m≤n) = cong suc (m≥n⇒m⊓n≡n m≤n)
⊓-operator : MinOperator ≤-totalPreorder
⊓-operator = record
{ x≤y⇒x⊓y≈x = m≤n⇒m⊓n≡m
; x≥y⇒x⊓y≈y = m≥n⇒m⊓n≡n
}
⊔-operator : MaxOperator ≤-totalPreorder
⊔-operator = record
{ x≤y⇒x⊔y≈y = m≤n⇒m⊔n≡n
; x≥y⇒x⊔y≈x = m≥n⇒m⊔n≡m
}
⊔≡⊔′ : ∀ m n → m ⊔ n ≡ m ⊔′ n
⊔≡⊔′ m n with m <ᵇ n in eq
... | false = m≥n⇒m⊔n≡m (≮⇒≥ (λ m<n → subst T eq (<⇒<ᵇ m<n)))
... | true = m≤n⇒m⊔n≡n (<⇒≤ (<ᵇ⇒< m n (subst T (sym eq) _)))
⊓≡⊓′ : ∀ m n → m ⊓ n ≡ m ⊓′ n
⊓≡⊓′ m n with m <ᵇ n in eq
... | false = m≥n⇒m⊓n≡n (≮⇒≥ (λ m<n → subst T eq (<⇒<ᵇ m<n)))
... | true = m≤n⇒m⊓n≡m (<⇒≤ (<ᵇ⇒< m n (subst T (sym eq) _)))
private
module ⊓-⊔-properties = MinMaxOp ⊓-operator ⊔-operator
module ⊓-⊔-latticeProperties = LatticeMinMaxOp ⊓-operator ⊔-operator
open ⊓-⊔-properties public
using
( ⊓-idem
; ⊓-sel
; ⊓-assoc
; ⊓-comm
; ⊔-idem
; ⊔-sel
; ⊔-assoc
; ⊔-comm
; ⊓-distribˡ-⊔
; ⊓-distribʳ-⊔
; ⊓-distrib-⊔
; ⊔-distribˡ-⊓
; ⊔-distribʳ-⊓
; ⊔-distrib-⊓
; ⊓-absorbs-⊔
; ⊔-absorbs-⊓
; ⊔-⊓-absorptive
; ⊓-⊔-absorptive
; ⊓-isMagma
; ⊓-isSemigroup
; ⊓-isCommutativeSemigroup
; ⊓-isBand
; ⊓-isSelectiveMagma
; ⊔-isMagma
; ⊔-isSemigroup
; ⊔-isCommutativeSemigroup
; ⊔-isBand
; ⊔-isSelectiveMagma
; ⊓-magma
; ⊓-semigroup
; ⊓-band
; ⊓-commutativeSemigroup
; ⊓-selectiveMagma
; ⊔-magma
; ⊔-semigroup
; ⊔-band
; ⊔-commutativeSemigroup
; ⊔-selectiveMagma
; ⊓-glb
; ⊓-triangulate
; ⊓-mono-≤
; ⊓-monoˡ-≤
; ⊓-monoʳ-≤
; ⊔-lub
; ⊔-triangulate
; ⊔-mono-≤
; ⊔-monoˡ-≤
; ⊔-monoʳ-≤
)
renaming
( x⊓y≈y⇒y≤x to m⊓n≡n⇒n≤m
; x⊓y≈x⇒x≤y to m⊓n≡m⇒m≤n
; x⊓y≤x to m⊓n≤m
; x⊓y≤y to m⊓n≤n
; x≤y⇒x⊓z≤y to m≤n⇒m⊓o≤n
; x≤y⇒z⊓x≤y to m≤n⇒o⊓m≤n
; x≤y⊓z⇒x≤y to m≤n⊓o⇒m≤n
; x≤y⊓z⇒x≤z to m≤n⊓o⇒m≤o
; x⊔y≈y⇒x≤y to m⊔n≡n⇒m≤n
; x⊔y≈x⇒y≤x to m⊔n≡m⇒n≤m
; x≤x⊔y to m≤m⊔n
; x≤y⊔x to m≤n⊔m
; x≤y⇒x≤y⊔z to m≤n⇒m≤n⊔o
; x≤y⇒x≤z⊔y to m≤n⇒m≤o⊔n
; x⊔y≤z⇒x≤z to m⊔n≤o⇒m≤o
; x⊔y≤z⇒y≤z to m⊔n≤o⇒n≤o
; x⊓y≤x⊔y to m⊓n≤m⊔n
)
open ⊓-⊔-latticeProperties public
using
( ⊓-isSemilattice
; ⊔-isSemilattice
; ⊔-⊓-isLattice
; ⊓-⊔-isLattice
; ⊔-⊓-isDistributiveLattice
; ⊓-⊔-isDistributiveLattice
; ⊓-semilattice
; ⊔-semilattice
; ⊔-⊓-lattice
; ⊓-⊔-lattice
; ⊔-⊓-distributiveLattice
; ⊓-⊔-distributiveLattice
)
⊔-identityˡ : LeftIdentity 0 _⊔_
⊔-identityˡ _ = refl
⊔-identityʳ : RightIdentity 0 _⊔_
⊔-identityʳ zero = refl
⊔-identityʳ (suc n) = refl
⊔-identity : Identity 0 _⊔_
⊔-identity = ⊔-identityˡ , ⊔-identityʳ
⊔-0-isMonoid : IsMonoid _⊔_ 0
⊔-0-isMonoid = record
{ isSemigroup = ⊔-isSemigroup
; identity = ⊔-identity
}
⊔-0-isCommutativeMonoid : IsCommutativeMonoid _⊔_ 0
⊔-0-isCommutativeMonoid = record
{ isMonoid = ⊔-0-isMonoid
; comm = ⊔-comm
}
⊔-0-monoid : Monoid 0ℓ 0ℓ
⊔-0-monoid = record
{ isMonoid = ⊔-0-isMonoid
}
⊔-0-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
⊔-0-commutativeMonoid = record
{ isCommutativeMonoid = ⊔-0-isCommutativeMonoid
}
mono-≤-distrib-⊔ : ∀ {f} → f Preserves _≤_ ⟶ _≤_ →
∀ m n → f (m ⊔ n) ≡ f m ⊔ f n
mono-≤-distrib-⊔ {f} = ⊓-⊔-properties.mono-≤-distrib-⊔ (cong f)
mono-≤-distrib-⊓ : ∀ {f} → f Preserves _≤_ ⟶ _≤_ →
∀ m n → f (m ⊓ n) ≡ f m ⊓ f n
mono-≤-distrib-⊓ {f} = ⊓-⊔-properties.mono-≤-distrib-⊓ (cong f)
antimono-≤-distrib-⊓ : ∀ {f} → f Preserves _≤_ ⟶ _≥_ →
∀ m n → f (m ⊓ n) ≡ f m ⊔ f n
antimono-≤-distrib-⊓ {f} = ⊓-⊔-properties.antimono-≤-distrib-⊓ (cong f)
antimono-≤-distrib-⊔ : ∀ {f} → f Preserves _≤_ ⟶ _≥_ →
∀ m n → f (m ⊔ n) ≡ f m ⊓ f n
antimono-≤-distrib-⊔ {f} = ⊓-⊔-properties.antimono-≤-distrib-⊔ (cong f)
m<n⇒m<n⊔o : ∀ {m n} o → m < n → m < n ⊔ o
m<n⇒m<n⊔o = m≤n⇒m≤n⊔o
m<n⇒m<o⊔n : ∀ {m n} o → m < n → m < o ⊔ n
m<n⇒m<o⊔n = m≤n⇒m≤o⊔n
m⊔n<o⇒m<o : ∀ m n {o} → m ⊔ n < o → m < o
m⊔n<o⇒m<o m n m⊔n<o = <-transʳ (m≤m⊔n m n) m⊔n<o
m⊔n<o⇒n<o : ∀ m n {o} → m ⊔ n < o → n < o
m⊔n<o⇒n<o m n m⊔n<o = <-transʳ (m≤n⊔m m n) m⊔n<o
⊔-mono-< : _⊔_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
⊔-mono-< = ⊔-mono-≤
⊔-pres-<m : ∀ {m n o} → n < m → o < m → n ⊔ o < m
⊔-pres-<m {m} n<m o<m = subst (_ <_) (⊔-idem m) (⊔-mono-< n<m o<m)
+-distribˡ-⊔ : _+_ DistributesOverˡ _⊔_
+-distribˡ-⊔ zero n o = refl
+-distribˡ-⊔ (suc m) n o = cong suc (+-distribˡ-⊔ m n o)
+-distribʳ-⊔ : _+_ DistributesOverʳ _⊔_
+-distribʳ-⊔ = comm+distrˡ⇒distrʳ +-comm +-distribˡ-⊔
+-distrib-⊔ : _+_ DistributesOver _⊔_
+-distrib-⊔ = +-distribˡ-⊔ , +-distribʳ-⊔
m⊔n≤m+n : ∀ m n → m ⊔ n ≤ m + n
m⊔n≤m+n m n with ⊔-sel m n
... | inj₁ m⊔n≡m rewrite m⊔n≡m = m≤m+n m n
... | inj₂ m⊔n≡n rewrite m⊔n≡n = m≤n+m n m
*-distribˡ-⊔ : _*_ DistributesOverˡ _⊔_
*-distribˡ-⊔ m zero o = sym (cong (_⊔ m * o) (*-zeroʳ m))
*-distribˡ-⊔ m (suc n) zero = begin-equality
m * (suc n ⊔ zero) ≡⟨⟩
m * suc n ≡˘⟨ ⊔-identityʳ (m * suc n) ⟩
m * suc n ⊔ zero ≡˘⟨ cong (m * suc n ⊔_) (*-zeroʳ m) ⟩
m * suc n ⊔ m * zero ∎
*-distribˡ-⊔ m (suc n) (suc o) = begin-equality
m * (suc n ⊔ suc o) ≡⟨⟩
m * suc (n ⊔ o) ≡⟨ *-suc m (n ⊔ o) ⟩
m + m * (n ⊔ o) ≡⟨ cong (m +_) (*-distribˡ-⊔ m n o) ⟩
m + (m * n ⊔ m * o) ≡⟨ +-distribˡ-⊔ m (m * n) (m * o) ⟩
(m + m * n) ⊔ (m + m * o) ≡˘⟨ cong₂ _⊔_ (*-suc m n) (*-suc m o) ⟩
(m * suc n) ⊔ (m * suc o) ∎
*-distribʳ-⊔ : _*_ DistributesOverʳ _⊔_
*-distribʳ-⊔ = comm+distrˡ⇒distrʳ *-comm *-distribˡ-⊔
*-distrib-⊔ : _*_ DistributesOver _⊔_
*-distrib-⊔ = *-distribˡ-⊔ , *-distribʳ-⊔
⊓-zeroˡ : LeftZero 0 _⊓_
⊓-zeroˡ _ = refl
⊓-zeroʳ : RightZero 0 _⊓_
⊓-zeroʳ zero = refl
⊓-zeroʳ (suc n) = refl
⊓-zero : Zero 0 _⊓_
⊓-zero = ⊓-zeroˡ , ⊓-zeroʳ
⊔-⊓-isSemiringWithoutOne : IsSemiringWithoutOne _⊔_ _⊓_ 0
⊔-⊓-isSemiringWithoutOne = record
{ +-isCommutativeMonoid = ⊔-0-isCommutativeMonoid
; *-cong = cong₂ _⊓_
; *-assoc = ⊓-assoc
; distrib = ⊓-distrib-⊔
; zero = ⊓-zero
}
⊔-⊓-isCommutativeSemiringWithoutOne
: IsCommutativeSemiringWithoutOne _⊔_ _⊓_ 0
⊔-⊓-isCommutativeSemiringWithoutOne = record
{ isSemiringWithoutOne = ⊔-⊓-isSemiringWithoutOne
; *-comm = ⊓-comm
}
⊔-⊓-commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne 0ℓ 0ℓ
⊔-⊓-commutativeSemiringWithoutOne = record
{ isCommutativeSemiringWithoutOne =
⊔-⊓-isCommutativeSemiringWithoutOne
}
m<n⇒m⊓o<n : ∀ {m n} o → m < n → m ⊓ o < n
m<n⇒m⊓o<n o m<n = <-transʳ (m⊓n≤m _ o) m<n
m<n⇒o⊓m<n : ∀ {m n} o → m < n → o ⊓ m < n
m<n⇒o⊓m<n o m<n = <-transʳ (m⊓n≤n o _) m<n
m<n⊓o⇒m<n : ∀ {m} n o → m < n ⊓ o → m < n
m<n⊓o⇒m<n = m≤n⊓o⇒m≤n
m<n⊓o⇒m<o : ∀ {m} n o → m < n ⊓ o → m < o
m<n⊓o⇒m<o = m≤n⊓o⇒m≤o
⊓-mono-< : _⊓_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
⊓-mono-< = ⊓-mono-≤
⊓-pres-m< : ∀ {m n o} → m < n → m < o → m < n ⊓ o
⊓-pres-m< {m} m<n m<o = subst (_< _) (⊓-idem m) (⊓-mono-< m<n m<o)
+-distribˡ-⊓ : _+_ DistributesOverˡ _⊓_
+-distribˡ-⊓ zero n o = refl
+-distribˡ-⊓ (suc m) n o = cong suc (+-distribˡ-⊓ m n o)
+-distribʳ-⊓ : _+_ DistributesOverʳ _⊓_
+-distribʳ-⊓ = comm+distrˡ⇒distrʳ +-comm +-distribˡ-⊓
+-distrib-⊓ : _+_ DistributesOver _⊓_
+-distrib-⊓ = +-distribˡ-⊓ , +-distribʳ-⊓
m⊓n≤m+n : ∀ m n → m ⊓ n ≤ m + n
m⊓n≤m+n m n with ⊓-sel m n
... | inj₁ m⊓n≡m rewrite m⊓n≡m = m≤m+n m n
... | inj₂ m⊓n≡n rewrite m⊓n≡n = m≤n+m n m
*-distribˡ-⊓ : _*_ DistributesOverˡ _⊓_
*-distribˡ-⊓ m 0 o = begin-equality
m * (0 ⊓ o) ≡⟨⟩
m * 0 ≡⟨ *-zeroʳ m ⟩
0 ≡⟨⟩
0 ⊓ (m * o) ≡˘⟨ cong (_⊓ (m * o)) (*-zeroʳ m) ⟩
(m * 0) ⊓ (m * o) ∎
*-distribˡ-⊓ m (suc n) 0 = begin-equality
m * (suc n ⊓ 0) ≡⟨⟩
m * 0 ≡⟨ *-zeroʳ m ⟩
0 ≡˘⟨ ⊓-zeroʳ (m * suc n) ⟩
(m * suc n) ⊓ 0 ≡˘⟨ cong (m * suc n ⊓_) (*-zeroʳ m) ⟩
(m * suc n) ⊓ (m * 0) ∎
*-distribˡ-⊓ m (suc n) (suc o) = begin-equality
m * (suc n ⊓ suc o) ≡⟨⟩
m * suc (n ⊓ o) ≡⟨ *-suc m (n ⊓ o) ⟩
m + m * (n ⊓ o) ≡⟨ cong (m +_) (*-distribˡ-⊓ m n o) ⟩
m + (m * n) ⊓ (m * o) ≡⟨ +-distribˡ-⊓ m (m * n) (m * o) ⟩
(m + m * n) ⊓ (m + m * o) ≡˘⟨ cong₂ _⊓_ (*-suc m n) (*-suc m o) ⟩
(m * suc n) ⊓ (m * suc o) ∎
*-distribʳ-⊓ : _*_ DistributesOverʳ _⊓_
*-distribʳ-⊓ = comm+distrˡ⇒distrʳ *-comm *-distribˡ-⊓
*-distrib-⊓ : _*_ DistributesOver _⊓_
*-distrib-⊓ = *-distribˡ-⊓ , *-distribʳ-⊓
0∸n≡0 : LeftZero zero _∸_
0∸n≡0 zero = refl
0∸n≡0 (suc _) = refl
n∸n≡0 : ∀ n → n ∸ n ≡ 0
n∸n≡0 zero = refl
n∸n≡0 (suc n) = n∸n≡0 n
pred[m∸n]≡m∸[1+n] : ∀ m n → pred (m ∸ n) ≡ m ∸ suc n
pred[m∸n]≡m∸[1+n] zero zero = refl
pred[m∸n]≡m∸[1+n] (suc m) zero = refl
pred[m∸n]≡m∸[1+n] zero (suc n) = refl
pred[m∸n]≡m∸[1+n] (suc m) (suc n) = pred[m∸n]≡m∸[1+n] m n
m∸n≤m : ∀ m n → m ∸ n ≤ m
m∸n≤m n zero = ≤-refl
m∸n≤m zero (suc n) = ≤-refl
m∸n≤m (suc m) (suc n) = ≤-trans (m∸n≤m m n) (n≤1+n m)
m≮m∸n : ∀ m n → m ≮ m ∸ n
m≮m∸n m zero = n≮n m
m≮m∸n (suc m) (suc n) = m≮m∸n m n ∘ ≤-trans (n≤1+n (suc m))
1+m≢m∸n : ∀ {m} n → suc m ≢ m ∸ n
1+m≢m∸n {m} n eq = m≮m∸n m n (≤-reflexive eq)
∸-mono : _∸_ Preserves₂ _≤_ ⟶ _≥_ ⟶ _≤_
∸-mono z≤n (s≤s n₁≥n₂) = z≤n
∸-mono (s≤s m₁≤m₂) (s≤s n₁≥n₂) = ∸-mono m₁≤m₂ n₁≥n₂
∸-mono m₁≤m₂ (z≤n {n = n₁}) = ≤-trans (m∸n≤m _ n₁) m₁≤m₂
∸-monoˡ-≤ : ∀ {m n} o → m ≤ n → m ∸ o ≤ n ∸ o
∸-monoˡ-≤ o m≤n = ∸-mono {u = o} m≤n ≤-refl
∸-monoʳ-≤ : ∀ {m n} o → m ≤ n → o ∸ m ≥ o ∸ n
∸-monoʳ-≤ _ m≤n = ∸-mono ≤-refl m≤n
∸-monoˡ-< : ∀ {m n o} → m < o → n ≤ m → m ∸ n < o ∸ n
∸-monoˡ-< {m} {zero} {o} m<o n≤m = m<o
∸-monoˡ-< {suc m} {suc n} {suc o} (s≤s m<o) (s≤s n≤m) = ∸-monoˡ-< m<o n≤m
∸-monoʳ-< : ∀ {m n o} → o < n → n ≤ m → m ∸ n < m ∸ o
∸-monoʳ-< {n = suc n} {zero} (s≤s o<n) (s≤s n<m) = s≤s (m∸n≤m _ n)
∸-monoʳ-< {n = suc n} {suc o} (s≤s o<n) (s≤s n<m) = ∸-monoʳ-< o<n n<m
∸-cancelʳ-≤ : ∀ {m n o} → m ≤ o → o ∸ n ≤ o ∸ m → m ≤ n
∸-cancelʳ-≤ {_} {_} z≤n _ = z≤n
∸-cancelʳ-≤ {suc m} {zero} (s≤s _) o<o∸m = contradiction o<o∸m (m≮m∸n _ m)
∸-cancelʳ-≤ {suc m} {suc n} (s≤s m≤o) o∸n<o∸m = s≤s (∸-cancelʳ-≤ m≤o o∸n<o∸m)
∸-cancelʳ-< : ∀ {m n o} → o ∸ m < o ∸ n → n < m
∸-cancelʳ-< {zero} {n} {o} o<o∸n = contradiction o<o∸n (m≮m∸n o n)
∸-cancelʳ-< {suc m} {zero} {_} o∸n<o∸m = 0<1+n
∸-cancelʳ-< {suc m} {suc n} {suc o} o∸n<o∸m = s≤s (∸-cancelʳ-< o∸n<o∸m)
∸-cancelˡ-≡ : ∀ {m n o} → n ≤ m → o ≤ m → m ∸ n ≡ m ∸ o → n ≡ o
∸-cancelˡ-≡ {_} z≤n z≤n _ = refl
∸-cancelˡ-≡ {o = suc o} z≤n (s≤s _) eq = contradiction eq (1+m≢m∸n o)
∸-cancelˡ-≡ {n = suc n} (s≤s _) z≤n eq = contradiction (sym eq) (1+m≢m∸n n)
∸-cancelˡ-≡ {_} (s≤s n≤m) (s≤s o≤m) eq = cong suc (∸-cancelˡ-≡ n≤m o≤m eq)
∸-cancelʳ-≡ : ∀ {m n o} → o ≤ m → o ≤ n → m ∸ o ≡ n ∸ o → m ≡ n
∸-cancelʳ-≡ z≤n z≤n eq = eq
∸-cancelʳ-≡ (s≤s o≤m) (s≤s o≤n) eq = cong suc (∸-cancelʳ-≡ o≤m o≤n eq)
m∸n≡0⇒m≤n : ∀ {m n} → m ∸ n ≡ 0 → m ≤ n
m∸n≡0⇒m≤n {zero} {_} _ = z≤n
m∸n≡0⇒m≤n {suc m} {suc n} eq = s≤s (m∸n≡0⇒m≤n eq)
m≤n⇒m∸n≡0 : ∀ {m n} → m ≤ n → m ∸ n ≡ 0
m≤n⇒m∸n≡0 {n = n} z≤n = 0∸n≡0 n
m≤n⇒m∸n≡0 {_} (s≤s m≤n) = m≤n⇒m∸n≡0 m≤n
m<n⇒0<n∸m : ∀ {m n} → m < n → 0 < n ∸ m
m<n⇒0<n∸m {zero} {suc n} _ = 0<1+n
m<n⇒0<n∸m {suc m} {suc n} (s≤s m<n) = m<n⇒0<n∸m m<n
m∸n≢0⇒n<m : ∀ {m n} → m ∸ n ≢ 0 → n < m
m∸n≢0⇒n<m {m} {n} m∸n≢0 with n <? m
... | yes n<m = n<m
... | no n≮m = contradiction (m≤n⇒m∸n≡0 (≮⇒≥ n≮m)) m∸n≢0
m>n⇒m∸n≢0 : ∀ {m n} → m > n → m ∸ n ≢ 0
m>n⇒m∸n≢0 {n = suc n} (s≤s m>n) = m>n⇒m∸n≢0 m>n
m≤n⇒n∸m≤n : ∀ {m n} → m ≤ n → n ∸ m ≤ n
m≤n⇒n∸m≤n z≤n = ≤-refl
m≤n⇒n∸m≤n (s≤s m≤n) = m≤n⇒m≤1+n (m≤n⇒n∸m≤n m≤n)
+-∸-comm : ∀ {m} n {o} → o ≤ m → (m + n) ∸ o ≡ (m ∸ o) + n
+-∸-comm {zero} _ {zero} _ = refl
+-∸-comm {suc m} _ {zero} _ = refl
+-∸-comm {suc m} n {suc o} (s≤s o≤m) = +-∸-comm n o≤m
∸-+-assoc : ∀ m n o → (m ∸ n) ∸ o ≡ m ∸ (n + o)
∸-+-assoc zero zero o = refl
∸-+-assoc zero (suc n) o = 0∸n≡0 o
∸-+-assoc (suc m) zero o = refl
∸-+-assoc (suc m) (suc n) o = ∸-+-assoc m n o
+-∸-assoc : ∀ m {n o} → o ≤ n → (m + n) ∸ o ≡ m + (n ∸ o)
+-∸-assoc m (z≤n {n = n}) = begin-equality m + n ∎
+-∸-assoc m (s≤s {m = o} {n = n} o≤n) = begin-equality
(m + suc n) ∸ suc o ≡⟨ cong (_∸ suc o) (+-suc m n) ⟩
suc (m + n) ∸ suc o ≡⟨⟩
(m + n) ∸ o ≡⟨ +-∸-assoc m o≤n ⟩
m + (n ∸ o) ∎
m+n≤o⇒m≤o∸n : ∀ m n o → m + n ≤ o → m ≤ o ∸ n
m+n≤o⇒m≤o∸n zero n o le = z≤n
m+n≤o⇒m≤o∸n (suc m) n (suc o) (s≤s le)
rewrite +-∸-assoc 1 (m+n≤o⇒n≤o m le) = s≤s (m+n≤o⇒m≤o∸n m n o le)
m≤o∸n⇒m+n≤o : ∀ m {n o} (n≤o : n ≤ o) → m ≤ o ∸ n → m + n ≤ o
m≤o∸n⇒m+n≤o m z≤n le rewrite +-identityʳ m = le
m≤o∸n⇒m+n≤o m {suc n} (s≤s n≤o) le rewrite +-suc m n = s≤s (m≤o∸n⇒m+n≤o m n≤o le)
m≤n+m∸n : ∀ m n → m ≤ n + (m ∸ n)
m≤n+m∸n zero n = z≤n
m≤n+m∸n (suc m) zero = ≤-refl
m≤n+m∸n (suc m) (suc n) = s≤s (m≤n+m∸n m n)
m+n∸n≡m : ∀ m n → m + n ∸ n ≡ m
m+n∸n≡m m n = begin-equality
(m + n) ∸ n ≡⟨ +-∸-assoc m (≤-refl {x = n}) ⟩
m + (n ∸ n) ≡⟨ cong (m +_) (n∸n≡0 n) ⟩
m + 0 ≡⟨ +-identityʳ m ⟩
m ∎
m+n∸m≡n : ∀ m n → m + n ∸ m ≡ n
m+n∸m≡n m n = trans (cong (_∸ m) (+-comm m n)) (m+n∸n≡m n m)
m+[n∸m]≡n : ∀ {m n} → m ≤ n → m + (n ∸ m) ≡ n
m+[n∸m]≡n {m} {n} m≤n = begin-equality
m + (n ∸ m) ≡⟨ sym $ +-∸-assoc m m≤n ⟩
(m + n) ∸ m ≡⟨ cong (_∸ m) (+-comm m n) ⟩
(n + m) ∸ m ≡⟨ m+n∸n≡m n m ⟩
n ∎
m∸n+n≡m : ∀ {m n} → n ≤ m → (m ∸ n) + n ≡ m
m∸n+n≡m {m} {n} n≤m = begin-equality
(m ∸ n) + n ≡⟨ sym (+-∸-comm n n≤m) ⟩
(m + n) ∸ n ≡⟨ m+n∸n≡m m n ⟩
m ∎
m∸[m∸n]≡n : ∀ {m n} → n ≤ m → m ∸ (m ∸ n) ≡ n
m∸[m∸n]≡n {m} {_} z≤n = n∸n≡0 m
m∸[m∸n]≡n {suc m} {suc n} (s≤s n≤m) = begin-equality
suc m ∸ (m ∸ n) ≡⟨ +-∸-assoc 1 (m∸n≤m m n) ⟩
suc (m ∸ (m ∸ n)) ≡⟨ cong suc (m∸[m∸n]≡n n≤m) ⟩
suc n ∎
[m+n]∸[m+o]≡n∸o : ∀ m n o → (m + n) ∸ (m + o) ≡ n ∸ o
[m+n]∸[m+o]≡n∸o zero n o = refl
[m+n]∸[m+o]≡n∸o (suc m) n o = [m+n]∸[m+o]≡n∸o m n o
*-distribʳ-∸ : _*_ DistributesOverʳ _∸_
*-distribʳ-∸ m zero zero = refl
*-distribʳ-∸ zero zero (suc o) = sym (0∸n≡0 (o * zero))
*-distribʳ-∸ (suc m) zero (suc o) = refl
*-distribʳ-∸ m (suc n) zero = refl
*-distribʳ-∸ m (suc n) (suc o) = begin-equality
(n ∸ o) * m ≡⟨ *-distribʳ-∸ m n o ⟩
n * m ∸ o * m ≡⟨ sym $ [m+n]∸[m+o]≡n∸o m _ _ ⟩
m + n * m ∸ (m + o * m) ∎
*-distribˡ-∸ : _*_ DistributesOverˡ _∸_
*-distribˡ-∸ = comm+distrʳ⇒distrˡ *-comm *-distribʳ-∸
*-distrib-∸ : _*_ DistributesOver _∸_
*-distrib-∸ = *-distribˡ-∸ , *-distribʳ-∸
even≢odd : ∀ m n → 2 * m ≢ suc (2 * n)
even≢odd (suc m) zero eq = contradiction (suc-injective eq) (m+1+n≢0 m)
even≢odd (suc m) (suc n) eq = even≢odd m n (suc-injective (begin-equality
suc (2 * m) ≡⟨ sym (+-suc m _) ⟩
m + suc (m + 0) ≡⟨ suc-injective eq ⟩
suc n + suc (n + 0) ≡⟨ cong suc (+-suc n _) ⟩
suc (suc (2 * n)) ∎))
m⊓n+n∸m≡n : ∀ m n → (m ⊓ n) + (n ∸ m) ≡ n
m⊓n+n∸m≡n zero n = refl
m⊓n+n∸m≡n (suc m) zero = refl
m⊓n+n∸m≡n (suc m) (suc n) = cong suc $ m⊓n+n∸m≡n m n
[m∸n]⊓[n∸m]≡0 : ∀ m n → (m ∸ n) ⊓ (n ∸ m) ≡ 0
[m∸n]⊓[n∸m]≡0 zero zero = refl
[m∸n]⊓[n∸m]≡0 zero (suc n) = refl
[m∸n]⊓[n∸m]≡0 (suc m) zero = refl
[m∸n]⊓[n∸m]≡0 (suc m) (suc n) = [m∸n]⊓[n∸m]≡0 m n
∸-distribˡ-⊓-⊔ : ∀ m n o → m ∸ (n ⊓ o) ≡ (m ∸ n) ⊔ (m ∸ o)
∸-distribˡ-⊓-⊔ m n o = antimono-≤-distrib-⊓ (∸-monoʳ-≤ m) n o
∸-distribʳ-⊓ : _∸_ DistributesOverʳ _⊓_
∸-distribʳ-⊓ m n o = mono-≤-distrib-⊓ (∸-monoˡ-≤ m) n o
∸-distribˡ-⊔-⊓ : ∀ m n o → m ∸ (n ⊔ o) ≡ (m ∸ n) ⊓ (m ∸ o)
∸-distribˡ-⊔-⊓ m n o = antimono-≤-distrib-⊔ (∸-monoʳ-≤ m) n o
∸-distribʳ-⊔ : _∸_ DistributesOverʳ _⊔_
∸-distribʳ-⊔ m n o = mono-≤-distrib-⊔ (∸-monoˡ-≤ m) n o
pred-mono : pred Preserves _≤_ ⟶ _≤_
pred-mono m≤n = ∸-mono m≤n (≤-refl {1})
pred[n]≤n : ∀ {n} → pred n ≤ n
pred[n]≤n {zero} = z≤n
pred[n]≤n {suc n} = n≤1+n n
≤pred⇒≤ : ∀ {m n} → m ≤ pred n → m ≤ n
≤pred⇒≤ {m} {zero} le = le
≤pred⇒≤ {m} {suc n} le = m≤n⇒m≤1+n le
≤⇒pred≤ : ∀ {m n} → m ≤ n → pred m ≤ n
≤⇒pred≤ {zero} le = le
≤⇒pred≤ {suc m} le = ≤-trans (n≤1+n m) le
<⇒≤pred : ∀ {m n} → m < n → m ≤ pred n
<⇒≤pred (s≤s le) = le
suc-pred : ∀ n .{{_ : NonZero n}} → suc (pred n) ≡ n
suc-pred (suc n) = refl
m≡n⇒∣m-n∣≡0 : ∀ {m n} → m ≡ n → ∣ m - n ∣ ≡ 0
m≡n⇒∣m-n∣≡0 {zero} refl = refl
m≡n⇒∣m-n∣≡0 {suc m} refl = m≡n⇒∣m-n∣≡0 {m} refl
∣m-n∣≡0⇒m≡n : ∀ {m n} → ∣ m - n ∣ ≡ 0 → m ≡ n
∣m-n∣≡0⇒m≡n {zero} {zero} eq = refl
∣m-n∣≡0⇒m≡n {suc m} {suc n} eq = cong suc (∣m-n∣≡0⇒m≡n eq)
m≤n⇒∣n-m∣≡n∸m : ∀ {m n} → m ≤ n → ∣ n - m ∣ ≡ n ∸ m
m≤n⇒∣n-m∣≡n∸m {_} {zero} z≤n = refl
m≤n⇒∣n-m∣≡n∸m {_} {suc m} z≤n = refl
m≤n⇒∣n-m∣≡n∸m {_} {_} (s≤s m≤n) = m≤n⇒∣n-m∣≡n∸m m≤n
m≤n⇒∣m-n∣≡n∸m : ∀ {m n} → m ≤ n → ∣ m - n ∣ ≡ n ∸ m
m≤n⇒∣m-n∣≡n∸m {_} {zero} z≤n = refl
m≤n⇒∣m-n∣≡n∸m {_} {suc n} z≤n = refl
m≤n⇒∣m-n∣≡n∸m {_} {_} (s≤s m≤n) = m≤n⇒∣m-n∣≡n∸m m≤n
∣m-n∣≡m∸n⇒n≤m : ∀ {m n} → ∣ m - n ∣ ≡ m ∸ n → n ≤ m
∣m-n∣≡m∸n⇒n≤m {zero} {zero} eq = z≤n
∣m-n∣≡m∸n⇒n≤m {suc m} {zero} eq = z≤n
∣m-n∣≡m∸n⇒n≤m {suc m} {suc n} eq = s≤s (∣m-n∣≡m∸n⇒n≤m eq)
∣n-n∣≡0 : ∀ n → ∣ n - n ∣ ≡ 0
∣n-n∣≡0 n = m≡n⇒∣m-n∣≡0 {n} refl
∣m-m+n∣≡n : ∀ m n → ∣ m - m + n ∣ ≡ n
∣m-m+n∣≡n zero n = refl
∣m-m+n∣≡n (suc m) n = ∣m-m+n∣≡n m n
∣m+n-m+o∣≡∣n-o∣ : ∀ m n o → ∣ m + n - m + o ∣ ≡ ∣ n - o ∣
∣m+n-m+o∣≡∣n-o∣ zero n o = refl
∣m+n-m+o∣≡∣n-o∣ (suc m) n o = ∣m+n-m+o∣≡∣n-o∣ m n o
m∸n≤∣m-n∣ : ∀ m n → m ∸ n ≤ ∣ m - n ∣
m∸n≤∣m-n∣ m n with ≤-total m n
... | inj₁ m≤n = subst (_≤ ∣ m - n ∣) (sym (m≤n⇒m∸n≡0 m≤n)) z≤n
... | inj₂ n≤m = subst (m ∸ n ≤_) (sym (m≤n⇒∣n-m∣≡n∸m n≤m)) ≤-refl
∣m-n∣≤m⊔n : ∀ m n → ∣ m - n ∣ ≤ m ⊔ n
∣m-n∣≤m⊔n zero m = ≤-refl
∣m-n∣≤m⊔n (suc m) zero = ≤-refl
∣m-n∣≤m⊔n (suc m) (suc n) = m≤n⇒m≤1+n (∣m-n∣≤m⊔n m n)
∣-∣-identityˡ : LeftIdentity 0 ∣_-_∣
∣-∣-identityˡ x = refl
∣-∣-identityʳ : RightIdentity 0 ∣_-_∣
∣-∣-identityʳ zero = refl
∣-∣-identityʳ (suc x) = refl
∣-∣-identity : Identity 0 ∣_-_∣
∣-∣-identity = ∣-∣-identityˡ , ∣-∣-identityʳ
∣-∣-comm : Commutative ∣_-_∣
∣-∣-comm zero zero = refl
∣-∣-comm zero (suc n) = refl
∣-∣-comm (suc m) zero = refl
∣-∣-comm (suc m) (suc n) = ∣-∣-comm m n
∣m-n∣≡[m∸n]∨[n∸m] : ∀ m n → (∣ m - n ∣ ≡ m ∸ n) ⊎ (∣ m - n ∣ ≡ n ∸ m)
∣m-n∣≡[m∸n]∨[n∸m] m n with ≤-total m n
... | inj₂ n≤m = inj₁ $ m≤n⇒∣n-m∣≡n∸m n≤m
... | inj₁ m≤n = inj₂ $ begin-equality
∣ m - n ∣ ≡⟨ ∣-∣-comm m n ⟩
∣ n - m ∣ ≡⟨ m≤n⇒∣n-m∣≡n∸m m≤n ⟩
n ∸ m ∎
private
*-distribˡ-∣-∣-aux : ∀ a m n → m ≤ n → a * ∣ n - m ∣ ≡ ∣ a * n - a * m ∣
*-distribˡ-∣-∣-aux a m n m≤n = begin-equality
a * ∣ n - m ∣ ≡⟨ cong (a *_) (m≤n⇒∣n-m∣≡n∸m m≤n) ⟩
a * (n ∸ m) ≡⟨ *-distribˡ-∸ a n m ⟩
a * n ∸ a * m ≡⟨ sym $′ m≤n⇒∣n-m∣≡n∸m (*-monoʳ-≤ a m≤n) ⟩
∣ a * n - a * m ∣ ∎
*-distribˡ-∣-∣ : _*_ DistributesOverˡ ∣_-_∣
*-distribˡ-∣-∣ a m n with ≤-total m n
... | inj₂ n≤m = *-distribˡ-∣-∣-aux a n m n≤m
... | inj₁ m≤n = begin-equality
a * ∣ m - n ∣ ≡⟨ cong (a *_) (∣-∣-comm m n) ⟩
a * ∣ n - m ∣ ≡⟨ *-distribˡ-∣-∣-aux a m n m≤n ⟩
∣ a * n - a * m ∣ ≡⟨ ∣-∣-comm (a * n) (a * m) ⟩
∣ a * m - a * n ∣ ∎
*-distribʳ-∣-∣ : _*_ DistributesOverʳ ∣_-_∣
*-distribʳ-∣-∣ = comm+distrˡ⇒distrʳ *-comm *-distribˡ-∣-∣
*-distrib-∣-∣ : _*_ DistributesOver ∣_-_∣
*-distrib-∣-∣ = *-distribˡ-∣-∣ , *-distribʳ-∣-∣
m≤n+∣n-m∣ : ∀ m n → m ≤ n + ∣ n - m ∣
m≤n+∣n-m∣ zero n = z≤n
m≤n+∣n-m∣ (suc m) zero = ≤-refl
m≤n+∣n-m∣ (suc m) (suc n) = s≤s (m≤n+∣n-m∣ m n)
m≤n+∣m-n∣ : ∀ m n → m ≤ n + ∣ m - n ∣
m≤n+∣m-n∣ m n = subst (m ≤_) (cong (n +_) (∣-∣-comm n m)) (m≤n+∣n-m∣ m n)
m≤∣m-n∣+n : ∀ m n → m ≤ ∣ m - n ∣ + n
m≤∣m-n∣+n m n = subst (m ≤_) (+-comm n _) (m≤n+∣m-n∣ m n)
∣-∣-triangle : TriangleInequality ∣_-_∣
∣-∣-triangle zero y z = m≤n+∣n-m∣ z y
∣-∣-triangle x zero z = begin
∣ x - z ∣ ≤⟨ ∣m-n∣≤m⊔n x z ⟩
x ⊔ z ≤⟨ m⊔n≤m+n x z ⟩
x + z ≡⟨ cong₂ _+_ (sym (∣-∣-identityʳ x)) refl ⟩
∣ x - 0 ∣ + z ∎
where open ≤-Reasoning
∣-∣-triangle x y zero = begin
∣ x - 0 ∣ ≡⟨ ∣-∣-identityʳ x ⟩
x ≤⟨ m≤∣m-n∣+n x y ⟩
∣ x - y ∣ + y ≡⟨ cong₂ _+_ refl (sym (∣-∣-identityʳ y)) ⟩
∣ x - y ∣ + ∣ y - 0 ∣ ∎
where open ≤-Reasoning
∣-∣-triangle (suc x) (suc y) (suc z) = ∣-∣-triangle x y z
∣-∣≡∣-∣′ : ∀ m n → ∣ m - n ∣ ≡ ∣ m - n ∣′
∣-∣≡∣-∣′ m n with m <ᵇ n in eq
... | false = m≤n⇒∣n-m∣≡n∸m {n} {m} (≮⇒≥ (λ m<n → subst T eq (<⇒<ᵇ m<n)))
... | true = m≤n⇒∣m-n∣≡n∸m {m} {n} (<⇒≤ (<ᵇ⇒< m n (subst T (sym eq) _)))
∣-∣-isProtoMetric : IsProtoMetric _≡_ ∣_-_∣
∣-∣-isProtoMetric = record
{ isPartialOrder = ≤-isPartialOrder
; ≈-isEquivalence = isEquivalence
; cong = cong₂ ∣_-_∣
; nonNegative = z≤n
}
∣-∣-isPreMetric : IsPreMetric _≡_ ∣_-_∣
∣-∣-isPreMetric = record
{ isProtoMetric = ∣-∣-isProtoMetric
; ≈⇒0 = m≡n⇒∣m-n∣≡0
}
∣-∣-isQuasiSemiMetric : IsQuasiSemiMetric _≡_ ∣_-_∣
∣-∣-isQuasiSemiMetric = record
{ isPreMetric = ∣-∣-isPreMetric
; 0⇒≈ = ∣m-n∣≡0⇒m≡n
}
∣-∣-isSemiMetric : IsSemiMetric _≡_ ∣_-_∣
∣-∣-isSemiMetric = record
{ isQuasiSemiMetric = ∣-∣-isQuasiSemiMetric
; sym = ∣-∣-comm
}
∣-∣-isMetric : IsMetric _≡_ ∣_-_∣
∣-∣-isMetric = record
{ isSemiMetric = ∣-∣-isSemiMetric
; triangle = ∣-∣-triangle
}
∣-∣-quasiSemiMetric : QuasiSemiMetric 0ℓ 0ℓ
∣-∣-quasiSemiMetric = record
{ isQuasiSemiMetric = ∣-∣-isQuasiSemiMetric
}
∣-∣-semiMetric : SemiMetric 0ℓ 0ℓ
∣-∣-semiMetric = record
{ isSemiMetric = ∣-∣-isSemiMetric
}
∣-∣-preMetric : PreMetric 0ℓ 0ℓ
∣-∣-preMetric = record
{ isPreMetric = ∣-∣-isPreMetric
}
∣-∣-metric : Metric 0ℓ 0ℓ
∣-∣-metric = record
{ isMetric = ∣-∣-isMetric
}
⌊n/2⌋-mono : ⌊_/2⌋ Preserves _≤_ ⟶ _≤_
⌊n/2⌋-mono z≤n = z≤n
⌊n/2⌋-mono (s≤s z≤n) = z≤n
⌊n/2⌋-mono (s≤s (s≤s m≤n)) = s≤s (⌊n/2⌋-mono m≤n)
⌈n/2⌉-mono : ⌈_/2⌉ Preserves _≤_ ⟶ _≤_
⌈n/2⌉-mono m≤n = ⌊n/2⌋-mono (s≤s m≤n)
⌊n/2⌋≤⌈n/2⌉ : ∀ n → ⌊ n /2⌋ ≤ ⌈ n /2⌉
⌊n/2⌋≤⌈n/2⌉ zero = z≤n
⌊n/2⌋≤⌈n/2⌉ (suc zero) = z≤n
⌊n/2⌋≤⌈n/2⌉ (suc (suc n)) = s≤s (⌊n/2⌋≤⌈n/2⌉ n)
⌊n/2⌋+⌈n/2⌉≡n : ∀ n → ⌊ n /2⌋ + ⌈ n /2⌉ ≡ n
⌊n/2⌋+⌈n/2⌉≡n zero = refl
⌊n/2⌋+⌈n/2⌉≡n (suc n) = begin-equality
⌊ suc n /2⌋ + suc ⌊ n /2⌋ ≡⟨ +-comm ⌊ suc n /2⌋ (suc ⌊ n /2⌋) ⟩
suc ⌊ n /2⌋ + ⌊ suc n /2⌋ ≡⟨⟩
suc (⌊ n /2⌋ + ⌊ suc n /2⌋) ≡⟨ cong suc (⌊n/2⌋+⌈n/2⌉≡n n) ⟩
suc n ∎
⌊n/2⌋≤n : ∀ n → ⌊ n /2⌋ ≤ n
⌊n/2⌋≤n zero = z≤n
⌊n/2⌋≤n (suc zero) = z≤n
⌊n/2⌋≤n (suc (suc n)) = s≤s (m≤n⇒m≤1+n (⌊n/2⌋≤n n))
⌊n/2⌋<n : ∀ n → ⌊ suc n /2⌋ < suc n
⌊n/2⌋<n zero = z<s
⌊n/2⌋<n (suc n) = s<s (s≤s (⌊n/2⌋≤n n))
n≡⌊n+n/2⌋ : ∀ n → n ≡ ⌊ n + n /2⌋
n≡⌊n+n/2⌋ zero = refl
n≡⌊n+n/2⌋ (suc zero) = refl
n≡⌊n+n/2⌋ (suc n′@(suc n)) =
cong suc (trans (n≡⌊n+n/2⌋ _) (cong ⌊_/2⌋ (sym (+-suc n n′))))
⌈n/2⌉≤n : ∀ n → ⌈ n /2⌉ ≤ n
⌈n/2⌉≤n zero = z≤n
⌈n/2⌉≤n (suc n) = s≤s (⌊n/2⌋≤n n)
⌈n/2⌉<n : ∀ n → ⌈ suc (suc n) /2⌉ < suc (suc n)
⌈n/2⌉<n n = s<s (⌊n/2⌋<n n)
n≡⌈n+n/2⌉ : ∀ n → n ≡ ⌈ n + n /2⌉
n≡⌈n+n/2⌉ zero = refl
n≡⌈n+n/2⌉ (suc zero) = refl
n≡⌈n+n/2⌉ (suc n′@(suc n)) =
cong suc (trans (n≡⌈n+n/2⌉ _) (cong ⌈_/2⌉ (sym (+-suc n n′))))
1≤n! : ∀ n → 1 ≤ n !
1≤n! zero = ≤-refl
1≤n! (suc n) = *-mono-≤ (m≤m+n 1 n) (1≤n! n)
infix 4 _!≢0 _!*_!≢0
_!≢0 : ∀ n → NonZero (n !)
n !≢0 = >-nonZero (1≤n! n)
_!*_!≢0 : ∀ m n → NonZero (m ! * n !)
m !* n !≢0 = m*n≢0 _ _ {{m !≢0}} {{n !≢0}}
≤′-trans : Transitive _≤′_
≤′-trans m≤n ≤′-refl = m≤n
≤′-trans m≤n (≤′-step n≤o) = ≤′-step (≤′-trans m≤n n≤o)
z≤′n : ∀ {n} → zero ≤′ n
z≤′n {zero} = ≤′-refl
z≤′n {suc n} = ≤′-step z≤′n
s≤′s : ∀ {m n} → m ≤′ n → suc m ≤′ suc n
s≤′s ≤′-refl = ≤′-refl
s≤′s (≤′-step m≤′n) = ≤′-step (s≤′s m≤′n)
≤′⇒≤ : _≤′_ ⇒ _≤_
≤′⇒≤ ≤′-refl = ≤-refl
≤′⇒≤ (≤′-step m≤′n) = m≤n⇒m≤1+n (≤′⇒≤ m≤′n)
≤⇒≤′ : _≤_ ⇒ _≤′_
≤⇒≤′ z≤n = z≤′n
≤⇒≤′ (s≤s m≤n) = s≤′s (≤⇒≤′ m≤n)
≤′-step-injective : ∀ {m n} {p q : m ≤′ n} → ≤′-step p ≡ ≤′-step q → p ≡ q
≤′-step-injective refl = refl
z<′s : ∀ {n} → zero <′ suc n
z<′s {zero} = <′-base
z<′s {suc n} = <′-step (z<′s {n})
s<′s : ∀ {m n} → m <′ n → suc m <′ suc n
s<′s <′-base = <′-base
s<′s (<′-step m<′n) = <′-step (s<′s m<′n)
<⇒<′ : ∀ {m n} → m < n → m <′ n
<⇒<′ z<s = z<′s
<⇒<′ (s<s m<n@(s≤s _)) = s<′s (<⇒<′ m<n)
<′⇒< : ∀ {m n} → m <′ n → m < n
<′⇒< <′-base = n<1+n _
<′⇒< (<′-step m<′n) = m<n⇒m<1+n (<′⇒< m<′n)
m<1+n⇒m<n∨m≡n′ : ∀ {m n} → m < suc n → m < n ⊎ m ≡ n
m<1+n⇒m<n∨m≡n′ m<n with <⇒<′ m<n
... | <′-base = inj₂ refl
... | <′-step m<′n = inj₁ (<′⇒< m<′n)
infix 4 _≤′?_ _<′?_ _≥′?_ _>′?_
_≤′?_ : Decidable _≤′_
m ≤′? n = map′ ≤⇒≤′ ≤′⇒≤ (m ≤? n)
_<′?_ : Decidable _<′_
m <′? n = suc m ≤′? n
_≥′?_ : Decidable _≥′_
_≥′?_ = flip _≤′?_
_>′?_ : Decidable _>′_
_>′?_ = flip _<′?_
m≤′m+n : ∀ m n → m ≤′ m + n
m≤′m+n m n = ≤⇒≤′ (m≤m+n m n)
n≤′m+n : ∀ m n → n ≤′ m + n
n≤′m+n zero n = ≤′-refl
n≤′m+n (suc m) n = ≤′-step (n≤′m+n m n)
⌈n/2⌉≤′n : ∀ n → ⌈ n /2⌉ ≤′ n
⌈n/2⌉≤′n zero = ≤′-refl
⌈n/2⌉≤′n (suc zero) = ≤′-refl
⌈n/2⌉≤′n (suc (suc n)) = s≤′s (≤′-step (⌈n/2⌉≤′n n))
⌊n/2⌋≤′n : ∀ n → ⌊ n /2⌋ ≤′ n
⌊n/2⌋≤′n zero = ≤′-refl
⌊n/2⌋≤′n (suc n) = ≤′-step (⌈n/2⌉≤′n n)
m<ᵇn⇒1+m+[n-1+m]≡n : ∀ m n → T (m <ᵇ n) → suc m + (n ∸ suc m) ≡ n
m<ᵇn⇒1+m+[n-1+m]≡n m n lt = m+[n∸m]≡n (<ᵇ⇒< m n lt)
m<ᵇ1+m+n : ∀ m {n} → T (m <ᵇ suc (m + n))
m<ᵇ1+m+n m = <⇒<ᵇ (m≤m+n (suc m) _)
<ᵇ⇒<″ : ∀ {m n} → T (m <ᵇ n) → m <″ n
<ᵇ⇒<″ {m} {n} leq = less-than-or-equal (m+[n∸m]≡n (<ᵇ⇒< m n leq))
<″⇒<ᵇ : ∀ {m n} → m <″ n → T (m <ᵇ n)
<″⇒<ᵇ {m} (less-than-or-equal refl) = <⇒<ᵇ (m≤m+n (suc m) _)
≤″⇒≤ : _≤″_ ⇒ _≤_
≤″⇒≤ {zero} (less-than-or-equal refl) = z≤n
≤″⇒≤ {suc m} (less-than-or-equal refl) =
s≤s (≤″⇒≤ (less-than-or-equal refl))
≤⇒≤″ : _≤_ ⇒ _≤″_
≤⇒≤″ = less-than-or-equal ∘ m+[n∸m]≡n
infix 4 _<″?_ _≤″?_ _≥″?_ _>″?_
_<″?_ : Decidable _<″_
m <″? n = map′ <ᵇ⇒<″ <″⇒<ᵇ (T? (m <ᵇ n))
_≤″?_ : Decidable _≤″_
zero ≤″? n = yes (less-than-or-equal refl)
suc m ≤″? n = m <″? n
_≥″?_ : Decidable _≥″_
_≥″?_ = flip _≤″?_
_>″?_ : Decidable _>″_
_>″?_ = flip _<″?_
≤″-irrelevant : Irrelevant _≤″_
≤″-irrelevant {m} (less-than-or-equal eq₁)
(less-than-or-equal eq₂)
with +-cancelˡ-≡ m _ _ (trans eq₁ (sym eq₂))
... | refl = cong less-than-or-equal (≡-irrelevant eq₁ eq₂)
<″-irrelevant : Irrelevant _<″_
<″-irrelevant = ≤″-irrelevant
>″-irrelevant : Irrelevant _>″_
>″-irrelevant = ≤″-irrelevant
≥″-irrelevant : Irrelevant _≥″_
≥″-irrelevant = ≤″-irrelevant
≤‴⇒≤″ : ∀{m n} → m ≤‴ n → m ≤″ n
≤‴⇒≤″ {m = m} ≤‴-refl = less-than-or-equal {k = 0} (+-identityʳ m)
≤‴⇒≤″ {m = m} (≤‴-step x) = less-than-or-equal (trans (+-suc m _) (_≤″_.proof ind)) where
ind = ≤‴⇒≤″ x
m≤‴m+k : ∀{m n k} → m + k ≡ n → m ≤‴ n
m≤‴m+k {m} {k = zero} refl = subst (λ z → m ≤‴ z) (sym (+-identityʳ m)) (≤‴-refl {m})
m≤‴m+k {m} {k = suc k} proof
= ≤‴-step (m≤‴m+k {k = k} (trans (sym (+-suc m _)) proof))
≤″⇒≤‴ : ∀{m n} → m ≤″ n → m ≤‴ n
≤″⇒≤‴ (less-than-or-equal {k} proof) = m≤‴m+k proof
0≤‴n : ∀{n} → 0 ≤‴ n
0≤‴n {n} = m≤‴m+k refl
<ᵇ⇒<‴ : ∀ {m n} → T (m <ᵇ n) → m <‴ n
<ᵇ⇒<‴ {m} {n} leq = ≤″⇒≤‴ (<ᵇ⇒<″ leq)
<‴⇒<ᵇ : ∀ {m n} → m <‴ n → T (m <ᵇ n)
<‴⇒<ᵇ leq = <″⇒<ᵇ (≤‴⇒≤″ leq)
infix 4 _<‴?_ _≤‴?_ _≥‴?_ _>‴?_
_<‴?_ : Decidable _<‴_
m <‴? n = map′ <ᵇ⇒<‴ <‴⇒<ᵇ (T? (m <ᵇ n))
_≤‴?_ : Decidable _≤‴_
zero ≤‴? n = yes 0≤‴n
suc m ≤‴? n = m <‴? n
_≥‴?_ : Decidable _≥‴_
_≥‴?_ = flip _≤‴?_
_>‴?_ : Decidable _>‴_
_>‴?_ = flip _<‴?_
≤⇒≤‴ : _≤_ ⇒ _≤‴_
≤⇒≤‴ = ≤″⇒≤‴ ∘ ≤⇒≤″
≤‴⇒≤ : _≤‴_ ⇒ _≤_
≤‴⇒≤ = ≤″⇒≤ ∘ ≤‴⇒≤″
eq? : ∀ {a} {A : Set a} → A ↣ ℕ → DecidableEquality A
eq? inj = via-injection inj _≟_
module _ {p} {P : Pred ℕ p} (P? : U.Decidable P) where
anyUpTo? : ∀ v → Dec (∃ λ n → n < v × P n)
anyUpTo? zero = no λ {(_ , () , _)}
anyUpTo? (suc v) with P? v | anyUpTo? v
... | yes Pv | _ = yes (v , ≤-refl , Pv)
... | _ | yes (n , n<v , Pn) = yes (n , m≤n⇒m≤1+n n<v , Pn)
... | no ¬Pv | no ¬Pn<v = no ¬Pn<1+v
where
¬Pn<1+v : (∃ λ n → n < suc v × P n) → ⊥
¬Pn<1+v (n , s≤s n≤v , Pn) with n ≟ v
... | yes refl = ¬Pv Pn
... | no n≢v = ¬Pn<v (n , ≤∧≢⇒< n≤v n≢v , Pn)
allUpTo? : ∀ v → Dec (∀ {n} → n < v → P n)
allUpTo? zero = yes λ()
allUpTo? (suc v) with P? v | allUpTo? v
... | no ¬Pv | _ = no (λ prf → ¬Pv (prf ≤-refl))
... | _ | no ¬Pn<v = no (λ prf → ¬Pn<v (prf ∘ m≤n⇒m≤1+n))
... | yes Pn | yes Pn<v = yes Pn<1+v
where
Pn<1+v : ∀ {n} → n < suc v → P n
Pn<1+v {n} (s≤s n≤v) with n ≟ v
... | yes refl = Pn
... | no n≢v = Pn<v (≤∧≢⇒< n≤v n≢v)
∀[m≤n⇒m≢o]⇒o<n : ∀ n o → (∀ {m} → m ≤ n → m ≢ o) → n < o
∀[m≤n⇒m≢o]⇒o<n = ∀[m≤n⇒m≢o]⇒n<o
{-# WARNING_ON_USAGE ∀[m≤n⇒m≢o]⇒o<n
"Warning: ∀[m≤n⇒m≢o]⇒o<n was deprecated in v1.3.
Please use ∀[m≤n⇒m≢o]⇒n<o instead."
#-}
∀[m<n⇒m≢o]⇒o≤n : ∀ n o → (∀ {m} → m < n → m ≢ o) → n ≤ o
∀[m<n⇒m≢o]⇒o≤n = ∀[m<n⇒m≢o]⇒n≤o
{-# WARNING_ON_USAGE ∀[m<n⇒m≢o]⇒o≤n
"Warning: ∀[m<n⇒m≢o]⇒o≤n was deprecated in v1.3.
Please use ∀[m<n⇒m≢o]⇒n≤o instead."
#-}
*-+-isSemiring = +-*-isSemiring
{-# WARNING_ON_USAGE *-+-isSemiring
"Warning: *-+-isSemiring was deprecated in v1.4.
Please use +-*-isSemiring instead."
#-}
*-+-isCommutativeSemiring = +-*-isCommutativeSemiring
{-# WARNING_ON_USAGE *-+-isCommutativeSemiring
"Warning: *-+-isCommutativeSemiring was deprecated in v1.4.
Please use +-*-isCommutativeSemiring instead."
#-}
*-+-semiring = +-*-semiring
{-# WARNING_ON_USAGE *-+-semiring
"Warning: *-+-semiring was deprecated in v1.4.
Please use +-*-semiring instead."
#-}
*-+-commutativeSemiring = +-*-commutativeSemiring
{-# WARNING_ON_USAGE *-+-commutativeSemiring
"Warning: *-+-commutativeSemiring was deprecated in v1.4.
Please use +-*-commutativeSemiring instead."
#-}
∣m+n-m+o∣≡∣n-o| = ∣m+n-m+o∣≡∣n-o∣
{-# WARNING_ON_USAGE ∣m+n-m+o∣≡∣n-o|
"Warning: ∣m+n-m+o∣≡∣n-o| was deprecated in v1.6.
Please use ∣m+n-m+o∣≡∣n-o∣ instead. Note the final is a \\| rather than a |"
#-}
m≤n⇒n⊔m≡n = m≥n⇒m⊔n≡m
{-# WARNING_ON_USAGE m≤n⇒n⊔m≡n
"Warning: m≤n⇒n⊔m≡n was deprecated in v1.6. Please use m≥n⇒m⊔n≡m instead."
#-}
m≤n⇒n⊓m≡m = m≥n⇒m⊓n≡n
{-# WARNING_ON_USAGE m≤n⇒n⊓m≡m
"Warning: m≤n⇒n⊓m≡m was deprecated in v1.6. Please use m≥n⇒m⊓n≡n instead."
#-}
n⊔m≡m⇒n≤m = m⊔n≡n⇒m≤n
{-# WARNING_ON_USAGE n⊔m≡m⇒n≤m
"Warning: n⊔m≡m⇒n≤m was deprecated in v1.6. Please use m⊔n≡n⇒m≤n instead."
#-}
n⊔m≡n⇒m≤n = m⊔n≡m⇒n≤m
{-# WARNING_ON_USAGE n⊔m≡n⇒m≤n
"Warning: n⊔m≡n⇒m≤n was deprecated in v1.6. Please use m⊔n≡m⇒n≤m instead."
#-}
n≤m⊔n = m≤n⊔m
{-# WARNING_ON_USAGE n≤m⊔n
"Warning: n≤m⊔n was deprecated in v1.6. Please use m≤n⊔m instead."
#-}
⊔-least = ⊔-lub
{-# WARNING_ON_USAGE ⊔-least
"Warning: ⊔-least was deprecated in v1.6. Please use ⊔-lub instead."
#-}
⊓-greatest = ⊓-glb
{-# WARNING_ON_USAGE ⊓-greatest
"Warning: ⊓-greatest was deprecated in v1.6. Please use ⊓-glb instead."
#-}
⊔-pres-≤m = ⊔-lub
{-# WARNING_ON_USAGE ⊔-pres-≤m
"Warning: ⊔-pres-≤m was deprecated in v1.6. Please use ⊔-lub instead."
#-}
⊓-pres-m≤ = ⊓-glb
{-# WARNING_ON_USAGE ⊓-pres-m≤
"Warning: ⊓-pres-m≤ was deprecated in v1.6. Please use ⊓-glb instead."
#-}
⊔-abs-⊓ = ⊔-absorbs-⊓
{-# WARNING_ON_USAGE ⊔-abs-⊓
"Warning: ⊔-abs-⊓ was deprecated in v1.6. Please use ⊔-absorbs-⊓ instead."
#-}
⊓-abs-⊔ = ⊓-absorbs-⊔
{-# WARNING_ON_USAGE ⊓-abs-⊔
"Warning: ⊓-abs-⊔ was deprecated in v1.6. Please use ⊓-absorbs-⊔ instead."
#-}
suc[pred[n]]≡n : ∀ {n} → n ≢ 0 → suc (pred n) ≡ n
suc[pred[n]]≡n {zero} 0≢0 = contradiction refl 0≢0
suc[pred[n]]≡n {suc n} _ = refl
{-# WARNING_ON_USAGE suc[pred[n]]≡n
"Warning: suc[pred[n]]≡n was deprecated in v2.0. Please use suc-pred instead. Note that the proof now uses instance arguments"
#-}
≤-step = m≤n⇒m≤1+n
{-# WARNING_ON_USAGE ≤-step
"Warning: ≤-step was deprecated in v2.0. Please use m≤n⇒m≤1+n instead. "
#-}
≤-stepsˡ = m≤n⇒m≤o+n
{-# WARNING_ON_USAGE ≤-stepsˡ
"Warning: ≤-stepsˡ was deprecated in v2.0. Please use m≤n⇒m≤o+n instead. "
#-}
≤-stepsʳ = m≤n⇒m≤n+o
{-# WARNING_ON_USAGE ≤-stepsʳ
"Warning: ≤-stepsʳ was deprecated in v2.0. Please use m≤n⇒m≤n+o instead. "
#-}
<-step = m<n⇒m<1+n
{-# WARNING_ON_USAGE <-step
"Warning: <-step was deprecated in v2.0. Please use m<n⇒m<1+n instead. "
#-}
open Data.Nat.Base public
using (*-rawMagma; *-1-rawMonoid)