[ Data.List ] function reverse-append _ʳ++_, simplify proofs about reverse

CHANGELOG.md

@@ -193,6 +193,10 @@ Other minor additions
   *-suc : m * sucℤ n ≡ m + m * n
   ```
 
+* Added to `Data.List` the reverse-append function `_ʳ++_`
+  which is `reverseAcc` with the intuitive argument order.
+  Generalized the properties of `reverse` to `_ʳ++_`.
+
 * Added new definitions to `Data.List.Relation.Unary.All`:
   ```agda
   Null = All (λ _ → ⊥)

src/Data/List/Base.agda

@@ -314,6 +314,13 @@ reverseAcc = foldl (flip _∷_)
 reverse : List A → List A
 reverse = reverseAcc []
 
+-- "Reverse append" xs ʳ++ ys = reverse xs ++ ys
+
+infixr 5 _ʳ++_
+
+_ʳ++_ : List A → List A → List A
+_ʳ++_ = flip reverseAcc
+
 -- Snoc.
 
 infixl 5 _∷ʳ_

src/Data/List/Properties.agda

@@ -764,84 +764,152 @@ module _ {P : A → Set p} (P? : Decidable P) where
   ...  | no ¬Px = P.cong (Prod.map id (x ∷_)) (partition-defn xs)
 
 ------------------------------------------------------------------------
--- reverse
+-- reverse is an involution in the list monoid
 
 module _ {a} {A : Set a} where
 
   open FunctionProperties {A = List A} _≡_
+  open P.≡-Reasoning
 
-  unfold-reverse : ∀ (x : A) xs → reverse (x ∷ xs) ≡ reverse xs ∷ʳ x
-  unfold-reverse x xs = helper [ x ] xs
-    where
-    open P.≡-Reasoning
-    helper : (xs ys : List A) → foldl (flip _∷_) xs ys ≡ reverse ys ++ xs
-    helper xs []       = refl
-    helper xs (y ∷ ys) = begin
-      foldl (flip _∷_) (y ∷ xs) ys  ≡⟨ helper (y ∷ xs) ys ⟩
-      reverse ys ++ y ∷ xs          ≡⟨ P.sym (++-assoc (reverse ys) _ _) ⟩
-      (reverse ys ∷ʳ y) ++ xs       ≡⟨ P.sym $ P.cong (_++ xs) (unfold-reverse y ys) ⟩
-      reverse (y ∷ ys) ++ xs        ∎
+  -- Defining property of reverse-append _ʳ++_.
 
-  reverse-++-commute : (xs ys : List A) →
-                       reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
-  reverse-++-commute []       ys = P.sym (++-identityʳ _)
-  reverse-++-commute (x ∷ xs) ys = begin
-    reverse (x ∷ xs ++ ys)               ≡⟨ unfold-reverse x (xs ++ ys) ⟩
-    reverse (xs ++ ys) ++ [ x ]          ≡⟨ P.cong (_++ [ x ]) (reverse-++-commute xs ys) ⟩
-    (reverse ys ++ reverse xs) ++ [ x ]  ≡⟨ ++-assoc (reverse ys) _ _ ⟩
-    reverse ys ++ (reverse xs ++ [ x ])  ≡⟨ P.sym $ P.cong (reverse ys ++_) (unfold-reverse x xs) ⟩
-    reverse ys ++ reverse (x ∷ xs)       ∎
-    where open P.≡-Reasoning
+  ʳ++-defn : ∀ (xs : List A) {ys} → xs ʳ++ ys ≡ reverse xs ++ ys
+  ʳ++-defn [] = refl
+  ʳ++-defn (x ∷ xs) {ys} = begin
+    (x ∷ xs)             ʳ++ ys   ≡⟨⟩
+    xs         ʳ++   x     ∷ ys   ≡⟨⟩
+    xs         ʳ++ [ x ]  ++ ys   ≡⟨ ʳ++-defn xs  ⟩
+    reverse xs  ++ [ x ]  ++ ys   ≡⟨ P.sym (++-assoc (reverse xs) _ _) ⟩
+    (reverse xs ++ [ x ]) ++ ys   ≡⟨ P.cong (_++ ys) (P.sym (ʳ++-defn xs)) ⟩
+    (xs ʳ++ [ x ])        ++ ys   ≡⟨⟩
+    reverse (x ∷ xs)      ++ ys   ∎
 
