Refactor Data.Vec.Properties : Add toList-injective and new lemmas (#2733)

* toList

* better proof

* update propreties

* Revert changes to WithK.agda

* update CHANGELOG

* fixwhitespace

* change L. to List.

* update 1

* fix-whitespace

* ∷-ʳ++-eqFree

* Update Changelog

* Update deprecation warnings

---------

Co-authored-by: MatthewDaggitt <[email protected]>

Author: jmougeot

CHANGELOG.md

@@ -137,6 +137,7 @@ Deprecated names
   ∈⇒∣product   ↦  Data.Nat.ListAction.Properties.∈⇒∣product
   product≢0    ↦  Data.Nat.ListAction.Properties.product≢0
   ∈⇒≤product   ↦  Data.Nat.ListAction.Properties.∈⇒≤product
+  ∷-ʳ++-eqFree ↦  Data.List.Properties.ʳ++-ʳ++-eqFree
   ```
 
 * In `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
@@ -366,6 +367,17 @@ Additions to existing modules
     LeftInverse (I ×ₛ A) (J ×ₛ B)
   ```
 
+* In `Data.Vec.Properties`:
+  ```agda
+  toList-injective : ∀ {m n} → .(m=n : m ≡ n) → (xs : Vec A m) (ys : Vec A n) → toList xs ≡ toList ys → xs ≈[ m=n ] ys
+
+  toList-∷ʳ : ∀ x (xs : Vec A n) → toList (xs ∷ʳ x) ≡ toList xs List.++ List.[ x ]
+
+  fromList-reverse : (xs : List A) → (fromList (List.reverse xs)) ≈[ List.length-reverse xs ] reverse (fromList xs)
+
+  fromList∘toList : ∀  (xs : Vec A n) → fromList (toList xs) ≈[ length-toList xs ] xs
+  ```
+
 * In `Data.Product.Nary.NonDependent`:
   ```agda
   HomoProduct′ n f = Product n (stabulate n (const _) f)

src/Data/Vec/Properties.agda

@@ -52,6 +52,15 @@ private
     m n o : ℕ
     ws xs ys zs : Vec A n
 
+------------------------------------------------------------------------
+-- Properties of toList
+
+toList-injective : .(m≡n : m ≡ n) → (xs : Vec A m) (ys : Vec A n) →
+                  toList xs ≡ toList ys → xs ≈[ m≡n ] ys
+toList-injective m≡n [] [] xs=ys = refl
+toList-injective m≡n (x ∷ xs) (y ∷ ys) xs=ys =
+  cong₂ _∷_ (List.∷-injectiveˡ xs=ys) (toList-injective (cong pred m≡n) xs ys (List.∷-injectiveʳ xs=ys))
+
 ------------------------------------------------------------------------
 -- Properties of propositional equality over vectors
 
@@ -1016,26 +1025,41 @@ map-reverse : ∀ (f : A → B) (xs : Vec A n) →
               map f (reverse xs) ≡ reverse (map f xs)
 map-reverse f []       = refl
 map-reverse f (x ∷ xs) = begin
-  map f (reverse (x ∷ xs))  ≡⟨  cong (map f) (reverse-∷ x xs) ⟩
-  map f (reverse xs ∷ʳ x)   ≡⟨  map-∷ʳ f x (reverse xs) ⟩
-  map f (reverse xs) ∷ʳ f x ≡⟨  cong (_∷ʳ f x) (map-reverse f xs ) ⟩
+  map f (reverse (x ∷ xs))  ≡⟨ cong (map f) (reverse-∷ x xs) ⟩
+  map f (reverse xs ∷ʳ x)   ≡⟨ map-∷ʳ f x (reverse xs) ⟩
+  map f (reverse xs) ∷ʳ f x ≡⟨ cong (_∷ʳ f x) (map-reverse f xs ) ⟩
   reverse (map f xs) ∷ʳ f x ≡⟨ reverse-∷ (f x) (map f xs) ⟨
   reverse (f x ∷ map f xs)  ≡⟨⟩
   reverse (map f (x ∷ xs))  ∎
   where open ≡-Reasoning
 
 -- append and reverse
+toList-∷ʳ : ∀ x (xs : Vec A n) → toList (xs ∷ʳ x) ≡ toList xs List.++ List.[ x ]
+toList-∷ʳ x []       = refl
+toList-∷ʳ x (y ∷ xs) = cong (y List.∷_) (toList-∷ʳ x xs)
+
+toList-reverse : ∀ (xs : Vec A n) → toList (reverse xs) ≡ List.reverse (toList xs)
+toList-reverse [] = refl
+toList-reverse (x ∷ xs) = begin
+  toList (reverse (x ∷ xs))                   ≡⟨ cong toList (reverse-∷ x xs) ⟩
+  toList (reverse xs ∷ʳ x)                    ≡⟨ toList-∷ʳ x (reverse xs) ⟩
+  toList (reverse xs) List.++ List.[ x ]      ≡⟨ cong (List._++ List.[ x ]) (toList-reverse xs) ⟩
+  List.reverse (toList xs) List.++ List.[ x ] ≡⟨ List.unfold-reverse x (toList xs) ⟨
+  List.reverse (toList (x ∷ xs))              ∎
+  where open ≡-Reasoning
 
-reverse-++-eqFree : ∀ (xs : Vec A m) (ys : Vec A n) → let eq = +-comm m n in
-                    cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
-reverse-++-eqFree {m = zero}  {n = n} []       ys = ≈-sym (++-identityʳ-eqFree (reverse ys))
-reverse-++-eqFree {m = suc m} {n = n} (x ∷ xs) ys = begin
-  reverse (x ∷ xs ++ ys)              ≂⟨ reverse-∷ x (xs ++ ys) ⟩
-  reverse (xs ++ ys) ∷ʳ x             ≈⟨ ≈-cong′ (_∷ʳ x) (reverse-++-eqFree xs ys) ⟩
-  (reverse ys ++ reverse xs) ∷ʳ x     ≈⟨ ++-∷ʳ-eqFree x (reverse ys) (reverse xs) ⟩
-  reverse ys ++ (reverse xs ∷ʳ x)     ≂⟨ cong (reverse ys ++_) (reverse-∷ x xs) ⟨
-  reverse ys ++ (reverse (x ∷ xs))    ∎
-  where open CastReasoning
+reverse-++-eqFree : ∀ (xs : Vec A m) (ys : Vec A n)
+                  → reverse (xs ++ ys) ≈[ +-comm m n ] reverse ys ++ reverse xs
+reverse-++-eqFree {m = m} {n = n} xs ys =
+  toList-injective (+-comm m n) (reverse (xs ++ ys)) (reverse ys ++ reverse xs) $
+  begin
+    toList (reverse (xs ++ ys))                               ≡⟨ toList-reverse ((xs ++ ys)) ⟩
+    List.reverse (toList (xs ++ ys))                          ≡⟨ cong List.reverse (toList-++ xs ys) ⟩
+    List.reverse (toList xs List.++ toList ys)                ≡⟨ List.reverse-++ (toList xs) (toList ys) ⟩
+    List.reverse (toList ys) List.++ List.reverse (toList xs) ≡⟨ cong₂ List._++_ (toList-reverse ys) (toList-reverse xs) ⟨
+    toList (reverse ys) List.++ toList (reverse xs)           ≡⟨ toList-++ (reverse ys) (reverse xs) ⟨
+    toList (reverse ys ++ reverse xs)                         ∎
+  where open ≡-Reasoning
 
 cast-reverse : ∀ .(eq : m ≡ n) → cast eq ∘ reverse {A = A} {n = m} ≗ reverse ∘ cast eq
 cast-reverse _ _ = ≈-cong′ reverse refl
@@ -1061,53 +1085,57 @@ foldr-ʳ++ B f {e} xs = foldl-fusion (foldr B f e) refl (λ _ _ → refl) xs
 map-ʳ++ : ∀ (f : A → B) (xs : Vec A m) →
           map f (xs ʳ++ ys) ≡ map f xs ʳ++ map f ys
 map-ʳ++ {ys = ys} f xs = begin
-  map f (xs ʳ++ ys)              ≡⟨  cong (map f) (unfold-ʳ++ xs ys) ⟩
-  map f (reverse xs ++ ys)       ≡⟨  map-++ f (reverse xs) ys ⟩
-  map f (reverse xs) ++ map f ys ≡⟨  cong (_++ map f ys) (map-reverse f xs) ⟩
+  map f (xs ʳ++ ys)              ≡⟨ cong (map f) (unfold-ʳ++ xs ys) ⟩
+  map f (reverse xs ++ ys)       ≡⟨ map-++ f (reverse xs) ys ⟩
+  map f (reverse xs) ++ map f ys ≡⟨ cong (_++ map f ys) (map-reverse f xs) ⟩
   reverse (map f xs) ++ map f ys ≡⟨ unfold-ʳ++ (map f xs) (map f ys) ⟨
   map f xs ʳ++ map f ys          ∎
   where open ≡-Reasoning
 
-∷-ʳ++-eqFree : ∀ a (xs : Vec A m) {ys : Vec A n} → let eq = sym (+-suc m n) in
-               cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
-∷-ʳ++-eqFree a xs {ys} = begin
-  (a ∷ xs) ʳ++ ys         ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩
-  reverse (a ∷ xs) ++ ys  ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩
-  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++-eqFree a (reverse xs) ⟩
-  reverse xs ++ (a ∷ ys)  ≂⟨ unfold-ʳ++ xs (a ∷ ys) ⟨
-  xs ʳ++ (a ∷ ys)         ∎
-  where open CastReasoning
+toList-ʳ++ : ∀ (xs : Vec A m) {ys : Vec A n} →
+            toList (xs ʳ++ ys) ≡ (toList xs) List.ʳ++ toList ys
+toList-ʳ++ xs {ys} = begin
+  toList (xs ʳ++ ys)                          ≡⟨ cong toList (unfold-ʳ++ xs ys) ⟩
+  toList (reverse xs ++ ys)                   ≡⟨ toList-++ ((reverse xs )) ys ⟩
+  toList (reverse xs) List.++ toList ys       ≡⟨ cong (List._++ toList ys) (toList-reverse xs) ⟩
+  List.reverse (toList xs) List.++ toList ys  ≡⟨ List.ʳ++-defn (toList xs) ⟨
+  toList xs List.ʳ++ toList ys                ∎
+  where open ≡-Reasoning
+
 
 ++-ʳ++-eqFree : ∀ (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → let eq = m+n+o≡n+[m+o] m n o in
                 cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
-++-ʳ++-eqFree {m = m} {n} {o} xs {ys} {zs} = begin
-  ((xs ++ ys) ʳ++ zs)              ≂⟨ unfold-ʳ++ (xs ++ ys) zs ⟩
-  reverse (xs ++ ys) ++ zs         ≈⟨ ≈-cong′ (_++ zs) (reverse-++-eqFree xs ys) ⟩
-  (reverse ys ++ reverse xs) ++ zs ≈⟨ ++-assoc-eqFree (reverse ys) (reverse xs) zs ⟩
-  reverse ys ++ (reverse xs ++ zs) ≂⟨ cong (reverse ys ++_) (unfold-ʳ++ xs zs) ⟨
-  reverse ys ++ (xs ʳ++ zs)        ≂⟨ unfold-ʳ++ ys (xs ʳ++ zs) ⟨
-  ys ʳ++ (xs ʳ++ zs)               ∎
-  where open CastReasoning
+++-ʳ++-eqFree {m = m} {n} {o} xs {ys} {zs} =
+  toList-injective (m+n+o≡n+[m+o] m n o) ((xs ++ ys) ʳ++ zs) (ys ʳ++ (xs ʳ++ zs)) $
+  begin
+    toList ((xs ++ ys) ʳ++ zs)                          ≡⟨ toList-ʳ++ (xs ++ ys) ⟩
+    toList (xs ++ ys) List.ʳ++ toList zs                ≡⟨ cong (List._ʳ++ toList zs) (toList-++ xs ys)  ⟩
+    ((toList xs) List.++ toList ys ) List.ʳ++ toList zs ≡⟨ List.++-ʳ++ (toList xs) ⟩
+    toList ys List.ʳ++ (toList xs List.ʳ++ toList zs)   ≡⟨ cong (toList ys List.ʳ++_) (toList-ʳ++ xs) ⟨
+    toList ys List.ʳ++ toList (xs ʳ++ zs)               ≡⟨ toList-ʳ++ ys ⟨
+    toList (ys ʳ++ (xs ʳ++ zs))                         ∎
+    where open ≡-Reasoning
 
 ʳ++-ʳ++-eqFree : ∀ (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → let eq = m+n+o≡n+[m+o] m n o in
                  cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
-ʳ++-ʳ++-eqFree {m = m} {n} {o} xs {ys} {zs} = begin
-  (xs ʳ++ ys) ʳ++ zs                         ≂⟨ cong (_ʳ++ zs) (unfold-ʳ++ xs ys) ⟩
-  (reverse xs ++ ys) ʳ++ zs                  ≂⟨ unfold-ʳ++ (reverse xs ++ ys) zs ⟩
-  reverse (reverse xs ++ ys) ++ zs           ≈⟨ ≈-cong′ (_++ zs) (reverse-++-eqFree (reverse xs) ys) ⟩
-  (reverse ys ++ reverse (reverse xs)) ++ zs ≂⟨ cong ((_++ zs) ∘ (reverse ys ++_)) (reverse-involutive xs) ⟩
-  (reverse ys ++ xs) ++ zs                   ≈⟨ ++-assoc-eqFree (reverse ys) xs zs ⟩
-  reverse ys ++ (xs ++ zs)                   ≂⟨ unfold-ʳ++ ys (xs ++ zs) ⟨
-  ys ʳ++ (xs ++ zs)                          ∎
-  where open CastReasoning
+ʳ++-ʳ++-eqFree {m = m} {n} {o} xs {ys} {zs} =
+  toList-injective (m+n+o≡n+[m+o] m n o) ((xs ʳ++ ys) ʳ++ zs) (ys ʳ++ (xs ++ zs)) $
+  begin
+    toList ((xs ʳ++ ys) ʳ++ zs)                       ≡⟨ toList-ʳ++ (xs ʳ++ ys) ⟩
+    toList (xs ʳ++ ys) List.ʳ++ toList zs             ≡⟨ cong (List._ʳ++ toList zs) (toList-ʳ++ xs) ⟩
+    (toList xs List.ʳ++ toList ys) List.ʳ++ toList zs ≡⟨ List.ʳ++-ʳ++ (toList xs) ⟩
+    toList ys List.ʳ++ (toList xs List.++ toList zs)  ≡⟨ cong (toList ys List.ʳ++_) (toList-++ xs zs) ⟨
+    toList ys List.ʳ++ (toList (xs ++ zs))            ≡⟨ toList-ʳ++ ys ⟨
+    toList (ys ʳ++ (xs ++ zs))                        ∎
+  where open ≡-Reasoning
 
 ------------------------------------------------------------------------
--- sum
+--sum
 
 sum-++ : ∀ (xs : Vec ℕ m) → sum (xs ++ ys) ≡ sum xs + sum ys
 sum-++ {_}       []       = refl
 sum-++ {ys = ys} (x ∷ xs) = begin
-  x + sum (xs ++ ys)     ≡⟨  cong (x +_) (sum-++ xs) ⟩
+  x + sum (xs ++ ys)     ≡⟨ cong (x +_) (sum-++ xs) ⟩
   x + (sum xs + sum ys)  ≡⟨ +-assoc x (sum xs) (sum ys) ⟨
   sum (x ∷ xs) + sum ys  ∎
   where open ≡-Reasoning
@@ -1293,6 +1321,10 @@ toList∘fromList : (xs : List A) → toList (fromList xs) ≡ xs
 toList∘fromList List.[]       = refl
 toList∘fromList (x List.∷ xs) = cong (x List.∷_) (toList∘fromList xs)
 
+fromList∘toList : ∀  (xs : Vec A n) → fromList (toList xs) ≈[ length-toList xs ] xs
+fromList∘toList [] = refl
+fromList∘toList (x ∷ xs) = cong (x ∷_) (fromList∘toList xs)
+
 toList-cast : ∀ .(eq : m ≡ n) (xs : Vec A m) → toList (cast eq xs) ≡ toList xs
 toList-cast {n = zero}  eq []       = refl
 toList-cast {n = suc _} eq (x ∷ xs) =
@@ -1318,33 +1350,42 @@ fromList-++ : ∀ (xs : List A) {ys : List A} →
 fromList-++ List.[]       {ys} = cast-is-id refl (fromList ys)
 fromList-++ (x List.∷ xs) {ys} = cong (x ∷_) (fromList-++ xs)
 
-fromList-reverse : (xs : List A) → cast (List.length-reverse xs) (fromList (List.reverse xs)) ≡ reverse (fromList xs)
-fromList-reverse List.[] = refl
-fromList-reverse (x List.∷ xs) = begin
-  fromList (List.reverse (x List.∷ xs))         ≈⟨ cast-fromList (List.ʳ++-defn xs) ⟩
-  fromList (List.reverse xs List.++ List.[ x ]) ≈⟨ fromList-++ (List.reverse xs) ⟩
-  fromList (List.reverse xs) ++ [ x ]           ≈⟨ unfold-∷ʳ-eqFree x (fromList (List.reverse xs)) ⟨
-  fromList (List.reverse xs) ∷ʳ x               ≈⟨ ≈-cong′ (_∷ʳ x) (fromList-reverse xs) ⟩
-  reverse (fromList xs) ∷ʳ x                    ≂⟨ reverse-∷ x (fromList xs) ⟨
-  reverse (x ∷ fromList xs)                     ≈⟨⟩
-  reverse (fromList (x List.∷ xs))              ∎
-  where open CastReasoning
+fromList-reverse : (xs : List A) →
+                  (fromList (List.reverse xs)) ≈[ List.length-reverse xs ] reverse (fromList xs)
+fromList-reverse xs =
+  toList-injective (List.length-reverse xs) (fromList (List.reverse xs)) (reverse (fromList xs)) $
+  begin
+    toList (fromList (List.reverse xs)) ≡⟨ toList∘fromList (List.reverse xs) ⟩
+    List.reverse xs                     ≡⟨ cong (λ x → List.reverse x) (toList∘fromList xs) ⟨
+    List.reverse (toList (fromList xs)) ≡⟨ toList-reverse (fromList xs) ⟨
+    toList (reverse (fromList xs))      ∎
+    where open ≡-Reasoning
+
 
 ------------------------------------------------------------------------
--- TRANSITION TO EQ-FREE LEMMA
+-- DEPRECATED NAMES
 ------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.3
+
+∷-ʳ++-eqFree : ∀ a (xs : Vec A m) {ys : Vec A n} → let eq = sym (+-suc m n) in
+               cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
+∷-ʳ++-eqFree a xs {ys} = ʳ++-ʳ++-eqFree (a ∷ []) {ys = xs} {zs = ys}
+{-# WARNING_ON_USAGE ∷-ʳ++-eqFree
+"Warning: ∷-ʳ++-eqFree was deprecated in v2.3.
+Please use ʳ++-ʳ++-eqFree instead, which does not take eq."
+#-}
+
+-- Version 2.2
+
+-- TRANSITION TO EQ-FREE LEMMA
+--
 -- Please use the new proofs, which do not require an `eq` parameter.
 -- In v3, `name` will be changed to be the same lemma as `name-eqFree`,
 -- and `name-eqFree` will be deprecated.
 
-++-assoc : ∀ .(eq : (m + n) + o ≡ m + (n + o)) (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) →
-           cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)
-++-assoc _ = ++-assoc-eqFree
-{-# WARNING_ON_USAGE ++-assoc
-"Warning: ++-assoc was deprecated in v2.2.
-Please use ++-assoc-eqFree instead, which does not take eq."
-#-}
-
 ++-identityʳ : ∀ .(eq : n + zero ≡ n) (xs : Vec A n) → cast eq (xs ++ []) ≡ xs
 ++-identityʳ _ = ++-identityʳ-eqFree
 {-# WARNING_ON_USAGE ++-identityʳ
@@ -1385,7 +1426,8 @@ Please use reverse-++-eqFree instead, which does not take eq."
 
 ∷-ʳ++ : ∀ .(eq : (suc m) + n ≡ m + suc n) a (xs : Vec A m) {ys} →
         cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
-∷-ʳ++ _ = ∷-ʳ++-eqFree
+∷-ʳ++ _ a xs {ys} = ʳ++-ʳ++-eqFree (a ∷ []) {ys = xs} {zs = ys}
+
 {-# WARNING_ON_USAGE ∷-ʳ++
 "Warning: ∷-ʳ++ was deprecated in v2.2.
 Please use ∷-ʳ++-eqFree instead, which does not take eq."
@@ -1407,11 +1449,13 @@ Please use ++-ʳ++-eqFree instead, which does not take eq."
 Please use ʳ++-ʳ++-eqFree instead, which does not take eq."
 #-}
 
-------------------------------------------------------------------------
--- DEPRECATED NAMES
-------------------------------------------------------------------------
--- Please use the new names as continuing support for the old names is
--- not guaranteed.
+++-assoc : ∀ .(eq : (m + n) + o ≡ m + (n + o)) (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) →
+           cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)
+++-assoc _ = ++-assoc-eqFree
+{-# WARNING_ON_USAGE ++-assoc
+"Warning: ++-assoc was deprecated in v2.2.
+Please use ++-assoc-eqFree instead, which does not take eq."
+#-}
 
 -- Version 2.0