Some properties of upTo and downFrom

CHANGELOG.md

@@ -140,6 +140,18 @@ Additions to existing modules
   pattern divides k eq = Data.Nat.Divisibility.divides k eq
   ```
 
+* In `Data.List.Properties`:
+  ```agda
+  applyUpTo-∷ʳ          : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)
+  applyDownFrom-∷ʳ      : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n)
+  upTo-∷ʳ               : upTo n ∷ʳ n ≡ upTo (suc n)
+  downFrom-∷ʳ           : applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n)
+  reverse-applyUpTo     : reverse (applyUpTo f n) ≡ applyDownFrom f n
+  reverse-upTo          : reverse (upTo n) ≡ downFrom n
+  reverse-applyDownFrom : reverse (applyDownFrom f n) ≡ applyUpTo f n
+  reverse-downFrom      : reverse (downFrom n) ≡ upTo n
+  ```
+
 * In `Data.List.Relation.Unary.All.Properties`:
   ```agda
   All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs)

src/Data/List/Properties.agda

@@ -657,8 +657,12 @@ lookup-applyUpTo : ∀ (f : ℕ → A) n i → lookup (applyUpTo f n) i ≡ f (t
 lookup-applyUpTo f (suc n) zero    = refl
 lookup-applyUpTo f (suc n) (suc i) = lookup-applyUpTo (f ∘ suc) n i
 
+applyUpTo-∷ʳ : ∀ (f : ℕ → A) n → applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)
+applyUpTo-∷ʳ f zero = refl
+applyUpTo-∷ʳ f (suc n) = cong (f 0 ∷_) (applyUpTo-∷ʳ (f ∘ suc) n)
+
 ------------------------------------------------------------------------
--- applyUpTo
+-- applyDownFrom
 
 module _ (f : ℕ → A) where
 
@@ -670,6 +674,10 @@ module _ (f : ℕ → A) where
   lookup-applyDownFrom (suc n) zero    = refl
   lookup-applyDownFrom (suc n) (suc i) = lookup-applyDownFrom n i
 
+  applyDownFrom-∷ʳ : ∀ n → applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n)
+  applyDownFrom-∷ʳ zero = refl
+  applyDownFrom-∷ʳ (suc n) = cong (f (suc n) ∷_) (applyDownFrom-∷ʳ n)
+
 ------------------------------------------------------------------------
 -- upTo
 
@@ -679,6 +687,9 @@ length-upTo = length-applyUpTo id
 lookup-upTo : ∀ n i → lookup (upTo n) i ≡ toℕ i
 lookup-upTo = lookup-applyUpTo id
 
+upTo-∷ʳ : ∀ n → upTo n ∷ʳ n ≡ upTo (suc n)
+upTo-∷ʳ = applyUpTo-∷ʳ id
+
 ------------------------------------------------------------------------
 -- downFrom
 
@@ -688,6 +699,9 @@ length-downFrom = length-applyDownFrom id
 lookup-downFrom : ∀ n i → lookup (downFrom n) i ≡ n ∸ (suc (toℕ i))
 lookup-downFrom = lookup-applyDownFrom id
 
+downFrom-∷ʳ : ∀ n → applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n)
+downFrom-∷ʳ = applyDownFrom-∷ʳ id
+
 ------------------------------------------------------------------------
 -- tabulate
 
@@ -1173,6 +1187,31 @@ reverse-foldl : ∀ (f : B → A → B) b xs →
                 foldl f b (reverse xs) ≡ foldr (flip f) b xs
 reverse-foldl f b xs = foldl-ʳ++ f b xs
 
+------------------------------------------------------------------------
+-- reverse, applyUpTo, and applyDownFrom
+
+reverse-applyUpTo : ∀ (f : ℕ → A) n → reverse (applyUpTo f n) ≡ applyDownFrom f n
+reverse-applyUpTo f zero = refl
+reverse-applyUpTo f (suc n) = begin
+  reverse (f 0 ∷ applyUpTo (f ∘ suc) n)  ≡⟨ reverse-++ [ f 0 ] (applyUpTo (f ∘ suc) n) ⟩
+  reverse (applyUpTo (f ∘ suc) n) ∷ʳ f 0 ≡⟨ cong (_∷ʳ f 0) (reverse-applyUpTo (f ∘ suc) n) ⟩
+  applyDownFrom (f ∘ suc) n ∷ʳ f 0       ≡⟨ applyDownFrom-∷ʳ f n ⟩
+  applyDownFrom f (suc n)                ∎
+
+reverse-upTo : ∀ n → reverse (upTo n) ≡ downFrom n
+reverse-upTo = reverse-applyUpTo id
+
+reverse-applyDownFrom : ∀ (f : ℕ → A) n → reverse (applyDownFrom f n) ≡ applyUpTo f n
+reverse-applyDownFrom f zero = refl
+reverse-applyDownFrom f (suc n) = begin
+  reverse (f n ∷ applyDownFrom f n)  ≡⟨ reverse-++ [ f n ] (applyDownFrom f n) ⟩
+  reverse (applyDownFrom f n) ∷ʳ f n ≡⟨ cong (_∷ʳ f n) (reverse-applyDownFrom f n) ⟩
+  applyUpTo f n ∷ʳ f n               ≡⟨ applyUpTo-∷ʳ f n ⟩
+  applyUpTo f (suc n)                ∎
+
+reverse-downFrom : ∀ n → reverse (downFrom n) ≡ upTo n
+reverse-downFrom = reverse-applyDownFrom id
+
 ------------------------------------------------------------------------
 -- _∷ʳ_