diff --git a/CHANGELOG.md b/CHANGELOG.md index 68c596e074..6936cd2385 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1413,7 +1413,7 @@ Deprecated names m) + using (DecidableEquality; Reflexive; Transitive; Antisymmetric; Total; Decidable; Irrelevant; Irreflexive; Asymmetric; LeftTrans; RightTrans; Trichotomous; tri≈; tri<; tri>) open import Relation.Binary.PropositionalEquality open import Relation.Nullary using (yes; no; ¬_) import Relation.Nullary.Reflects as Reflects @@ -276,17 +276,17 @@ drop‿-<- (-<- n0 mod≢0) mod≤1+j , j≤k)) divₕ-offsetEq d (suc n) (suc j) (suc k) j≤d k≤d (inj₃ (eq , k; tri<; _Respects₂_) + using (DecidableEquality; Irrelevant; Reflexive; Antisymmetric; Transitive; Total; Decidable; Connex; Irreflexive; Asymmetric; LeftTrans; RightTrans; Trichotomous; tri≈; tri>; tri<; _Respects₂_) open import Relation.Binary.Consequences using (flip-Connex) open import Relation.Binary.PropositionalEquality open import Relation.Nullary hiding (Irrelevant) @@ -52,6 +51,12 @@ open import Algebra.Definitions using (LeftCancellative; RightCancellative; Cancellative) open import Algebra.Structures {A = ℕ} _≡_ + +private + variable + m n o k : ℕ + + ------------------------------------------------------------------------ -- Properties of NonZero ------------------------------------------------------------------------ @@ -64,8 +69,8 @@ nonZero? (suc n) = yes _ -- Properties of _≡_ ------------------------------------------------------------------------ -suc-injective : ∀ {m n} → suc m ≡ suc n → m ≡ n -suc-injective refl = refl +suc-injective : suc m ≡ suc n → m ≡ n +suc-injective = cong pred ≡ᵇ⇒≡ : ∀ m n → T (m ≡ᵇ n) → m ≡ n ≡ᵇ⇒≡ zero zero _ = refl @@ -88,7 +93,7 @@ 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 : (eq : m ≡ n) → (m ≟ n) ≡ yes eq ≟-diag = ≡-≟-identity _≟_ ≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ}) @@ -104,13 +109,13 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n)) ; isDecEquivalence = ≡-isDecEquivalence } -0≢1+n : ∀ {n} → 0 ≢ suc n +0≢1+n : 0 ≢ suc n 0≢1+n () -1+n≢0 : ∀ {n} → suc n ≢ 0 +1+n≢0 : suc n ≢ 0 1+n≢0 () -1+n≢n : ∀ {n} → suc n ≢ n +1+n≢n : suc n ≢ n 1+n≢n {suc n} = 1+n≢n ∘ suc-injective ------------------------------------------------------------------------ @@ -121,7 +126,7 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n)) <ᵇ⇒< zero (suc n) m?_ = flip _0⇒n≢0 : ∀ {n} → n > 0 → n ≢ 0 +n>0⇒n≢0 : n > 0 → n ≢ 0 n>0⇒n≢0 {suc n} _ () -n≢0⇒n>0 : ∀ {n} → n ≢ 0 → n > 0 +n≢0⇒n>0 : n ≢ 0 → n > 0 n≢0⇒n>0 {zero} 0≢0 = contradiction refl 0≢0 n≢0⇒n>0 {suc n} _ = 0<1+n -m0 m n = >-nonZero⁻¹ (m ^ n) {{m^n≢0 m n}} ------------------------------------------------------------------------ -- Basic specification in terms of _≤_ -m≤n⇒m⊔n≡n : ∀ {m n} → m ≤ n → m ⊔ n ≡ n +m≤n⇒m⊔n≡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 : 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 : 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 : 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) @@ -1286,23 +1291,23 @@ antimono-≤-distrib-⊔ : ∀ {f} → f Preserves _≤_ ⟶ _≥_ → ∀ m n → f (m ⊔ n) ≡ f m ⊓ f n antimono-≤-distrib-⊔ {f} = ⊓-⊔-properties.antimono-≤-distrib-⊔ (cong f) -mn⇒m∸n≢0 : ∀ {m n} → m > n → m ∸ n ≢ 0 +m>n⇒m∸n≢0 : 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 : 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) @@ -1605,7 +1610,7 @@ m+n∸n≡m m n = begin-equality 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 ∸ 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) ⟩ @@ -1689,19 +1694,19 @@ m⊓n+n∸m≡n (suc m) (suc n) = cong suc $ m⊓n+n∸m≡n m n pred-mono : pred Preserves _≤_ ⟶ _≤_ pred-mono m≤n = ∸-mono m≤n (≤-refl {1}) -pred[n]≤n : ∀ {n} → pred n ≤ n +pred[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 ≤ pred n → m ≤ n +≤pred⇒≤ {n = zero} le = le +≤pred⇒≤ {n = suc n} le = m≤n⇒m≤1+n le -≤⇒pred≤ : ∀ {m n} → m ≤ n → pred m ≤ n +≤⇒pred≤ : 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 : m < n → m ≤ pred n <⇒≤pred (s≤s le) = le suc-pred : ∀ n .{{_ : NonZero n}} → suc (pred n) ≡ n @@ -1714,25 +1719,25 @@ suc-pred (suc n) = refl ------------------------------------------------------------------------ -- Basic -m≡n⇒∣m-n∣≡0 : ∀ {m n} → m ≡ n → ∣ m - n ∣ ≡ 0 +m≡n⇒∣m-n∣≡0 : 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 : ∣ 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⇒∣n-m∣≡n∸m : m ≤ n → ∣ n - m ∣ ≡ n ∸ m +m≤n⇒∣n-m∣≡n∸m {n = zero} z≤n = refl +m≤n⇒∣n-m∣≡n∸m {n = suc n} z≤n = refl +m≤n⇒∣n-m∣≡n∸m {n = _} (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 ∣ ≡ n ∸ m +m≤n⇒∣m-n∣≡n∸m {n = zero} z≤n = refl +m≤n⇒∣m-n∣≡n∸m {n = suc n} z≤n = refl +m≤n⇒∣m-n∣≡n∸m {n = _} (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 : ∣ 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) @@ -1971,11 +1976,11 @@ m !* n !≢0 = m*n≢0 _ _ {{m !≢0}} {{n !≢0}} ≤′-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 ≤′ n z≤′n {zero} = ≤′-refl z≤′n {suc n} = ≤′-step z≤′n -s≤′s : ∀ {m n} → m ≤′ n → suc m ≤′ suc n +s≤′s : m ≤′ n → suc m ≤′ suc n s≤′s ≤′-refl = ≤′-refl s≤′s (≤′-step m≤′n) = ≤′-step (s≤′s m≤′n) @@ -1987,30 +1992,30 @@ s≤′s (≤′-step m≤′n) = ≤′-step (s≤′s 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 : {p q : m ≤′ n} → ≤′-step p ≡ ≤′-step q → p ≡ q ≤′-step-injective refl = refl ------------------------------------------------------------------------ -- Properties of _<′_ and _<_ ------------------------------------------------------------------------ -z<′s : ∀ {n} → zero <′ suc n +z<′s : 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 : 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 +<⇒<′ : m < n → m <′ n <⇒<′ z