diff --git a/CHANGELOG.md b/CHANGELOG.md index bf2d01d6a3..d1558b79c6 100644 --- a/CHANGELOG.md +++ b/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 + ``` diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index d762e10007..132529eb7d 100644 --- a/src/Data/Fin/Base.agda +++ b/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 → ℕ diff --git a/src/Data/Fin/Mod.agda b/src/Data/Fin/Mod.agda new file mode 100644 index 0000000000..816a2a8f71 --- /dev/null +++ b/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 diff --git a/src/Data/Fin/Mod/Induction.agda b/src/Data/Fin/Mod/Induction.agda new file mode 100644 index 0000000000..7b86adffb2 --- /dev/null +++ b/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 diff --git a/src/Data/Fin/Mod/Properties.agda b/src/Data/Fin/Mod/Properties.agda new file mode 100644 index 0000000000..f808e6da27 --- /dev/null +++ b/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