use it in proofs

Author: mildsunrise

doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda

@@ -20,6 +20,7 @@ open import Data.Nat.Properties
 open import Data.Vec.Base
 open import Data.Vec.Properties
 open import Data.Vec.Relation.Binary.Equality.Cast
+open import Function using (_∘_)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; sym; cong; module ≡-Reasoning)
 
@@ -187,7 +188,7 @@ example3a-fromList-++-++ {xs = xs} {ys} {zs} eq = begin
   fromList (xs List.++ ys List.++ zs)
     ≈⟨ fromList-++ xs ⟩
   fromList xs ++ fromList (ys List.++ zs)
-    ≈⟨ ≈-cong (fromList xs ++_) (cast-++ʳ (List.length-++ ys) (fromList xs)) (fromList-++ ys) ⟩
+    ≈⟨ ≈-cong′ (fromList xs ++_) (fromList-++ ys) ⟩
   fromList xs ++ fromList ys ++ fromList zs
     ∎
   where open CastReasoning
@@ -218,9 +219,7 @@ example4-cong² : ∀ .(eq : (m + 1) + n ≡ n + suc m) a (xs : Vec A m) ys →
           cast eq (reverse ((xs ++ [ a ]) ++ ys)) ≡ ys ʳ++ reverse (xs ∷ʳ a)
 example4-cong² {m = m} {n} eq a xs ys = begin
   reverse ((xs ++ [ a ]) ++ ys)
-    ≈⟨ ≈-cong reverse (cast-reverse (cong (_+ n) (+-comm 1 m)) ((xs ∷ʳ a) ++ ys))
-                                             (≈-cong (_++ ys) (cast-++ˡ (+-comm 1 m) (xs ∷ʳ a))
-                                                     (unfold-∷ʳ _ a xs)) ⟨
+    ≈⟨ ≈-cong′ (reverse ∘ (_++ ys)) (unfold-∷ʳ (+-comm 1 m) a xs) ⟨
   reverse ((xs ∷ʳ a) ++ ys)
     ≈⟨ reverse-++ (+-comm (suc m) n) (xs ∷ʳ a) ys ⟩
   reverse ys ++ reverse (xs ∷ʳ a)
@@ -264,7 +263,7 @@ example6a-reverse-∷ʳ {n = n} x xs = begin-≡
   reverse (xs ∷ʳ x)
     ≡⟨ ≈-reflexive refl ⟨
   reverse (xs ∷ʳ x)
-    ≈⟨ ≈-cong reverse (cast-reverse _ _) (unfold-∷ʳ (+-comm 1 n) x xs) ⟩
+    ≈⟨ ≈-cong′ reverse (unfold-∷ʳ (+-comm 1 n) x xs) ⟩
   reverse (xs ++ [ x ])
     ≈⟨ reverse-++ (+-comm n 1) xs [ x ] ⟩
   x ∷ reverse xs

src/Data/Vec/Properties.agda

@@ -1016,8 +1016,7 @@ reverse-++ : ∀ .(eq : m + n ≡ n + m) (xs : Vec A m) (ys : Vec A n) →
 reverse-++ {m = zero}  {n = n} eq []       ys = ≈-sym (++-identityʳ (sym eq) (reverse ys))
 reverse-++ {m = suc m} {n = n} eq (x ∷ xs) ys = begin
   reverse (x ∷ xs ++ ys)              ≂⟨ reverse-∷ x (xs ++ ys) ⟩
-  reverse (xs ++ ys) ∷ʳ x             ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (+-comm m n)) x (reverse (xs ++ ys)))
-                                                (reverse-++ _ xs ys) ⟩
+  reverse (xs ++ ys) ∷ʳ x             ≈⟨ ≈-cong′ (_∷ʳ x) (reverse-++ (+-comm m n) xs ys) ⟩
   (reverse ys ++ reverse xs) ∷ʳ x     ≈⟨ ++-∷ʳ (sym (+-suc n m)) x (reverse ys) (reverse xs) ⟩
   reverse ys ++ (reverse xs ∷ʳ x)     ≂⟨ cong (reverse ys ++_) (reverse-∷ x xs) ⟨
   reverse ys ++ (reverse (x ∷ xs))    ∎
@@ -1068,8 +1067,7 @@ map-ʳ++ {ys = ys} f xs = begin
          cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
 ++-ʳ++ {m = m} {n} {o} eq xs {ys} {zs} = begin
   ((xs ++ ys) ʳ++ zs)              ≂⟨ unfold-ʳ++ (xs ++ ys) zs ⟩
-  reverse (xs ++ ys) ++ zs         ≈⟨ ≈-cong (_++ zs) (cast-++ˡ (+-comm m n) (reverse (xs ++ ys)))
-                                             (reverse-++ (+-comm m n) xs ys) ⟩
+  reverse (xs ++ ys) ++ zs         ≈⟨ ≈-cong′ (_++ zs) (reverse-++ (+-comm m n) xs ys) ⟩
   (reverse ys ++ reverse xs) ++ zs ≈⟨ ++-assoc (trans (cong (_+ o) (+-comm n m)) eq) (reverse ys) (reverse xs) zs ⟩
   reverse ys ++ (reverse xs ++ zs) ≂⟨ cong (reverse ys ++_) (unfold-ʳ++ xs zs) ⟨
   reverse ys ++ (xs ʳ++ zs)        ≂⟨ unfold-ʳ++ ys (xs ʳ++ zs) ⟨
@@ -1081,8 +1079,7 @@ map-ʳ++ {ys = ys} f xs = begin
 ʳ++-ʳ++ {m = m} {n} {o} eq 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) (cast-++ˡ (+-comm m n) (reverse (reverse xs ++ ys)))
-                                                       (reverse-++ (+-comm m n) (reverse xs) ys) ⟩
+  reverse (reverse xs ++ ys) ++ zs           ≈⟨ ≈-cong′ (_++ zs) (reverse-++ (+-comm m n) (reverse xs) ys) ⟩
   (reverse ys ++ reverse (reverse xs)) ++ zs ≂⟨ cong ((_++ zs) ∘ (reverse ys ++_)) (reverse-involutive xs) ⟩
   (reverse ys ++ xs) ++ zs                   ≈⟨ ++-assoc (+-assoc n m o) (reverse ys) xs zs ⟩
   reverse ys ++ (xs ++ zs)                   ≂⟨ unfold-ʳ++ ys (xs ++ zs) ⟨
@@ -1312,8 +1309,7 @@ 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-∷ʳ (+-comm 1 _) x (fromList (List.reverse xs)) ⟨
-  fromList (List.reverse xs) ∷ʳ x               ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (List.length-reverse xs)) _ _)
-                                                          (fromList-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))              ∎