------------------------------------------------------------------------ -- The Agda standard library -- -- Finite sets ------------------------------------------------------------------------ -- Note that elements of Fin n can be seen as natural numbers in the -- set {m | m < n}. The notation "m" in comments below refers to this -- natural number view. {-# OPTIONS --cubical-compatible --safe #-} module Data.Fin.Base where open import Data.Bool.Base using (Bool; T) open import Data.Nat.Base as ℕ using (ℕ; zero; suc) open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′) open import Function.Base using (id; _∘_; _on_; flip; _$_) open import Level using (0ℓ) open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong) open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel) open import Relation.Nullary.Negation.Core using (contradiction) private variable m n : ℕ ------------------------------------------------------------------------ -- Types -- Fin n is a type with n elements. data Fin : ℕ → Set where zero : Fin (suc n) suc : (i : Fin n) → Fin (suc n) -- A conversion: toℕ "i" = i. toℕ : Fin n → ℕ toℕ zero = 0 toℕ (suc i) = suc (toℕ i) -- A Fin-indexed variant of Fin. Fin′ : Fin n → Set Fin′ i = Fin (toℕ i) ------------------------------------------------------------------------ -- A cast that actually computes on constructors (as opposed to subst) cast : .(m ≡ n) → Fin m → Fin n cast {zero} {zero} eq k = k cast {suc m} {suc n} eq zero = zero cast {suc m} {suc n} eq (suc k) = suc (cast (cong ℕ.pred eq) k) ------------------------------------------------------------------------ -- Conversions -- toℕ is defined above. -- fromℕ n = "n". fromℕ : (n : ℕ) → Fin (suc n) fromℕ zero = zero fromℕ (suc n) = suc (fromℕ n) -- fromℕ< {m} _ = "m". fromℕ< : .(m ℕ.< n) → Fin n fromℕ< {zero} {suc _} _ = zero fromℕ< {suc m} {suc _} m<n = suc (fromℕ< (ℕ.s<s⁻¹ m<n)) -- fromℕ<″ m _ = "m". fromℕ<″ : ∀ m {n} → .(m ℕ.<″ n) → Fin n fromℕ<″ zero {suc _} _ = zero fromℕ<″ (suc m) {suc _} m<″n = suc (fromℕ<″ m (ℕ.s<″s⁻¹ m<″n)) -- canonical liftings of i:Fin m to larger index -- injection on the left: "i" ↑ˡ n = "i" in Fin (m + n) infixl 5 _↑ˡ_ _↑ˡ_ : ∀ {m} → Fin m → ∀ n → Fin (m ℕ.+ n) zero ↑ˡ n = zero (suc i) ↑ˡ n = suc (i ↑ˡ n) -- injection on the right: n ↑ʳ "i" = "n + i" in Fin (n + m) infixr 5 _↑ʳ_ _↑ʳ_ : ∀ {m} n → Fin m → Fin (n ℕ.+ m) zero ↑ʳ i = i (suc n) ↑ʳ i = suc (n ↑ʳ i) -- reduce≥ "m + i" _ = "i". reduce≥ : ∀ (i : Fin (m ℕ.+ n)) → .(m ℕ.≤ toℕ i) → Fin n reduce≥ {zero} i _ = i reduce≥ {suc _} (suc i) m≤i = reduce≥ i (ℕ.s≤s⁻¹ m≤i) -- inject⋆ m "i" = "i". inject : ∀ {i : Fin n} → Fin′ i → Fin n inject {i = suc i} zero = zero inject {i = suc i} (suc j) = suc (inject j) inject! : ∀ {i : Fin (suc n)} → Fin′ i → Fin n inject! {n = suc _} {i = suc _} zero = zero inject! {n = suc _} {i = suc _} (suc j) = suc (inject! j) inject₁ : Fin n → Fin (suc n) inject₁ zero = zero inject₁ (suc i) = suc (inject₁ i) inject≤ : Fin m → .(m ℕ.≤ n) → Fin n inject≤ {n = suc _} zero _ = zero inject≤ {n = suc _} (suc i) m≤n = suc (inject≤ i (ℕ.s≤s⁻¹ m≤n)) -- lower₁ "i" _ = "i". lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n lower₁ {zero} zero ne = contradiction refl ne lower₁ {suc n} zero _ = zero lower₁ {suc n} (suc i) ne = suc (lower₁ i (ne ∘ cong suc)) -- A strengthening injection into the minimal Fin fibre. strengthen : ∀ (i : Fin n) → Fin′ (suc i) strengthen zero = zero strengthen (suc i) = suc (strengthen i) -- splitAt m "i" = inj₁ "i" if i < m -- inj₂ "i - m" if i ≥ m -- This is dual to splitAt from Data.Vec. splitAt : ∀ m {n} → Fin (m ℕ.+ n) → Fin m ⊎ Fin n splitAt zero i = inj₂ i splitAt (suc m) zero = inj₁ zero splitAt (suc m) (suc i) = Sum.map₁ suc (splitAt m i) -- inverse of above function join : ∀ m n → Fin m ⊎ Fin n → Fin (m ℕ.+ n) join m n = [ _↑ˡ n , m ↑ʳ_ ]′ -- quotRem k "i" = "i % k" , "i / k" -- This is dual to group from Data.Vec. quotRem : ∀ n → Fin (m ℕ.* n) → Fin n × Fin m quotRem {suc m} n i = [ (_, zero) , Product.map₂ suc ∘ quotRem {m} n ]′ $ splitAt n i -- a variant of quotRem the type of whose result matches the order of multiplication remQuot : ∀ n → Fin (m ℕ.* n) → Fin m × Fin n remQuot i = Product.swap ∘ quotRem i quotient : ∀ n → Fin (m ℕ.* n) → Fin m quotient n = proj₁ ∘ remQuot n remainder : ∀ n → Fin (m ℕ.* n) → Fin n remainder {m} n = proj₂ ∘ remQuot {m} n -- inverse of remQuot combine : Fin m → Fin n → Fin (m ℕ.* n) combine {suc m} {n} zero j = j ↑ˡ (m ℕ.* n) combine {suc m} {n} (suc i) j = n ↑ʳ (combine i j) -- Next in progression after splitAt and remQuot finToFun : Fin (m ℕ.^ n) → (Fin n → Fin m) finToFun {m} {suc n} i zero = quotient (m ℕ.^ n) i finToFun {m} {suc n} i (suc j) = finToFun (remainder {m} (m ℕ.^ n) i) j -- inverse of above function funToFin : (Fin m → Fin n) → Fin (n ℕ.^ m) funToFin {zero} f = zero funToFin {suc m} f = combine (f zero) (funToFin (f ∘ suc)) ------------------------------------------------------------------------ -- Operations -- Folds. fold : ∀ {t} (T : ℕ → Set t) {m} → (∀ {n} → T n → T (suc n)) → (∀ {n} → T (suc n)) → Fin m → T m fold T f x zero = x fold T f x (suc i) = f (fold T f x i) fold′ : ∀ {n t} (T : Fin (suc n) → Set t) → (∀ i → T (inject₁ i) → T (suc i)) → T zero → ∀ i → T i fold′ T f x zero = x fold′ {n = suc n} T f x (suc i) = f i (fold′ (T ∘ inject₁) (f ∘ inject₁) x i) -- Lifts functions. lift : ∀ k → (Fin m → Fin n) → Fin (k ℕ.+ m) → Fin (k ℕ.+ n) lift zero f i = f i lift (suc k) f zero = zero lift (suc k) f (suc i) = suc (lift k f i) -- "i" + "j" = "i + j". infixl 6 _+_ _+_ : ∀ (i : Fin m) (j : Fin n) → Fin (toℕ i ℕ.+ n) zero + j = j suc i + j = suc (i + j) -- "i" - "j" = "i ∸ j". infixl 6 _-_ _-_ : ∀ (i : Fin n) (j : Fin′ (suc i)) → Fin (n ℕ.∸ toℕ j) i - zero = i suc i - suc j = i - j -- m ℕ- "i" = "m ∸ i". infixl 6 _ℕ-_ _ℕ-_ : (n : ℕ) (j : Fin (suc n)) → Fin (suc n ℕ.∸ toℕ j) n ℕ- zero = fromℕ n suc n ℕ- suc i = n ℕ- i -- m ℕ-ℕ "i" = m ∸ i. infixl 6 _ℕ-ℕ_ _ℕ-ℕ_ : (n : ℕ) → Fin (suc n) → ℕ n ℕ-ℕ zero = n suc n ℕ-ℕ suc i = n ℕ-ℕ i -- pred "i" = "pred i". pred : Fin n → Fin n pred zero = zero pred (suc i) = inject₁ i -- opposite "i" = "n - i" (i.e. the additive inverse). opposite : Fin n → Fin n opposite {suc n} zero = fromℕ n opposite {suc n} (suc i) = inject₁ (opposite i) -- The function f(i,j) = if j>i then j-1 else j -- This is a variant of the thick function from Conor -- McBride's "First-order unification by structural recursion". punchOut : ∀ {i j : Fin (suc n)} → i ≢ j → Fin n punchOut {_} {zero} {zero} i≢j = contradiction refl i≢j punchOut {_} {zero} {suc j} _ = j punchOut {suc _} {suc i} {zero} _ = zero punchOut {suc _} {suc i} {suc j} i≢j = suc (punchOut (i≢j ∘ cong suc)) -- The function f(i,j) = if j≥i then j+1 else j punchIn : Fin (suc n) → Fin n → Fin (suc n) punchIn zero j = suc j punchIn (suc i) zero = zero punchIn (suc i) (suc j) = suc (punchIn i j) -- The function f(i,j) such that f(i,j) = if j≤i then j else j-1 pinch : Fin n → Fin (suc n) → Fin n pinch {suc n} _ zero = zero pinch {suc n} zero (suc j) = j pinch {suc n} (suc i) (suc j) = suc (pinch i j) ------------------------------------------------------------------------ -- Order relations infix 4 _≤_ _≥_ _<_ _>_ _≤_ : IRel Fin 0ℓ i ≤ j = toℕ i ℕ.≤ toℕ j _≥_ : IRel Fin 0ℓ i ≥ j = toℕ i ℕ.≥ toℕ j _<_ : IRel Fin 0ℓ i < j = toℕ i ℕ.< toℕ j _>_ : IRel Fin 0ℓ i > j = toℕ i ℕ.> toℕ j ------------------------------------------------------------------------ -- An ordering view. data Ordering {n : ℕ} : Fin n → Fin n → Set where less : ∀ greatest (least : Fin′ greatest) → Ordering (inject least) greatest equal : ∀ i → Ordering i i greater : ∀ greatest (least : Fin′ greatest) → Ordering greatest (inject least) compare : ∀ (i j : Fin n) → Ordering i j compare zero zero = equal zero compare zero (suc j) = less (suc j) zero compare (suc i) zero = greater (suc i) zero compare (suc i) (suc j) with compare i j ... | less greatest least = less (suc greatest) (suc least) ... | greater greatest least = greater (suc greatest) (suc least) ... | equal i = equal (suc i) ------------------------------------------------------------------------ -- DEPRECATED NAMES ------------------------------------------------------------------------ -- Please use the new names as continuing support for the old names is -- not guaranteed. -- Version 2.0 raise = _↑ʳ_ {-# WARNING_ON_USAGE raise "Warning: raise was deprecated in v2.0. Please use _↑ʳ_ instead." #-} inject+ : ∀ {m} n → Fin m → Fin (m ℕ.+ n) inject+ n i = i ↑ˡ n {-# WARNING_ON_USAGE inject+ "Warning: inject+ was deprecated in v2.0. Please use _↑ˡ_ instead. NB argument order has been flipped: the left-hand argument is the Fin m the right-hand is the Nat index increment." #-} data _≺_ : ℕ → ℕ → Set where _≻toℕ_ : ∀ n (i : Fin n) → toℕ i ≺ n {-# WARNING_ON_USAGE _≺_ "Warning: _≺_ was deprecated in v2.0. Please use equivalent relation _<_ instead." #-} {-# WARNING_ON_USAGE _≻toℕ_ "Warning: _≻toℕ_ was deprecated in v2.0. Please use toℕ<n from Data.Fin.Properties instead." #-}