Proof with foldr and map is rejected

[facundominguez]

I discovered this failing example which I think LH should accept.

module Test where
{-@ LIQUID "--save" @-}
{-@ LIQUID "--ple" @-}
{-@ LIQUID "--reflection" @-}

{-@ reflect myFoldr @-}
myFoldr :: (a -> b -> b) -> b -> [a] -> b
myFoldr f z [] = z
myFoldr f z (x : xs) = f x (myFoldr f z xs)

{-@ reflect intSum @-}
intSum :: [Int] -> Int
intSum ys = myFoldr (+) 0 ys

{-@ reflect myMap @-}
myMap :: (a -> b) -> [a] -> [b]
myMap f [] = []
myMap f (x:xs) = f x : myMap f xs

{-@ lemma_sumPlusOne :: xs:[Int] -> { intSum (myMap (\x:Int -> x+1) xs) == intSum xs + len xs } @-}
lemma_sumPlusOne :: [Int] -> ()
lemma_sumPlusOne [] = ()
lemma_sumPlusOne (x:xs) = lemma_sumPlusOne xs

-- intSum (map (\x:Int -> x+1) (x:xs)) == intSum (x:xs) + len (x:xs)
-- x + 1 + intSum (map (\x:Int -> x+1) xs) == x + 1 + len xs

Looking at the PLE dump and the environment of the failing constraint, all necessary equalities seem to be present, and liquid-fixpoint stills rejects it.

[ranjitjhala]

I wonder if it is the lambda in the type.

Does it work if you instead define, reflect and use

Inc x = x + 1

[facundominguez]

Defining inc still makes the verification fail at the same spot (second equation of the lemma). I'm copying the error for the reference.

Test.hs:28:27: error:                                                                                                                                                                                 
    Liquid Type Mismatch
    .                                     
    The inferred type
      VV : {v : () | v == Test.lemma_sumPlusOne xs##aGf
                     && Test.intSum (Test.myMap Test.inc xs##aGf) == Test.intSum xs##aGf + GHC.Types_LHAssumptions.len xs##aGf}
    .
    is not a subtype of the required type
      VV : {VV##1069 : () | Test.intSum (Test.myMap Test.inc ?a) == Test.intSum ?a + GHC.Types_LHAssumptions.len ?a}
    .
    in the context
      x##aGe : GHC.Types.Int
       
      ?a : {?a : [GHC.Types.Int] | GHC.Types_LHAssumptions.len ?a >= 0}
       
      ?b : {?b : [GHC.Types.Int] | ?b == ?a
                                   && ?b == GHC.Types.: x##aGe xs##aGf
                                   && GHC.Types_LHAssumptions.len ?b == 1 + GHC.Types_LHAssumptions.len xs##aGf
                                   && head ?b == x##aGe
                                   && lqdc##$select##GHC.Types.:##1 ?b == x##aGe
                                   && lqdc##$select##GHC.Types.:##2 ?b == xs##aGf
                                   && tail ?b == xs##aGf
                                   && GHC.Types_LHAssumptions.len ?b >= 0}
       
      xs##aGf : {v : [GHC.Types.Int] | GHC.Types_LHAssumptions.len v >= 0}
    Constraint id 5
   |
28 | lemma_sumPlusOne (x:xs) = lemma_sumPlusOne xs
   |

[facundominguez]

If I redefine intSum as follows, verification passes.

{-@ reflect intSum @-}
intSum :: [Int] -> Int
intSum ys = myFoldr add 0 ys

{-@ reflect add @-}
add :: Int -> Int -> Int
add = (+)

The input to the smt solver uses GHC.Internal.Num.$43$ instead of + if I don't define add.

inc is not necessary for verification if one uses the --etabeta flag.

[facundominguez]

Probably this is because CoreToLogic replaces occurrences of GHC.Internal.Num.+ with + only when the application is saturated.

Replacing add with \x y -> x + y and using --etabeta also passes verification.

It is not obvious how to improve LH though.

1. LF represents addition with a special construct EBin Plus e1 e2. We would have to change this representation to allow for partial applications.
2. At the moment, LH replaces GHC.Internal.Num.+ with + without regarding the type of the operator. It always assumes that the meaning of both operators match for every Num instance.

Perhaps it would be fine to eta-expand partial applications in CoreToLogic so the application of GHC.Internal.Num.+ is saturated. This doesn't address (2), but perhaps it could be considered separately.

[ranjitjhala]

Interesting!

Yes I agree with you - the right approach is

Perhaps it would be fine to eta-expand partial applications in CoreToLogic