module PreludeProps where
{-P: {- -}
property Univ = Gfp X. X
property Undef = Lfp X. X
property Absurdity = $Undef
assert Extensionality = All f . f ::: $Univ ==> {\x->f x} === f
assert undefined ::: Undef
property Finite = $ (Lfp P. ([] \/ Univ : $P))
property LeftUnit op e = All x . {e `op` x} === x
property RightUnit op e = All x. {x `op` e} === x
property Assoc op = All x, y, z. {(x `op` y) `op` z} === {x `op` (y `op` z)}
property Monoid op e = Assoc op /\ RightUnit op e /\ LeftUnit op e
property Strict = Undef -> Undef
--assert P1 /\ P1
assert P1 = All x, y. {const x y} === x
assert All f, x. {const x . f} === {const x}
assert All f, x. {f . const x} === {const (f x)}
assert sum === {foldr (+) 0}
assert {sum undefined} === undefined
assert {sum undefined} ::: Undef
assert {sum []} === 0
assert All x, xs. {sum (x:xs)} === {x + sum xs}
assert All xs, ys. {sum (xs ++ ys)} === {sum xs + sum ys}
assert {sum . map length} === {length . concat}
assert length === {sum . map (const 1)}
assert All xs, ys. {length (xs ++ ys)} === {length xs + length ys}
assert {length undefined} === {undefined}
assert {length []} === 0
assert All x, xs. {length (x:xs)} === {1 + length xs}
assert length === {foldl (\u us -> 1 + us) 0}
-- assert All xs. Finite xs ==> {length xs} =/= _|_
assert All xs. -/ Finite xs \/ -/ ({length xs} === {undefined})
assert All xs. -/ (Finite xs /\ {length xs} === {undefined})
assert All xs. -/ (Finite xs /\ {length xs} ::: Undef)
assert All xs. Finite xs ==> -/ {length xs} ::: Undef
assert All xs. {length xs} === 0 ==> xs === {[]}
assert All xs. -/ {length xs} === 0 \/ xs === {[]}
assert All xs. -/ {length xs} === 0 \/ xs ::: $[]
assert All f, xs. {length (map f xs)} === {length xs}
assert All xs. {length (reverse xs)} === {length xs}
assert All f, a. {foldl f a undefined} === undefined
assert All f, a. {foldl f a []} === a
assert All f, a, x, xs. {foldl f a (x:xs)} === {foldl f (f a x) xs}
-- assert All f, a. Monoid f a /\ (All x. {f x undefined} === undefined})
-- /\ (All y. {f undefined y} === undefomed) ===>
-- All xs. {foldr f a xs} === {foldl f a xs}
-- assert All f, a. Monoid f a /\ (All x. {f x undefined} === undefined})
-- /\ (All y. {f undefined y} === undefomed) ===>
-- All x, xs. {foldl f xs} === {f x (foldl f a xs)}
-- assert All p. {filter p} === {foldr q []
-- where q x us = if p x then x:us else us}
assert All p. {filter p} === {let q x us = if p x then x:us else us
in foldr q []}
assert All p. {filter p undefined} === undefined
assert All p. {filter p []} === {[]}
assert All p, xs, ys. {filter p (xs ++ ys)} ===
{filter p xs ++ filter p ys}
assert All p. {filter p . concat} === {concat . map (filter p)}
-- assert All p, x, xs. case {p x} of
-- undefined -> {filter p (x:xs)} === undefined
-- {True} -> {filter p (x:xs)} === {x : filter p xs}
-- {False} -> {filter p (x:xs) === {filter p xs}
-- assert All p, x, xs. {p x} ==> {filter p (x:xs)} ===
-- {x : filter p xs}
assert All p, x, xs. -/ ({p x} ::: $True)
\/ {filter p (x:xs)} === {x : filter p xs}
assert All p, x, xs. {p x} ::: $True ==>
{filter p (x:xs)} === {x : filter p xs}
assert All p, x, xs. ({p x} ::: False)
\/ {filter p (x:xs)} === {x : filter p xs}
assert All p, x, xs. -/ {p x} ::: $False
\/ {filter p (x:xs)} === {filter p xs}
assert All p, x, xs. {p x} ::: $False ==>
{filter p (x:xs)} === {filter p xs}
assert All p, x, xs. {p x} ::: True
\/ {filter p (x:xs)} === {filter p xs}
-- the above assertions use:
assert All x. (x ::: $True \/ x ::: False) /\ (x ::: True \/ x ::: $False)
rev ys [] = ys
rev ys (u:us) = rev (u:ys) us
assert All ys. {rev ys undefined} === undefined
assert All ys. {rev ys undefined} ::: Undef
assert All ys. {rev ys []} === ys
assert All x, xs, ys. {rev ys (x:xs)} === {rev (x:ys) xs}
assert All xs, ys. {rev ys xs} === {reverse (xs ++ ys)}
assert All xs. {reverse xs} === {rev [] xs}
assert {head undefined} === {undefined}
assert {head undefined} ::: Undef
assert {head []} === undefined
assert {head []} ::: Undef
assert All x, xs. {head (x:xs)} === x
assert {concat undefined} === undefined
assert {concat undefined} ::: Undef
assert {concat []} === {[]}
assert {concat []} ::: $[]
assert All xs, xss. {concat (xs:xss)} === {xs ++ concat xss}
assert concat === {foldr (++) []}
assert {concat . concat} === {concat . map concat}
assert All f, a. Monoid f a ==> {foldr f a . map (foldr f a)} === {foldr f a . concat}
assert All xss, yss. {concat (xss ++ yss)} === {concat xss ++ concat yss}
assert Monoid (++) {[]}
property NonMono1 = Lfp P. {| x | -/ x ::: P |}
--property NonMono2 Q = Lfp P. {| x | -/ x ::: P /\ (Q P) |}
-- Pred a = a -> Prop ??
------------------------
-- how to write "implies" and "iff" nicely?
-- foldr
assert All f, a . {foldr f a} ::: Undef -> Undef
assert All f, a . {foldr f a []} === a
assert All f, a, x, xs . {foldr f a (x:xs)} === {f x (foldr f a xs)}
assert All f, a, xs, ys . {foldr f a (xs ++ ys)} === {foldr f (foldr f a ys) xs}
assert All xs, ys . {xs ++ ys} === {foldr (:) ys xs}
assert All f, a .
(Strict f /\ Monoid f a) ==>
All xs, ys .
{foldr f a (xs ++ ys)} === {f (foldr f a xs) (foldr f a ys)}
-- map
assert All f . {map f} ::: Undef -> Undef
assert All f . {map f []} ::: []
assert All f, x, xs . {map f (x:xs)} === {f x : map f xs}
assert All xs, ys, f . {map f (xs ++ ys)} === {map f xs ++ map f ys}
assert All xs . {map id xs} === xs
assert All f, g . {map (f . g)} === {map f . map g}
assert All xs, f . {reverse (map f xs)} === {map f (reverse xs)}
assert All xs, f . {map f xs} === {[f x | x<-xs]}
assert All f . {map f} === {foldr (\u us -> f u : us) []}
-- id, (.)
assert All x . {id x} === x
assert All f, g, x . {f (g x)} === {(f . g) x}
assert LeftUnit (.) id
assert RightUnit (.) id
assert Assoc (.)
assert Monoid (.) id
assert Finite {[]}
-- is there a nicer way to write iff?
--
--assert All xs, x . Finite {xs} iff Finite {x:xs}
--assert All xs, f . Finite {xs} iff Finite {map f xs}
--assert All xs . Finite {xs} iff Finite {reverse xs}
--assert All xs, ys . Finite {xs ++ ys} iff (Finite {xs} /\ Finite {ys})
assert All xs, x . (-/ Finite {xs} \/ Finite {x:xs}) /\ --
(-/ Finite {x:xs} \/ Finite {xs})
assert All xs, x . Finite {xs} <==> Finite {x:xs}
assert All xs, f . (-/ Finite {xs} \/ Finite {map f xs}) /\
(-/ Finite {map f xs} \/ Finite {xs})
assert All xs, f . (Finite {xs} <==> Finite {map f xs})
assert All xs . (-/ Finite {xs} \/ Finite {reverse xs}) /\ --
(-/ Finite {reverse xs} \/ Finite {xs})
assert All xs . Finite {xs} <==> Finite {reverse xs}
assert All xs, ys . (-/ Finite {xs ++ ys} \/ (Finite {xs} /\ Finite {ys})) /\ --
(-/ (Finite {xs} /\ Finite {ys}) \/ Finite {xs ++ ys})
assert All xs, ys . Finite {xs ++ ys} <==> (Finite {xs} /\ Finite {ys})
-- reverse
assert reverse ::: Undef -> Undef
assert {reverse []} === {[]}
assert All x, xs . {reverse (x:xs)} === {reverse xs ++ [x]}
assert All xs . {reverse xs} === {[]} ==> xs === {[]}
assert All xs, ys . -/ (Finite xs) \/ {reverse (ys ++ xs)} === {reverse ys ++ reverse xs}
assert All xs . -/ Finite xs \/ {reverse (reverse xs)} === xs
assert All f, xs . -/ Strict f \/ {head (map f xs)} === {f (head xs)}
assert All xs . {head (reverse xs)} === {last xs}
assert All xs . {last (reverse xs)} === {head xs}
assert All xs, f . -/ Strict f \/ {last (map f xs)} === {f (last xs)}
assert All xs, f . -/ (Finite xs /\ -/ xs:::[]) \/ {last (map f xs)} === {f (last xs)}
assert All xs, f . Strict f ==> {last (map f xs)} === {f (last xs)}
assert All xs, f . (Finite xs /\ -/ xs:::[]) ==> {last (map f xs)} === {f (last xs)}
-- last
assert last ::: Undef -> Undef
assert last ::: [] -> Undef
assert All x, xs . {last (x:xs)} === {case xs of { [] -> x; (u:us) -> last (u:us)}}
assert All x . {last [x]} === x
assert All x, y, ys . {last (x:y:ys)} === {last (y:ys)}
assert All xs, ys . -/ Finite xs \/ (ys ::: [] /\ {last (xs ++ ys)} === {last ys})
assert All xs, ys . Finite xs ==> (ys ::: $[] /\ {last (xs ++ ys)} === {last xs})
-}