From 19566db3e4401a51165b33010896adaa269bc53d Mon Sep 17 00:00:00 2001 From: Guilherme Date: Sun, 27 Aug 2023 16:21:12 +0200 Subject: [PATCH 01/23] Added Z mod n as Fin --- CHANGELOG.md | 17 +++++++ src/Data/Fin/Mod.agda | 107 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 124 insertions(+) create mode 100644 src/Data/Fin/Mod.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 5138c4017f..52617ec357 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3361,3 +3361,20 @@ This is a full list of proofs that have changed form to use irrelevant instance c ≈⟨ c≈d ⟩ d ∎ ``` + +* Added new file `Data.Fin.Mod` + ```agda + suc : Fin n → Fin n + pred : Fin n → Fin n + _ℕ+_ : ℕ → Fin n → Fin n + _+_ : Fin m → Fin n → Fin n + _+‵_ : Fin n → Fin n → Fin n + _-_ : Fin n → Fin n → Fin n + suc-inj≡fsuc : ∀ i → suc (inject₁ i) ≡ F.suc i + pred-fsuc≡inj : ∀ i → pred (F.suc i) ≡ inject₁ i + suc-pred≡id : ∀ i → suc (pred i) ≡ i + pred-suc≡id : ∀ i → pred (suc i) ≡ i + +-identityˡ : LeftIdentity {ℕ.suc n} zero _+_ + +ℕ-identityʳ : m ℕ.≤ suc n → toℕ (m ℕ+ zero) ≡ m + +-identityʳ : RightIdentity zero _+_ + ``` diff --git a/src/Data/Fin/Mod.agda b/src/Data/Fin/Mod.agda new file mode 100644 index 0000000000..266e4d9729 --- /dev/null +++ b/src/Data/Fin/Mod.agda @@ -0,0 +1,107 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- ℤ module n +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.Fin.Mod where + +open import Function using (_$_; _∘_) +open import Data.Bool using (true; false) +open import Data.Nat as ℕ using (ℕ; s≤s) +open import Data.Nat.Properties as ℕ + using (m≤n⇒m≤1+n; 1+n≰n; module ≤-Reasoning) +open import Data.Fin as F hiding (suc; pred; _+_; _-_) +open import Data.Fin.Properties +open import Relation.Nullary using (Dec; yes; no; contradiction) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl; sym; trans; cong; module ≡-Reasoning) +import Algebra.Definitions as ADef + +private variable + m n : ℕ + +open module AD {n} = ADef {A = Fin n} _≡_ + +private + hs : ∀ {i : Fin (ℕ.suc n)} → i ≢ fromℕ n → Fin (ℕ.suc n) + hs {i = i} i≢n = lower₁ (F.suc i) help + where + help : _ + help = i≢n ∘ sym ∘ toℕ-injective ∘ trans (toℕ-fromℕ _) ∘ cong ℕ.pred + +suc : Fin n → Fin n +suc {ℕ.suc n} i with i ≟ fromℕ n +... | yes _ = zero +... | no i≢n = hs i≢n + +pred : Fin n → Fin n +pred zero = fromℕ _ +pred (F.suc i) = inject₁ i + +_ℕ+_ : ℕ → Fin n → Fin n +ℕ.zero ℕ+ i = i +ℕ.suc n ℕ+ i = suc (n ℕ+ i) + +_+_ : Fin m → Fin n → Fin n +i + j = toℕ i ℕ+ j + +_+‵_ : Fin n → Fin n → Fin n +_+‵_ = _+_ + +_-_ : Fin n → Fin n → Fin n +i - j = i + opposite j + +private + inject₁≢fromℕ : {i : Fin n} → inject₁ i ≢ fromℕ n + inject₁≢fromℕ {n} {i} i≡n = 1+n≰n $ begin-strict + toℕ (fromℕ n) ≡˘⟨ cong toℕ i≡n ⟩ + toℕ (inject₁ i) <⟨ inject₁ℕ< i ⟩ + n ≡˘⟨ toℕ-fromℕ n ⟩ + toℕ (fromℕ n) ∎ + where open ≤-Reasoning + +suc-inj≡fsuc : (i : Fin n) → suc (inject₁ i) ≡ F.suc i +suc-inj≡fsuc {n} i with inject₁ i ≟ fromℕ _ +... | yes i≡n = contradiction i≡n inject₁≢fromℕ +... | no i≢n = cong F.suc (toℕ-injective (trans (toℕ-lower₁ _ _) (toℕ-inject₁ _))) + +pred-fsuc≡inj : (i : Fin n) → pred (F.suc i) ≡ inject₁ i +pred-fsuc≡inj _ = refl + +suc-pred≡id : (i : Fin n) → suc (pred i) ≡ i +suc-pred≡id {ℕ.suc n} zero with fromℕ n ≟ fromℕ n +... | yes _ = refl +... | no n≢n = contradiction refl n≢n +suc-pred≡id {ℕ.suc n} (F.suc i) = suc-inj≡fsuc i + +pred-suc≡id : (i : Fin n) → pred (suc i) ≡ i +pred-suc≡id {ℕ.suc n} i with i ≟ fromℕ n +... | yes refl = refl +... | no _ = inject₁-lower₁ _ _ + ++-identityˡ : LeftIdentity {ℕ.suc n} zero _+_ ++-identityˡ _ = refl + ++ℕ-identityʳ : ∀ {n′} (let n = ℕ.suc n′) → m ℕ.≤ n → toℕ (m ℕ+ zero {n}) ≡ m ++ℕ-identityʳ {ℕ.zero} m≤n = refl ++ℕ-identityʳ {ℕ.suc m} {n} (s≤s m≤n) with (m ℕ+ zero) ≟ F.suc (fromℕ n) +... | yes m+0≡sn = contradiction (begin-strict + ℕ.suc n ≡˘⟨ cong ℕ.suc (toℕ-fromℕ n) ⟩ + ℕ.suc (toℕ (fromℕ n)) ≡˘⟨ cong toℕ m+0≡sn ⟩ + toℕ (m ℕ+ zero) ≡⟨ +ℕ-identityʳ (m≤n⇒m≤1+n m≤n) ⟩ + m <⟨ s≤s m≤n ⟩ + ℕ.suc n ∎) 1+n≰n + where open ≤-Reasoning + +... | no _ = cong ℕ.suc (begin + toℕ (lower₁ (m ℕ+ zero) _) ≡⟨ toℕ-lower₁ (m ℕ+ zero) _ ⟩ + toℕ (m ℕ+ zero) ≡⟨ +ℕ-identityʳ (m≤n⇒m≤1+n m≤n) ⟩ + m ∎) + where open ≡-Reasoning + ++-identityʳ : RightIdentity {ℕ.suc n} zero _+_ ++-identityʳ {ℕ.zero} zero = refl ++-identityʳ {ℕ.suc _} = toℕ-injective ∘ +ℕ-identityʳ ∘ toℕ≤pred[n] From c87e35aa7e40b7fda3fcba2e9fe60cc6a08bde5b Mon Sep 17 00:00:00 2001 From: Guilherme Date: Sun, 8 Oct 2023 00:36:40 +0200 Subject: [PATCH 02/23] changed suc and pred definitions --- src/Data/Fin/Mod.agda | 88 +++++++++++++++++++------------------------ 1 file changed, 39 insertions(+), 49 deletions(-) diff --git a/src/Data/Fin/Mod.agda b/src/Data/Fin/Mod.agda index 266e4d9729..38b9e0aa3d 100644 --- a/src/Data/Fin/Mod.agda +++ b/src/Data/Fin/Mod.agda @@ -10,12 +10,15 @@ module Data.Fin.Mod where open import Function using (_$_; _∘_) open import Data.Bool using (true; false) -open import Data.Nat as ℕ using (ℕ; s≤s) +open import Data.Product +open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s) open import Data.Nat.Properties as ℕ using (m≤n⇒m≤1+n; 1+n≰n; module ≤-Reasoning) -open import Data.Fin as F hiding (suc; pred; _+_; _-_) +open import Data.Fin.Base as F hiding (suc; pred; _+_; _-_) open import Data.Fin.Properties -open import Relation.Nullary using (Dec; yes; no; contradiction) +open import Data.Fin.Relation.Unary.Top +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) import Algebra.Definitions as ADef @@ -24,18 +27,14 @@ private variable m n : ℕ open module AD {n} = ADef {A = Fin n} _≡_ +open ≡-Reasoning -private - hs : ∀ {i : Fin (ℕ.suc n)} → i ≢ fromℕ n → Fin (ℕ.suc n) - hs {i = i} i≢n = lower₁ (F.suc i) help - where - help : _ - help = i≢n ∘ sym ∘ toℕ-injective ∘ trans (toℕ-fromℕ _) ∘ cong ℕ.pred +infixl 6 _+_ _+‵_ suc : Fin n → Fin n -suc {ℕ.suc n} i with i ≟ fromℕ n -... | yes _ = zero -... | no i≢n = hs i≢n +suc i with view i +... | ‵fromℕ = zero +... | ‵inj₁ i = F.suc ⟦ i ⟧ pred : Fin n → Fin n pred zero = fromℕ _ @@ -45,6 +44,7 @@ _ℕ+_ : ℕ → Fin n → Fin n ℕ.zero ℕ+ i = i ℕ.suc n ℕ+ i = suc (n ℕ+ i) + _+_ : Fin m → Fin n → Fin n i + j = toℕ i ℕ+ j @@ -54,54 +54,44 @@ _+‵_ = _+_ _-_ : Fin n → Fin n → Fin n i - j = i + opposite j -private - inject₁≢fromℕ : {i : Fin n} → inject₁ i ≢ fromℕ n - inject₁≢fromℕ {n} {i} i≡n = 1+n≰n $ begin-strict - toℕ (fromℕ n) ≡˘⟨ cong toℕ i≡n ⟩ - toℕ (inject₁ i) <⟨ inject₁ℕ< i ⟩ - n ≡˘⟨ toℕ-fromℕ n ⟩ - toℕ (fromℕ n) ∎ - where open ≤-Reasoning - suc-inj≡fsuc : (i : Fin n) → suc (inject₁ i) ≡ F.suc i -suc-inj≡fsuc {n} i with inject₁ i ≟ fromℕ _ -... | yes i≡n = contradiction i≡n inject₁≢fromℕ -... | no i≢n = cong F.suc (toℕ-injective (trans (toℕ-lower₁ _ _) (toℕ-inject₁ _))) +suc-inj≡fsuc i rewrite view-inject₁ i = cong F.suc (view-complete (view i)) + +sucFromℕ≡0 : ∀ n → suc (fromℕ n) ≡ zero +sucFromℕ≡0 n rewrite view-fromℕ n = refl pred-fsuc≡inj : (i : Fin n) → pred (F.suc i) ≡ inject₁ i pred-fsuc≡inj _ = refl suc-pred≡id : (i : Fin n) → suc (pred i) ≡ i -suc-pred≡id {ℕ.suc n} zero with fromℕ n ≟ fromℕ n -... | yes _ = refl -... | no n≢n = contradiction refl n≢n -suc-pred≡id {ℕ.suc n} (F.suc i) = suc-inj≡fsuc i +suc-pred≡id zero = sucFromℕ≡0 _ +suc-pred≡id (F.suc i) = suc-inj≡fsuc i pred-suc≡id : (i : Fin n) → pred (suc i) ≡ i -pred-suc≡id {ℕ.suc n} i with i ≟ fromℕ n -... | yes refl = refl -... | no _ = inject₁-lower₁ _ _ +pred-suc≡id i with view i +... | ‵fromℕ = refl +... | ‵inj₁ p = cong inject₁ (view-complete p) +-identityˡ : LeftIdentity {ℕ.suc n} zero _+_ +-identityˡ _ = refl -+ℕ-identityʳ : ∀ {n′} (let n = ℕ.suc n′) → m ℕ.≤ n → toℕ (m ℕ+ zero {n}) ≡ m -+ℕ-identityʳ {ℕ.zero} m≤n = refl -+ℕ-identityʳ {ℕ.suc m} {n} (s≤s m≤n) with (m ℕ+ zero) ≟ F.suc (fromℕ n) -... | yes m+0≡sn = contradiction (begin-strict - ℕ.suc n ≡˘⟨ cong ℕ.suc (toℕ-fromℕ n) ⟩ - ℕ.suc (toℕ (fromℕ n)) ≡˘⟨ cong toℕ m+0≡sn ⟩ - toℕ (m ℕ+ zero) ≡⟨ +ℕ-identityʳ (m≤n⇒m≤1+n m≤n) ⟩ - m <⟨ s≤s m≤n ⟩ - ℕ.suc n ∎) 1+n≰n - where open ≤-Reasoning - -... | no _ = cong ℕ.suc (begin - toℕ (lower₁ (m ℕ+ zero) _) ≡⟨ toℕ-lower₁ (m ℕ+ zero) _ ⟩ - toℕ (m ℕ+ zero) ≡⟨ +ℕ-identityʳ (m≤n⇒m≤1+n m≤n) ⟩ - m ∎) - where open ≡-Reasoning ++ℕ-identityʳ : ∀ {n′} (let n = ℕ.suc n′) (m≤n : m ℕ.≤ n′) → + m ℕ+ zero {n′} ≡ fromℕ< (s≤s m≤n) ++ℕ-identityʳ {ℕ.zero} z≤n = refl ++ℕ-identityʳ {ℕ.suc m} {n} (s≤s m≤n) = begin + suc (m ℕ+ zero) ≡⟨ cong suc (+ℕ-identityʳ {m} (m≤n⇒m≤1+n m≤n)) ⟩ + suc (fromℕ< {m} {ℕ.suc n} (s≤s (m≤n⇒m≤1+n m≤n))) + ≡⟨ cong suc (toℕ-injective helper2) ⟩ + suc (inject₁ (fromℕ< (s≤s m≤n))) ≡⟨ helper ⟩ + F.suc (fromℕ< (s≤s m≤n)) ∎ + + where + + helper : suc (inject₁ (fromℕ< (s≤s m≤n))) ≡ F.suc (fromℕ< (s≤s m≤n)) + helper rewrite view-inject₁ $ fromℕ< $ s≤s m≤n = cong F.suc + (view-complete (view $ fromℕ< (s≤s m≤n))) + + helper2 = trans (toℕ-fromℕ< _) (sym (trans (toℕ-inject₁ _) (toℕ-fromℕ< _))) +-identityʳ : RightIdentity {ℕ.suc n} zero _+_ -+-identityʳ {ℕ.zero} zero = refl -+-identityʳ {ℕ.suc _} = toℕ-injective ∘ +ℕ-identityʳ ∘ toℕ≤pred[n] ++-identityʳ {n} i rewrite +ℕ-identityʳ {m = toℕ i} {n} _ = fromℕ<-toℕ _ (toℕ≤pred[n] _) From af96faa93734ed1f3fe5aa99ebbb766754a96aac Mon Sep 17 00:00:00 2001 From: Guilherme Date: Sun, 8 Oct 2023 12:36:36 +0200 Subject: [PATCH 03/23] removed addition and added new identity --- src/Data/Fin/Mod.agda | 26 ++++++++++++++++++++------ 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/src/Data/Fin/Mod.agda b/src/Data/Fin/Mod.agda index 38b9e0aa3d..1602d17858 100644 --- a/src/Data/Fin/Mod.agda +++ b/src/Data/Fin/Mod.agda @@ -29,7 +29,7 @@ private variable open module AD {n} = ADef {A = Fin n} _≡_ open ≡-Reasoning -infixl 6 _+_ _+‵_ +infixl 6 _+_ _-_ suc : Fin n → Fin n suc i with view i @@ -44,13 +44,9 @@ _ℕ+_ : ℕ → Fin n → Fin n ℕ.zero ℕ+ i = i ℕ.suc n ℕ+ i = suc (n ℕ+ i) - _+_ : Fin m → Fin n → Fin n i + j = toℕ i ℕ+ j -_+‵_ : Fin n → Fin n → Fin n -_+‵_ = _+_ - _-_ : Fin n → Fin n → Fin n i - j = i + opposite j @@ -75,8 +71,26 @@ pred-suc≡id i with view i +-identityˡ : LeftIdentity {ℕ.suc n} zero _+_ +-identityˡ _ = refl ++ℕ-identityʳ-toℕ : ∀ {n′} (let n = ℕ.suc n′) (m≤n : m ℕ.≤ n′) → + toℕ (m ℕ+ zero {n′}) ≡ m ++ℕ-identityʳ-toℕ {ℕ.zero} m≤n = refl ++ℕ-identityʳ-toℕ {ℕ.suc m} {n} (s≤s m≤n) = begin + toℕ (suc (m ℕ+ zero)) ≡⟨ cong (toℕ ∘ suc) (toℕ-injective toℕm≡fromℕ<) ⟩ + toℕ (suc (inject₁ (fromℕ< (s≤s m≤n)))) ≡⟨ cong toℕ (suc-inj≡fsuc _) ⟩ + ℕ.suc (toℕ (fromℕ< (s≤s m≤n))) ≡⟨ cong ℕ.suc (toℕ-fromℕ< _) ⟩ + -- ? ≡⟨ ? ⟩ + ℕ.suc m ∎ + where + + toℕm≡fromℕ< = begin + toℕ (m ℕ+ zero {n}) ≡⟨ +ℕ-identityʳ-toℕ (m≤n⇒m≤1+n m≤n) ⟩ + m ≡˘⟨ toℕ-fromℕ< _ ⟩ + toℕ (fromℕ< (s≤s m≤n)) ≡˘⟨ toℕ-inject₁ _ ⟩ + toℕ (inject₁ (fromℕ< (s≤s m≤n))) ∎ + + +ℕ-identityʳ : ∀ {n′} (let n = ℕ.suc n′) (m≤n : m ℕ.≤ n′) → - m ℕ+ zero {n′} ≡ fromℕ< (s≤s m≤n) + m ℕ+ zero ≡ fromℕ< (s≤s m≤n) +ℕ-identityʳ {ℕ.zero} z≤n = refl +ℕ-identityʳ {ℕ.suc m} {n} (s≤s m≤n) = begin suc (m ℕ+ zero) ≡⟨ cong suc (+ℕ-identityʳ {m} (m≤n⇒m≤1+n m≤n)) ⟩ From 7e6a3923f8838232a1d8cf729682db4b5478a938 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Sun, 8 Oct 2023 12:40:02 +0200 Subject: [PATCH 04/23] removed unnecessary implicit arguments --- src/Data/Fin/Mod.agda | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/src/Data/Fin/Mod.agda b/src/Data/Fin/Mod.agda index 1602d17858..86b0d2aaf0 100644 --- a/src/Data/Fin/Mod.agda +++ b/src/Data/Fin/Mod.agda @@ -71,30 +71,26 @@ pred-suc≡id i with view i +-identityˡ : LeftIdentity {ℕ.suc n} zero _+_ +-identityˡ _ = refl -+ℕ-identityʳ-toℕ : ∀ {n′} (let n = ℕ.suc n′) (m≤n : m ℕ.≤ n′) → - toℕ (m ℕ+ zero {n′}) ≡ m ++ℕ-identityʳ-toℕ : (m≤n : m ℕ.≤ n) → toℕ (m ℕ+ zero {n}) ≡ m +ℕ-identityʳ-toℕ {ℕ.zero} m≤n = refl -+ℕ-identityʳ-toℕ {ℕ.suc m} {n} (s≤s m≤n) = begin ++ℕ-identityʳ-toℕ {ℕ.suc m} (s≤s m≤n) = begin toℕ (suc (m ℕ+ zero)) ≡⟨ cong (toℕ ∘ suc) (toℕ-injective toℕm≡fromℕ<) ⟩ toℕ (suc (inject₁ (fromℕ< (s≤s m≤n)))) ≡⟨ cong toℕ (suc-inj≡fsuc _) ⟩ ℕ.suc (toℕ (fromℕ< (s≤s m≤n))) ≡⟨ cong ℕ.suc (toℕ-fromℕ< _) ⟩ - -- ? ≡⟨ ? ⟩ ℕ.suc m ∎ where toℕm≡fromℕ< = begin - toℕ (m ℕ+ zero {n}) ≡⟨ +ℕ-identityʳ-toℕ (m≤n⇒m≤1+n m≤n) ⟩ + toℕ (m ℕ+ zero) ≡⟨ +ℕ-identityʳ-toℕ (m≤n⇒m≤1+n m≤n) ⟩ m ≡˘⟨ toℕ-fromℕ< _ ⟩ toℕ (fromℕ< (s≤s m≤n)) ≡˘⟨ toℕ-inject₁ _ ⟩ toℕ (inject₁ (fromℕ< (s≤s m≤n))) ∎ - -+ℕ-identityʳ : ∀ {n′} (let n = ℕ.suc n′) (m≤n : m ℕ.≤ n′) → - m ℕ+ zero ≡ fromℕ< (s≤s m≤n) ++ℕ-identityʳ : ∀ {n} (m≤n : m ℕ.≤ n) → m ℕ+ zero ≡ fromℕ< (s≤s m≤n) +ℕ-identityʳ {ℕ.zero} z≤n = refl -+ℕ-identityʳ {ℕ.suc m} {n} (s≤s m≤n) = begin ++ℕ-identityʳ {ℕ.suc m} (s≤s m≤n) = begin suc (m ℕ+ zero) ≡⟨ cong suc (+ℕ-identityʳ {m} (m≤n⇒m≤1+n m≤n)) ⟩ - suc (fromℕ< {m} {ℕ.suc n} (s≤s (m≤n⇒m≤1+n m≤n))) + suc (fromℕ< (s≤s (m≤n⇒m≤1+n m≤n))) ≡⟨ cong suc (toℕ-injective helper2) ⟩ suc (inject₁ (fromℕ< (s≤s m≤n))) ≡⟨ helper ⟩ F.suc (fromℕ< (s≤s m≤n)) ∎ From 467b190cacfe541efda991cd01e57bb69ce7d6c6 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Sun, 8 Oct 2023 12:57:37 +0200 Subject: [PATCH 05/23] removed unnecessary identity part --- src/Data/Fin/Mod.agda | 21 +++++---------------- 1 file changed, 5 insertions(+), 16 deletions(-) diff --git a/src/Data/Fin/Mod.agda b/src/Data/Fin/Mod.agda index 86b0d2aaf0..ef20a034cc 100644 --- a/src/Data/Fin/Mod.agda +++ b/src/Data/Fin/Mod.agda @@ -86,22 +86,11 @@ pred-suc≡id i with view i toℕ (fromℕ< (s≤s m≤n)) ≡˘⟨ toℕ-inject₁ _ ⟩ toℕ (inject₁ (fromℕ< (s≤s m≤n))) ∎ -+ℕ-identityʳ : ∀ {n} (m≤n : m ℕ.≤ n) → m ℕ+ zero ≡ fromℕ< (s≤s m≤n) -+ℕ-identityʳ {ℕ.zero} z≤n = refl -+ℕ-identityʳ {ℕ.suc m} (s≤s m≤n) = begin - suc (m ℕ+ zero) ≡⟨ cong suc (+ℕ-identityʳ {m} (m≤n⇒m≤1+n m≤n)) ⟩ - suc (fromℕ< (s≤s (m≤n⇒m≤1+n m≤n))) - ≡⟨ cong suc (toℕ-injective helper2) ⟩ - suc (inject₁ (fromℕ< (s≤s m≤n))) ≡⟨ helper ⟩ - F.suc (fromℕ< (s≤s m≤n)) ∎ - - where - - helper : suc (inject₁ (fromℕ< (s≤s m≤n))) ≡ F.suc (fromℕ< (s≤s m≤n)) - helper rewrite view-inject₁ $ fromℕ< $ s≤s m≤n = cong F.suc - (view-complete (view $ fromℕ< (s≤s m≤n))) - - helper2 = trans (toℕ-fromℕ< _) (sym (trans (toℕ-inject₁ _) (toℕ-fromℕ< _))) ++ℕ-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ʳ : RightIdentity {ℕ.suc n} zero _+_ +-identityʳ {n} i rewrite +ℕ-identityʳ {m = toℕ i} {n} _ = fromℕ<-toℕ _ (toℕ≤pred[n] _) From 600035c2973ecb21adc14d57ef0c0d3018cd407f Mon Sep 17 00:00:00 2001 From: Guilherme Date: Sun, 8 Oct 2023 13:00:00 +0200 Subject: [PATCH 06/23] added my modifications to CHANGELOG --- CHANGELOG.md | 4 ++-- src/Data/Fin/Mod.agda | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a842af1bd4..59a9a62d30 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3795,13 +3795,13 @@ This is a full list of proofs that have changed form to use irrelevant instance pred : Fin n → Fin n _ℕ+_ : ℕ → Fin n → Fin n _+_ : Fin m → Fin n → Fin n - _+‵_ : Fin n → Fin n → Fin n _-_ : Fin n → Fin n → Fin n suc-inj≡fsuc : ∀ i → suc (inject₁ i) ≡ F.suc i pred-fsuc≡inj : ∀ i → pred (F.suc i) ≡ inject₁ i suc-pred≡id : ∀ i → suc (pred i) ≡ i pred-suc≡id : ∀ i → pred (suc i) ≡ i +-identityˡ : LeftIdentity {ℕ.suc n} zero _+_ - +ℕ-identityʳ : m ℕ.≤ suc n → toℕ (m ℕ+ zero) ≡ m + +ℕ-identityʳ-toℕ : m ℕ.≤ n → toℕ (m ℕ+ zero) ≡ m + +ℕ-identityʳ : (m≤n : m ℕ.≤ n) → m ℕ+ zero ≡ fromℕ< (s≤s m≤n) +-identityʳ : RightIdentity zero _+_ ``` diff --git a/src/Data/Fin/Mod.agda b/src/Data/Fin/Mod.agda index ef20a034cc..dc3b1366ee 100644 --- a/src/Data/Fin/Mod.agda +++ b/src/Data/Fin/Mod.agda @@ -71,7 +71,7 @@ pred-suc≡id i with view i +-identityˡ : LeftIdentity {ℕ.suc n} zero _+_ +-identityˡ _ = refl -+ℕ-identityʳ-toℕ : (m≤n : m ℕ.≤ n) → toℕ (m ℕ+ zero {n}) ≡ m ++ℕ-identityʳ-toℕ : m ℕ.≤ n → toℕ (m ℕ+ zero {n}) ≡ m +ℕ-identityʳ-toℕ {ℕ.zero} m≤n = refl +ℕ-identityʳ-toℕ {ℕ.suc m} (s≤s m≤n) = begin toℕ (suc (m ℕ+ zero)) ≡⟨ cong (toℕ ∘ suc) (toℕ-injective toℕm≡fromℕ<) ⟩ From 5cdbaf7c7a969a36541467b744f26d09bd1b2fee Mon Sep 17 00:00:00 2001 From: Guilherme Date: Fri, 20 Oct 2023 16:43:11 +0200 Subject: [PATCH 07/23] added induction --- CHANGELOG.md | 1 + src/Data/Fin/Mod.agda | 21 ++++++++++++++++++--- 2 files changed, 19 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 59a9a62d30..411b260c8f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3804,4 +3804,5 @@ This is a full list of proofs that have changed form to use irrelevant instance +ℕ-identityʳ-toℕ : m ℕ.≤ n → toℕ (m ℕ+ zero) ≡ m +ℕ-identityʳ : (m≤n : m ℕ.≤ n) → m ℕ+ zero ≡ fromℕ< (s≤s m≤n) +-identityʳ : RightIdentity zero _+_ + induction : P zero → (P i → P (suc i)) → ∀ i → P i ``` diff --git a/src/Data/Fin/Mod.agda b/src/Data/Fin/Mod.agda index dc3b1366ee..a89983aa32 100644 --- a/src/Data/Fin/Mod.agda +++ b/src/Data/Fin/Mod.agda @@ -8,7 +8,7 @@ module Data.Fin.Mod where -open import Function using (_$_; _∘_) +open import Function using (id; _$_; _∘_) open import Data.Bool using (true; false) open import Data.Product open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s) @@ -16,12 +16,14 @@ open import Data.Nat.Properties as ℕ using (m≤n⇒m≤1+n; 1+n≰n; module ≤-Reasoning) open import Data.Fin.Base as F hiding (suc; pred; _+_; _-_) open import Data.Fin.Properties +open import Data.Fin.Induction using (<-weakInduction) open import Data.Fin.Relation.Unary.Top 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) import Algebra.Definitions as ADef +open import Relation.Unary using (Pred) private variable m n : ℕ @@ -74,9 +76,9 @@ pred-suc≡id i with view i +ℕ-identityʳ-toℕ : m ℕ.≤ n → toℕ (m ℕ+ zero {n}) ≡ m +ℕ-identityʳ-toℕ {ℕ.zero} m≤n = refl +ℕ-identityʳ-toℕ {ℕ.suc m} (s≤s m≤n) = begin - toℕ (suc (m ℕ+ zero)) ≡⟨ cong (toℕ ∘ suc) (toℕ-injective toℕm≡fromℕ<) ⟩ + toℕ (suc (m ℕ+ zero)) ≡⟨ cong (toℕ ∘ suc) (toℕ-injective toℕm≡fromℕ<) ⟩ toℕ (suc (inject₁ (fromℕ< (s≤s m≤n)))) ≡⟨ cong toℕ (suc-inj≡fsuc _) ⟩ - ℕ.suc (toℕ (fromℕ< (s≤s m≤n))) ≡⟨ cong ℕ.suc (toℕ-fromℕ< _) ⟩ + ℕ.suc (toℕ (fromℕ< (s≤s m≤n))) ≡⟨ cong ℕ.suc (toℕ-fromℕ< _) ⟩ ℕ.suc m ∎ where @@ -94,3 +96,16 @@ pred-suc≡id i with view i +-identityʳ : RightIdentity {ℕ.suc n} zero _+_ +-identityʳ {n} i rewrite +ℕ-identityʳ {m = toℕ i} {n} _ = fromℕ<-toℕ _ (toℕ≤pred[n] _) + +induction : ∀ {ℓ} (P : Pred (Fin (ℕ.suc n)) ℓ) + → P zero + → (∀ {i} → P i → P (suc i)) + → ∀ i → P i +induction P P₀ Pᵢ⇒Pᵢ₊₁ i = <-weakInduction P P₀ Pᵢ⇒Pᵢ₊₁′ i + where + + PInj : ∀ {i} → P (suc (inject₁ i)) → P (F.suc i) + PInj {i} rewrite suc-inj≡fsuc i = id + + Pᵢ⇒Pᵢ₊₁′ : ∀ i → P (inject₁ i) → P (F.suc i) + Pᵢ⇒Pᵢ₊₁′ _ Pi = PInj (Pᵢ⇒Pᵢ₊₁ Pi) From e64b5434c10b0f94ee92179891922ba82a56b82b Mon Sep 17 00:00:00 2001 From: Guilherme Date: Sat, 21 Oct 2023 10:52:43 +0200 Subject: [PATCH 08/23] added a little change --- src/Data/Fin/Mod.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Fin/Mod.agda b/src/Data/Fin/Mod.agda index a89983aa32..d448cb5406 100644 --- a/src/Data/Fin/Mod.agda +++ b/src/Data/Fin/Mod.agda @@ -84,7 +84,7 @@ pred-suc≡id i with view i toℕm≡fromℕ< = begin toℕ (m ℕ+ zero) ≡⟨ +ℕ-identityʳ-toℕ (m≤n⇒m≤1+n m≤n) ⟩ - m ≡˘⟨ toℕ-fromℕ< _ ⟩ + m ≡˘⟨ toℕ-fromℕ< _ ⟩ toℕ (fromℕ< (s≤s m≤n)) ≡˘⟨ toℕ-inject₁ _ ⟩ toℕ (inject₁ (fromℕ< (s≤s m≤n))) ∎ From 1d28e8e7303ac10737ae6439d06c98ab56541f79 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Thu, 4 Jan 2024 10:55:19 +0100 Subject: [PATCH 09/23] added modifications --- src/Data/Fin/Mod.agda | 68 ++++++++++++++++---------------- src/Data/Fin/Mod/Properties.agda | 3 ++ src/Data/Fin/Properties.agda | 3 ++ 3 files changed, 40 insertions(+), 34 deletions(-) create mode 100644 src/Data/Fin/Mod/Properties.agda diff --git a/src/Data/Fin/Mod.agda b/src/Data/Fin/Mod.agda index d448cb5406..ed2a5d0fc5 100644 --- a/src/Data/Fin/Mod.agda +++ b/src/Data/Fin/Mod.agda @@ -1,17 +1,17 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- ℤ module n +-- ℕ module n ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Data.Fin.Mod where -open import Function using (id; _$_; _∘_) -open import Data.Bool using (true; false) -open import Data.Product -open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s) +open import Function.Base using (id; _$_; _∘_) +open import Data.Bool.Base using (true; false) +open import Data.Product.Base +open import Data.Nat.Base as ℕ using (ℕ; 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 as F hiding (suc; pred; _+_; _-_) @@ -25,48 +25,48 @@ open import Relation.Binary.PropositionalEquality import Algebra.Definitions as ADef open import Relation.Unary using (Pred) -private variable - m n : ℕ - open module AD {n} = ADef {A = Fin n} _≡_ open ≡-Reasoning +private variable + m n : ℕ + infixl 6 _+_ _-_ -suc : Fin n → Fin n -suc i with view i +sucAbsorb : Fin n → Fin n +sucAbsorb i with view i ... | ‵fromℕ = zero ... | ‵inj₁ i = F.suc ⟦ i ⟧ -pred : Fin n → Fin n -pred zero = fromℕ _ -pred (F.suc i) = inject₁ i +predAbsorb : Fin n → Fin n +predAbsorb zero = fromℕ _ +predAbsorb (F.suc i) = inject₁ i _ℕ+_ : ℕ → Fin n → Fin n ℕ.zero ℕ+ i = i -ℕ.suc n ℕ+ i = suc (n ℕ+ i) +ℕ.suc n ℕ+ i = sucAbsorb (n ℕ+ i) _+_ : Fin m → Fin n → Fin n i + j = toℕ i ℕ+ j -_-_ : Fin n → Fin n → Fin n -i - j = i + opposite j +_-_ : Fin m → Fin n → Fin m +i - j = opposite j + i -suc-inj≡fsuc : (i : Fin n) → suc (inject₁ i) ≡ F.suc i -suc-inj≡fsuc i rewrite view-inject₁ i = cong F.suc (view-complete (view i)) +suc-inject₁ : (i : Fin n) → sucAbsorb (inject₁ i) ≡ F.suc i +suc-inject₁ i rewrite view-inject₁ i = cong F.suc (view-complete (view i)) -sucFromℕ≡0 : ∀ n → suc (fromℕ n) ≡ zero -sucFromℕ≡0 n rewrite view-fromℕ n = refl +suc-fromℕ : ∀ n → sucAbsorb (fromℕ n) ≡ zero +suc-fromℕ n rewrite view-fromℕ n = refl -pred-fsuc≡inj : (i : Fin n) → pred (F.suc i) ≡ inject₁ i -pred-fsuc≡inj _ = refl +pred-sucAbsorb : (i : Fin n) → predAbsorb (F.suc i) ≡ inject₁ i +pred-sucAbsorb _ = refl -suc-pred≡id : (i : Fin n) → suc (pred i) ≡ i -suc-pred≡id zero = sucFromℕ≡0 _ -suc-pred≡id (F.suc i) = suc-inj≡fsuc i +suc-pred≡id : (i : Fin n) → sucAbsorb (predAbsorb i) ≡ i +suc-pred≡id zero = suc-fromℕ _ +suc-pred≡id (F.suc i) = suc-inject₁ i -pred-suc≡id : (i : Fin n) → pred (suc i) ≡ i -pred-suc≡id i with view i +pred-suc : (i : Fin n) → predAbsorb (sucAbsorb i) ≡ i +pred-suc i with view i ... | ‵fromℕ = refl ... | ‵inj₁ p = cong inject₁ (view-complete p) @@ -76,8 +76,8 @@ pred-suc≡id i with view i +ℕ-identityʳ-toℕ : m ℕ.≤ n → toℕ (m ℕ+ zero {n}) ≡ m +ℕ-identityʳ-toℕ {ℕ.zero} m≤n = refl +ℕ-identityʳ-toℕ {ℕ.suc m} (s≤s m≤n) = begin - toℕ (suc (m ℕ+ zero)) ≡⟨ cong (toℕ ∘ suc) (toℕ-injective toℕm≡fromℕ<) ⟩ - toℕ (suc (inject₁ (fromℕ< (s≤s m≤n)))) ≡⟨ cong toℕ (suc-inj≡fsuc _) ⟩ + toℕ (sucAbsorb (m ℕ+ zero)) ≡⟨ cong (toℕ ∘ sucAbsorb) (toℕ-injective toℕm≡fromℕ<) ⟩ + toℕ (sucAbsorb (inject₁ (fromℕ< (s≤s m≤n)))) ≡⟨ cong toℕ (suc-inject₁ _) ⟩ ℕ.suc (toℕ (fromℕ< (s≤s m≤n))) ≡⟨ cong ℕ.suc (toℕ-fromℕ< _) ⟩ ℕ.suc m ∎ where @@ -94,18 +94,18 @@ pred-suc≡id i with view i m ≡˘⟨ toℕ-fromℕ< _ ⟩ toℕ (fromℕ< (s≤s m≤n)) ∎) -+-identityʳ : RightIdentity {ℕ.suc n} zero _+_ -+-identityʳ {n} i rewrite +ℕ-identityʳ {m = toℕ i} {n} _ = fromℕ<-toℕ _ (toℕ≤pred[n] _) ++-identityʳ : .⦃ n≢0 : NonZero n ⦄ → RightIdentity {n = n} zeroFromNonZero _+_ ++-identityʳ {ℕ.suc n} i rewrite +ℕ-identityʳ {m = toℕ i} {n} _ = fromℕ<-toℕ _ (toℕ≤pred[n] _) induction : ∀ {ℓ} (P : Pred (Fin (ℕ.suc n)) ℓ) → P zero - → (∀ {i} → P i → P (suc i)) + → (∀ {i} → P i → P (sucAbsorb i)) → ∀ i → P i induction P P₀ Pᵢ⇒Pᵢ₊₁ i = <-weakInduction P P₀ Pᵢ⇒Pᵢ₊₁′ i where - PInj : ∀ {i} → P (suc (inject₁ i)) → P (F.suc i) - PInj {i} rewrite suc-inj≡fsuc i = id + PInj : ∀ {i} → P (sucAbsorb (inject₁ i)) → P (F.suc i) + PInj {i} rewrite suc-inject₁ i = id Pᵢ⇒Pᵢ₊₁′ : ∀ i → P (inject₁ i) → P (F.suc i) Pᵢ⇒Pᵢ₊₁′ _ Pi = PInj (Pᵢ⇒Pᵢ₊₁ Pi) diff --git a/src/Data/Fin/Mod/Properties.agda b/src/Data/Fin/Mod/Properties.agda new file mode 100644 index 0000000000..e408d088df --- /dev/null +++ b/src/Data/Fin/Mod/Properties.agda @@ -0,0 +1,3 @@ +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.Fin.Mod.Properties where diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 303cf64905..89d2a80ba1 100644 --- a/src/Data/Fin/Properties.agda +++ b/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 From 3773f2c12c4a6641bcc3f7c759225e6b90f4515e Mon Sep 17 00:00:00 2001 From: Guilherme Date: Thu, 4 Jan 2024 11:02:55 +0100 Subject: [PATCH 10/23] changed Mod to properties --- src/Data/Fin/Mod.agda | 78 +----------------------------- src/Data/Fin/Mod/Properties.agda | 82 ++++++++++++++++++++++++++++++++ 2 files changed, 84 insertions(+), 76 deletions(-) diff --git a/src/Data/Fin/Mod.agda b/src/Data/Fin/Mod.agda index ed2a5d0fc5..8aaf23ed90 100644 --- a/src/Data/Fin/Mod.agda +++ b/src/Data/Fin/Mod.agda @@ -8,25 +8,9 @@ module Data.Fin.Mod where -open import Function.Base using (id; _$_; _∘_) -open import Data.Bool.Base using (true; false) -open import Data.Product.Base -open import Data.Nat.Base as ℕ using (ℕ; 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 as F hiding (suc; pred; _+_; _-_) -open import Data.Fin.Properties -open import Data.Fin.Induction using (<-weakInduction) +open import Data.Nat.Base as ℕ using (ℕ) +open import Data.Fin.Base as F hiding (_+_; _-_) open import Data.Fin.Relation.Unary.Top -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) -import Algebra.Definitions as ADef -open import Relation.Unary using (Pred) - -open module AD {n} = ADef {A = Fin n} _≡_ -open ≡-Reasoning private variable m n : ℕ @@ -51,61 +35,3 @@ i + j = toℕ i ℕ+ j _-_ : Fin m → Fin n → Fin m i - j = opposite j + i - -suc-inject₁ : (i : Fin n) → sucAbsorb (inject₁ i) ≡ F.suc i -suc-inject₁ i rewrite view-inject₁ i = cong F.suc (view-complete (view i)) - -suc-fromℕ : ∀ n → sucAbsorb (fromℕ n) ≡ zero -suc-fromℕ n rewrite view-fromℕ n = refl - -pred-sucAbsorb : (i : Fin n) → predAbsorb (F.suc i) ≡ inject₁ i -pred-sucAbsorb _ = refl - -suc-pred≡id : (i : Fin n) → sucAbsorb (predAbsorb i) ≡ i -suc-pred≡id zero = suc-fromℕ _ -suc-pred≡id (F.suc i) = suc-inject₁ i - -pred-suc : (i : Fin n) → predAbsorb (sucAbsorb i) ≡ i -pred-suc i with view i -... | ‵fromℕ = refl -... | ‵inj₁ p = cong inject₁ (view-complete p) - -+-identityˡ : LeftIdentity {ℕ.suc n} zero _+_ -+-identityˡ _ = refl - -+ℕ-identityʳ-toℕ : m ℕ.≤ n → toℕ (m ℕ+ zero {n}) ≡ m -+ℕ-identityʳ-toℕ {ℕ.zero} m≤n = refl -+ℕ-identityʳ-toℕ {ℕ.suc m} (s≤s m≤n) = begin - toℕ (sucAbsorb (m ℕ+ zero)) ≡⟨ cong (toℕ ∘ sucAbsorb) (toℕ-injective toℕm≡fromℕ<) ⟩ - toℕ (sucAbsorb (inject₁ (fromℕ< (s≤s m≤n)))) ≡⟨ cong toℕ (suc-inject₁ _) ⟩ - ℕ.suc (toℕ (fromℕ< (s≤s m≤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ℕ< (s≤s m≤n)) ≡˘⟨ toℕ-inject₁ _ ⟩ - toℕ (inject₁ (fromℕ< (s≤s m≤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ʳ : .⦃ n≢0 : NonZero n ⦄ → RightIdentity {n = n} zeroFromNonZero _+_ -+-identityʳ {ℕ.suc n} i rewrite +ℕ-identityʳ {m = toℕ i} {n} _ = fromℕ<-toℕ _ (toℕ≤pred[n] _) - -induction : ∀ {ℓ} (P : Pred (Fin (ℕ.suc n)) ℓ) - → P zero - → (∀ {i} → P i → P (sucAbsorb i)) - → ∀ i → P i -induction P P₀ Pᵢ⇒Pᵢ₊₁ i = <-weakInduction P P₀ Pᵢ⇒Pᵢ₊₁′ i - where - - PInj : ∀ {i} → P (sucAbsorb (inject₁ i)) → P (F.suc i) - PInj {i} rewrite suc-inject₁ i = id - - Pᵢ⇒Pᵢ₊₁′ : ∀ i → P (inject₁ i) → P (F.suc i) - Pᵢ⇒Pᵢ₊₁′ _ Pi = PInj (Pᵢ⇒Pᵢ₊₁ Pi) diff --git a/src/Data/Fin/Mod/Properties.agda b/src/Data/Fin/Mod/Properties.agda index e408d088df..4e0317ae9e 100644 --- a/src/Data/Fin/Mod/Properties.agda +++ b/src/Data/Fin/Mod/Properties.agda @@ -1,3 +1,85 @@ {-# 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 (ℕ; 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 as F 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) +import Algebra.Definitions as ADef +open import Relation.Unary using (Pred) + +private + open module AD {n} = ADef {A = Fin n} _≡_ +open ≡-Reasoning + +private variable + m n : ℕ + +suc-inject₁ : (i : Fin n) → sucAbsorb (inject₁ i) ≡ F.suc i +suc-inject₁ i rewrite view-inject₁ i = cong F.suc (view-complete (view i)) + +suc-fromℕ : ∀ n → sucAbsorb (fromℕ n) ≡ zero +suc-fromℕ n rewrite view-fromℕ n = refl + +pred-sucAbsorb : (i : Fin n) → predAbsorb (F.suc i) ≡ inject₁ i +pred-sucAbsorb _ = refl + +suc-pred≡id : (i : Fin n) → sucAbsorb (predAbsorb i) ≡ i +suc-pred≡id zero = suc-fromℕ _ +suc-pred≡id (F.suc i) = suc-inject₁ i + +pred-suc : (i : Fin n) → predAbsorb (sucAbsorb i) ≡ i +pred-suc i with view i +... | ‵fromℕ = refl +... | ‵inj₁ p = cong inject₁ (view-complete p) + ++-identityˡ : LeftIdentity {ℕ.suc n} zero _+_ ++-identityˡ _ = refl + ++ℕ-identityʳ-toℕ : m ℕ.≤ n → toℕ (m ℕ+ zero {n}) ≡ m ++ℕ-identityʳ-toℕ {ℕ.zero} m≤n = refl ++ℕ-identityʳ-toℕ {ℕ.suc m} (s≤s m≤n) = begin + toℕ (sucAbsorb (m ℕ+ zero)) ≡⟨ cong (toℕ ∘ sucAbsorb) (toℕ-injective toℕm≡fromℕ<) ⟩ + toℕ (sucAbsorb (inject₁ (fromℕ< (s≤s m≤n)))) ≡⟨ cong toℕ (suc-inject₁ _) ⟩ + ℕ.suc (toℕ (fromℕ< (s≤s m≤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ℕ< (s≤s m≤n)) ≡˘⟨ toℕ-inject₁ _ ⟩ + toℕ (inject₁ (fromℕ< (s≤s m≤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ʳ : .⦃ n≢0 : NonZero n ⦄ → RightIdentity {n = n} zeroFromNonZero _+_ ++-identityʳ {ℕ.suc n} i rewrite +ℕ-identityʳ {m = toℕ i} {n} _ = fromℕ<-toℕ _ (toℕ≤pred[n] _) + +induction : ∀ {ℓ} (P : Pred (Fin (ℕ.suc n)) ℓ) + → P zero + → (∀ {i} → P i → P (sucAbsorb i)) + → ∀ i → P i +induction P P₀ Pᵢ⇒Pᵢ₊₁ i = <-weakInduction P P₀ Pᵢ⇒Pᵢ₊₁′ i + where + + PInj : ∀ {i} → P (sucAbsorb (inject₁ i)) → P (F.suc i) + PInj {i} rewrite suc-inject₁ i = id + + Pᵢ⇒Pᵢ₊₁′ : ∀ i → P (inject₁ i) → P (F.suc i) + Pᵢ⇒Pᵢ₊₁′ _ Pi = PInj (Pᵢ⇒Pᵢ₊₁ Pi) From e85305933acaf145ff566914cdb8d4639c18a9dd Mon Sep 17 00:00:00 2001 From: Guilherme Date: Thu, 4 Jan 2024 11:06:18 +0100 Subject: [PATCH 11/23] added header --- src/Data/Fin/Mod/Properties.agda | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Data/Fin/Mod/Properties.agda b/src/Data/Fin/Mod/Properties.agda index 4e0317ae9e..af888e0708 100644 --- a/src/Data/Fin/Mod/Properties.agda +++ b/src/Data/Fin/Mod/Properties.agda @@ -1,3 +1,9 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties related to mod fin +------------------------------------------------------------------------ + {-# OPTIONS --cubical-compatible --safe #-} module Data.Fin.Mod.Properties where From fccf44d08c680376cbf5396595c29f1f19372166 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Thu, 4 Jan 2024 11:38:23 +0100 Subject: [PATCH 12/23] added changes to CHANGELOG --- CHANGELOG.md | 30 +++++++++++++++++++++++++++++- src/Data/Fin/Mod/Properties.agda | 6 +++--- 2 files changed, 32 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2402e80d18..0ed859d2e9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -29,7 +29,7 @@ Deprecated names New modules ----------- -* Added new file `Data.Fin.Mod` +* Added new files `Data.Fin.Mod` and `Data.Fin.Mod.Properties` Additions to existing modules ----------------------------- @@ -82,3 +82,31 @@ 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 + sucAbsorb : Fin n → Fin n + predAbsorb : Fin n → Fin n + _ℕ+_ : ℕ → Fin n → Fin n + _+_ : Fin m → Fin n → Fin n + _-_ : Fin m → Fin n → Fin m + ``` + +* In `Data.Fin.Mod.Properties`: + ```agda + suc-inject₁ : ∀ i → sucAbsorb (inject₁ i) ≡ F.suc i + suc-fromℕ : ∀ n → sucAbsorb (fromℕ n) ≡ zero + pred-sucAbsorb : ∀ i → predAbsorb (F.suc i) ≡ inject₁ i + suc-pred≡id : ∀ i → sucAbsorb (predAbsorb i) ≡ i + pred-suc : ∀ i → predAbsorb (sucAbsorb 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 (sucAbsorb i)) → ∀ i → P i + ``` diff --git a/src/Data/Fin/Mod/Properties.agda b/src/Data/Fin/Mod/Properties.agda index af888e0708..958bacace4 100644 --- a/src/Data/Fin/Mod/Properties.agda +++ b/src/Data/Fin/Mod/Properties.agda @@ -50,8 +50,8 @@ pred-suc i with view i ... | ‵fromℕ = refl ... | ‵inj₁ p = cong inject₁ (view-complete p) -+-identityˡ : LeftIdentity {ℕ.suc n} zero _+_ -+-identityˡ _ = refl ++-identityˡ : .⦃ _ : NonZero n ⦄ → LeftIdentity zeroFromNonZero _+_ ++-identityˡ {ℕ.suc _} _ = refl +ℕ-identityʳ-toℕ : m ℕ.≤ n → toℕ (m ℕ+ zero {n}) ≡ m +ℕ-identityʳ-toℕ {ℕ.zero} m≤n = refl @@ -74,7 +74,7 @@ pred-suc i with view i m ≡˘⟨ toℕ-fromℕ< _ ⟩ toℕ (fromℕ< (s≤s m≤n)) ∎) -+-identityʳ : .⦃ n≢0 : NonZero n ⦄ → RightIdentity {n = n} zeroFromNonZero _+_ ++-identityʳ : .⦃ _ : NonZero n ⦄ → RightIdentity {n = n} zeroFromNonZero _+_ +-identityʳ {ℕ.suc n} i rewrite +ℕ-identityʳ {m = toℕ i} {n} _ = fromℕ<-toℕ _ (toℕ≤pred[n] _) induction : ∀ {ℓ} (P : Pred (Fin (ℕ.suc n)) ℓ) From e7edaee8158713e513e6a333d666eb1a32fd96c6 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Mon, 15 Jan 2024 11:07:08 +0800 Subject: [PATCH 13/23] Minor refactorings --- src/Data/Fin/Mod.agda | 21 +++---- src/Data/Fin/Mod/Properties.agda | 95 ++++++++++++++++++-------------- 2 files changed, 65 insertions(+), 51 deletions(-) diff --git a/src/Data/Fin/Mod.agda b/src/Data/Fin/Mod.agda index 8aaf23ed90..2fc89257b2 100644 --- a/src/Data/Fin/Mod.agda +++ b/src/Data/Fin/Mod.agda @@ -8,8 +8,9 @@ module Data.Fin.Mod where -open import Data.Nat.Base as ℕ using (ℕ) -open import Data.Fin.Base as F hiding (_+_; _-_) +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 @@ -17,18 +18,18 @@ private variable infixl 6 _+_ _-_ -sucAbsorb : Fin n → Fin n -sucAbsorb i with view i +sucMod : Fin n → Fin n +sucMod i with view i ... | ‵fromℕ = zero -... | ‵inj₁ i = F.suc ⟦ i ⟧ +... | ‵inj₁ i = suc ⟦ i ⟧ -predAbsorb : Fin n → Fin n -predAbsorb zero = fromℕ _ -predAbsorb (F.suc i) = inject₁ i +predMod : Fin n → Fin n +predMod zero = fromℕ _ +predMod (suc i) = inject₁ i _ℕ+_ : ℕ → Fin n → Fin n -ℕ.zero ℕ+ i = i -ℕ.suc n ℕ+ i = sucAbsorb (n ℕ+ i) +zero ℕ+ i = i +suc n ℕ+ i = sucMod (n ℕ+ i) _+_ : Fin m → Fin n → Fin n i + j = toℕ i ℕ+ j diff --git a/src/Data/Fin/Mod/Properties.agda b/src/Data/Fin/Mod/Properties.agda index 958bacace4..1209b3e488 100644 --- a/src/Data/Fin/Mod/Properties.agda +++ b/src/Data/Fin/Mod/Properties.agda @@ -10,10 +10,10 @@ 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 (ℕ; z≤n; s≤s; NonZero) +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 as F hiding (_+_; _-_) +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 @@ -22,70 +22,83 @@ 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) -import Algebra.Definitions as ADef open import Relation.Unary using (Pred) -private - open module AD {n} = ADef {A = Fin n} _≡_ +module _ {n : ℕ} where + open import Algebra.Definitions {A = Fin n} _≡_ public + open ≡-Reasoning private variable m n : ℕ -suc-inject₁ : (i : Fin n) → sucAbsorb (inject₁ i) ≡ F.suc i -suc-inject₁ i rewrite view-inject₁ i = cong F.suc (view-complete (view i)) +------------------------------------------------------------------------ +-- sucMod -suc-fromℕ : ∀ n → sucAbsorb (fromℕ n) ≡ zero -suc-fromℕ n rewrite view-fromℕ n = refl +sucMod-inject₁ : (i : Fin n) → sucMod (inject₁ i) ≡ suc i +sucMod-inject₁ i rewrite view-inject₁ i = + cong suc (view-complete (view i)) -pred-sucAbsorb : (i : Fin n) → predAbsorb (F.suc i) ≡ inject₁ i -pred-sucAbsorb _ = refl +sucMod-fromℕ : ∀ n → sucMod (fromℕ n) ≡ zero +sucMod-fromℕ n rewrite view-fromℕ n = refl -suc-pred≡id : (i : Fin n) → sucAbsorb (predAbsorb i) ≡ i -suc-pred≡id zero = suc-fromℕ _ -suc-pred≡id (F.suc i) = suc-inject₁ i +------------------------------------------------------------------------ +-- predMod -pred-suc : (i : Fin n) → predAbsorb (sucAbsorb i) ≡ i -pred-suc i with view i +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) -+-identityˡ : .⦃ _ : NonZero n ⦄ → LeftIdentity zeroFromNonZero _+_ -+-identityˡ {ℕ.suc _} _ = 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} (s≤s m≤n) = begin - toℕ (sucAbsorb (m ℕ+ zero)) ≡⟨ cong (toℕ ∘ sucAbsorb) (toℕ-injective toℕm≡fromℕ<) ⟩ - toℕ (sucAbsorb (inject₁ (fromℕ< (s≤s m≤n)))) ≡⟨ cong toℕ (suc-inject₁ _) ⟩ - ℕ.suc (toℕ (fromℕ< (s≤s m≤n))) ≡⟨ cong ℕ.suc (toℕ-fromℕ< _) ⟩ - ℕ.suc 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ℕ< (s≤s m≤n)) ≡˘⟨ toℕ-inject₁ _ ⟩ - toℕ (inject₁ (fromℕ< (s≤s m≤n))) ∎ + 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ℕ (m ℕ+ zero) ≡⟨ +ℕ-identityʳ-toℕ m≤n ⟩ + m ≡⟨ toℕ-fromℕ< _ ⟨ toℕ (fromℕ< (s≤s m≤n)) ∎) + +------------------------------------------------------------------------ +-- _+_ -+-identityʳ : .⦃ _ : NonZero n ⦄ → RightIdentity {n = n} zeroFromNonZero _+_ -+-identityʳ {ℕ.suc n} i rewrite +ℕ-identityʳ {m = toℕ i} {n} _ = fromℕ<-toℕ _ (toℕ≤pred[n] _) ++-identityˡ : .{{ _ : NonZero n }} → LeftIdentity zeroFromNonZero _+_ ++-identityˡ {suc _} _ = refl -induction : ∀ {ℓ} (P : Pred (Fin (ℕ.suc n)) ℓ) - → P zero - → (∀ {i} → P i → P (sucAbsorb i)) - → ∀ i → P i ++-identityʳ : .{{ _ : NonZero n }} → RightIdentity zeroFromNonZero _+_ ++-identityʳ {suc n} i rewrite +ℕ-identityʳ {m = toℕ i} {n} _ = fromℕ<-toℕ _ (toℕ≤pred[n] _) + +induction : + ∀ {ℓ} (P : Pred (Fin (ℕ.suc n)) ℓ) → + P zero → + (∀ {i} → P i → P (sucMod i)) → + ∀ i → P i induction P P₀ Pᵢ⇒Pᵢ₊₁ i = <-weakInduction P P₀ Pᵢ⇒Pᵢ₊₁′ i where + PInj : ∀ {i} → P (sucMod (inject₁ i)) → P (suc i) + PInj {i} rewrite sucMod-inject₁ i = id - PInj : ∀ {i} → P (sucAbsorb (inject₁ i)) → P (F.suc i) - PInj {i} rewrite suc-inject₁ i = id - - Pᵢ⇒Pᵢ₊₁′ : ∀ i → P (inject₁ i) → P (F.suc i) - Pᵢ⇒Pᵢ₊₁′ _ Pi = PInj (Pᵢ⇒Pᵢ₊₁ Pi) + Pᵢ⇒Pᵢ₊₁′ : ∀ i → P (inject₁ i) → P (suc i) + Pᵢ⇒Pᵢ₊₁′ _ Pᵢ = PInj (Pᵢ⇒Pᵢ₊₁ Pᵢ) From ab5493d9432406820b8d9e9edaeed2aed2d4b550 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 15 Jan 2024 09:22:24 +0100 Subject: [PATCH 14/23] changed + definition --- src/Data/Fin/Mod.agda | 6 +++--- src/Data/Fin/Mod/Properties.agda | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Data/Fin/Mod.agda b/src/Data/Fin/Mod.agda index 2fc89257b2..780fea2ade 100644 --- a/src/Data/Fin/Mod.agda +++ b/src/Data/Fin/Mod.agda @@ -31,8 +31,8 @@ _ℕ+_ : ℕ → Fin n → Fin n zero ℕ+ i = i suc n ℕ+ i = sucMod (n ℕ+ i) -_+_ : Fin m → Fin n → Fin n -i + j = toℕ i ℕ+ j +_+_ : Fin n → Fin m → Fin n +i + j = toℕ j ℕ+ i _-_ : Fin m → Fin n → Fin m -i - j = opposite j + i +i - j = opposite i + j diff --git a/src/Data/Fin/Mod/Properties.agda b/src/Data/Fin/Mod/Properties.agda index 1209b3e488..79ae2d5dee 100644 --- a/src/Data/Fin/Mod/Properties.agda +++ b/src/Data/Fin/Mod/Properties.agda @@ -85,10 +85,10 @@ sucMod-predMod (suc i) = sucMod-inject₁ i -- _+_ +-identityˡ : .{{ _ : NonZero n }} → LeftIdentity zeroFromNonZero _+_ -+-identityˡ {suc _} _ = refl ++-identityˡ {suc n} i rewrite +ℕ-identityʳ {m = toℕ i} {n} _ = fromℕ<-toℕ _ (toℕ≤pred[n] _) +-identityʳ : .{{ _ : NonZero n }} → RightIdentity zeroFromNonZero _+_ -+-identityʳ {suc n} i rewrite +ℕ-identityʳ {m = toℕ i} {n} _ = fromℕ<-toℕ _ (toℕ≤pred[n] _) ++-identityʳ {suc _} _ = refl induction : ∀ {ℓ} (P : Pred (Fin (ℕ.suc n)) ℓ) → From 7ccd05ed14c4617e44bf19c55442fc0e03aa51a1 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 15 Jan 2024 09:24:24 +0100 Subject: [PATCH 15/23] added new _+_ to changelog --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0ed859d2e9..ce2e791892 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -93,7 +93,7 @@ Additions to existing modules sucAbsorb : Fin n → Fin n predAbsorb : Fin n → Fin n _ℕ+_ : ℕ → Fin n → Fin n - _+_ : Fin m → Fin n → Fin n + _+_ : Fin n → Fin m → Fin n _-_ : Fin m → Fin n → Fin m ``` From 644a8cb2234928a4d5d1af242400b60c76efaa35 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Tue, 16 Jan 2024 11:35:18 +0100 Subject: [PATCH 16/23] added new induction property --- src/Data/Fin/Mod/Induction.agda | 43 ++++++++++++++++++++++++++++++++ src/Data/Fin/Mod/Properties.agda | 12 --------- 2 files changed, 43 insertions(+), 12 deletions(-) create mode 100644 src/Data/Fin/Mod/Induction.agda 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 index 79ae2d5dee..0d63b5e7fb 100644 --- a/src/Data/Fin/Mod/Properties.agda +++ b/src/Data/Fin/Mod/Properties.agda @@ -90,15 +90,3 @@ sucMod-predMod (suc i) = sucMod-inject₁ i +-identityʳ : .{{ _ : NonZero n }} → RightIdentity zeroFromNonZero _+_ +-identityʳ {suc _} _ = refl -induction : - ∀ {ℓ} (P : Pred (Fin (ℕ.suc n)) ℓ) → - P zero → - (∀ {i} → P i → P (sucMod i)) → - ∀ i → P i -induction P P₀ Pᵢ⇒Pᵢ₊₁ i = <-weakInduction P P₀ Pᵢ⇒Pᵢ₊₁′ i - 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ᵢ₊₁′ _ Pᵢ = PInj (Pᵢ⇒Pᵢ₊₁ Pᵢ) From 417fa28bc6c077c4c941be2da2b30f7e0f01523b Mon Sep 17 00:00:00 2001 From: Guilherme Date: Tue, 16 Jan 2024 11:38:27 +0100 Subject: [PATCH 17/23] added induction to CHANGELOG --- CHANGELOG.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index ce2e791892..4b3260ceef 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -110,3 +110,8 @@ Additions to existing modules +-identityʳ : .⦃ NonZero n ⦄ → RightIdentity zeroFromNonZero _+_ induction : ∀ P → P zero → (P i → P (sucAbsorb i)) → ∀ i → P i ``` + +* In `Data.Fin.Mod.Induction`: + ```agda + induction : ∀ P → P k → (P i → P (sucAbsorb i)) → ∀ i → P i + ``` From 4d3a4ab2968e13be91e17ce167a3e7d4a75eb32c Mon Sep 17 00:00:00 2001 From: Guilherme Date: Tue, 16 Jan 2024 11:42:54 +0100 Subject: [PATCH 18/23] changed - definition --- src/Data/Fin/Mod.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Fin/Mod.agda b/src/Data/Fin/Mod.agda index 780fea2ade..b2b827e606 100644 --- a/src/Data/Fin/Mod.agda +++ b/src/Data/Fin/Mod.agda @@ -34,5 +34,5 @@ suc n ℕ+ i = sucMod (n ℕ+ i) _+_ : Fin n → Fin m → Fin n i + j = toℕ j ℕ+ i -_-_ : Fin m → Fin n → Fin m -i - j = opposite i + j +_-_ : Fin n → Fin m → Fin n +i - j = i + opposite j From 84cc27b5ba3df64fad90469ac877995a234d46d5 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Tue, 16 Jan 2024 11:43:07 +0100 Subject: [PATCH 19/23] updated CHANGELOG --- CHANGELOG.md | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4b3260ceef..5603ea05cb 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -90,28 +90,28 @@ Additions to existing modules * In `Data.Fin.Mod`: ```agda - sucAbsorb : Fin n → Fin n - predAbsorb : Fin n → Fin n - _ℕ+_ : ℕ → Fin n → Fin n - _+_ : Fin n → Fin m → Fin n - _-_ : Fin m → Fin n → Fin m + 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 → sucAbsorb (inject₁ i) ≡ F.suc i - suc-fromℕ : ∀ n → sucAbsorb (fromℕ n) ≡ zero - pred-sucAbsorb : ∀ i → predAbsorb (F.suc i) ≡ inject₁ i - suc-pred≡id : ∀ i → sucAbsorb (predAbsorb i) ≡ i - pred-suc : ∀ i → predAbsorb (sucAbsorb i) ≡ i + 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 (sucAbsorb i)) → ∀ i → P i + 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 (sucAbsorb i)) → ∀ i → P i + induction : ∀ P → P k → (P i → P (sucMod i)) → ∀ i → P i ``` From 473ac6d4b941453603dcb767546c651744bbacd9 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Thu, 18 Jan 2024 13:17:29 +0100 Subject: [PATCH 20/23] changed sucMod definition --- src/Data/Fin/Mod.agda | 10 ++++++---- src/Data/Fin/Mod/Properties.agda | 18 ++++++++++-------- 2 files changed, 16 insertions(+), 12 deletions(-) diff --git a/src/Data/Fin/Mod.agda b/src/Data/Fin/Mod.agda index b2b827e606..816a2a8f71 100644 --- a/src/Data/Fin/Mod.agda +++ b/src/Data/Fin/Mod.agda @@ -19,12 +19,14 @@ private variable infixl 6 _+_ _-_ sucMod : Fin n → Fin n -sucMod i with view i -... | ‵fromℕ = zero -... | ‵inj₁ i = suc ⟦ i ⟧ +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 zero = fromℕ _ predMod (suc i) = inject₁ i _ℕ+_ : ℕ → Fin n → Fin n diff --git a/src/Data/Fin/Mod/Properties.agda b/src/Data/Fin/Mod/Properties.agda index 0d63b5e7fb..d081ffde58 100644 --- a/src/Data/Fin/Mod/Properties.agda +++ b/src/Data/Fin/Mod/Properties.agda @@ -36,11 +36,12 @@ private variable -- 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-inject₁ zero = refl +sucMod-inject₁ (suc i) rewrite sucMod-inject₁ i = refl sucMod-fromℕ : ∀ n → sucMod (fromℕ n) ≡ zero -sucMod-fromℕ n rewrite view-fromℕ n = refl +sucMod-fromℕ zero = refl +sucMod-fromℕ (suc n) rewrite sucMod-fromℕ n = refl ------------------------------------------------------------------------ -- predMod @@ -49,9 +50,11 @@ 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) +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ℕ _ @@ -80,7 +83,7 @@ sucMod-predMod (suc i) = sucMod-inject₁ i toℕ (m ℕ+ zero) ≡⟨ +ℕ-identityʳ-toℕ m≤n ⟩ m ≡⟨ toℕ-fromℕ< _ ⟨ toℕ (fromℕ< (s≤s m≤n)) ∎) - + ------------------------------------------------------------------------ -- _+_ @@ -89,4 +92,3 @@ sucMod-predMod (suc i) = sucMod-inject₁ i +-identityʳ : .{{ _ : NonZero n }} → RightIdentity zeroFromNonZero _+_ +-identityʳ {suc _} _ = refl - From b539e70dbc1880b776d249207f4b5d5109a98026 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Thu, 18 Jan 2024 16:17:12 +0100 Subject: [PATCH 21/23] added more properties of Fin Mod --- CHANGELOG.md | 17 +++++++-------- src/Data/Fin/Mod/Properties.agda | 36 +++++++++++++++++++++++++++++++- 2 files changed, 42 insertions(+), 11 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5603ea05cb..0a6fb691d7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -99,16 +99,13 @@ Additions to existing modules * 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 + 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`: diff --git a/src/Data/Fin/Mod/Properties.agda b/src/Data/Fin/Mod/Properties.agda index d081ffde58..cae09b6349 100644 --- a/src/Data/Fin/Mod/Properties.agda +++ b/src/Data/Fin/Mod/Properties.agda @@ -14,7 +14,7 @@ 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.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 @@ -43,6 +43,40 @@ 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 From aeb1c4a21287b97f27c4f9a293d25a385c785591 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Fri, 19 Jan 2024 14:11:41 +0100 Subject: [PATCH 22/23] renamed zero+ --- CHANGELOG.md | 4 ++-- src/Data/Fin/Base.agda | 5 +++++ src/Data/Fin/Mod/Properties.agda | 4 ++-- src/Data/Fin/Properties.agda | 3 --- 4 files changed, 9 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0a6fb691d7..4304a11ff9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -83,9 +83,9 @@ Additions to existing modules pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n ``` -* In `Data.Fin.Properties`: +* In `Data.Fin.Base`: ```agda - zeroFromNonZero : .⦃ NonZero n ⦄ → Fin n + zero⁺ : .⦃ NonZero n ⦄ → Fin n ``` * In `Data.Fin.Mod`: diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index d762e10007..15e3c6a17a 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -35,6 +35,11 @@ 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 + -- A conversion: toℕ "i" = i. toℕ : Fin n → ℕ diff --git a/src/Data/Fin/Mod/Properties.agda b/src/Data/Fin/Mod/Properties.agda index cae09b6349..f808e6da27 100644 --- a/src/Data/Fin/Mod/Properties.agda +++ b/src/Data/Fin/Mod/Properties.agda @@ -121,8 +121,8 @@ sucMod-predMod (suc i) = sucMod-inject₁ i ------------------------------------------------------------------------ -- _+_ -+-identityˡ : .{{ _ : NonZero n }} → LeftIdentity zeroFromNonZero _+_ ++-identityˡ : .{{ _ : NonZero n }} → LeftIdentity zero⁺ _+_ +-identityˡ {suc n} i rewrite +ℕ-identityʳ {m = toℕ i} {n} _ = fromℕ<-toℕ _ (toℕ≤pred[n] _) -+-identityʳ : .{{ _ : NonZero n }} → RightIdentity zeroFromNonZero _+_ ++-identityʳ : .{{ _ : NonZero n }} → RightIdentity zero⁺ _+_ +-identityʳ {suc _} _ = refl diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 89d2a80ba1..303cf64905 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -68,9 +68,6 @@ private nonZeroIndex : Fin n → ℕ.NonZero n nonZeroIndex {n = suc _} _ = _ -zeroFromNonZero : .⦃ _ : ℕ.NonZero n ⦄ → Fin n -zeroFromNonZero {n = suc _} = zero - ------------------------------------------------------------------------ -- Bundles From bdf0651218679af7e7cec256b2064497a9fa7e32 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Fri, 19 Jan 2024 16:40:48 +0100 Subject: [PATCH 23/23] added suc+ --- CHANGELOG.md | 1 + src/Data/Fin/Base.agda | 5 ++++- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4304a11ff9..d1558b79c6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -86,6 +86,7 @@ Additions to existing modules * In `Data.Fin.Base`: ```agda zero⁺ : .⦃ NonZero n ⦄ → Fin n + suc⁺ : .⦃ NonZero n ⦄ → Fin (pred n) → Fin n ``` * In `Data.Fin.Mod`: diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index 15e3c6a17a..132529eb7d 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -37,9 +37,12 @@ data Fin : ℕ → Set where -- Homogeneous Constructors -zero⁺ : .⦃ _ : ℕ.NonZero n ⦄ → Fin n +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 → ℕ