Merge pull request #884 from mattpolzin/list-reverse-involutory

Add proof that list reverse is involutive into base.

libs/base/Data/List.idr

@@ -670,6 +670,14 @@ revAppend (v :: vs) ns
             rewrite appendAssociative (reverse ns) (reverse vs) [v] in
               Refl
 
+||| List reverse applied twice yields the identity function.
+export
+reverseInvolutive : (xs : List a) -> reverse (reverse xs) = xs
+reverseInvolutive [] = Refl
+reverseInvolutive (x :: xs) = rewrite revOnto [x] xs in
+                                rewrite sym (revAppend (reverse xs) [x]) in
+                                  cong (x ::) $ reverseInvolutive xs
+
 export
 dropFusion : (n, m : Nat) -> (l : List t) -> drop n (drop m l) = drop (n+m) l
 dropFusion  Z     m    l      = Refl

libs/contrib/Data/List/Palindrome.idr

@@ -22,8 +22,8 @@ palindromeReverse : (xs : List a) -> Palindrome xs -> reverse xs = xs
 palindromeReverse [] Empty = Refl
 palindromeReverse [_] Single = Refl
 palindromeReverse ([x] ++ ys ++ [x]) (Multi pf) =
-  rewrite reverseAppend ([x] ++ ys) [x] in
-    rewrite reverseAppend [x] ys in
+  rewrite sym $ revAppend ([x] ++ ys) [x] in
+    rewrite sym $ revAppend [x] ys in
       rewrite palindromeReverse ys pf in
         Refl
 
@@ -38,7 +38,7 @@ reversePalindromeEqualsLemma x x' xs prf = equateInnerAndOuter flipHeadX
     flipHeadX : reverse (xs ++ [x']) ++ [x] = x :: (xs ++ [x'])
     flipHeadX = rewrite (sym (reverseCons x (xs ++ [x']))) in prf
     flipLastX' : reverse (xs ++ [x']) = x :: xs -> (x' :: reverse xs) = (x :: xs)
-    flipLastX' prf = rewrite (sym $ reverseAppend xs [x']) in prf
+    flipLastX' prf = rewrite (revAppend xs [x']) in prf
     cancelOuter : (reverse (xs ++ [x'])) = x :: xs -> reverse xs = xs
     cancelOuter prf = snd (consInjective (flipLastX' prf))
     equateInnerAndOuter

libs/contrib/Data/List/Reverse.idr

@@ -5,6 +5,10 @@ import Data.Nat
 import Data.List
 import Data.List.Equalities
 
+-- Additional properties coming out of base's Data.List
+--  - revAppend (i.e. reverse xs ++ reverse ys = reverse (ys ++ xs)
+--  - reverseInvolutive (i.e. reverse (reverse xs) = xs)
+
 %default total
 
 export
@@ -30,17 +34,6 @@ export
 reverseCons : (x : a) -> (xs : List a) -> reverse (x::xs) = reverse xs `snoc` x
 reverseCons x xs = reverseOntoSpec [x] xs
 
-||| Reversing an append is appending reversals backwards.
-export
-reverseAppend : (xs, ys : List a) ->
-  reverse (xs ++ ys) = reverse ys ++ reverse xs
-reverseAppend [] ys = sym (appendNilRightNeutral (reverse ys))
-reverseAppend (x :: xs) ys =
-  rewrite reverseCons x (xs ++ ys) in
-    rewrite reverseAppend xs ys in
-      rewrite reverseCons x xs in
-        sym $ appendAssociative (reverse ys) (reverse xs) [x]
-
 ||| A slow recursive definition of reverse.
 public export
 0 slowReverse : List a -> List a
@@ -53,7 +46,7 @@ reverseEquiv : (xs : List a) -> slowReverse xs = reverse xs
 reverseEquiv [] = Refl
 reverseEquiv (x :: xs) =
   rewrite reverseEquiv xs in
-    rewrite reverseAppend [x] xs in
+    rewrite revAppend [x] xs in
       Refl
 
 ||| Reversing a singleton list is a no-op.
@@ -61,16 +54,6 @@ export
 reverseSingletonId : (x : a) -> reverse [x] = [x]
 reverseSingletonId _ = Refl
 
-||| Reversing a reverse gives the original.
-export
-reverseReverseId : (xs : List a) -> reverse (reverse xs) = xs
-reverseReverseId [] = Refl
-reverseReverseId (x :: xs) =
-  rewrite reverseCons x xs in
-    rewrite reverseAppend (reverse xs) [x] in
-      rewrite reverseReverseId xs in
-        Refl
-
 ||| Reversing onto preserves list length.
 export
 reverseOntoLength : (xs, acc : List a) ->
@@ -89,6 +72,6 @@ reverseLength xs = reverseOntoLength xs []
 export
 reverseEqual : (xs, ys : List a) -> reverse xs = reverse ys -> xs = ys
 reverseEqual xs ys prf =
-  rewrite sym $ reverseReverseId xs in
+  rewrite sym $ reverseInvolutive xs in
     rewrite prf in
-      reverseReverseId ys
+      reverseInvolutive ys