[ new ] Fin n as a refinement

CHANGELOG.md

@@ -122,6 +122,11 @@ Deprecated names
   truncate-irrelevant  ↦  Relation.Binary.PropositionalEquality.Core.refl
   ```
 
+* In `Function.Base`:
+  ```agda
+  λ∙ : (.(x : A) → B x) → ((x : A) → B x)
+  ```
+
 * In `Relation.Binary.Construct.Intersection`:
   ```agda
   decidable     ↦   _∩?_
@@ -184,6 +189,11 @@ New modules
   Data.List.NonEmpty.Membership.Setoid
   ```
 
+* A variation on `Fin` seen as a `Nat` refinement
+  ```
+  Data.Nat.Bounded.Base
+  ```
+
 * Refactoring of `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties` as smaller modules:
   ```
   Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Lookup
@@ -391,6 +401,7 @@ Additions to existing modules
   m⊔n∸[m∸n]≡n : ∀ m n → m ⊔ n ∸ (m ∸ n) ≡ n
   m⊔n≡m∸n+n : ∀ m n → m ⊔ n ≡ m ∸ n + n
   ∣m-n∣≡m⊔n∸m⊓n : ∀ m n → ∣ m - n ∣ ≡ m ⊔ n ∸ m ⊓ n
+  <″⇒< : _<″_ ⇒ _<_
   ```
 
 * In `Data.Product.Properties`:

src/Data/Fin/Base.agda

@@ -54,6 +54,17 @@ 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)
 
+-- Tests showing that cast does compute on constructors
+
+module _ .(eqs : suc m ≡ suc n) where
+
+  _ : cast eqs zero ≡ zero
+  _ = refl
+
+  _ : .(eq : m ≡ n) (k : Fin m) →
+      cast eqs (suc k) ≡ suc (cast eq k)
+  _ = λ eq k → refl
+
 ------------------------------------------------------------------------
 -- Conversions
 
@@ -77,7 +88,7 @@ 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
+-- Canonical liftings of i:Fin m to larger index
 
 -- injection on the left: "i" ↑ˡ n = "i" in Fin (m + n)
 infixl 5 _↑ˡ_
@@ -91,6 +102,7 @@ _↑ʳ_ : ∀ {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

src/Data/Nat/Bounded/Base.agda

@@ -0,0 +1,329 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Bounded Natural numbers (Fin, without the runtime overhead)
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Nat.Bounded.Base where
+
+open import Data.Bool.Base using (T; true; false)
+import Data.Bool.Properties as Boolₚ
+open import Data.Empty using (⊥-elim)
+open import Data.Irrelevant as Irrelevant using (Irrelevant; [_]; pure; _<*>_)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; z<s; s<s; s<s⁻¹; NonZero)
+import Data.Nat.Properties as ℕₚ
+import Data.Nat.DivMod as ℕₚ
+open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)
+open import Data.Refinement as Refinement using (Refinement; _,_; Refinement-syntax; proof)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
+
+open import Function.Base using (id; _$_; _∘_; λ∙; _on_)
+open import Function.Bundles using (Equivalence); open Equivalence using (from)
+
+open import Level using (0ℓ)
+
+open import Relation.Binary.Core using (Rel; _⇒_)
+open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; _≢_; refl; cong; subst; sym; ≢-sym)
+open import Relation.Nullary.Decidable using (recompute; T?; yes; no)
+open import Relation.Nullary.Negation.Core using (¬_)
+
+private
+  variable
+    m n : ℕ
+
+------------------------------------------------------------------------
+-- Types
+
+-- Fin n is a type with n elements.
+
+Fin : ℕ → Set
+Fin n = [ m ∈ ℕ ∣ m ℕ.< n ]
+
+¬Fin0 : ¬ (Fin 0)
+¬Fin0 ()
+
+nonZeroIndex : Fin n → ℕ.NonZero n
+nonZeroIndex {n = suc _} _ = _
+
+-- Recovering constructors and pattern matching
+
+fzero : ∀ {n} → Fin (suc n)
+fzero = 0 , [ z<s ]
+
+fsuc : ∀ {n} → Fin n → Fin (suc n)
+fsuc = Refinement.map suc s<s
+
+data View : ∀ {n} (k : Fin n) → Set where
+  zero : View {suc n} fzero
+  suc  : (k : Fin n) → View (fsuc k)
+
+view : (k : Fin n) → View k
+view {suc n} (0 , prf)     = zero
+view {suc n} (suc k , prf) = suc (k , (| s<s⁻¹ prf |))
+
+unview : {k : Fin n} → View k → Fin n
+unview {k = k} _ = k
+
+-- A conversion: toℕ "i" = i.
+
+toℕ : Fin n → ℕ
+toℕ = Refinement.value
+
+-- 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 {m = m} {n = n} eq
+  = Refinement.map id
+  $ subst (_ ℕ.<_) (recompute (m ℕₚ.≟ n) eq)
+
+-- Tests showing that cast does compute on constructors
+
+module _ .(eqs : suc m ≡ suc n) where
+
+  _ : cast eqs fzero ≡ fzero
+  _ = refl
+
+  _ : .(eq : m ≡ n) (k : Fin m) →
+      cast eqs (fsuc k) ≡ fsuc (cast eq k)
+  _ = λ eq k → refl
+
+------------------------------------------------------------------------
+-- Conversions
+
+-- toℕ is defined above.
+
+-- fromℕ n = "n".
+
+fromℕ : (n : ℕ) → Fin (suc n)
+fromℕ n = n , [ ℕₚ.n<1+n n ]
+
+-- fromℕ< {m} _ = "m".
+
+fromℕ< : .(m ℕ.< n) → Fin n
+fromℕ< m<n = _ , [ m<n ]
+
+fromℕ<ᵇ : T (m ℕ.<ᵇ n) → Fin n
+fromℕ<ᵇ p = fromℕ< (ℕₚ.<ᵇ⇒< _ _ p)
+
+-- fromℕ<″ m _ = "m".
+
+fromℕ<″ : ∀ m {n} → .(m ℕ.<″ n) → Fin n
+fromℕ<″ m m<″n = m , [ ℕₚ.<″⇒< m<″n ]
+
+-- Canonical liftings of i:Fin m to a larger index
+
+-- injection on the left: "i" ↑ˡ n = "i" in Fin (m + n)
+infixl 5 _↑ˡ_
+_↑ˡ_ : ∀ {m} → Fin m → ∀ n → Fin (m ℕ.+ n)
+_↑ˡ_ {m} i n = Refinement.map id prf i where
+
+  prf : ∀ {k} → k ℕ.< m → k ℕ.< m ℕ.+ n
+  prf {k} k<m = let open ℕₚ.≤-Reasoning in begin-strict
+    k       ≡⟨ ℕₚ.+-identityʳ k ⟨
+    k ℕ.+ 0 <⟨ ℕₚ.+-mono-<-≤ k<m z≤n ⟩
+    m ℕ.+ n ∎
+
+-- injection on the right: n ↑ʳ "i" = "n + i" in Fin (n + m)
+infixr 5 _↑ʳ_
+_↑ʳ_ : ∀ {m} n → Fin m → Fin (n ℕ.+ m)
+n ↑ʳ i = Refinement.map (n ℕ.+_) (ℕₚ.+-monoʳ-< n) i
+
+-- reduce≥ "m + i" _ = "i".
+
+reduce≥ : ∀ (i : Fin (m ℕ.+ n)) → .(m ℕ.≤ toℕ i) → Fin n
+reduce≥ {m = m} {n = n} (k , prf) m≤i
+  = k ℕ.∸ m , (| go prf [ m≤i ] |) where
+
+  go : k ℕ.< m ℕ.+ n → m ℕ.≤ k → k ℕ.∸ m ℕ.< n
+  go k<m+n m≤k = let open ℕₚ.≤-Reasoning in begin-strict
+    k ℕ.∸ m       <⟨ ℕₚ.∸-monoˡ-< k<m+n m≤k ⟩
+    m ℕ.+ n ℕ.∸ m ≡⟨ ℕₚ.m+n∸m≡n m n ⟩
+    n             ∎
+
+-- inject⋆ m "i" = "i".
+
+inject : ∀ {i : Fin n} → Fin′ i → Fin n
+inject {i = i} (k , k<i) = k , (| ℕₚ.<-trans k<i (proof i)|)
+
+inject! : ∀ {i : Fin (suc n)} → Fin′ i → Fin n
+inject! {i = i} (k , k<i)
+  = k , (| ℕₚ.<-≤-trans k<i (| ℕ.s≤s⁻¹ (proof i)|) |)
+
+inject₁ : Fin n → Fin (suc n)
+inject₁ (k , k<n) = k , (| ℕₚ.m<n⇒m<1+n k<n |)
+
+inject≤ : Fin m → .(m ℕ.≤ n) → Fin n
+inject≤ (k , k<m) m≤n
+  = k , (| ℕₚ.<-≤-trans k<m [ m≤n ] |)
+
+-- lower₁ "i" _ = "i".
+
+lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n
+lower₁ (k , k<1+n) n≢i
+  = k , (| ℕₚ.≤∧≢⇒< (| ℕ.s≤s⁻¹ k<1+n |) [ ≢-sym n≢i ] |)
+
+lower : ∀ (i : Fin m) → .(toℕ i ℕ.< n) → Fin n
+lower (k , _) k<n = k , [ k<n ]
+
+-- A strengthening injection into the minimal Fin fibre.
+
+strengthen : ∀ (i : Fin n) → Fin′ (fsuc i)
+strengthen (k , prf) = (k , [ ℕₚ.≤-refl ])
+
+-- 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 m i@(k , prf) with T? (k ℕ.<ᵇ m)
+... | yes k<ᵇm = inj₁ (k , [ ℕₚ.<ᵇ⇒< k m k<ᵇm ])
+... | no  k≮ᵇm = inj₂ (reduce≥ i (ℕₚ.≮⇒≥ (k≮ᵇm ∘ ℕₚ.<⇒<ᵇ)))
+
+-- inverse of above function
+join : ∀ m n → Fin m ⊎ Fin n → Fin (m ℕ.+ n)
+join m n = [ _↑ˡ n , m ↑ʳ_ ]′
+
+-- quotRem n "i" = "i % n" , "i / n"
+-- This is dual to group from Data.Vec.
+
+quotRem : ∀ n → Fin (m ℕ.* n) → Fin n × Fin m
+quotRem {m = m} zero i = ⊥-elim (¬Fin0 (subst Fin (ℕₚ.*-zeroʳ m) i))
+quotRem {m = m} n@(suc _) (i , i<m*n)
+  = (i ℕ.% n , [ ℕₚ.m%n<n i n ])
+  , (i ℕ./ n , (| ℕₚ.m<n*o⇒m/o<n i<m*n |))
+
+-- 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 {m = suc m} {n = n} (k , k<m) (l , l<n)
+  = (k ℕ.* n) ℕ.+ l , (| go (| ℕ.s≤s⁻¹ k<m |) l<n |)
+
+  where
+
+  go : k ℕ.≤ m → l ℕ.< n → k ℕ.* n ℕ.+ l ℕ.< suc m ℕ.* n
+  go k≤m l<n = let open ℕₚ.≤-Reasoning in begin-strict
+    k ℕ.* n ℕ.+ l <⟨ ℕₚ.+-mono-≤-< (ℕₚ.*-monoˡ-≤ n k≤m) l<n ⟩
+    m ℕ.* n ℕ.+ n ≡⟨ ℕₚ.+-comm (m ℕ.* n) n ⟩
+    n ℕ.+ m ℕ.* n ∎
+
+-- Next in progression after splitAt and remQuot
+finToFun : Fin (m ℕ.^ n) → (Fin n → Fin m)
+finToFun {m = m} {n = suc n} i j with view j
+... | zero    = quotient (m ℕ.^ 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 = fzero
+funToFin {suc m} f = combine (f fzero) (funToFin (f ∘ fsuc))
+
+------------------------------------------------------------------------
+-- 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 k with view k
+... | zero    = x
+... | (suc i) = f (fold T f x i)
+
+fold′ : ∀ {n t} (T : Fin (suc n) → Set t) →
+        (∀ i → T (inject₁ i) → T (fsuc i)) →
+        T fzero →
+        ∀ i → T i
+fold′ T f x k with view k
+... | zero = x
+fold′ {n = suc n} T f x k | (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 {n = n} k f i = [ _↑ˡ n , (k ↑ʳ_) ∘ f ]′ (splitAt k i)
+
+-- "i" + "j" = "i + j".
+
+infixl 6 _+_
+_+_ : ∀ (i : Fin m) (j : Fin n) → Fin (toℕ i ℕ.+ n)
+_+_ {m = m} {n = n} (i , i<m) (j , j<n)
+  = i ℕ.+ j , (| (ℕₚ.+-monoʳ-< i) j<n |)
+
+-- "i" - "j" = "i ∸ j".
+
+infixl 6 _-_
+_-_ : ∀ (i : Fin n) (j : Fin′ (fsuc i)) → Fin (n ℕ.∸ toℕ j)
+(i , i<n) - (j , j<1+i)
+  = i ℕ.∸ j
+  , (| ℕₚ.∸-monoˡ-< i<n (| ℕ.s≤s⁻¹ j<1+i |) |)
+
+-- m ℕ- "i" = "m ∸ i".
+
+infixl 6 _ℕ-_
+_ℕ-_ : (n : ℕ) (j : Fin (suc n)) → Fin (suc n ℕ.∸ toℕ j)
+n ℕ- (j , j<1+n)
+  = n ℕ.∸ j
+  , (| (ℕₚ.≤-reflexive ∘ sym ∘ (λ∙ ℕₚ.∸-suc) ∘ ℕ.s≤s⁻¹) j<1+n |)
+
+-- m ℕ-ℕ "i" = m ∸ i.
+
+infixl 6 _ℕ-ℕ_
+_ℕ-ℕ_ : (n : ℕ) → Fin (suc n) → ℕ
+n ℕ-ℕ (i , i<1+m) = n ℕ.∸ i
+
+-- pred "i" = "pred i".
+
+pred : Fin n → Fin n
+pred (k , k<n) = ℕ.pred k , (| (ℕₚ.≤-<-trans ℕₚ.pred[n]≤n) k<n |)
+
+-- opposite "i" = "pred n - i" (i.e. the additive inverse).
+
+opposite : Fin n → Fin n
+opposite {n = n@(suc m)} i@(k , _)
+  = m ℕ.∸ k , [ ℕₚ.m<n+o⇒m∸n<o m k (ℕₚ.m≤n+m n k) ]
+
+
+
+------------------------------------------------------------------------
+-- 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
+
+_≰_ : ∀ {n} → Rel (Fin n) 0ℓ
+i ≰ j = ¬ (i ≤ j)
+
+_≮_ : ∀ {n} → Rel (Fin n) 0ℓ
+i ≮ j = ¬ (i < j)