content: module PreludeProps where
  
  {-P: {- -}
  
  
  property Univ      = Gfp X. X
  property Undef     = Lfp X. X
  property Absurdity = $Undef
  
  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. All y. All 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. All y. {const x y} === x
  assert All f. All x. {const x . f} === {const x}
  assert All f. All 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. All xs. {sum (x:xs)} === {x + sum xs} 
  assert All xs. All ys. {sum (xs ++ ys)} === {sum xs + sum ys}
  assert {sum . map length} === {length . concat}
  assert length === {sum . map (const 1)}
  assert All xs. All ys. {length (xs ++ ys)} === {length xs + length ys}
  assert {length undefined} === {undefined}
  assert {length []} === 0
  assert All x. All 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. All xs. {length (map f xs)} === {length xs}
  assert All xs. {length (reverse xs)} === {length xs}
  assert All f. All a. {foldl f a undefined} === undefined
  assert All f. All a. {foldl f a []} === a
  assert All f. All a. All x. All xs. {foldl f a (x:xs)} === {foldl f (f a x) xs}
  -- assert All f. All 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. All a. Monoid f a /\ (All x. {f x undefined} === undefined})
  --               /\ (All y. {f undefined y} === undefomed) ===>
  --              All x. All 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. All xs. All ys. {filter p (xs ++ ys)} === 
                                                  {filter p xs ++ filter p ys}
  assert All p. {filter p . concat} === {concat . map (filter p)}
  
  -- assert All p. All x. All 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. All x. All 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. All x. All xs. ({p x} ::: False) 
                              \/ {filter p (x:xs)} === {x : filter p xs}
  
  assert All p. All x. All xs. -/ {p x} ::: $False 
                              \/ {filter p (x:xs)} === {filter p xs}
  
  assert All p. All x. All xs. {p x} ::: $False ==>
                               {filter p (x:xs)} === {filter p xs}
  
  assert All p. All x. All 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. All xs. All ys. {rev ys (x:xs)} === {rev (x:ys) xs}
  assert All xs. All 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. All xs. {head (x:xs)} === x
  
  assert {concat undefined} === undefined
  assert {concat undefined} ::: Undef
  
  assert {concat []} === {[]}
  assert {concat []} ::: $[]
  
  assert All xs. All xss. {concat (xs:xss)} === {xs ++ concat xss}
  assert concat === {foldr (++) []}
  assert {concat . concat} === {concat . map concat}
  
  assert All f. All a. Monoid f a ==> {foldr f a . map (foldr f a)} === {foldr f a . concat}
  
  assert All xss. All 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 . All a .                  {foldr f a} ::: Undef -> Undef
  assert All f . All a .                  {foldr f a []} === a
  assert All f . All a . All x . All xs . {foldr f a (x:xs)} === {f x (foldr f a xs)}
  
  assert All f . All a . All xs . All ys . {foldr f a (xs ++ ys)} === {foldr f (foldr f a ys) xs}
  assert All xs . All ys .                 {xs ++ ys} === {foldr (:) ys xs}
  
  assert All f . All a .
      (Strict f /\ Monoid f a) ==>
        All xs . All 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 . All x . All xs . {map f (x:xs)} === {f x : map f xs}
  
  assert All xs . All ys . All f . {map f (xs ++ ys)} === {map f xs ++ map f ys}
  assert All xs .                  {map id xs} === xs
  assert All f. All g .            {map (f . g)} === {map f . map g}
  assert All xs . All f .          {reverse (map f xs)} === {map f (reverse xs)}
  assert All xs . All 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 . All g . All 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 . All x . Finite {xs} iff Finite {x:xs}
  --assert All xs . All f . Finite {xs} iff Finite {map f xs}
  --assert All xs . Finite {xs} iff Finite {reverse xs}
  --assert All xs . All ys . Finite {xs ++ ys} iff (Finite {xs} /\ Finite {ys})
  
  assert All xs . All x .  (-/ Finite {xs} \/ Finite {x:xs}) /\ --
                           (-/ Finite {x:xs} \/ Finite {xs})
  
  assert All xs . All x .  Finite {xs} <==> Finite {x:xs}
  
  assert All xs . All f .  (-/ Finite {xs} \/ Finite {map f xs}) /\ 
                           (-/ Finite {map f xs} \/ Finite {xs})
  
  assert All xs . All 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 . All ys . (-/ Finite {xs ++ ys} \/ (Finite {xs} /\ Finite {ys})) /\ --
                           (-/ (Finite {xs} /\ Finite {ys}) \/ Finite {xs ++ ys})
  
  assert All xs . All ys . Finite {xs ++ ys} <==> (Finite {xs} /\ Finite {ys})
  
  
  
  -- reverse
  assert                  reverse ::: Undef -> Undef
  assert                  {reverse []}     === {[]}
  assert All x . All xs . {reverse (x:xs)} === {reverse xs ++ [x]}
  
  assert All xs . {reverse xs} === {[]} ==> xs === {[]}
  
  assert All xs . All ys . -/ (Finite xs) \/ {reverse (ys ++ xs)} === {reverse ys ++ reverse xs}
  assert All xs . -/ Finite xs \/ {reverse (reverse xs)} === xs
  assert All f . All 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 . All f . -/ Strict f                  \/ {last (map f xs)} === {f (last xs)}
  assert All xs . All f . -/ (Finite xs /\ -/ xs:::[]) \/ {last (map f xs)} === {f (last xs)}
  
  assert All xs . All f . Strict f ==> {last (map f xs)} === {f (last xs)}
  assert All xs . All f . (Finite xs /\ -/ xs:::[]) ==> {last (map f xs)} === {f (last xs)}
  
  
  -- last
  assert last ::: Undef -> Undef
  assert last ::: [] -> Undef
  assert All x . All xs . {last (x:xs)} === {case xs of { [] -> x; (u:us) -> last (u:us)}}
  assert All x . {last [x]} === x
  assert All x . All y . All ys . {last (x:y:ys)} === {last (y:ys)}
  assert All xs . All ys . -/ Finite xs \/ (ys ::: [] /\ {last (xs ++ ys)} === {last ys})
  
  assert All xs . All ys . Finite xs ==> (ys ::: $[] /\ {last (xs ++ ys)} === {last xs}) 
  
  -}
  