Some lemmata for non-empty lists

CHANGELOG.md

@@ -260,6 +260,7 @@ Additions to existing modules
 
 * In `Data.List.Properties`:
   ```agda
+  length-++-≤ : ∀ (xs : List A) → length xs ≤ length (xs ++ ys)
   map-applyUpTo : ∀ (f : ℕ → A) (g : A → B) n → map g (applyUpTo f n) ≡ applyUpTo (g ∘ f) n
   map-applyDownFrom : ∀ (f : ℕ → A) (g : A → B) n → map g (applyDownFrom f n) ≡ applyDownFrom (g ∘ f) n
   map-upTo : ∀ (f : ℕ → A) n → map f (upTo n) ≡ applyUpTo f n
@@ -276,6 +277,22 @@ Additions to existing modules
   filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
   ```
 
+* In `Data.List.NonEmpty.Properties`:
+  ```agda
+  ∷→∷⁺ : (x List.∷ xs) ≡ (y List.∷ ys) →
+         (x List⁺.∷ xs) ≡ (y List⁺.∷ ys)
+  ∷⁺→∷ : (x List⁺.∷ xs) ≡ (y List⁺.∷ ys) →
+         (x List.∷ xs) ≡ (y List.∷ ys)
+  length-⁺++⁺ : (xs ys : List⁺ A) → length (xs ⁺++⁺ ys) ≡ length xs + length ys
+  length-⁺++⁺-≤ : (xs ys : List⁺ A) → length xs ≤ length (xs ⁺++⁺ ys)
+  map-⁺++⁺ : ∀ (f : A → B) xs ys → map f (xs ⁺++⁺ ys) ≡ map f xs ⁺++⁺ map f ys
+  ⁺++⁺-assoc : Associative _⁺++⁺_
+  ⁺++⁺-cancelˡ : LeftCancellative _⁺++⁺_
+  ⁺++⁺-cancelʳ : RightCancellative _⁺++⁺_
+  ⁺++⁺-cancel : Cancellative _⁺++⁺_
+  map-id : map id ≗ id {A = List⁺ A}
+  ```
+
 * In `Data.Product.Function.Dependent.Propositional`:
   ```agda
   Σ-↪ : (I↪J : I ↪ J) → (∀ {j} → A (from I↪J j) ↪ B j) → Σ I A ↪ Σ J B

src/Data/List/NonEmpty/Properties.agda

@@ -8,25 +8,28 @@
 
 module Data.List.NonEmpty.Properties where
 
+import Algebra.Definitions as AlgebraicDefinitions
 open import Effect.Monad using (RawMonad)
-open import Data.Nat.Base using (suc; _+_)
+open import Data.Nat.Base using (suc; _+_; _≤_; s≤s)
 open import Data.Nat.Properties using (suc-injective)
 open import Data.Maybe.Properties using (just-injective)
 open import Data.Bool.Base using (Bool; true; false)
 open import Data.List.Base as List using (List; []; _∷_; _++_)
 open import Data.List.Effectful using () renaming (monad to listMonad)
+open import Data.List.Properties using (length-++; length-++-≤; ++-assoc; map-++)
 open import Data.List.NonEmpty.Effectful using () renaming (monad to list⁺Monad)
-open import Data.List.NonEmpty
+open import Data.List.NonEmpty as List⁺
   using (List⁺; _∷_; tail; head; toList; _⁺++_; _⁺++⁺_; _++⁺_; length; fromList;
     drop+; map; inits; tails; groupSeqs; ungroupSeqs)
 open import Data.List.NonEmpty.Relation.Unary.All using (All; toList⁺; _∷_)
 open import Data.List.Relation.Unary.All using ([]; _∷_) renaming (All to ListAll)
 import Data.List.Properties as List
+open import Data.Product.Base using (_,_)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Sum.Relation.Unary.All using (inj₁; inj₂)
 import Data.Sum.Relation.Unary.All as Sum using (All; inj₁; inj₂)
 open import Level using (Level)
-open import Function.Base using (_∘_; _$_)
+open import Function.Base using (id; _∘_; _$_)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; cong; cong₂; _≗_)
 open import Relation.Binary.PropositionalEquality.Properties
@@ -69,6 +72,47 @@ toList->>= f (x ∷ xs) = begin
   List.concat (List.map toList (List.map f (x ∷ xs)))
     ∎
 
+-- turning equalities of lists that are not empty to equalities on non-empty lists ...
+∷→∷⁺ : ∀ {x y : A} {xs ys : List A} →
+      (x List.∷ xs) ≡ (y List.∷ ys) →
+      (x List⁺.∷ xs) ≡ (y List⁺.∷ ys)
+∷→∷⁺ refl = refl
+
+-- ... and vice versa
+∷⁺→∷ : ∀ {x y : A} {xs ys : List A} →
+      (x List⁺.∷ xs) ≡ (y List⁺.∷ ys) →
+      (x List.∷ xs) ≡ (y List.∷ ys)
+∷⁺→∷ refl = refl
+
+------------------------------------------------------------------------
+-- _⁺++⁺_
+length-⁺++⁺ : (xs ys : List⁺ A) →
+              length (xs ⁺++⁺ ys) ≡ length xs + length ys
+length-⁺++⁺ (x ∷ xs) (y ∷ ys) = length-++ (x ∷ xs)
+
+length-⁺++⁺-≤ : (xs ys : List⁺ A) →
+                length xs ≤ length (xs ⁺++⁺ ys)
+length-⁺++⁺-≤ (x ∷ xs) (y ∷ ys) = s≤s (length-++-≤ xs)
+
+map-⁺++⁺ : ∀ (f : A → B) xs ys →
+           map f (xs ⁺++⁺ ys) ≡ map f xs ⁺++⁺ map f ys
+map-⁺++⁺ f (x ∷ xs) (y ∷ ys) = ∷→∷⁺ (map-++ f (x ∷ xs) (y ∷ ys))
+
+module _ {A : Set a} where
+  open AlgebraicDefinitions {A = List⁺ A} _≡_
+
+  ⁺++⁺-assoc : Associative _⁺++⁺_
+  ⁺++⁺-assoc (x ∷ xs) (y ∷ ys) (z ∷ zs) = cong (x ∷_) (++-assoc xs (y ∷ ys) (z ∷ zs))
+
+  ⁺++⁺-cancelˡ : LeftCancellative _⁺++⁺_
+  ⁺++⁺-cancelˡ (x ∷ xs) (y ∷ ys) (z ∷ zs) eq = ∷→∷⁺ (List.++-cancelˡ (x ∷ xs) (y ∷ ys) (z ∷ zs) (∷⁺→∷ eq))
+
+  ⁺++⁺-cancelʳ : RightCancellative _⁺++⁺_
+  ⁺++⁺-cancelʳ (x ∷ xs) (y ∷ ys) (z ∷ zs) eq = ∷→∷⁺ (List.++-cancelʳ (x ∷ xs) (y ∷ ys) (z ∷ zs) (∷⁺→∷ eq))
+
+  ⁺++⁺-cancel : Cancellative _⁺++⁺_
+  ⁺++⁺-cancel = ⁺++⁺-cancelˡ , ⁺++⁺-cancelʳ
+
 ------------------------------------------------------------------------
 -- _++⁺_
 
@@ -118,6 +162,9 @@ map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (List.map-cong f≗g xs)
 map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f
 map-∘ (x ∷ xs) = cong (_ ∷_) (List.map-∘ xs)
 
+map-id : map id ≗ id {A = List⁺ A}
+map-id (x ∷ xs) = cong (x ∷_) (List.map-id xs)
+
 ------------------------------------------------------------------------
 -- inits
 

src/Data/List/Properties.agda

@@ -131,6 +131,11 @@ length-++ : ∀ (xs : List A) {ys} →
 length-++ []       = refl
 length-++ (x ∷ xs) = cong suc (length-++ xs)
 
+length-++-≤ : ∀ (xs : List A) {ys} →
+              length xs ≤ length (xs ++ ys)
+length-++-≤ []       = z≤n
+length-++-≤ (x ∷ xs) = s≤s (length-++-≤ xs)
+
 module _ {A : Set a} where
 
   open AlgebraicDefinitions {A = List A} _≡_