Add alternative Fin operators for Fin with non-zero size

CHANGELOG.md

@@ -1139,6 +1139,31 @@ Deprecated names
   map-++-commute ↦  map-++
   ```
 
+* In `Data.Vec.Relation.Unary.All`:
+  for `{{NonZero n}}`, as per issue #1686
+
+  ```agda
+  head′ : All P xs → P (Vec.head′ {n = n} xs)
+  tail′ : All P xs → All P (Vec.tail′ {n = n} xs)
+  uncons′ : All P xs → P (Vec.head′ {n = n} xs) × All P (Vec.tail′ {n = n} xs)
+  ```
+
+* In `Data.Vec.Relation.Unary.Any`:
+  for `{{NonZero n}}`, as per issue #1686
+
+  ```agda
+  head′ : ¬ Any P (Vec.tail′ {n = n} xs) → Any P xs → P (Vec.head′ {n = n} xs)
+  tail′ : ¬ P (Vec.head′ {n = n} xs) → Any P xs → Any P (Vec.tail′ {n = n} xs)
+  ```
+
+* In `Data.Vec.Relation.Unary.Linked.Properties`:
+  for `{{NonZero n}}`, as per issue #1686
+
+  ```agda
+  Linked⇒All′ : ∀ {v} {xs : Vec _ n} → R v (head′ xs) →
+                Linked R xs → All (R v) xs
+  ```
+
 * In `Function.Construct.Composition`:
   ```
   _∘-⟶_   ↦   _⟶-∘_
@@ -1557,6 +1582,8 @@ Other minor changes
   leftSemimedial : LeftSemimedial _∙_
   rightSemimedial : RightSemimedial _∙_
   middleSemimedial : ∀ x y z → (x ∙ y) ∙ (z ∙ x) ≈ (x ∙ z) ∙ (y ∙ x)
+
+  sum-remove′ : ∀ {n} {{_ : NonZero n}} {i : Fin n} t → sum t ≈ t i + sum (remove′ i t)
   ```
 
 * Added new proofs to `Algebra.Properties.Semigroup`:
@@ -1627,6 +1654,21 @@ Other minor changes
   quotient  : Fin (m * n) → Fin m
   remainder : Fin (m * n) → Fin n
   ```
+
+  Additionally, as per issue #1686, primed functionality in cases
+  where the `Fin` index `n` is `NonZero`: 
+  ```
+  zero′     : Fin n
+  suc'      : Fin (ℕ.pred n) → Fin n
+  inject!′  : {i : Fin n} → Fin′ i → Fin (ℕ.pred n)
+  inject₁′  : Fin (ℕ.pred n) → Fin n
+  lower₁′   : (i : Fin n) → n ≢ suc (toℕ i) → Fin (ℕ.pred n)
+  _ℕ-′_     : (j : Fin n) → Fin (n ℕ.∸ toℕ j)
+  _ℕ-ℕ′_    : Fin n → ℕ
+  punchOut′ : {i j : Fin n} → i ≢ j → Fin (ℕ.pred n)
+  punchIn′  : Fin n → Fin (ℕ.pred n) → Fin n
+  pinch′    : Fin (ℕ.pred n) → Fin n → Fin (ℕ.pred n)
+  ```	
 
 * Added new proofs in `Data.Fin.Induction`:
   every (strict) partial order is well-founded and Noetherian.
@@ -1691,6 +1733,29 @@ Other minor changes
   cast-trans    : cast eq₂ (cast eq₁ k) ≡ cast (trans eq₁ eq₂) k
   ```
 
+  Additionally properties of the primed functionality as in `Data.Fin.Base`:
+  ```
+  inject₁-lower₁′ : (n≢i+1 : n ≢ suc (toℕ i)) →
+                   inject₁′ (lower₁′ i n≢i+1) ≡ i
+  lower₁-irrelevant′ : (n≢i₁+1 n≢i₂+1 : n ≢ suc (toℕ i)) →
+                       lower₁′ i n≢i₁+1 ≡ lower₁′ i n≢i₂+1
+  inject₁≡⇒lower₁≡′ : (n≢j+1 : n ≢ suc (toℕ j)) → inject₁′ i ≡ j → lower₁′ j n≢j+1 ≡ i
+  pred<′ : (i : Fin n) → i ≢ zero′ → pred i < i
+  punchOut-cong′ : {i≢j : i ≢ j} {i≢k : i ≢ k} →
+                  j ≡ k → punchOut′ i≢j ≡ punchOut′ i≢k
+  punchOut-injective′ : (i≢j : i ≢ j) (i≢k : i ≢ k) →
+                       punchOut′ i≢j ≡ punchOut′ i≢k → j ≡ k
+  punchIn-punchOut′ : {i j : Fin n} (i≢j : i ≢ j) →
+                     punchIn′ i (punchOut′ i≢j) ≡ j
+
+  pinch-injective′ : {i : Fin (ℕ.pred n)} {j k : Fin n} →
+                     suc′ i ≢ j → suc′ i ≢ k → pinch′ i j ≡ pinch′ i k → j ≡ k
+  ```
+
+  NB Adding `punchOut-cong′` for the sake of uniformity with the 'primed' naming scheme
+  for  `NonZero` instances, entailed renaming the old `punchOut-cong′` to `punchOut-cong-eq`,
+  with knock-on effect in two places in `Data.Fin.Permutation`
+
 * Added new functions in `Data.Integer.Base`:
   ```
   _^_ : ℤ → ℕ → ℤ
