gistfile1.hs

total
fold_length : List a -> Nat
fold_length = foldl (\n, _ => S n) Z

total
foldr_reduce : (n : Nat) -> (xs : List a) ->
               let f : (Nat -> a -> Nat) = (\n, _ => S n) in
                   S (foldr (flip (.) . flip f) id xs n) = foldr (flip (.) . flip f) id xs (S n)
foldr_reduce n Nil = refl
foldr_reduce n (x :: xs) = let ih = foldr_reduce (S n) xs in
                               rewrite sym ih in
                                       refl

total
fold_length_correct : (l : List a) -> fold_length l = length l
fold_length_correct Nil       = refl
fold_length_correct (x :: xs) = let ih = fold_length_correct xs in
                                    rewrite sym ih in
                                            rewrite foldr_reduce Z xs in
                                                    refl