-  reverse-involutive : Involutive reverse
-  reverse-involutive [] = refl
-  reverse-involutive (x ∷ xs) = begin
-    reverse (reverse (x ∷ xs))   ≡⟨ P.cong reverse $ unfold-reverse x xs ⟩
-    reverse (reverse xs ∷ʳ x)    ≡⟨ reverse-++-commute (reverse xs) ([ x ]) ⟩
-    x ∷ reverse (reverse (xs))   ≡⟨ P.cong (x ∷_) $ reverse-involutive xs ⟩
-    x ∷ xs                       ∎
-    where open P.≡-Reasoning
+  -- Corollary: reverse of cons is snoc of reverse.
 
-  length-reverse : (xs : List A) → length (reverse xs) ≡ length xs
-  length-reverse []       = refl
-  length-reverse (x ∷ xs) = begin
-    length (reverse (x ∷ xs))   ≡⟨ P.cong length $ unfold-reverse x xs ⟩
-    length (reverse xs ∷ʳ x)    ≡⟨ length-++ (reverse xs) ⟩
-    length (reverse xs) + 1     ≡⟨ P.cong (_+ 1) (length-reverse xs) ⟩
-    length xs + 1               ≡⟨ +-comm _ 1 ⟩
-    suc (length xs)             ∎
-    where open P.≡-Reasoning
+  unfold-reverse : ∀ (x : A) xs → reverse (x ∷ xs) ≡ reverse xs ∷ʳ x
+  unfold-reverse x xs = ʳ++-defn xs
 
-reverse-map-commute : (f : A → B) (xs : List A) →
-                      map f (reverse xs) ≡ reverse (map f xs)
-reverse-map-commute f []       = refl
-reverse-map-commute f (x ∷ xs) = begin
-  map f (reverse (x ∷ xs))   ≡⟨ P.cong (map f) $ unfold-reverse x xs ⟩
-  map f (reverse xs ∷ʳ x)    ≡⟨ map-++-commute f (reverse xs) ([ x ]) ⟩
-  map f (reverse xs) ∷ʳ f x  ≡⟨ P.cong (_∷ʳ f x) $ reverse-map-commute f xs ⟩
-  reverse (map f xs) ∷ʳ f x  ≡⟨ P.sym $ unfold-reverse (f x) (map f xs) ⟩
-  reverse (map f (x ∷ xs))   ∎
-  where open P.≡-Reasoning
+  -- Reverse-append of append is reverse-append after reverse-append.
+  -- Simple inductive proof.
 
-reverse-foldr : ∀ (f : A → B → B) x ys →
-                foldr f x (reverse ys) ≡ foldl (flip f) x ys
-reverse-foldr f x []       = refl
-reverse-foldr f x (y ∷ ys) = begin
-  foldr f x (reverse (y ∷ ys)) ≡⟨ P.cong (foldr f x) (unfold-reverse y ys) ⟩
-  foldr f x ((reverse ys) ∷ʳ y) ≡⟨ foldr-∷ʳ f x y (reverse ys) ⟩
-  foldr f (f y x) (reverse ys)  ≡⟨ reverse-foldr f (f y x) ys ⟩
-  foldl (flip f) (f y x) ys     ∎
-  where open P.≡-Reasoning
+  ʳ++-++ : ∀ (xs {ys zs} : List A) → (xs ++ ys) ʳ++ zs ≡ ys ʳ++ xs ʳ++ zs
+  ʳ++-++ [] = refl
+  ʳ++-++ (x ∷ xs) {ys} {zs} = begin
+    (x ∷ xs ++ ys) ʳ++ zs   ≡⟨⟩
+    (xs ++ ys) ʳ++ x ∷ zs   ≡⟨ ʳ++-++ xs ⟩
+    ys ʳ++ xs ʳ++ x ∷ zs    ≡⟨⟩
+    ys ʳ++ (x ∷ xs) ʳ++ zs  ∎
 
