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

@@ -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

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

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