From 1c0396ca8786c48f6bacceb501074cc09b459cdb Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 25 Jan 2024 18:19:39 +0100 Subject: [PATCH] Triangular numbers (#1044) * triangular numbers * add instance for nat * export naturals * add forgetter * update * export more, to make the use of Nat as a CSR more natural * update references, cosmetics * organize imports * Cleanup * cleanup, remove reexport of Nat, suc, zero * qualify import * description --- Cubical/Algebra/CommSemiring/Base.agda | 63 ++++++++++++------- .../Algebra/CommSemiring/Instances/Nat.agda | 30 +++++++++ Cubical/Data/Nat/Triangular.agda | 56 +++++++++++++++++ 3 files changed, 127 insertions(+), 22 deletions(-) create mode 100644 Cubical/Algebra/CommSemiring/Instances/Nat.agda create mode 100644 Cubical/Data/Nat/Triangular.agda diff --git a/Cubical/Algebra/CommSemiring/Base.agda b/Cubical/Algebra/CommSemiring/Base.agda index 7763d65208..5874310b9f 100644 --- a/Cubical/Algebra/CommSemiring/Base.agda +++ b/Cubical/Algebra/CommSemiring/Base.agda @@ -38,27 +38,46 @@ record CommSemiringStr (A : Type ℓ) : Type (ℓ-suc ℓ) where CommSemiring : ∀ ℓ → Type (ℓ-suc ℓ) CommSemiring ℓ = TypeWithStr ℓ CommSemiringStr -makeIsCommSemiring : {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R} - (is-setR : isSet R) - (+Assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z) - (+IdR : (x : R) → x + 0r ≡ x) - (+Comm : (x y : R) → x + y ≡ y + x) - (·Assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z) - (·IdR : (x : R) → x · 1r ≡ x) - (·DistR+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z)) - (AnnihilL : (x : R) → 0r · x ≡ 0r) - (·Comm : (x y : R) → x · y ≡ y · x) - → IsCommSemiring 0r 1r _+_ _·_ +CommSemiring→Semiring : CommSemiring ℓ → Semiring ℓ +CommSemiring→Semiring CS .fst = CS .fst +CommSemiring→Semiring CS .snd = str + where + open IsCommSemiring + open CommSemiringStr + open SemiringStr + + CS-str = CS .snd + + str : SemiringStr (CS .fst) + 0r str = CS-str .0r + 1r str = CS-str .1r + _+_ str = CS-str ._+_ + _·_ str = CS-str ._·_ + isSemiring str = (CS-str .isCommSemiring) .isSemiring + +makeIsCommSemiring : + {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R} + (is-setR : isSet R) + (+Assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z) + (+IdR : (x : R) → x + 0r ≡ x) + (+Comm : (x y : R) → x + y ≡ y + x) + (·Assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z) + (·IdR : (x : R) → x · 1r ≡ x) + (·DistR+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z)) + (AnnihilL : (x : R) → 0r · x ≡ 0r) + (·Comm : (x y : R) → x · y ≡ y · x) + → IsCommSemiring 0r 1r _+_ _·_ makeIsCommSemiring {_+_ = _+_} {_·_ = _·_} is-setR +Assoc +IdR +Comm ·Assoc ·IdR ·DistR+ AnnihilL ·Comm = x - where x : IsCommSemiring _ _ _ _ - IsCommSemiring.isSemiring x = - makeIsSemiring - is-setR +Assoc +IdR +Comm ·Assoc - ·IdR (λ x → ·Comm _ x ∙ (·IdR x)) - ·DistR+ (λ x y z → (x + y) · z ≡⟨ ·Comm (x + y) z ⟩ - z · (x + y) ≡⟨ ·DistR+ z x y ⟩ - (z · x) + (z · y) ≡[ i ]⟨ (·Comm z x i + ·Comm z y i) ⟩ - (x · z) + (y · z) ∎ ) - ( λ x → ·Comm x _ ∙ AnnihilL x) AnnihilL - IsCommSemiring.·Comm x = ·Comm + where + x : IsCommSemiring _ _ _ _ + IsCommSemiring.isSemiring x = + makeIsSemiring + is-setR +Assoc +IdR +Comm ·Assoc + ·IdR (λ x → ·Comm _ x ∙ (·IdR x)) + ·DistR+ (λ x y z → (x + y) · z ≡⟨ ·Comm (x + y) z ⟩ + z · (x + y) ≡⟨ ·DistR+ z x y ⟩ + (z · x) + (z · y) ≡[ i ]⟨ (·Comm z x i + ·Comm z y i) ⟩ + (x · z) + (y · z) ∎ ) + ( λ x → ·Comm x _ ∙ AnnihilL x) AnnihilL + IsCommSemiring.·Comm x = ·Comm diff --git a/Cubical/Algebra/CommSemiring/Instances/Nat.agda b/Cubical/Algebra/CommSemiring/Instances/Nat.agda new file mode 100644 index 0000000000..cc3c80de59 --- /dev/null +++ b/Cubical/Algebra/CommSemiring/Instances/Nat.agda @@ -0,0 +1,30 @@ +{-# OPTIONS --safe #-} +module Cubical.Algebra.CommSemiring.Instances.Nat where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels + +import Cubical.Data.Nat as Nat +open import Cubical.Data.Nat using (ℕ; suc; zero) + +open import Cubical.Algebra.CommSemiring + +ℕasCSR : CommSemiring ℓ-zero +ℕasCSR .fst = ℕ +ℕasCSR .snd = str + where + open CommSemiringStr + + str : CommSemiringStr ℕ + 0r str = zero + 1r str = suc zero + _+_ str = Nat._+_ + _·_ str = Nat._·_ + isCommSemiring str = + makeIsCommSemiring + Nat.isSetℕ + Nat.+-assoc Nat.+-zero Nat.+-comm + Nat.·-assoc Nat.·-identityʳ + (λ x y z → sym (Nat.·-distribˡ x y z)) + (λ _ → refl) + Nat.·-comm diff --git a/Cubical/Data/Nat/Triangular.agda b/Cubical/Data/Nat/Triangular.agda new file mode 100644 index 0000000000..c9d9fed3e8 --- /dev/null +++ b/Cubical/Data/Nat/Triangular.agda @@ -0,0 +1,56 @@ +{-# OPTIONS --safe #-} +{- + In this module, the commonly known identity between the sum of the first (n+1) natural + numbers (also known as the n-th triangular number) and the product ½ · n · (n+1) is + proven in the equivalent form: + + 2 · (∑ (first (suc n))) ≡ n · (n + 1) +-} +module Cubical.Data.Nat.Triangular where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function + +open import Cubical.Data.FinData as Fin +open import Cubical.Data.Nat using (ℕ; suc; zero) + +open import Cubical.Algebra.CommSemiring +open import Cubical.Algebra.CommSemiring.Instances.Nat +open import Cubical.Algebra.Semiring.BigOps + +open import Cubical.Tactics.NatSolver.Reflection + +open Sum (CommSemiring→Semiring ℕasCSR) +open CommSemiringStr (snd ℕasCSR) + +-- the first n natural number, i.e. {0,1,...,n-1} +first : (n : ℕ) → FinVec ℕ n +first n i = toℕ i + +firstDecompose : (n : ℕ) → first (suc n) ∘ weakenFin ≡ first n +firstDecompose n i l = + Fin.elim + (λ l → first (suc _) (weakenFin l) ≡ first _ l) + refl + (λ _ → weakenRespToℕ _) + l i + +sumFormula : (n : ℕ) → 2 · (∑ (first (suc n))) ≡ n · (n + 1) +sumFormula zero = refl +sumFormula (suc n) = + 2 · ∑ (first (2 + n)) ≡⟨ step0 ⟩ + 2 · (∑ (first (2 + n) ∘ weakenFin) + first (2 + n) (fromℕ (suc n))) ≡⟨ step1 ⟩ + 2 · (∑ (first (2 + n) ∘ weakenFin) + (suc n)) ≡⟨ step2 ⟩ + 2 · (∑ (first (1 + n)) + (suc n)) ≡⟨ step3 ⟩ + 2 · ∑ (first (1 + n)) + 2 · (suc n) ≡⟨ step4 ⟩ + n · (n + 1) + 2 · (suc n) ≡⟨ useSolver n ⟩ + (suc n) · (suc (n + 1)) ∎ + where + step0 = cong (λ u → 2 · u) (∑Last (first (2 + n))) + step1 = cong (λ u → 2 · (∑ (first (2 + n) ∘ weakenFin) + u)) (toFromId _) + step2 = cong (λ u → 2 · ((∑ u) + (suc n))) (firstDecompose (suc n)) + step3 = ·DistR+ 2 (∑ (first (1 + n))) (suc n) + step4 = cong (λ u → u + 2 · (suc n)) (sumFormula n) + + useSolver : ∀ (n : ℕ) → n · (n + 1) + 2 · (suc n) ≡ (suc n) · (suc (n + 1)) + useSolver = solve