Fill in a little more of the PLFA Lists example

playground/samples/Lists.newt

@@ -0,0 +1,92 @@
+module Concat
+
+data Nat : U where
+    Z : Nat
+    S : Nat -> Nat
+
+infixl 7 _+_
+_+_ : Nat -> Nat -> Nat
+Z + m = m
+S n + m = S (n + m)
+
+infixr 3 _::_
+data List : U -> U where
+    Nil : {A : U} -> List A
+    _::_ : {A : U} -> A -> List A -> List A
+
+length : {A : U} -> List A -> Nat
+length Nil = Z
+length (x :: xs) = S (length xs)
+
+infixl 2 _++_
+
+_++_ : {A : U} -> List A -> List A -> List A
+Nil ++ ys = ys
+x :: xs ++ ys = x :: (xs ++ ys)
+
+infixl 1 _≡_
+data _≡_ : {A : U} -> A -> A -> U where
+    Refl : {A : U} {a : A} -> a ≡ a
+
+sym : {A : U} {a b : A} -> a ≡ b -> b ≡ a
+sym Refl = Refl
+
+trans : {A : U} {a b c : A} -> a ≡ b -> b ≡ c -> a ≡ c
+trans Refl x = x
+
+replace : {A : U} {a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b
+replace p Refl x = x
+
+cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
+
+length-++ : {A : U} (xs ys : List A) -> length (xs ++ ys) ≡ length xs + length ys
+length-++ Nil ys = Refl
+length-++ (x :: xs) ys = cong S (length-++ xs ys)
+
+-- PLFA definition
+reverse : {A : U} -> (xs : List A) -> List A
+reverse Nil = Nil
+reverse (x :: xs) = reverse xs ++ (x :: Nil)
+
+++-identity : {A : U} -> (xs : List A) -> xs ++ Nil ≡ xs
+++-identity Nil = Refl
+++-identity (x :: xs) = cong (_::_ x) (++-identity xs)
+
+++-associative : {A : U} (xs ys zs : List A) -> xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
+
+-- TODO port equational reasoning
+reverse-++-distrib : {A : U} -> (xs ys : List A) -> reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
+reverse-++-distrib Nil ys = sym (++-identity (reverse ys))
+reverse-++-distrib (x :: xs) ys =
+  trans (cong (\ z => z ++ (x :: Nil)) (reverse-++-distrib xs ys))
+        (sym (++-associative (reverse ys) (reverse xs) (x :: Nil)))
+
+-- rewrite version
+reverse-++-distrib' : {A : U} -> (xs ys : List A) -> reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
+reverse-++-distrib' Nil ys = sym (++-identity (reverse ys))
+reverse-++-distrib' {A} (x :: xs) ys =
+  replace (\ z => (reverse (xs ++ ys) ++ (x :: Nil)) ≡ z)
+          (sym (++-associative (reverse ys) (reverse xs) (x :: Nil)))
+          (replace (\ z => (reverse (xs ++ ys)) ++ (x :: Nil) ≡ z ++ (x :: Nil)) (reverse-++-distrib' xs ys) Refl)
+
+reverse-involutive : {A : U} -> (xs : List A) -> reverse (reverse xs) ≡ xs
+reverse-involutive Nil = Refl
+reverse-involutive (x :: xs) =
+  trans (reverse-++-distrib (reverse xs) (x :: Nil))
+        (cong (_::_ x) (reverse-involutive xs))
+
+shunt : {A : U} -> List A -> List A -> List A
+shunt Nil ys = ys
+shunt (x :: xs) ys = shunt xs (x :: ys)
+
+shunt-reverse : {A : U} (xs ys : List A) -> shunt xs ys ≡ reverse xs ++ ys
+shunt-reverse Nil ys = Refl
+shunt-reverse (x :: xs) ys =
+  trans (shunt-reverse xs (x :: ys))
+        (++-associative (reverse xs) (x :: Nil) ys)
+
+reverse' : {A : U} -> List A -> List A
+reverse' xs = shunt xs Nil
+
+reverses : {A : U} → (xs : List A) → reverse' xs ≡ reverse xs
+reverses xs = trans (shunt-reverse xs Nil) (++-identity _)