Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Are constructive programs better?
import Data.List
import Data.List.Views
import Data.Vect
import Data.Vect.Views
%default total
-- Constructive
rotate : Vect len elem -> Vect len elem
rotate xs {len} with (snocVect xs)
rotate [] | Empty = []
rotate (ys ++ [y]) {len=m + S Z} | Snoc z = rewrite (plusCommutative m 1)
in [y] ++ ys
-- Proof Carrying
rotate' : (xs : List elem) -> (xs' : List elem ** length xs = length xs')
rotate' xs with (snocList xs)
rotate' [] | Empty = ([] ** Refl)
rotate' (ys ++ [y]) | Snoc z = ([y] ++ ys ** rewrite (lengthAppend ys [y]) in
rewrite (plusCommutative (length ys) 1) in
Refl)
-- Separate Proof
rotate'' : List elem -> List elem
rotate'' xs with (snocList xs)
rotate'' [] | Empty = []
rotate'' (ys ++ [y]) | Snoc z = [y] ++ ys
rotate''PreservesLength : (xs : List a) -> (length xs = length (rotate'' xs))
rotate''PreservesLength xs with (snocList xs)
rotate''PreservesLength [] | Empty = Refl
rotate''PreservesLength (ys ++ [y]) | Snoc z = rewrite (lengthAppend ys [y]) in
rewrite (plusCommutative (length ys) 1) in
Refl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.