-reverse-foldl : ∀ (f : A → B → A) x ys →
-                foldl f x (reverse ys) ≡ foldr (flip f) x ys
-reverse-foldl f x []       = refl
-reverse-foldl f x (y ∷ ys) = begin
-  foldl f x (reverse (y ∷ ys)) ≡⟨ P.cong (foldl f x) (unfold-reverse y ys) ⟩
-  foldl f x ((reverse ys) ∷ʳ y) ≡⟨ foldl-∷ʳ f x y (reverse ys) ⟩
-  f (foldl f x (reverse ys)) y ≡⟨ P.cong (flip f y) (reverse-foldl f x ys) ⟩
-  f (foldr (flip f) x ys) y    ∎
-  where open P.≡-Reasoning
+  -- Corollary: reverse is an involution with respect to append.
+
+  reverse-++-commute : (xs ys : List A) →
+                       reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
+  reverse-++-commute xs ys = begin
+    reverse (xs ++ ys)         ≡⟨⟩
+    (xs ++ ys) ʳ++ []          ≡⟨ ʳ++-++ xs ⟩
+    ys ʳ++ xs ʳ++ []           ≡⟨⟩
+    ys ʳ++ reverse xs          ≡⟨ ʳ++-defn ys ⟩
+    reverse ys ++ reverse xs   ∎
+
+  -- Reverse-append of reverse-append is commuted reverse-append after append.
+  -- Simple inductive proof.
+
+  ʳ++-ʳ++ : ∀ (xs {ys zs} : List A) → (xs ʳ++ ys) ʳ++ zs ≡ ys ʳ++ xs ++ zs
+  ʳ++-ʳ++ [] = refl
+  ʳ++-ʳ++ (x ∷ xs) {ys} {zs} = begin
+    ((x ∷ xs) ʳ++ ys) ʳ++ zs   ≡⟨⟩
+    (xs ʳ++ x ∷ ys) ʳ++ zs     ≡⟨ ʳ++-ʳ++ xs ⟩
+    (x ∷ ys) ʳ++ xs ++ zs      ≡⟨⟩
+    ys ʳ++ (x ∷ xs) ++ zs      ∎
+
+  -- Corollary: reverse is involutive.
+
+  reverse-involutive : Involutive reverse
+  reverse-involutive xs = begin
+    reverse (reverse xs)  ≡⟨⟩
+    (xs ʳ++ []) ʳ++ []    ≡⟨ ʳ++-ʳ++ xs ⟩
+    [] ʳ++  xs ++ []      ≡⟨⟩
+    xs ++ []              ≡⟨ ++-identityʳ xs ⟩
+    xs                    ∎
+
+  -- length of reverse-append
+
+  length-ʳ++ : ∀ (xs {ys} : List A) → length (xs ʳ++ ys) ≡ length xs + length ys
+  length-ʳ++ [] = refl
+  length-ʳ++ (x ∷ xs) {ys} = begin
+    length ((x ∷ xs) ʳ++ ys)      ≡⟨⟩
+    length (xs ʳ++ x ∷ ys)        ≡⟨ length-ʳ++ xs ⟩
+    length xs + length (x ∷ ys)   ≡⟨ +-suc _ _ ⟩
+    length (x ∷ xs) + length ys   ∎
+
+  -- Corollary: reverse preserves the length.
+
+  length-reverse : length ∘ reverse ≗ length
+  length-reverse xs = begin
+    length (reverse xs)   ≡⟨⟩
+    length (xs ʳ++ [])    ≡⟨ length-ʳ++ xs ⟩
+    length xs + 0         ≡⟨ +-identityʳ _ ⟩
+    length xs             ∎
+
+  -- map distributes over reverse-append.
+
+  map-ʳ++ : (f : A → B) (xs {ys} : List A) →
+            map f (xs ʳ++ ys) ≡ map f xs ʳ++ map f ys
+  map-ʳ++ f []            = refl
+  map-ʳ++ f (x ∷ xs) {ys} = begin
+    map f ((x ∷ xs) ʳ++ ys)         ≡⟨⟩
+    map f (xs ʳ++ x ∷ ys)           ≡⟨ map-ʳ++ f xs ⟩
+    map f xs ʳ++ map f (x ∷ ys)     ≡⟨⟩
+    map f xs ʳ++ f x ∷ map f ys     ≡⟨⟩
+    (f x ∷ map f xs) ʳ++ map f ys   ≡⟨⟩
+    map f (x ∷ xs)   ʳ++ map f ys   ∎
+
+  -- Instance of map-ʳ++: map commutes with reverse.
+
+  reverse-map-commute : (f : A → B) → map f ∘ reverse ≗ reverse ∘ map f
+  reverse-map-commute f xs = begin
+    map f (reverse xs) ≡⟨⟩
+    map f (xs ʳ++ [])  ≡⟨ map-ʳ++ f xs ⟩
+    map f xs ʳ++ []    ≡⟨⟩
+    reverse (map f xs) ∎
+
+  -- A foldr after a reverse is a foldl.
+  -- Simple inductive proof.
+
+  foldr-ʳ++ : ∀ (f : A → B → B) b xs {ys} →
+              foldr f b (xs ʳ++ ys) ≡ foldl (flip f) (foldr f b ys) xs
+  foldr-ʳ++ f b [] = refl
+  foldr-ʳ++ f b (x ∷ xs) {ys} = begin
+    foldr f b ((x ∷ xs) ʳ++ ys)              ≡⟨⟩
+    foldr f b (xs ʳ++ x ∷ ys)                ≡⟨ foldr-ʳ++ f b xs ⟩
+    foldl (flip f) (foldr f b (x ∷ ys)) xs   ≡⟨⟩
+    foldl (flip f) (f x (foldr f b ys)) xs   ≡⟨⟩
+    foldl (flip f) (foldr f b ys) (x ∷ xs)   ∎
+
+  -- Instantiation to reverse.
+
+  reverse-foldr : ∀ (f : A → B → B) b →
+                  foldr f b ∘ reverse ≗ foldl (flip f) b
+  reverse-foldr f b xs = foldr-ʳ++ f b xs
+
+  -- A foldl after a reverse is a foldr.
+  -- Simple inductive proof.
+
+  foldl-ʳ++ : ∀ (f : B → A → B) b xs {ys} →
+              foldl f b (xs ʳ++ ys) ≡ foldl f (foldr (flip f) b xs) ys
+  foldl-ʳ++ f b [] = refl
+  foldl-ʳ++ f b (x ∷ xs) {ys} = begin
+    foldl f b ((x ∷ xs) ʳ++ ys)              ≡⟨⟩
+    foldl f b (xs ʳ++ x ∷ ys)                ≡⟨ foldl-ʳ++ f b xs ⟩
+    foldl f (foldr (flip f) b xs) (x ∷ ys)   ≡⟨⟩
+    foldl f (f (foldr (flip f) b xs) x) ys   ≡⟨⟩
+    foldl f (foldr (flip f) b (x ∷ xs)) ys   ∎
+
+  -- Instantiation to reverse.
+
+  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
 
 ------------------------------------------------------------------------
 -- _∷ʳ_

