Rename inject+ and raise to left and right infix addition #1589 (#1592)

* committed changes as per Issue \#1589

* changes in line with Matthew and Jacques's comments; new lemma added

* fixed whitespace

* deprecated code, commented out, now removed entirely; types retained for documentation/argument order shenanigans

* added new proof to Data.vec.properties

* Update CHANGELOG.md

Added new proof to `Data.Vec.Properties`

* added fixities

Author: jamesmckinna

CHANGELOG.md

@@ -335,6 +335,28 @@ Deprecated names
   sym-↔   ↦   ↔-sym
   ```
 
+* In `Data.Fin.Base`: 
+two new, hopefully more memorable, names `↑ˡ` `↑ʳ` for the 'left', resp. 'right' injection of a Fin m into a 'larger' type, `Fin (m + n)`, resp. `Fin (n + m)`, with argument order to reflect the position of the Fin m argument. 
+  ```
+  inject+   ↦   flip _↑ˡ_
+  raise     ↦   _↑ʳ_
+  ```
+
+* In `Data.Fin.Properties`: 
+  ```
+  toℕ-raise       ↦ toℕ-↑ʳ
+  toℕ-inject+ n i ↦ sym (toℕ-↑ˡ i n)
+  splitAt-inject+ m n i ↦ splitAt-↑ˡ m i n
+  splitAt-raise ↦ splitAt-↑ʳ
+  ```
+
+* In `Data.Vec.Properties`: 
+  ```
+  []≔-++-inject+       ↦ []≔-++-↑ˡ
+  ```
+  Additionally, `[]≔-++-↑ʳ`, by analogy. 
+
+
 New modules
 -----------
 
@@ -518,6 +540,7 @@ Other minor changes
   map-⊛ : ∀ {n} (f : A → B → C) (g : A → B) (xs : Vec A n) → (map f xs ⊛ map g xs) ≡ map (f ˢ g) xs
   ⊛-is->>= : ∀ {n} (fs : Vec (A → B) n) (xs : Vec A n) → (fs ⊛ xs) ≡ (fs DiagonalBind.>>= flip map xs)
   transpose-replicate : ∀ {m n} (xs : Vec A m) → transpose (replicate {n = n} xs) ≡ map replicate xs
+  []≔-++-↑ʳ : ∀ {m n y} (xs : Vec A m) (ys : Vec A n) i → (xs ++ ys) [ m ↑ʳ i ]≔ y ≡ xs ++ (ys [ i ]≔ y)
   ```
 
 * Added new proofs in `Function.Construct.Symmetry`:

HACKING.md

@@ -81,7 +81,7 @@ How to make changes
    thrown up until the tests are passed. Note that the tests
    require the use of a tool called `fix-whitespace`. See the
    instructions at the end of this file for how to install this.
-   
+
    Note this step is optional as these tests will also be run automatically
    by our CI infrastructure when you open a pull request on Github, but it
    can be useful to run it locally to get a faster turn around time when finding

src/Data/Fin/Base.agda

