T1382.hs

-- https://github.com/ucsd-progsys/liquidhaskell/issues/1382

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple-local"  @-} 

{- 
$ stack exec -- liquid Lists.hs --checks=lemma_app_assoc0
Time (0.37s) for action ["Lists.lemma_app_assoc0"]

$ stack exec -- liquid Lists.hs --checks=lemma_app_assoc1
Time (0.23s) for action ["Lists.lemma_app_assoc1"]

$ stack exec -- liquid Lists.hs --checks=lemma_app_assoc2
Time (1.60s) for action ["Lists.lemma_app_assoc2"]
-}

module Lists where 

import Prelude hiding ((++))
import Language.Haskell.Liquid.ProofCombinators 

data List a = Nil | Cons a (List a)

{-@ infixr ++  @-}
{-@ reflect ++ @-}
(++) :: List a -> List a -> List a 
Nil         ++ ys = ys 
(Cons x xs) ++ ys = Cons x (xs ++ ys)

-------------------------------------------------------------------------------

-- Full equational proof 

{-@ lemma_app_assoc0 :: xs:_ -> ys:_ -> zs:_ -> 
      { (xs ++ ys) ++ zs = xs ++ (ys ++ zs) } @-} 
lemma_app_assoc0 :: List a -> List a -> List a -> () 
lemma_app_assoc0 Nil     ys zs 
  =   (Nil ++ ys) ++ zs 
  === ys ++ zs 
  === Nil ++ (ys ++ zs)
  *** QED 

lemma_app_assoc0 (Cons x xs) ys zs 
  =   ((Cons x xs) ++ ys) ++ zs 
  === (Cons x (xs ++ ys)) ++ zs 
  === Cons x ((xs ++ ys) ++ zs) 
    ? lemma_app_assoc0 xs ys zs
  === Cons x (xs ++ (ys ++ zs))
  === (Cons x xs) ++ (ys ++ zs)
  *** QED 

-------------------------------------------------------------------------------
-- Short PLE proof 

{-@ ple lemma_app_assoc1 @-}
{-@ lemma_app_assoc1 :: xs:_ -> ys:_ -> zs:_ -> 
      { (xs ++ ys) ++ zs = xs ++ (ys ++ zs) } @-} 
lemma_app_assoc1 :: List a -> List a -> List a -> () 
lemma_app_assoc1 Nil         ys zs = () 
lemma_app_assoc1 (Cons x xs) ys zs = lemma_app_assoc1 xs ys zs

-------------------------------------------------------------------------------
-- Running PLE on equational proof

{-@ ple lemma_app_assoc2 @-}
{-@ lemma_app_assoc2 :: xs:_ -> ys:_ -> zs:_ -> 
      { (xs ++ ys) ++ zs = xs ++ (ys ++ zs) } @-} 
lemma_app_assoc2 :: List a -> List a -> List a -> () 
lemma_app_assoc2 Nil     ys zs 
  =   (Nil ++ ys) ++ zs 
  === ys ++ zs 
  === Nil ++ (ys ++ zs)
  *** QED 

lemma_app_assoc2 (Cons x xs) ys zs 
  =   ((Cons x xs) ++ ys) ++ zs 
  === (Cons x (xs ++ ys)) ++ zs 
  === Cons x ((xs ++ ys) ++ zs) 
    ? lemma_app_assoc2 xs ys zs
  === Cons x (xs ++ (ys ++ zs))
  === (Cons x xs) ++ (ys ++ zs)
  *** QED 


{-@ foo :: forall a b <pa :: a -> Bool, pb :: b -> Bool>. a<pa> -> b<pb> -> a<pa> @-}
foo :: a -> b -> a 
foo = undefined

infixl 3 ???

{-@ (???) :: forall a b <pa :: a -> Bool, pb :: b -> Bool>. a<pa> -> b<pb> -> a<pa> @-}
(???) :: a -> b -> a 
x ??? _ = x 
{-# INLINE (???)   #-} 



{- 

Here is the ANF-ed code that LH sees: 

Lists.lemma_app_assoc2
   = \ (@ a) (ds_d2zM :: [a]) (ys :: [a]) (zs :: [a]) ->
       case ds_d2zM of lq_anf$##7205759403792803514 {
         [] ->
           let { a0 = GHC.Types.[]    } in
           let { a1 = Lists.++ a0 ys  } in
           let { a2 = Lists.++ a1 zs  } in
           let { a3 = Lists.++ ys zs  } in
           let { a4 = (===) a2 a3     } in   -- <<< 
           let { a5 = GHC.Types.[]    } in
           let { a6 = Lists.++ ys zs  } in
           let { a7 = Lists.++ a5  a6 } in   -- <<< 
           let { a8 = (===) a4 a7     } in
             (***) a8 QED;

         : x xs ->
           let { a0 = GHC.Types.:  x xs } in
           let { a1 = Lists.++    a0 ys } in
           let { a2 = Lists.++    a1 zs } in
           let { a3 = Lists.++    xs ys } in
           let { a4 = GHC.Types.: x  a3 } in
           let { a5 = Lists.++    a4 zs } in
           let { a6 = (===) a2 a5       } in -- <<<
           let { a7 = Lists.++    xs ys } in
           let { a8 = Lists.++    a7 zs } in
           let { a9 = GHC.Types.: x  a8 } in
           let { a10 = (===) a6 a9      } in                                        -- <<< 
           let { a11 = Lists.lemma_app_assoc2 xs ys zs } in
           let { a12 = Language.Haskell.Liquid.ProofCombinators.? a10 a11 } in
           let { a13 = Lists.++ ys zs } in
           let { a14 = Lists.++ xs a13 } in
           let { a15 = GHC.Types.: x a14 } in
           let { a16 = (ProofCombinators.===) a12 a15 } in
           let { a17 = GHC.Types.: x xs } in
           let { a18 = Lists.++ ys  zs } in
           let { a19 = Lists.++ a17 a18 } in
           let { a20 = (===) a16 a19 } in                                           -- <<<
           (***) a20 QED
       };,
 -}