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,34 @@ 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.Base`:
+  ```agda
+  zero⁺ : .⦃ NonZero n ⦄ → Fin n
+  suc⁺  : .⦃ NonZero n ⦄ → Fin (pred 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
+  sucMod-fromℕ          : ∀ n → sucMod (fromℕ n) ≡ zero
+  suc[fromℕ]≡zero       : ∀ n → sucMod (fromℕ n) ≡ zero
+  suc[fromℕ]≡zero⁻¹     : ∀ i : Fin (ℕ.suc n)) → (sucMod i ≡ zero) → i ≡ fromℕ n
+  suc[inject₁]≡suc[j]   : ∀ j → sucMod (inject₁ j) ≡ suc j
+  suc[inject₁]≡suc[j]⁻¹ : ∀ i j → (sucMod i ≡ suc j) → i ≡ inject₁ j
+  suc-injective         : ∀ {i j} → sucMod i ≡ sucMod j → i ≡ j
+  ```
+
+* In `Data.Fin.Mod.Induction`:
+  ```agda
+  induction : ∀ P → P k → (P i → P (sucMod i)) → ∀ i → P i
+  ```

src/Data/Fin/Base.agda

@@ -35,6 +35,14 @@ data Fin : ℕ → Set where
   zero : Fin (suc n)
   suc  : (i : Fin n) → Fin (suc n)
 
+-- Homogeneous Constructors
+
+zero⁺ : .⦃ ℕ.NonZero n ⦄ → Fin n
+zero⁺ {n = suc _} = zero
+
+suc⁺ : .⦃ ℕ.NonZero n ⦄ → Fin (ℕ.pred n) → Fin n
+suc⁺ {n = suc _} = suc
+
 -- A conversion: toℕ "i" = i.
 
 toℕ : Fin n → ℕ

src/Data/Fin/Mod.agda

@@ -0,0 +1,40 @@
+------------------------------------------------------------------------
+-- 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 {suc zero}    zero = zero
+sucMod {suc (suc n)} zero = suc zero
+sucMod {suc n@(suc _)} (suc i) with sucMod {n} i
+... | zero      = zero
+... | j@(suc _) = suc j
+
+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,128 @@
+------------------------------------------------------------------------
+-- 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 as Fin hiding (suc-injective)
+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₁ zero = refl
+sucMod-inject₁ (suc i) rewrite sucMod-inject₁ i = refl
+
+sucMod-fromℕ : ∀ n → sucMod (fromℕ n) ≡ zero
+sucMod-fromℕ zero = refl
+sucMod-fromℕ (suc n) rewrite sucMod-fromℕ n = refl
+
+suc[fromℕ]≡zero : ∀ n → sucMod (fromℕ n) ≡ zero
+suc[fromℕ]≡zero ℕ.zero                              = refl
+suc[fromℕ]≡zero (ℕ.suc n) rewrite suc[fromℕ]≡zero n = refl
+
+suc[fromℕ]≡zero⁻¹ : (i : Fin (ℕ.suc n)) → (sucMod i ≡ zero) → i ≡ fromℕ n
+suc[fromℕ]≡zero⁻¹ {n = ℕ.zero}  zero        _ = refl
+suc[fromℕ]≡zero⁻¹ {n = ℕ.suc _} (suc i) _ with zero ← sucMod i in eq
+  = cong suc (suc[fromℕ]≡zero⁻¹ i eq)
+
+suc[inject₁]≡suc[j] : (j : Fin n) → sucMod (inject₁ j) ≡ suc j
+suc[inject₁]≡suc[j] zero                                      = refl
+suc[inject₁]≡suc[j] (suc j) rewrite suc[inject₁]≡suc[j] j = refl
+
+suc[inject₁]≡suc[j]⁻¹ : (i : Fin (ℕ.suc n)) {j : Fin n} →
+                        (sucMod i ≡ suc j) → i ≡ inject₁ j
+suc[inject₁]≡suc[j]⁻¹ zero        {zero} = λ _ → refl
+suc[inject₁]≡suc[j]⁻¹ (suc i) {j}    with sucMod i in eqᵢ
+... | zero      rewrite eqᵢ = λ ()
+... | suc p rewrite eqᵢ = λ eq → begin
+  suc i           ≡⟨ cong suc (suc[inject₁]≡suc[j]⁻¹ i eqᵢ) ⟩
+  inject₁ (suc p) ≡⟨ cong inject₁ (Fin.suc-injective eq) ⟩
+  inject₁ j ∎ where open ≡-Reasoning
+
+suc-injective : {i j : Fin n} → sucMod i ≡ sucMod j → i ≡ j
+suc-injective {n = n} {i} {j} eq with sucMod i in eqᵢ | sucMod j in eqⱼ
+... | zero      | zero
+    = trans (suc[fromℕ]≡zero⁻¹ i eqᵢ) (sym (suc[fromℕ]≡zero⁻¹ j eqⱼ))
+... | suc p | suc q
+    = begin
+  i         ≡⟨ suc[inject₁]≡suc[j]⁻¹ i eqᵢ ⟩
+  inject₁ p ≡⟨ cong inject₁ (Fin.suc-injective eq) ⟩
+  inject₁ q ≡⟨ sym (suc[inject₁]≡suc[j]⁻¹ j eqⱼ) ⟩
+  j ∎ where open ≡-Reasoning
+
+------------------------------------------------------------------------
+-- 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 {suc zero} zero = refl
+predMod-sucMod {suc (suc n)} zero = refl
+predMod-sucMod {suc (suc n)} (suc i) with sucMod i | predMod-sucMod i
+... | zero   | eq rewrite eq = refl
+... | suc c1 | eq rewrite eq = refl
+
+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 zero⁺ _+_
++-identityˡ {suc n} i rewrite +ℕ-identityʳ {m = toℕ i} {n} _ = fromℕ<-toℕ _ (toℕ≤pred[n] _)
+
++-identityʳ : .{{ _ : NonZero n }} → RightIdentity zero⁺ _+_
++-identityʳ {suc _} _ = refl