@@ -17,7 +17,7 @@ open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s)
 open import Data.Nat.Properties.Core using (≤-pred)
 open import Data.Product as Product using (_×_; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
-open import Function.Base using (id; _∘_; _on_)
+open import Function.Base using (id; _∘_; _on_; flip)
 open import Level using (0ℓ)
 open import Relation.Nullary using (yes; no)
 open import Relation.Nullary.Decidable.Core using (True; toWitness)
@@ -77,11 +77,19 @@ fromℕ<″ zero    (ℕ.less-than-or-equal refl) = zero
 fromℕ<″ (suc m) (ℕ.less-than-or-equal refl) =
   suc (fromℕ<″ m (ℕ.less-than-or-equal refl))
 
--- raise m "i" = "m + i".
+-- canonical liftings of i:Fin m to larger index
 
-raise : ∀ {m} n → Fin m → Fin (n ℕ.+ m)
-raise zero    i = i
-raise (suc n) i = suc (raise n i)
+-- 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".
 
@@ -99,10 +107,6 @@ inject! : ∀ {n} {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+ : ∀ {m} n → Fin m → Fin (m ℕ.+ n)
-inject+ n zero    = zero
-inject+ n (suc i) = suc (inject+ n i)
-
 inject₁ : ∀ {m} → Fin m → Fin (suc m)
 inject₁ zero    = zero
 inject₁ (suc i) = suc (inject₁ i)
@@ -134,7 +138,7 @@ splitAt (suc m) (suc i) = Sum.map suc id (splitAt m i)
 
 -- inverse of above function
 join : ∀ m n → Fin m ⊎ Fin n → Fin (m ℕ.+ n)
-join m n = [ inject+ n , raise {n} m ]′
+join m n = [ _↑ˡ n , m ↑ʳ_ ]′
 
 -- quotRem k "i" = "i % k" , "i / k"
 -- This is dual to group from Data.Vec.
@@ -150,8 +154,8 @@ remQuot k = Product.swap ∘ quotRem k
 
 -- inverse of remQuot
 combine : ∀ {n k} → Fin n → Fin k → Fin (n ℕ.* k)
-combine {suc n} {k} zero y = inject+ (n ℕ.* k) y
-combine {suc n} {k} (suc x) y = raise k (combine x y)
+combine {suc n} {k} zero y = y ↑ˡ (n ℕ.* k)
+combine {suc n} {k} (suc x) y = k ↑ʳ (combine x y)
 
 ------------------------------------------------------------------------
 -- Operations
@@ -307,3 +311,20 @@ fromℕ≤″ = fromℕ<″
 "Warning: fromℕ≤″ was deprecated in v1.2.
 Please use fromℕ<″ instead."
 #-}
+
+-- 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."
+#-}

src/Data/Fin/Properties.agda

@@ -21,7 +21,7 @@ open import Data.Unit using (tt)
 open import Data.Product using (Σ-syntax; ∃; ∃₂; ∄; _×_; _,_; map; proj₁; uncurry; <_,_>)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′)
 open import Data.Sum.Properties using ([,]-map-commute; [,]-∘-distr)
-open import Function.Base using (_∘_; id; _$_)
+open import Function.Base using (_∘_; id; _$_; flip)
 open import Function.Bundles using (_↔_; mk↔′)
 open import Function.Definitions.Core2 using (Surjective)
 open import Function.Equivalence using (_⇔_; equivalence)
@@ -105,9 +105,21 @@ toℕ-strengthen : ∀ {n} (i : Fin n) → toℕ (strengthen i) ≡ toℕ i
 toℕ-strengthen zero    = refl
 toℕ-strengthen (suc i) = cong suc (toℕ-strengthen i)
 
-toℕ-raise : ∀ {m} n (i : Fin m) → toℕ (raise n i) ≡ n ℕ.+ toℕ i
-toℕ-raise zero    i = refl
-toℕ-raise (suc n) i = cong suc (toℕ-raise n i)
+------------------------------------------------------------------------
+-- toℕ-↑ˡ: "i" ↑ˡ n = "i" in Fin (m + n)
+------------------------------------------------------------------------
+
+toℕ-↑ˡ : ∀ {m} (i : Fin m) n → toℕ (i ↑ˡ n) ≡ toℕ i
+toℕ-↑ˡ zero    n = refl
+toℕ-↑ˡ (suc i) n = cong suc (toℕ-↑ˡ i n)
+
+------------------------------------------------------------------------
+-- toℕ-↑ʳ: n ↑ʳ "i" = "n + i" in Fin (n + m)
+------------------------------------------------------------------------
+
+toℕ-↑ʳ : ∀ {m} n (i : Fin m) → toℕ (n ↑ʳ i) ≡ n ℕ.+ toℕ i
+toℕ-↑ʳ zero    i = refl
+toℕ-↑ʳ (suc n) i = cong suc (toℕ-↑ʳ n i)
 
 toℕ<n : ∀ {n} (i : Fin n) → toℕ i ℕ.< n
 toℕ<n zero    = s≤s z≤n
@@ -371,14 +383,6 @@ toℕ-inject : ∀ {n} {i : Fin n} (j : Fin′ i) →
 toℕ-inject {i = suc i} zero    = refl
 toℕ-inject {i = suc i} (suc j) = cong suc (toℕ-inject j)
 
-------------------------------------------------------------------------
--- inject+
-------------------------------------------------------------------------
-
-toℕ-inject+ : ∀ {m} n (i : Fin m) → toℕ i ≡ toℕ (inject+ n i)
-toℕ-inject+ n zero    = refl
-toℕ-inject+ n (suc i) = cong suc (toℕ-inject+ n i)
-
 ------------------------------------------------------------------------
 -- inject₁
 ------------------------------------------------------------------------
@@ -490,25 +494,25 @@ pred< (suc i) p = ≤̄⇒inject₁< ℕₚ.≤-refl
 
 -- Fin (m + n) ↔ Fin m ⊎ Fin n
 
-splitAt-inject+ : ∀ m n i → splitAt m (inject+ n i) ≡ inj₁ i
-splitAt-inject+ (suc m) n zero = refl
-splitAt-inject+ (suc m) n (suc i) rewrite splitAt-inject+ m n i = refl
+splitAt-↑ˡ : ∀ m i n → splitAt m (i ↑ˡ n) ≡ inj₁ i
+splitAt-↑ˡ (suc m) zero    n = refl
+splitAt-↑ˡ (suc m) (suc i) n rewrite splitAt-↑ˡ m i n = refl
 
-splitAt-raise : ∀ m n i → splitAt m (raise {n} m i) ≡ inj₂ i
-splitAt-raise zero    n i = refl
-splitAt-raise (suc m) n i rewrite splitAt-raise m n i = refl
+splitAt-↑ʳ : ∀ m n i → splitAt m (m ↑ʳ i) ≡ inj₂ {B = Fin n} i
+splitAt-↑ʳ zero    n i = refl
+splitAt-↑ʳ (suc m) n i rewrite splitAt-↑ʳ m n i = refl
 
 splitAt-join : ∀ m n i → splitAt m (join m n i) ≡ i
-splitAt-join m n (inj₁ x) = splitAt-inject+ m n x
-splitAt-join m n (inj₂ y) = splitAt-raise m n y
+splitAt-join m n (inj₁ x) = splitAt-↑ˡ m x n
+splitAt-join m n (inj₂ y) = splitAt-↑ʳ m n y
 
 join-splitAt : ∀ m n i → join m n (splitAt m i) ≡ i
 join-splitAt zero    n i       = refl
 join-splitAt (suc m) n zero    = refl
 join-splitAt (suc m) n (suc i) = begin
-  [ inject+ n , raise {n} (suc m) ]′ (splitAt (suc m) (suc i))  ≡⟨ [,]-map-commute (splitAt m i) ⟩
-  [ suc ∘ (inject+ n) , suc ∘ (raise {n} m) ]′ (splitAt m i)    ≡˘⟨ [,]-∘-distr suc (splitAt m i) ⟩
-  suc ([ inject+ n , raise {n} m ]′ (splitAt m i))              ≡⟨ cong suc (join-splitAt m n i) ⟩
+  [ _↑ˡ n , (suc m) ↑ʳ_ ]′ (splitAt (suc m) (suc i)) ≡⟨ [,]-map-commute (splitAt m i) ⟩
+  [ suc ∘ (_↑ˡ n) , suc ∘ (m ↑ʳ_) ]′ (splitAt m i)   ≡˘⟨ [,]-∘-distr suc (splitAt m i) ⟩
+  suc ([ _↑ˡ n , m ↑ʳ_ ]′ (splitAt m i))             ≡⟨ cong suc (join-splitAt m n i) ⟩
   suc i                                                         ∎
   where open ≡-Reasoning
 
@@ -537,8 +541,8 @@ splitAt-≥ (suc m) (suc i) (s≤s i≥m) = cong (Sum.map suc id) (splitAt-≥ m
 -- Fin (m * n) ↔ Fin m × Fin n
 
 remQuot-combine : ∀ {n k} (x : Fin n) y → remQuot k (combine x y) ≡ (x , y)
-remQuot-combine {suc n} {k} 0F y rewrite splitAt-inject+ k (n ℕ.* k) y = refl
-remQuot-combine {suc n} {k} (suc x) y rewrite splitAt-raise k (n ℕ.* k) (combine x y) = cong (Data.Product.map₁ suc) (remQuot-combine x y)
+remQuot-combine {suc n} {k} 0F y rewrite splitAt-↑ˡ k y (n ℕ.* k) = refl
+remQuot-combine {suc n} {k} (suc x) y rewrite splitAt-↑ʳ k (n ℕ.* k) (combine x y) = cong (Data.Product.map₁ suc) (remQuot-combine x y)
 
 combine-remQuot : ∀ {n} k (i : Fin (n ℕ.* k)) → uncurry combine (remQuot {n} k i) ≡ i
 combine-remQuot {suc n} k i with splitAt k i | P.inspect (splitAt k) i
@@ -548,10 +552,10 @@ combine-remQuot {suc n} k i with splitAt k i | P.inspect (splitAt k) i
   i                              ∎
   where open ≡-Reasoning
 ... | inj₂ j | P.[ eq ] = begin
-  raise {n ℕ.* k} k (uncurry combine (remQuot {n} k j)) ≡⟨ cong (raise k) (combine-remQuot {n} k j) ⟩
-  join k (n ℕ.* k) (inj₂ j)                             ≡˘⟨ cong (join k (n ℕ.* k)) eq ⟩
-  join k (n ℕ.* k) (splitAt k i)                        ≡⟨ join-splitAt k (n ℕ.* k) i ⟩
-  i                                                     ∎
+  k ↑ʳ (uncurry combine (remQuot {n} k j)) ≡⟨ cong (k ↑ʳ_) (combine-remQuot {n} k j) ⟩
+  join k (n ℕ.* k) (inj₂ j)                ≡˘⟨ cong (join k (n ℕ.* k)) eq ⟩
+  join k (n ℕ.* k) (splitAt k i)           ≡⟨ join-splitAt k (n ℕ.* k) i ⟩
+  i                                        ∎
   where open ≡-Reasoning
 
 ------------------------------------------------------------------------
@@ -890,3 +894,33 @@ inject+-raise-splitAt = join-splitAt
 "Warning: decSetoid was deprecated in v1.5.
 Please use join-splitAt instead."
 #-}
+
+-- Version 2.0
+
+toℕ-raise = toℕ-↑ʳ
+{-# WARNING_ON_USAGE toℕ-raise
+"Warning: toℕ-raise was deprecated in v2.0.
+Please use toℕ-↑ʳ instead."
+#-}
+toℕ-inject+ : ∀ {m} n (i : Fin m) → toℕ i ≡ toℕ (i ↑ˡ n)
+toℕ-inject+ n i = sym (toℕ-↑ˡ i n)
+{-# WARNING_ON_USAGE toℕ-inject+
+"Warning: toℕ-inject+ was deprecated in v2.0.
+Please use toℕ-↑ˡ instead.
+NB argument order has been flipped:
+the left-hand argument is the Fin m
+the right-hand is the Nat index increment."
+#-}
+splitAt-inject+ : ∀ m n i → splitAt m (i ↑ˡ n) ≡ inj₁ i
+splitAt-inject+ m n i = splitAt-↑ˡ m i n
+{-# WARNING_ON_USAGE splitAt-inject+
+"Warning: splitAt-inject+ was deprecated in v2.0.
+Please use splitAt-↑ˡ instead.
+NB argument order has been flipped."
+#-}
+splitAt-raise : ∀ m n i → splitAt m (m ↑ʳ i) ≡ inj₂ {B = Fin n} i
+splitAt-raise = splitAt-↑ʳ
+{-# WARNING_ON_USAGE splitAt-raise
+"Warning: splitAt-raise was deprecated in v2.0.
+Please use splitAt-↑ʳ instead."
+#-}

src/Data/Vec/Functional.agda

@@ -138,10 +138,10 @@ unzip : ∀ {n} → Vector (A × B) n → Vector A n × Vector B n
 unzip = unzipWith id
 
 take : ∀ m {n} → Vector A (m ℕ.+ n) → Vector A m
-take _ {n = n} xs = xs ∘ inject+ n
+take _ {n = n} xs = xs ∘ (_↑ˡ n)
 
 drop : ∀ m {n} → Vector A (m ℕ.+ n) → Vector A n
-drop m xs = xs ∘ raise m
+drop m xs = xs ∘ (m ↑ʳ_)
 
 reverse : ∀ {n} → Vector A n → Vector A n
 reverse xs = xs ∘ opposite

src/Data/Vec/Functional/Properties.agda

@@ -166,12 +166,12 @@ lookup-++-≥ : ∀ {m n} (xs : Vector A m) (ys : Vector A n) →
 lookup-++-≥ {m = m} xs ys i i≥m = cong Sum.[ xs , ys ] (Finₚ.splitAt-≥ m i i≥m)
 
 lookup-++ˡ : ∀ {m n} (xs : Vector A m) (ys : Vector A n) i →
-             (xs ++ ys) (inject+ n i) ≡ xs i
-lookup-++ˡ {m = m} {n = n} xs ys i = cong Sum.[ xs , ys ] (Finₚ.splitAt-inject+ m n i)
+             (xs ++ ys) (i ↑ˡ n) ≡ xs i
+lookup-++ˡ {m = m} {n = n} xs ys i = cong Sum.[ xs , ys ] (Finₚ.splitAt-↑ˡ m i n)
 
 lookup-++ʳ : ∀ {m n} (xs : Vector A m) (ys : Vector A n) i →
-             (xs ++ ys) (raise m i) ≡ ys i
-lookup-++ʳ {m = m} {n = n} xs ys i = cong Sum.[ xs , ys ] (Finₚ.splitAt-raise m n i)
+             (xs ++ ys) (m ↑ʳ i) ≡ ys i
+lookup-++ʳ {m = m} {n = n} xs ys i = cong Sum.[ xs , ys ] (Finₚ.splitAt-↑ʳ m n i)
 
 module _ {m} {ys ys′ : Vector A m} where
 
@@ -194,19 +194,19 @@ module _ {m} {ys ys′ : Vector A m} where
   ++-injectiveˡ : ∀ {n} (xs xs′ : Vector A n) →
                   xs ++ ys ≗ xs′ ++ ys′ → xs ≗ xs′
   ++-injectiveˡ xs xs′ eq i = begin
-    xs i                        ≡˘⟨ lookup-++ˡ xs ys i ⟩
-    (xs ++ ys) (inject+ m i)    ≡⟨ eq (inject+ m i) ⟩
-    (xs′ ++ ys′) (inject+ m i)  ≡⟨ lookup-++ˡ xs′ ys′ i ⟩
-    xs′ i                       ∎
+    xs i                   ≡˘⟨ lookup-++ˡ xs ys i ⟩
+    (xs ++ ys) (i ↑ˡ m)    ≡⟨ eq (i ↑ˡ m) ⟩
+    (xs′ ++ ys′) (i ↑ˡ m)  ≡⟨ lookup-++ˡ xs′ ys′ i ⟩
+    xs′ i                  ∎
     where open ≡-Reasoning
 
   ++-injectiveʳ : ∀ {n} (xs xs′ : Vector A n) →
                   xs ++ ys ≗ xs′ ++ ys′ → ys ≗ ys′
   ++-injectiveʳ {n} xs xs′ eq i = begin
-    ys i                      ≡˘⟨ lookup-++ʳ xs ys i ⟩
-    (xs ++ ys) (raise n i)    ≡⟨ eq (raise n i)   ⟩
-    (xs′ ++ ys′) (raise n i)  ≡⟨ lookup-++ʳ xs′ ys′ i ⟩
-    ys′ i                     ∎
+    ys i                   ≡˘⟨ lookup-++ʳ xs ys i ⟩
+    (xs ++ ys) (n ↑ʳ i)    ≡⟨ eq (n ↑ʳ i)   ⟩
+    (xs′ ++ ys′) (n ↑ʳ i)  ≡⟨ lookup-++ʳ xs′ ys′ i ⟩
+    ys′ i                  ∎
     where open ≡-Reasoning
 
   ++-injective : ∀ {n} (xs xs′ : Vector A n) →

src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda

@@ -120,13 +120,13 @@ module _ (R : REL A B r) where
 
   ++⁻ˡ : ∀ {m n} (xs : Vector A m) (ys : Vector B m) {xs′ ys′} →
          Pointwise R (xs ++ xs′) (ys ++ ys′) → Pointwise R xs ys
-  ++⁻ˡ {m} {n} _ _ rs i with rs (inject+ n i)
-  ... | r rewrite splitAt-inject+ m n i = r
+  ++⁻ˡ {m} {n} _ _ rs i with rs (i ↑ˡ n)
+  ... | r rewrite splitAt-↑ˡ m i n = r
 
   ++⁻ʳ : ∀ {m n} (xs : Vector A m) (ys : Vector B m) {xs′ ys′} →
          Pointwise R (xs ++ xs′) (ys ++ ys′) → Pointwise R xs′ ys′
-  ++⁻ʳ {m} {n} _ _ rs i with rs (raise m i)
-  ... | r rewrite splitAt-raise m n i = r
+  ++⁻ʳ {m} {n} _ _ rs i with rs (m ↑ʳ i)
+  ... | r rewrite splitAt-↑ʳ m n i = r
 
   ++⁻ : ∀ {m n} xs ys {xs′ ys′} →
         Pointwise R (xs ++ xs′) (ys ++ ys′) →

src/Data/Vec/Functional/Relation/Unary/All/Properties.agda

@@ -97,12 +97,12 @@ module _ (P : Pred A p) {m n : ℕ} {xs : Vector A m} {ys : Vector A n} where
 module _ (P : Pred A p) {m n : ℕ} (xs : Vector A m) {ys : Vector A n} where
 
   ++⁻ˡ : All P (xs ++ ys) → All P xs
-  ++⁻ˡ ps i with ps (inject+ n i)
-  ... | p rewrite splitAt-inject+ m n i = p
+  ++⁻ˡ ps i with ps (i ↑ˡ n)
+  ... | p rewrite splitAt-↑ˡ m i n = p
 
   ++⁻ʳ : All P (xs ++ ys) → All P ys
-  ++⁻ʳ ps i with ps (raise m i)
-  ... | p rewrite splitAt-raise m n i = p
+  ++⁻ʳ ps i with ps (m ↑ʳ i)
+  ... | p rewrite splitAt-↑ʳ m n i = p
 
   ++⁻ : All P (xs ++ ys) → All P xs × All P ys
   ++⁻ ps = ++⁻ˡ ps , ++⁻ʳ ps