add comments to Lists.newt

playground/samples/Lists.newt

@@ -3,68 +3,88 @@ module Lists
 -- From the "Lists" chapter of Programming Language Foundations in Agda
 -- https://plfa.github.io/Lists/
 
+-- We define a few types and functions on lists and prove a couple of properties
+-- about them
+
+-- Natural numbers are zero (Z) or the successor (S) of a natural number
+-- We'll use these to represent the length of lists
 data Nat : U where
     Z : Nat
     S : Nat -> Nat
 
+-- declare a plus operator and define the corresponding function
 infixl 7 _+_
 _+_ : Nat -> Nat -> Nat
 Z + m = m
 S n + m = S (n + m)
 
+-- A list is empty (Nil) or a value followed by a list (separated by the :: operator)
 infixr 3 _::_
 data List : U -> U where
     Nil : {A : U} -> List A
     _::_ : {A : U} -> A -> List A -> List A
 
+-- length of a list is defined inductively
 length : {A : U} -> List A -> Nat
 length Nil = Z
 length (x :: xs) = S (length xs)
 
+-- List concatenation
 infixl 2 _++_
-
 _++_ : {A : U} -> List A -> List A -> List A
 Nil ++ ys = ys
 x :: xs ++ ys = x :: (xs ++ ys)
 
+-- Equality type is the ≡ operator
+-- The only constructor is Refl which says a ≡ a
+-- Magic happens in the compiler when it tries to make the types
+-- fit into this.
 infixl 1 _≡_
 data _≡_ : {A : U} -> A -> A -> U where
     Refl : {A : U} {a : A} -> a ≡ a
 
+-- If a ≡ b then b ≡ a
 sym : {A : U} {a b : A} -> a ≡ b -> b ≡ a
 sym Refl = Refl
 
+-- if a ≡ b and b ≡ c then a ≡ c
 trans : {A : U} {a b c : A} -> a ≡ b -> b ≡ c -> a ≡ c
 trans Refl x = x
 
+-- This lets us replace a with b inside an expression if a ≡ b
 replace : {A : U} {a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b
 replace p Refl x = x
 
+-- if a ≡ b then f a ≡ f b
 cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
 
+-- if concatenate two lists, the length is the sum of the lengths
+-- of the original lists
 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
+-- a function to reverse a list
-reverse : {A : U} -> (xs : List A) -> List A
+reverse : {A : U} -> List A -> List A
 reverse Nil = Nil
 reverse (x :: xs) = reverse xs ++ (x :: Nil)
 
+-- if we add an empty list to a list, we get the original back
 ++-identity : {A : U} -> (xs : List A) -> xs ++ Nil ≡ xs
 ++-identity Nil = Refl
 ++-identity (x :: xs) = cong (_::_ x) (++-identity xs)
 
+-- concatenation is associative
 ++-associative : {A : U} (xs ys zs : List A) -> xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
 
--- TODO port equational reasoning
+-- reverse distributes over ++, but switches order
 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
+-- same thing, but using `replace` in the proof
 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 =
@@ -72,24 +92,29 @@ reverse-++-distrib' {A} (x :: xs) ys =
           (sym (++-associative (reverse ys) (reverse xs) (x :: Nil)))
           (replace (\ z => (reverse (xs ++ ys)) ++ (x :: Nil) ≡ z ++ (x :: Nil)) (reverse-++-distrib' xs ys) Refl)
 
+-- reverse of reverse gives you the original list
 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))
 
+-- helper for a different version of reverse
 shunt : {A : U} -> List A -> List A -> List A
 shunt Nil ys = ys
 shunt (x :: xs) ys = shunt xs (x :: ys)
 
+-- lemma
 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)
 
+-- an alternative definition of reverse
 reverse' : {A : U} -> List A -> List A
 reverse' xs = shunt xs Nil
 
+-- proof that the reverse and reverse' give the same results
 reverses : {A : U} → (xs : List A) → reverse' xs ≡ reverse xs
 reverses xs = trans (shunt-reverse xs Nil) (++-identity _)