src/Data/List/Relation/Binary/Equality/Setoid.agda

@@ -121,7 +121,10 @@ module _ {P : Pred A p} (P? : U.Decidable P) (resp : P Respects _≈_)
   filter⁺ xs≋ys = PW.filter⁺ P? P? resp (resp ∘ sym) xs≋ys
 
 ------------------------------------------------------------------------
--- filter
+-- reverse
+
+ʳ++⁺ : ∀{xs xs′ ys ys′} → xs ≋ xs′ → ys ≋ ys′ → xs ʳ++ ys ≋ xs′ ʳ++ ys′
+ʳ++⁺ = PW.ʳ++⁺
 
 reverse⁺ : ∀ {xs ys} → xs ≋ ys → reverse xs ≋ reverse ys
 reverse⁺ = PW.reverse⁺

src/Data/List/Relation/Binary/Pointwise.agda

@@ -243,6 +243,12 @@ module _ {R : REL A B ℓ} where
   reverseAcc⁺ rs′ []       = rs′
   reverseAcc⁺ rs′ (r ∷ rs) = reverseAcc⁺ (r ∷ rs′) rs
 
+  ʳ++⁺ : ∀ {as bs as′ bs′} →
+           Pointwise R as bs →
+           Pointwise R as′ bs′ →
+           Pointwise R (as ʳ++ as′) (bs ʳ++ bs′)
+  ʳ++⁺ rs rs′ = reverseAcc⁺ rs′ rs
+
   reverse⁺ : ∀ {as bs} → Pointwise R as bs → Pointwise R (reverse as) (reverse bs)
   reverse⁺ = reverseAcc⁺ []
 