@@ -2044,12 +2109,33 @@ Other minor changes
 
   cast : .(eq : m ≡ n) → Vec A m → Vec A n
   ```
+  And for `{{NonZero n}}` as per issue 1686
+  ```
+  head′   : Vec A n → A
+  tail′   : Vec A n → A ^ (pred n)
+  uncons′ : Vec A n → A × Vec A (pred n)
+  insert′ : Vec A (pred n) → Fin n → A → Vec A n
+  remove′ : Vec A n → Fin n → Vec A (pred n)
+  init′   : (xs : Vec A n) → Vec A (pred n)
+  last′   : (xs : Vec A n) → A
+  ```
 
 * Added new instance in `Data.Vec.Categorical`:
   ```agda
   monad : RawMonad (λ (A : Set a) → Vec A n)
   ```
 
+* Added new functions in `Data.Vec.Functional` for `{{NonZero n}}`:
+  ```
+  head′   : Vector A n → A
+  tail′   : Vector A n → A ^ (pred n)
+  uncons′ : Vector A n → A × Vector A (pred n)
+  insert′ : Vector A (pred n) → Fin n → A → Vector A n
+  remove′ : Vector A n → Fin n → Vector A (pred n)
+  init′   : (xs : Vector A n) → Vector A (pred n)
+  last′   : (xs : Vector A n) → A
+  ```
+
 * Added new proofs in `Data.Vec.Properties`:
   ```agda
   padRight-refl      : padRight ≤-refl a xs ≡ xs
@@ -2111,6 +2197,20 @@ Other minor changes
   lookup-cast₁  : lookup (cast eq xs) i ≡ lookup xs (Fin.cast (sym eq) i)
   lookup-cast₂  : lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i
   ```
+  And for `{{NonZero n}}`:
+  ```
+  insert-lookup′ : (xs : Vec A (pred n)) (i : Fin n) (v : A) →
+                  lookup (insert′ xs i v) i ≡ v
+  insert-punchIn′ : (xs : Vec A (pred n)) (i : Fin n) (v : A) (j : Fin (pred n)) →
+                   lookup (insert′ xs i v) (Fin.punchIn′ i j) ≡ lookup xs j
+
+  ```
+* Added new functions in `Data.Vec.Recursive` for `{{NonZero n}}`:
+  ```
+  uncons′ : A ^ n → A × A ^ (pred n)
+  head′   : A ^ n → A
+  tail′   : A ^ n → A ^ (pred n)
+  ```
 
 * Added new proofs in `Data.Vec.Functional.Properties`:
   ```

src/Algebra/Properties/CommutativeMonoid/Sum.agda

@@ -59,6 +59,9 @@ sum-remove {suc n} {suc i}  xs = begin
   ∑t = sum t
   ∑t′ = sum (remove i t)
 
+sum-remove′ : ∀ {n} {{_ : NonZero n}} {i : Fin n} t → sum t ≈ t i + sum (remove′ i t)
+sum-remove′ {n = suc n} = sum-remove
+
 -- The '∑' operator distributes over addition.
 ∑-distrib-+ : ∀ {n} (f g : Vector Carrier n) → ∑[ i < n ] (f i + g i) ≈ ∑[ i < n ] f i + ∑[ i < n ] g i
 ∑-distrib-+ {zero}  f g = sym (+-identityˡ _)

src/Data/Fin/Base.agda

@@ -7,13 +7,14 @@
 -- 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 --without-K --safe #-}
 
 module Data.Fin.Base where
 
 open import Data.Bool.Base using (Bool; true; false; T; not)
 open import Data.Empty using (⊥-elim)
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; z<s; s<s; _^_)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero; z≤n; s≤s; z<s; s<s; _^_)
 open import Data.Product as Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (id; _∘_; _on_; flip)
@@ -38,6 +39,27 @@ data Fin : ℕ → Set where
   zero : Fin (suc n)
   suc  : (i : Fin n) → Fin (suc n)
 
