liquidhaskell-0.8.10.7: benchmarks/popl18/nople/pos/MonadReader.hs

{-@ LIQUID "--higherorder"       @-}
{-@ LIQUID "--exact-data-cons"   @-}

-- NOPROP probably breaks some fixpoint flag 

{-@ LIQUID "--alphaequivalence"  @-}
{-@ LIQUID "--betaequivalence"   @-}
{-@ LIQUID "--normalform"        @-} 

{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE FlexibleContexts    #-}

module MonadReader where

import Prelude hiding (return, Maybe(..), (>>=))

import Proves
import Helper 

-- | Monad Laws :
-- | Left identity:	  return a >>= f  ≡ f a
-- | Right identity:	m >>= return    ≡ m
-- | Associativity:	  (m >>= f) >>= g ≡	m >>= (\x -> f x >>= g)

{-@ data Reader r a = Reader { runIdentity :: r -> a } @-}
data Reader r a     = Reader { runIdentity :: r -> a }

{-@ axiomatize return @-}
return :: a -> Reader r a
return x = Reader (\r -> x)

{-@ axiomatize bind @-}
bind :: Reader r a -> (a -> Reader r b) -> Reader r b
bind (Reader x) f = Reader (\r -> fromReader (f (x r)) r)

{-@ measure fromReader @-}
fromReader :: Reader r a -> r -> a 
fromReader (Reader f) = f

-- NV TODO the following is needed because Reader is not interpreted by
-- Contraints.Generate.lamExpr

{-@ axiomatize reader @-}
reader x = Reader x 

 
{-@ readerId :: f:(Reader r a) -> {f == Reader (fromReader f)} @-} 
readerId :: (Reader r a) -> Proof 
readerId (Reader f)  
  =   Reader (fromReader (Reader f))
  ==. Reader f 
  *** QED 


-- | Left Identity
{-@ left_identity :: x:a -> f:(a -> Reader r b) -> { bind (return x) f == f x } @-}
left_identity :: Arg r => a -> (a -> Reader r b) -> Proof
left_identity x f
  =   bind (return x) f 
  ==. bind (Reader (\r -> x)) f
  ==. Reader (\r' -> fromReader (f ((\r -> x) r')) r')
  ==. Reader (\r' -> fromReader (f x) r') ? left_identity_helper x f 
  ==. Reader (fromReader (f x)) ? lambda_expand (fromReader (f x))
  ==. f x                       ? readerId (f x)
  *** QED 


