Some lemmata for lists and non-empty lists (#2730)

* [add]: map-id for Data.List.NonEmpty

* [changelog]: map-id for Data.List.NonEmpty

* [add]: some lemmata for ⁺++⁺ of Data.List.NonEmpty

* [changelog]: some lemmata for ⁺++⁺

* [add]: ∷→∷⁺ and ∷⁺→∷

* [changelog]: ∷→∷⁺ and ∷⁺→∷

* [add]: ⁺++⁺-assoc for Data.List.NonEmpty

* [changelog]: ⁺++⁺-assoc for Data.List.NonEmpty

* [add]: ⁺++⁺-cancelˡ for Data.List.Empty

* [changelog]: ⁺++⁺-cancelˡ for Data.List.Empty

* [add]: ⁺++⁺-cancelʳ for Data.List.Empty

* [changelog]: ⁺++⁺-cancelʳ for Data.List.Empty

* [add]: ⁺++⁺-cancel for Data.List.NonEmpty

* [changelog]: ⁺++⁺-cancel for Data.List.NonEmpty

* [add]: map-⁺++⁺

* [changelog]: map-⁺++⁺

* [changelog] remove implicit args in List.NonEmpty

* [changelog]: style adaptions for List.NonEmpty

* [add]: length-++-≤ in Data.List.Properties

* [changelog]: length-++-≤ in Data.List.Properties

* [refactor] avoid rewrite in length-⁺++⁺-≤

* [add]: length-++-sucˡ, length-++-sucʳ

* [changelog]: length-++-sucˡ, length-++-sucʳ

* [refactor]: rename length-++-≤ to length-++-≤ˡ

* [refactor]: anon. modules Data.List.Properties

separates the anonymous module for algebraic definitions and structures
around _++_ into two modules

* [refactor]: move length-++ theorems

moves these theorems below the theorems on the algebraic properties of
_++_ so that we can later reuse them for further symmetric theorems

* [add]: length-++-comm

* [changelog]: length-++-comm

* [add]: length-++-≤ʳ

* [changelog]: length-++-≤ʳ

* [add]: length-⁺++⁺-≤ʳ

* [changelog]: length-⁺++⁺-≤ʳ

* [add]: length-⁺++⁺-comm

* [changelog]: length-⁺++⁺-comm

Author: pmbittner

CHANGELOG.md

@@ -264,6 +264,11 @@ Additions to existing modules
 
 * In `Data.List.Properties`:
   ```agda
+  length-++-sucˡ : ∀ (x : A) (xs ys : List A) → length (x ∷ xs ++ ys) ≡ suc (length (xs ++ ys))
+  length-++-sucʳ : ∀ (xs : List A) (y : A) (ys : List A) → length (xs ++ y ∷ ys) ≡ suc (length (xs ++ ys))
+  length-++-comm : ∀ (xs ys : List A) → length (xs ++ ys) ≡ length (ys ++ xs)
+  length-++-≤ˡ : ∀ (xs : List A) → length xs ≤ length (xs ++ ys)
+  length-++-≤ʳ : ∀ (ys : List A) → length ys ≤ 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
@@ -280,6 +285,24 @@ 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-⁺++⁺-comm : ∀ (xs ys : List⁺ A) → length (xs ⁺++⁺ ys) ≡ length (ys ⁺++⁺ xs)
+  length-⁺++⁺-≤ˡ : (xs ys : List⁺ A) → length xs ≤ length (xs ⁺++⁺ ys)
+  length-⁺++⁺-≤ʳ : (xs ys : List⁺ A) → length ys ≤ 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-++-comm; 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,56 @@ 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-⁺++⁺-comm : ∀ (xs ys : List⁺ A) →
+                   length (xs ⁺++⁺ ys) ≡ length (ys ⁺++⁺ xs)
+length-⁺++⁺-comm (x ∷ xs) (y ∷ ys) = length-++-comm (x ∷ xs) (y ∷ ys)
+
+length-⁺++⁺-≤ˡ : (xs ys : List⁺ A) →
+                length xs ≤ length (xs ⁺++⁺ ys)
+length-⁺++⁺-≤ˡ (x ∷ xs) (y ∷ ys) = s≤s (length-++-≤ˡ xs)
+
+length-⁺++⁺-≤ʳ : (xs ys : List⁺ A) →
+                length ys ≤ length (xs ⁺++⁺ ys)
+length-⁺++⁺-≤ʳ (x ∷ xs) (y ∷ ys) = length-++-≤ʳ (y ∷ ys) {x ∷ 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 +171,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

@@ -134,7 +134,6 @@ length-++ (x ∷ xs) = cong suc (length-++ xs)
 module _ {A : Set a} where
 
   open AlgebraicDefinitions {A = List A} _≡_
-  open AlgebraicStructures  {A = List A} _≡_
 
   ++-assoc : Associative _++_
   ++-assoc []       ys zs = refl
@@ -190,6 +189,47 @@ module _ {A : Set a} where
   ++-conical : Conical [] _++_
   ++-conical = ++-conicalˡ , ++-conicalʳ
 
+length-++-sucˡ : ∀ (x : A) (xs ys : List A) →
+                 length (x ∷ xs ++ ys) ≡ suc (length (xs ++ ys))
+length-++-sucˡ _ _ _ = refl
+
+length-++-sucʳ : ∀ (xs : List A) (y : A) (ys : List A) →
+                 length (xs ++ y ∷ ys) ≡ suc (length (xs ++ ys))
+length-++-sucʳ []       _ _  = refl
+length-++-sucʳ (_ ∷ xs) y ys = cong suc (length-++-sucʳ xs y ys)
+
+length-++-comm : ∀ (xs ys : List A) →
+                 length (xs ++ ys) ≡ length (ys ++ xs)
+length-++-comm xs       []       = cong length (++-identityʳ xs)
+length-++-comm []       (y ∷ ys) = sym (cong length (++-identityʳ (y ∷ ys)))
+length-++-comm (x ∷ xs) (y ∷ ys) =
+  begin
+    length (x ∷ xs ++ y ∷ ys)
+  ≡⟨⟩
+    suc (length (xs ++ y ∷ ys))
+  ≡⟨ cong suc (length-++-sucʳ xs y ys) ⟩
+    suc (suc (length (xs ++ ys)))
+  ≡⟨ cong suc (cong suc (length-++-comm xs ys)) ⟩
+    suc (suc (length (ys ++ xs)))
+  ≡⟨ cong suc (length-++-sucʳ ys x xs) ⟨
+    suc (length (ys ++ x ∷ xs))
+  ≡⟨⟩
+    length (y ∷ ys ++ x ∷ xs)
+  ∎
+
+length-++-≤ˡ : ∀ (xs : List A) {ys} →
+              length xs ≤ length (xs ++ ys)
+length-++-≤ˡ []       = z≤n
+length-++-≤ˡ (x ∷ xs) = s≤s (length-++-≤ˡ xs)
+
+length-++-≤ʳ : ∀ (ys : List A) {xs} →
+              length ys ≤ length (xs ++ ys)
+length-++-≤ʳ ys {xs} = ≤-trans (length-++-≤ˡ ys) (≤-reflexive (length-++-comm ys xs))
+
+module _ {A : Set a} where
+
+  open AlgebraicStructures  {A = List A} _≡_
+
   ++-isMagma : IsMagma _++_
   ++-isMagma = record
     { isEquivalence = isEquivalence