Equivalent definitions giving different results

[ranjitjhala]

Here are two definitions of a reflect-ed function -- one works and the other does not. Why?

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple"        @-}
{-@ infixr ++             @-}

module Tmp where

import ProofCombinators

data Pair a b = P a b 

{-@ measure pFst @-}
pFst :: Pair a b -> a 
pFst (P x _) = x 

{-@ measure pSnd @-}
pSnd :: Pair a b -> b 
pSnd (P _ y) = y 

{-@ reflect select @-}
{-@ select :: _ -> l:_ -> Pair a {v:_|len v = len l} @-}
select :: (Ord a) => a -> [a] -> Pair a [a]
select x []    = P x []
select x (h:t) 
  | x <= h     = -- THIS DEF IS SAFE
                 -- let s_x_t = select x t in P (pFst s_x_t) (h : pSnd s_x_t)

                 -- THIS DEF IS NOT SAFE! 
                 let P j l' = select x t in P j (h:l')  
  | otherwise  = let P j l' = select h t in P j (x:l') 

{- lem_select_1 :: x:_ -> l:_ -> { pFst (select x l) <= x } @-}
lem_select_1 :: (Ord a) => a -> [a] -> Proof 
lem_select_1 _ []    = () 
lem_select_1 x (h:t) 
  | x <= h           = let s_x_t  = select x t
                           s_x_ht = P (pFst s_x_t) (h : pSnd s_x_t)  
                       in 
                         select x (h:t) === s_x_ht *** QED

  | otherwise        = undefined 

[facundominguez]

Verification passes if the measures are changed to reflected functions. It would be worth looking at the equalities that PLE produces in each case.

[facundominguez]

Oh, I know what it is. The measure equalities are not in scope where they are needed in the unsafe variant. We have discussed this a few times in other issues by now.

Change the let by a case in lem_select and it will pass verification.

lem_select_1 x (h:t) 
  | x <= h           = case select x t of
                         P j l' -> let s_x_ht = P j (h : l')
                           in 
                              select x (h:t) === s_x_ht *** QED

  | otherwise        = undefined

The only way I can imagine improving the experience is augmenting the error message with the equalities that are used in the failed constrained. Seeing that the measures are missing is perhaps enough (?)