{-@ left_identity_helper :: x:a -> f:(a -> Reader r b) 
  -> {  (\r':r -> (fromReader (f ((\r:r -> x) (r')) ) (r'))) ==  (\r':r -> (fromReader (f x) (r')))  } @-}
left_identity_helper :: Arg r => a -> (a -> Reader r b) -> Proof
left_identity_helper x f
  =   simpleProof

-- | Right Identity


{-@ right_identity :: x:Reader r a -> { bind x return == x }
 @-}
right_identity :: Arg r => Reader r a -> Proof
right_identity (Reader x)
  =   bind (Reader x) return
  ==. Reader (\r -> fromReader (return (x r)) r)
  ==. Reader (\r -> fromReader (reader (\r' ->  (x r))) (r))
       ? right_identity_helper x 
  ==. Reader (\r -> (\r' ->  (x r)) (r)) 
       ? right_identity_helper1 x 
  ==. Reader (\r -> x r)           
       -- ? right_identity_helper2 x       
  ==. Reader x                           
       ? lambda_expand x 
  *** QED 


right_identity_helper1 :: Arg r => (r -> a) -> Proof 
{-@ right_identity_helper1 :: Arg r => x:(r -> a) 
  -> {(\r:r -> fromReader (reader (\r':r ->  (x r))) (r)) == (\r:r -> (\r':r ->  (x r)) (r))} @-}
right_identity_helper1 x =
  ((\r -> (\r' ->  (x r)) (r)) =*=: (\r -> fromReader (reader (\r' ->  (x r))) (r)))
    (right_identity_helper1_body x) *** QED 


right_identity_helper1_body :: Arg r => (r -> a) -> r -> Proof 
{-@ right_identity_helper1_body :: Arg r => x:(r -> a) -> r:r 
  -> {(fromReader (reader (\r':r ->  (x r))) (r) == (\r':r ->  (x r)) (r))
    && ((\r:r -> fromReader (reader (\r':r ->  (x r))) (r)) (r) == (fromReader (reader (\r':r ->  (x r))) (r))) 
    && ((\r:r -> (\r':r ->  (x r)) (r)) (r) == ((\r':r ->  (x r)) (r)))
    } @-}
right_identity_helper1_body x r
  =  fromReader (reader (\r' -> (x r))) r 
  ==. (\r' -> x r) r 
  *** QED 


right_identity_helper2 :: Arg r => (r -> a) -> Proof 
{-@ right_identity_helper2 :: Arg r => x:(r -> a) 
  -> { (\r:r -> (\r':r ->  (x r)) (r)) ==  (\r:r -> x r) } @-}
right_identity_helper2 _ = simpleProof


right_identity_helper :: Arg r => (r -> a) -> Proof 
{-@ right_identity_helper :: Arg r => x:(r -> a) 
  -> {(\r:r -> fromReader (return (x r)) r) == (\r:r -> fromReader (reader (\r':r ->  (x r))) (r))} @-}
right_identity_helper x
  =  (
     (\r -> fromReader (return (x r)) r)
     =*=: 
     (\r -> fromReader (reader (\r' ->  (x r))) (r))
     )  (right_identity_helper_body x) *** QED 

right_identity_helper_body :: Arg r => (r -> a) -> r -> Proof 
{-@ right_identity_helper_body :: Arg r => x:(r -> a) -> r:r
  -> { (fromReader (return (x r)) r == fromReader (reader (\r':r ->  (x r))) (r))
       && (((\r:r -> fromReader (return (x r)) r)) (r) == (fromReader (return (x r)) r))
       && ((\r:r -> fromReader (reader (\r':r ->  (x r))) (r))(r) == (fromReader (reader (\r':r ->  (x r))) (r)))
      } @-}
right_identity_helper_body x r 
  =   fromReader (return (x r)) r
  ==. fromReader (reader (\r' ->  (x r))) r
  *** QED 

-- | Associativity:	  (m >>= f) >>= g ≡	m >>= (\x -> f x >>= g)
{-@ associativity :: x:Reader r a -> f: (a -> Reader r a) -> g:(a -> Reader r a) 
  -> {bind (bind x f) g      ==  bind x (\r4:a ->(bind (f r4) g)) } @-}
associativity :: (Arg r, Arg a) =>  Reader r a -> (a -> Reader r a) -> (a -> Reader r a) -> Proof
associativity (Reader x) f g
  =   bind (bind (Reader x) f) g
  -- unfold inner bind 
  ==. bind (Reader (\r1 -> fromReader (f (x r1)) r1)) g 
  -- unfold outer bind 
  ==. Reader (\r2 -> fromReader (g ((\r1 -> fromReader (f (x r1)) r1) (r2))) (r2))
  -- apply    r1 := r2
  ==. Reader (\r2 -> fromReader (g (fromReader (f (x r2)) r2) )  r2)
  -- abstract r3 := r2 
  ==. Reader (\r2 -> 
          (\r3 -> fromReader (g ((fromReader (f (x r2))) r3) ) r3)
         r2)
  -- apply measure fromReader (Reader f) == f 
  ==. Reader (\r2 -> fromReader (
          (reader (\r3 -> fromReader (g ((fromReader (f (x r2))) r3) ) r3))
        ) r2)
        ? associativity_helper0 x f g 
  -- abstract r4 := x r2 
  ==. Reader (\r2 -> fromReader ((\r4 -> 
          (reader (\r3 -> fromReader (g ((fromReader (f r4)) r3) ) r3))
        ) (x r2)) r2) 
      ? associativity_helper2 x f g 
  -- fold (bind (f r4) g)
  ==. Reader (\r2 -> fromReader ((\r4 -> 
           (bind (f r4) g)
        ) (x r2)) r2)  
     ? associativity_helper1 x f g 
  -- fold bind 
  ==. bind (Reader x) (\r4 ->(bind (f r4) g))
  *** QED  

{-@ associativity_helper0 :: x:(r -> a) -> f:(a -> Reader r b) -> g:(b -> Reader r c) 
  -> {  (\r2:r -> (\r3:r -> fromReader (g (fromReader (f ( x r2)) r3)) (r3)) (r2)) 
      ==   (\r2:r -> (fromReader (reader (\r3:r -> fromReader (g (fromReader (f (x r2)) r3)) (r3)))) (r2)) 
          } @-}
associativity_helper0 :: Arg r => (r -> a) -> (a -> Reader r b) -> (b -> Reader r c) -> Proof
associativity_helper0 x f g
  =    ((\r2 -> (\r3 -> fromReader (g (fromReader (f ( x r2)) r3)) (r3)) (r2)) 
  =*=:  (\r2 -> fromReader (reader (\r3 -> fromReader (g (fromReader (f (x r2)) r3)) (r3))) (r2)))
         (associativity_helper0_body x f g) *** QED 
          
associativity_helper0_body :: (r -> a) -> (a -> Reader r b) -> (b -> Reader r c)-> r  -> Proof
{-@ associativity_helper0_body :: x:(r -> a) -> f:(a -> Reader r b) -> g:(b -> Reader r c) -> r2:r
  -> {    (\r3:r -> fromReader (g (fromReader (f ( x r2)) r3)) (r3)) (r2)
      ==  (fromReader (reader (\r3:r -> fromReader (g (fromReader (f (x r2)) r3)) (r3)))) (r2)
       && 
           ((\r2:r -> (\r3:r -> fromReader (g (fromReader (f ( x r2)) r3)) (r3)) (r2))) (r2) == (\r3:r -> fromReader (g (fromReader (f ( x r2)) r3)) (r3)) (r2)
       && 
           (\r2:r -> (fromReader (reader (\r3:r -> fromReader (g (fromReader (f (x r2)) r3)) (r3)))) (r2)) (r2) == (fromReader (reader (\r3:r -> fromReader (g (fromReader (f (x r2)) r3)) (r3)))) (r2)
          } @-}
associativity_helper0_body x f g r2
  = readerId' (\r3 -> fromReader (g (fromReader (f ( x r2)) r3)) (r3))

{-@ readerId' :: x:(r -> a) -> {x == fromReader (reader x)} @-} 
readerId' :: (r -> a) -> Proof 
readerId' x  
  =   fromReader (reader x)
  ==. fromReader (Reader x)
  ==. x 
  *** QED 


{-@ associativity_helper2 :: x:(r -> a) -> f:(a -> Reader r b) -> g:(b -> Reader r c) 
  -> {  (\r2:r -> fromReader (reader (\r3:r -> fromReader (g (fromReader (f (x r2)) r3)) (r3))) (r2))  
      ==   (\r2:r -> fromReader ( (\r4:a -> ( reader (\r3:r -> fromReader (g (fromReader (f r4 ) r3)) (r3))))  (x r2)) (r2))  
         } @-}
associativity_helper2 :: (r -> a) -> (a -> Reader r b) -> (b -> Reader r c) -> Proof
associativity_helper2 x f g = simpleProof

{-@ associativity_helper1 :: x:(r -> a) -> f:(a -> Reader r b) -> g:(b -> Reader r c) 
  -> {   (\r2:r -> fromReader ( (\r4:a -> ( reader (\r3:r -> fromReader (g (fromReader (f r4 ) r3)) (r3))))  (x r2)) (r2))  
      ==    (\r2:r -> fromReader ( (\r4:a -> ( bind (f r4) g))  (x r2)) (r2))  
    } @-}
associativity_helper1 :: (Arg r, Arg a) => (r -> a) -> (a -> Reader r b) -> (b -> Reader r c) -> Proof
associativity_helper1 x f g
  = ((\r2 -> fromReader ( (\r4 -> ( reader (\r3 -> fromReader (g (fromReader (f r4 ) r3)) (r3))))  (x r2)) (r2))  
      =*=:    (\r2 -> fromReader ( (\r4 -> ( bind (f r4) g))  (x r2)) (r2))  
    ) (associativity_helper1_body x f g)  *** QED 

{-@ associativity_helper1_body :: x:(r -> a) -> f:(a -> Reader r b) -> g:(b -> Reader r c) -> r2:r
  -> {  fromReader ( (\r4:a -> ( reader (\r3:r -> fromReader (g (fromReader (f r4 ) r3)) (r3))))  (x r2)) (r2)  
      ==   fromReader ( (\r4:a -> ( bind (f r4) g))  (x r2)) (r2)
      && 
        ((\r2:r -> fromReader ( (\r4:a -> ( reader (\r3:r -> fromReader (g (fromReader (f r4 ) r3)) (r3))))  (x r2)) (r2))) (r2)
        == fromReader ( (\r4:a -> ( reader (\r3:r -> fromReader (g (fromReader (f r4 ) r3)) (r3))))  (x r2)) (r2)
      && 
        (\r2:r -> fromReader ( (\r4:a -> ( bind (f r4) g))  (x r2)) (r2)) (r2)
        == fromReader ( (\r4:a -> ( bind (f r4) g))  (x r2)) (r2)
    } @-}
associativity_helper1_body :: (Arg r, Arg a ) => (r -> a) -> (a -> Reader r b) -> (b -> Reader r c) -> r -> Proof
associativity_helper1_body x f g r2 
  =   fromReader ( (\r4 -> ( reader (\r3 -> fromReader (g (fromReader (f r4 ) r3)) (r3))))  (x r2)) (r2)
  ==. fromReader ( (\r4 -> ( bind (f r4) g))  (x r2)) (r2)
      ? helper_of_helper x f g r2
  *** QED 


{-@ helper_of_helper :: x:(r -> a) -> f:(a -> Reader r b) -> g:(b -> Reader r c) -> r2:r
  -> {   \r4:a -> (reader (\r3:r -> fromReader (g (fromReader (f r4 ) r3)) (r3)))
      == \r4:a -> (bind (f r4) g)
    } @-}
helper_of_helper :: (Arg r, Arg a) => (r -> a) -> (a -> Reader r b) -> (b -> Reader r c) -> r -> Proof
helper_of_helper x f g r2 
  =  ( (\r4 -> (reader (\r3 -> fromReader (g (fromReader (f r4 ) r3)) (r3))))
      =*=: (\r4 -> (bind (f r4) g))) (helper_of_helper_body x f g r2) *** QED 

{-@ helper_of_helper_body :: x:(r -> a) -> f:(a -> Reader r b) -> g:(b -> Reader r c) -> r2:r -> r4:a
  -> {   (reader (\r3:r -> fromReader (g (fromReader (f r4 ) r3)) (r3)))
      == (bind (f r4) g)
      && 
         (\r4:a -> (reader (\r3:r -> fromReader (g (fromReader (f r4 ) r3)) (r3)))) (r4)
      ==  (reader (\r3:r -> fromReader (g (fromReader (f r4 ) r3)) (r3)))
      && 
         (\r4:a -> (bind (f r4) g)) (r4) == (bind (f r4) g)

    } @-}
helper_of_helper_body :: Arg r => (r -> a) -> (a -> Reader r b) -> (b -> Reader r c) -> r -> a -> Proof
helper_of_helper_body x f g r2 r4 
  = case f r4 of 
      Reader _ -> reader (\r3 -> fromReader (g (fromReader (f r4 ) r3)) (r3)) 
                  ==. bind (f r4) g 
                   *** QED 



{-@ helper_of_helper_body' :: x:(r -> a) -> y:(Reader r b) -> g:(b -> Reader r c) -> r2:r -> r4:a
  -> {   (Reader (\r3:r -> fromReader (g ( (fromReader y) (r3))) (r3)))
      == (bind y g)
    } @-}
helper_of_helper_body' :: Arg r => (r -> a) -> (Reader r b) -> (b -> Reader r c) -> r -> a -> Proof
helper_of_helper_body' x y@(Reader _) g r2 r4  
  =   reader (\r3 -> fromReader (g ( (fromReader y) r3)) (r3)) 
  ==. bind y g 
  *** QED 



{-@ qual :: f:(r -> a) -> {v:Reader r a | v == Reader f} @-}
qual :: (r -> a) -> Reader r a 
qual = Reader