Added Z mod n as Fin

CHANGELOG.md

@@ -29,6 +29,8 @@ Deprecated names
 New modules
 -----------
 
+* Added new files `Data.Fin.Mod` and `Data.Fin.Mod.Properties`
+
 Additions to existing modules
 -----------------------------
 
@@ -80,3 +82,36 @@ Additions to existing modules
   pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n
   pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n
   ```
+
+* In `Data.Fin.Properties`:
+  ```agda
+  zeroFromNonZero : .⦃ NonZero n ⦄ → Fin n
+  ```
+
+* In `Data.Fin.Mod`:
+  ```agda
+  sucMod  : Fin n → Fin n
+  predMod : Fin n → Fin n
+  _ℕ+_    : ℕ → Fin n → Fin n
+  _+_     : Fin n → Fin m → Fin n
+  _-_     : Fin n → Fin m → Fin n
+  ```
+
+* In `Data.Fin.Mod.Properties`:
+  ```agda
+  suc-inject₁      : ∀ i → sucMod (inject₁ i) ≡ F.suc i
+  suc-fromℕ        : ∀ n → sucMod (fromℕ n) ≡ zero
+  pred-sucMod      : ∀ i → predMod (F.suc i) ≡ inject₁ i
+  suc-pred≡id      : ∀ i → sucMod (predMod i) ≡ i
+  pred-suc         : ∀ i → predMod (sucMod i) ≡ i
+  +-identityˡ      : .⦃ NonZero n ⦄ → LeftIdentity zeroFromNonZero _+_
+  +ℕ-identityʳ-toℕ : m ℕ.≤ n → toℕ (m ℕ+ zero {n}) ≡ m
+  +ℕ-identityʳ     : ∀ m≤n → m ℕ+ zero ≡ fromℕ< (s≤s m≤n)
+  +-identityʳ      : .⦃ NonZero n ⦄ → RightIdentity zeroFromNonZero _+_
+  induction        : ∀ P → P zero → (P i → P (sucMod i)) → ∀ i → P i
+  ```
+
+* In `Data.Fin.Mod.Induction`:
+  ```agda
+  induction : ∀ P → P k → (P i → P (sucMod i)) → ∀ i → P i
+  ```

src/Data/Fin/Mod.agda

@@ -0,0 +1,38 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- ℕ module n
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Fin.Mod where
+
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Fin.Base
+  using (Fin; zero; suc; toℕ; fromℕ; inject₁; opposite)
+open import Data.Fin.Relation.Unary.Top
+
+private variable
+  m n : ℕ
+
+infixl 6 _+_ _-_
+
+sucMod : Fin n → Fin n
+sucMod i with view i
+... | ‵fromℕ = zero
+... | ‵inj₁ i = suc ⟦ i ⟧
+
+predMod : Fin n → Fin n
+predMod zero = fromℕ _
+predMod (suc i) = inject₁ i
+
+_ℕ+_ : ℕ → Fin n → Fin n
+zero  ℕ+ i = i
+suc n ℕ+ i = sucMod (n ℕ+ i)
+
+_+_ : Fin n → Fin m → Fin n
+i + j = toℕ j ℕ+ i
+
+_-_ : Fin n → Fin m → Fin n
+i - j  = i + opposite j

src/Data/Fin/Mod/Induction.agda

@@ -0,0 +1,43 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Induction related to mod fin
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Fin.Mod.Induction where
+
+open import Function.Base using (id; _∘_; _$_)
+open import Data.Fin.Base hiding (_+_; _-_)
+open import Data.Fin.Induction using (<-weakInduction-startingFrom; <-weakInduction)
+open import Data.Fin.Properties
+open import Data.Fin.Mod
+open import Data.Fin.Mod.Properties
+open import Data.Nat.Base as ℕ using (ℕ; z≤n)
+open import Relation.Unary using (Pred)
+open import Relation.Binary.PropositionalEquality using (subst)
+
+private variable
+  m n : ℕ
+
+module _ {ℓ} (P : Pred (Fin (ℕ.suc n)) ℓ)
+  (Pᵢ⇒Pᵢ₊₁ : ∀ {i} → P i → P (sucMod i)) where
+
+  module _ {k} (Pₖ : P k) where
+
+    induction-≥ : ∀ {i} → i ≥ k → P i
+    induction-≥ = <-weakInduction-startingFrom P Pₖ Pᵢ⇒Pᵢ₊₁′
+      where
+      PInj : ∀ {i} → P (sucMod (inject₁ i)) → P (suc i)
+      PInj {i} rewrite sucMod-inject₁ i = id
+
+      Pᵢ⇒Pᵢ₊₁′ : ∀ i → P (inject₁ i) → P (suc i)
+      Pᵢ⇒Pᵢ₊₁′ _ = PInj ∘ Pᵢ⇒Pᵢ₊₁
+
+    induction-0 : P zero
+    induction-0 = subst P (sucMod-fromℕ _) $ Pᵢ⇒Pᵢ₊₁ $ induction-≥ $ ≤fromℕ _
+
+
+  induction : ∀ {k} (Pₖ : P k) → ∀ i → P i
+  induction Pₖ i = induction-≥ (induction-0 Pₖ) z≤n

src/Data/Fin/Mod/Properties.agda

@@ -0,0 +1,92 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties related to mod fin
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Fin.Mod.Properties where
+
+open import Function.Base using (id; _$_; _∘_)
+open import Data.Bool.Base using (true; false)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; NonZero)
+open import Data.Nat.Properties as ℕ
+  using (m≤n⇒m≤1+n; 1+n≰n; module ≤-Reasoning)
+open import Data.Fin.Base hiding (_+_; _-_)
+open import Data.Fin.Properties
+open import Data.Fin.Induction using (<-weakInduction)
+open import Data.Fin.Relation.Unary.Top
+open import Data.Fin.Mod
+open import Relation.Nullary.Decidable.Core using (Dec; yes; no)
+open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; _≢_; refl; sym; trans; cong; module ≡-Reasoning)
+open import Relation.Unary using (Pred)
+
+module _ {n : ℕ} where
+  open import Algebra.Definitions {A = Fin n} _≡_ public
+
+open ≡-Reasoning
+
+private variable
+  m n : ℕ
+
+------------------------------------------------------------------------
+-- sucMod
+
+sucMod-inject₁ : (i : Fin n) → sucMod (inject₁ i) ≡ suc i
+sucMod-inject₁ i rewrite view-inject₁ i =
+  cong suc (view-complete (view i))
+
+sucMod-fromℕ : ∀ n → sucMod (fromℕ n) ≡ zero
+sucMod-fromℕ n rewrite view-fromℕ n = refl
+
+------------------------------------------------------------------------
+-- predMod
+
+predMod-suc : (i : Fin n) → predMod (suc i) ≡ inject₁ i
+predMod-suc _ = refl
+
+predMod-sucMod : (i : Fin n) → predMod (sucMod i) ≡ i
+predMod-sucMod i with view i
+... | ‵fromℕ = refl
+... | ‵inj₁ p = cong inject₁ (view-complete p)
+
+sucMod-predMod : (i : Fin n) → sucMod (predMod i) ≡ i
+sucMod-predMod zero = sucMod-fromℕ _
+sucMod-predMod (suc i) = sucMod-inject₁ i
+
+------------------------------------------------------------------------
+-- _+ℕ_
+
++ℕ-identityʳ-toℕ : m ℕ.≤ n → toℕ (m ℕ+ zero {n}) ≡ m
++ℕ-identityʳ-toℕ {zero} m≤n = refl
++ℕ-identityʳ-toℕ {suc m} 1+m≤1+n@(s≤s m≤n) = begin
+  toℕ (sucMod (m ℕ+ zero))                ≡⟨ cong (toℕ ∘ sucMod) (toℕ-injective toℕm≡fromℕ<) ⟩
+  toℕ (sucMod (inject₁ (fromℕ< 1+m≤1+n))) ≡⟨ cong toℕ (sucMod-inject₁ _) ⟩
+  suc (toℕ (fromℕ< 1+m≤1+n))              ≡⟨ cong suc (toℕ-fromℕ< _) ⟩
+  suc m                                     ∎
+  where
+
+  toℕm≡fromℕ< = begin
+    toℕ (m ℕ+ zero)                ≡⟨ +ℕ-identityʳ-toℕ (m≤n⇒m≤1+n m≤n) ⟩
+    m                                ≡⟨ toℕ-fromℕ< _ ⟨
+    toℕ (fromℕ< 1+m≤1+n)           ≡⟨ toℕ-inject₁ _ ⟨
+    toℕ (inject₁ (fromℕ< 1+m≤1+n)) ∎
+
++ℕ-identityʳ : (m≤n : m ℕ.≤ n) → m ℕ+ zero ≡ fromℕ< (s≤s m≤n)
++ℕ-identityʳ {m} m≤n = toℕ-injective (begin
+  toℕ (m ℕ+ zero)        ≡⟨ +ℕ-identityʳ-toℕ m≤n ⟩
+  m                        ≡⟨ toℕ-fromℕ< _ ⟨
+  toℕ (fromℕ< (s≤s m≤n)) ∎)
+
+------------------------------------------------------------------------
+-- _+_
+
++-identityˡ : .{{ _ : NonZero n }} → LeftIdentity zeroFromNonZero _+_
++-identityˡ {suc n} i rewrite +ℕ-identityʳ {m = toℕ i} {n} _ = fromℕ<-toℕ _ (toℕ≤pred[n] _)
+
++-identityʳ : .{{ _ : NonZero n }} → RightIdentity zeroFromNonZero _+_
++-identityʳ {suc _} _ = refl
+

src/Data/Fin/Properties.agda

@@ -68,6 +68,9 @@ private
 nonZeroIndex : Fin n → ℕ.NonZero n
 nonZeroIndex {n = suc _} _ = _
 
+zeroFromNonZero : .⦃ _ : ℕ.NonZero n ⦄ → Fin n
+zeroFromNonZero {n = suc _} = zero
+
 ------------------------------------------------------------------------
 -- Bundles