[ re #432 ] Setoid version of Sublist type and properties

src/Data/List/Base.agda

@@ -14,7 +14,9 @@ open import Data.Bool.Base
 open import Data.Maybe.Base using (Maybe; nothing; just)
 open import Data.Product as Prod using (_×_; _,_)
 open import Data.These using (These; this; that; these)
+open import Function using (id; _∘_; _∘′_; flip)
 open import Function using (id; _∘_ ; _∘′_)
+
 open import Relation.Nullary using (yes; no)
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Unary.Properties using (∁?)
@@ -286,8 +288,13 @@ break P? = span (∁? P?)
 ------------------------------------------------------------------------
 -- Operations for reversing lists
 
-reverse : ∀ {a} {A : Set a} → List A → List A
-reverse = foldl (λ rev x → x ∷ rev) []
+module _ {a} {A : Set a} where
+
+  reverseAcc : List A → List A → List A
+  reverseAcc = foldl (flip _∷_)
+
+  reverse : List A → List A
+  reverse = reverseAcc []
 
 -- Snoc.
 

src/Data/List/Properties.agda

@@ -637,17 +637,17 @@ module _ {a p} {A : Set a} {P : A → Set p} (P? : Decidable P) where
 
 module _ {a} {A : Set a} where
 
-  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        ∎
+  unfold-reverseAcc : (acc xs : List A) → reverseAcc acc xs ≡ reverse xs ++ acc
+  unfold-reverse    : ∀ (x : A) xs → reverse (x ∷ xs) ≡ reverse xs ∷ʳ x
+
+  unfold-reverse x xs = unfold-reverseAcc [ x ] xs
+
+  unfold-reverseAcc xs []       = refl
+  unfold-reverseAcc xs (y ∷ ys) = begin
+    foldl (flip _∷_) (y ∷ xs) ys  ≡⟨ unfold-reverseAcc (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        ∎ where open P.≡-Reasoning
 
   reverse-++-commute : (xs ys : List A) →
                        reverse (xs ++ ys) ≡ reverse ys ++ reverse xs

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

@@ -55,4 +55,5 @@ open PW public using
   ; tabulate⁻
   ; ++⁺
   ; concat⁺
+  ; reverse⁺
   )

src/Data/List/Relation/Pointwise.agda

@@ -10,6 +10,7 @@ open import Function
 open import Function.Inverse using (Inverse)
 open import Data.Product hiding (map)
 open import Data.List.Base hiding (map ; head ; tail)
+open import Data.List.Properties using (unfold-reverse)
 open import Data.Fin using (Fin) renaming (zero to fzero; suc to fsuc)
 open import Data.Nat using (ℕ; zero; suc)
 open import Level
@@ -205,6 +206,21 @@ module _ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} where
   concat⁺ []                = []
   concat⁺ (xs∼ys ∷ xss∼yss) = ++⁺ xs∼ys (concat⁺ xss∼yss)
 
+
+------------------------------------------------------------------------
+-- reverse
+
+module _ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} where
+
+  reverseAcc⁺ : ∀ {xs ys us vs} → Pointwise _∼_ us vs → Pointwise _∼_ xs ys →
+                Pointwise _∼_ (reverseAcc us xs) (reverseAcc vs ys)
+  reverseAcc⁺ acc []            = acc
+  reverseAcc⁺ acc (x∼y ∷ xs∼ys) = reverseAcc⁺ (x∼y ∷ acc) xs∼ys
+
+  reverse⁺ : ∀ {xs ys} → Pointwise _∼_ xs ys →
+             Pointwise _∼_ (reverse xs) (reverse ys)
+  reverse⁺ = reverseAcc⁺ []
+
 ------------------------------------------------------------------------
 -- length