src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda

@@ -292,6 +292,12 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
   reverseAcc⁺ (y ∷ʳ abs) cds = reverseAcc⁺ abs (y ∷ʳ cds)
   reverseAcc⁺ (r ∷ abs)  cds = reverseAcc⁺ abs (r ∷ cds)
 
+  ʳ++⁺ : ∀ {as bs cs ds} →
+         Sublist R as bs →
+         Sublist R cs ds →
+         Sublist R (as ʳ++ cs) (bs ʳ++ ds)
+  ʳ++⁺ = reverseAcc⁺
+
   reverse⁺ : ∀ {as bs} → Sublist R as bs → Sublist R (reverse as) (reverse bs)
   reverse⁺ rs = reverseAcc⁺ rs []
 

src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda

@@ -195,6 +195,12 @@ module _ {as bs : List A} where
                 reverseAcc cs as ⊆ reverseAcc ds bs
   reverseAcc⁺ = HeteroProperties.reverseAcc⁺
 
+  ʳ++⁺ : ∀ {cs ds} →
+         as ⊆ bs →
+         cs ⊆ ds →
+         as ʳ++ cs ⊆ bs ʳ++ ds
+  ʳ++⁺ = reverseAcc⁺
+
   reverse⁺ : as ⊆ bs → reverse as ⊆ reverse bs
   reverse⁺ = HeteroProperties.reverse⁺
 

src/Data/List/Relation/Ternary/Interleaving/Properties.agda

@@ -38,14 +38,16 @@ module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
 -- _++_
 
   ++⁺ : ∀ {as₁ as₂ l₁ l₂ r₁ r₂} →
-        Interleaving L R as₁ l₁ r₁ → Interleaving L R as₂ l₂ r₂ →
+        Interleaving L R as₁ l₁ r₁ →
+        Interleaving L R as₂ l₂ r₂ →
         Interleaving L R (as₁ ++ as₂) (l₁ ++ l₂) (r₁ ++ r₂)
   ++⁺ []         sp₂ = sp₂
   ++⁺ (l ∷ˡ sp₁) sp₂ = l ∷ˡ (++⁺ sp₁ sp₂)
   ++⁺ (r ∷ʳ sp₁) sp₂ = r ∷ʳ (++⁺ sp₁ sp₂)
 
   ++-disjoint : ∀ {as₁ as₂ l₁ r₂} →
-                Interleaving L R l₁ [] as₁ → Interleaving L R [] r₂ as₂ →
+                Interleaving L R l₁ [] as₁ →
+                Interleaving L R [] r₂ as₂ →
                 Interleaving L R l₁ r₂ (as₁ ++ as₂)
   ++-disjoint []         sp₂ = sp₂
   ++-disjoint (l ∷ˡ sp₁) sp₂ = l ∷ˡ ++-disjoint sp₁ sp₂
@@ -91,6 +93,12 @@ module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
   reverseAcc⁺ sp₁ (l ∷ˡ sp₂) = reverseAcc⁺ (l ∷ˡ sp₁) sp₂
   reverseAcc⁺ sp₁ (r ∷ʳ sp₂) = reverseAcc⁺ (r ∷ʳ sp₁) sp₂
 
+  ʳ++⁺ : ∀ {as₁ as₂ l₁ l₂ r₁ r₂} →
+         Interleaving L R l₁ r₁ as₁ →
+         Interleaving L R l₂ r₂ as₂ →
+         Interleaving L R (l₁ ʳ++ l₂) (r₁ ʳ++ r₂) (as₁ ʳ++ as₂)
+  ʳ++⁺ sp₁ sp₂ = reverseAcc⁺ sp₂ sp₁
+
   reverse⁺ : ∀ {as l r} → Interleaving L R l r as →
              Interleaving L R (reverse l) (reverse r) (reverse as)
   reverse⁺ = reverseAcc⁺ []