+------------------------------------------------------------------------
+-- Much of the power of dependently-typed programming comes from the
+-- ability of pattern-matching over inhomogeneous telescopes of types
+-- to discriminate aruments to functions in sharper ways.
+
+-- The Fin type exemplifies this behaviour, but at the cost of not always
+-- being able to know in a function defintion which case one is in by virtue
+-- of an explicit constructor (ℕ.suc) symbol occurring in the type. So
+-- (issue #1686) we also consider constructors and functions defined over
+-- homogeneous telescopes of the form  {n} (i : Fin n) subject to n being
+-- NonZero, to be instantiated at any cal-site by instance inference.
+-- This additional functionality will be systematically marked by use of a prime \'.
+
+-- 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 → ℕ
@@ -111,21 +133,31 @@ 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!′ : .{{NonZero n}} → {i : Fin n} → Fin′ i → Fin (ℕ.pred n)
+inject!′ {n = suc _} = inject!
+
 inject₁ : Fin n → Fin (suc n)
 inject₁ zero    = zero
 inject₁ (suc i) = suc (inject₁ i)
 
+inject₁′ : .{{NonZero n}} → Fin (ℕ.pred n) → Fin n
+inject₁′ {n = suc _} = inject₁
+
 inject≤ : Fin m → m ℕ.≤ n → Fin n
 inject≤ {_} {suc n} zero    _        = zero
 inject≤ {_} {suc n} (suc i) (s≤s m≤n) = suc (inject≤ i m≤n)
 
 -- lower₁ "i" _ = "i".
 
-lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n
+lower₁ : (i : Fin (suc n)) → n ≢ toℕ i → Fin n
 lower₁ {zero}  zero    ne = ⊥-elim (ne refl)
 lower₁ {suc n} zero    _  = zero
 lower₁ {suc n} (suc i) ne = suc (lower₁ i (ne ∘ cong suc))
 
+lower₁′ : .{{NonZero n}} →
+          (i : Fin n) → n ≢ suc (toℕ i) → Fin (ℕ.pred n)
+lower₁′ {n = suc _} i ne = lower₁ i (ne ∘ cong suc)
+
 -- A strengthening injection into the minimal Fin fibre.
 strengthen : ∀ (i : Fin n) → Fin′ (suc i)
 strengthen zero    = zero
@@ -222,20 +254,26 @@ suc i - suc j  = i - j
 
 -- m ℕ- "i" = "m ∸ i".
 
-infixl 6 _ℕ-_
+infixl 6 _ℕ-_ _ℕ-′_
 
 _ℕ-_ : (n : ℕ) (j : Fin (suc n)) → Fin (suc n ℕ.∸ toℕ j)
 n     ℕ- zero   = fromℕ n
 suc n ℕ- suc i  = n ℕ- i
 
+_ℕ-′_ : (n : ℕ) {{_ : NonZero n}} (j : Fin n) → Fin (n ℕ.∸ toℕ j)
+(suc n) ℕ-′ i = n ℕ- i
+
 -- m ℕ-ℕ "i" = m ∸ i.
 
-infixl 6 _ℕ-ℕ_
+infixl 6 _ℕ-ℕ_ _ℕ-ℕ′_
 
 _ℕ-ℕ_ : (n : ℕ) → Fin (suc n) → ℕ
 n     ℕ-ℕ zero   = n
 suc n ℕ-ℕ suc i  = n ℕ-ℕ i
 
+_ℕ-ℕ′_ : (n : ℕ) {{_ : NonZero n}} → Fin n → ℕ
+suc n ℕ-ℕ′ i  = n ℕ-ℕ i
+
 -- pred "i" = "pred i".
 
 pred : Fin n → Fin n
@@ -258,20 +296,32 @@ 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))
 
+punchOut′ : .{{NonZero n}} →
+           {i j : Fin n} → i ≢ j → Fin (ℕ.pred n)
+punchOut′ {n = suc _} = punchOut
+
 -- 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)
 
+punchIn′ : .{{NonZero n}} →
+          Fin n → Fin (ℕ.pred n) → Fin n
+punchIn′ {n = suc _} = punchIn
+
 -- 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)
 
+pinch′ : .{{NonZero n}} →
+        Fin (ℕ.pred n) → Fin n → Fin (ℕ.pred n)
+pinch′ {n = suc _} = pinch
+
 ------------------------------------------------------------------------
 -- Order relations
 

src/Data/Fin/Permutation.agda

@@ -145,15 +145,15 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′
   inverseʳ′ : Inverseʳ _≡_ _≡_ to from
   inverseʳ′ j = begin
     from (to j)                                                      ≡⟨⟩
-    punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _  ≡⟨ punchOut-cong′ i (cong πˡ (punchIn-punchOut _)) ⟩
+    punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _  ≡⟨ punchOut-cong-eq i (cong πˡ (punchIn-punchOut _)) ⟩
     punchOut {i = i} {πˡ (πʳ (punchIn i j))}                      _  ≡⟨ punchOut-cong i (inverseˡ π) ⟩
     punchOut {i = i} {punchIn i j}                                _  ≡⟨ punchOut-punchIn i ⟩
     j                                                                ∎
 
   inverseˡ′ : Inverseˡ _≡_ _≡_ to from
   inverseˡ′ j = begin
     to (from j)                                                       ≡⟨⟩
-    punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))}  _  ≡⟨ punchOut-cong′ (πʳ i) (cong πʳ (punchIn-punchOut _)) ⟩
+    punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))}  _  ≡⟨ punchOut-cong-eq (πʳ i) (cong πʳ (punchIn-punchOut _)) ⟩
     punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))}               _  ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩
     punchOut {i = πʳ i} {punchIn (πʳ i) j}                         _  ≡⟨ punchOut-punchIn (πʳ i) ⟩
     j                                                                 ∎