Reasoning about equationally-defined functions is difficult

[rosekunkel]

Given the definitions

data Foo = A
data Bar = B | C

{-@ reflect f @-}
f :: Foo -> Bar
f A = B

{-@ reflect g @-}
g :: Foo -> Bar
g A = f A

{-@ reflect h @-}
h :: Foo -> Bar
h A =
  g A
  === f A
  === B

I would like to be able to write a proof like

{-@ hProof :: {h A = B} @-}
hProof :: Proof
hProof =
  h A
  === B
  *** QED

But this doesn't go through. I can write

{-@ hProof :: {h A = B} @-}
hProof :: Proof
hProof =
  h A
  === (g A
       === f A
       === B)
  *** Admit

but it's not clear where to go from here. If I reflect the definition of ===, then I can write the proof as

{-@ hProof :: {h A = B} @-}
hProof :: Proof
hProof =
  h A
  === (g A
       === f A
       === B)
  === (f A
       === B)
  === B

but this is cumbersome (I need a new step for each equality) and also brittle (it breaks whenever the proof of h is changed, even if the final "definition" is unchanged).

If in addition to reflecting ===, I enable PLE, then I can do the original proof. I see a few solutions to this problem:

• Reflect the definitions of proof combinators and accept that we will have to enable PLE to do nontrivial proofs with them.
• Provide some mechanism for specifying that the definition of h A is actually B (this might also allow us to avoid relying on GHC's optimizer to remove the equational reasoning steps).
• Make Liquid Haskell smarter somehow so that it can deduce that h A is equal to B without the extra steps. I'm surprised that the SMT solver can't figure this out from the refinement on ===, actually.

There is a full example here: https://gist.github.com/wkunkel/36dd0d39311822cc9a7119492e01f763 For some reason I had to use --prune-unsorted; I'm not totally sure what this flag does (which is why I opened #1262).

[ranjitjhala]

@wkunkel -- yes I think so far we've not had a reason to actually "reflect" the proofs; whats the use case here? Is it not possible to define h"directly"? i.e. why use the equations?

[rosekunkel]

@ranjitjhala The idea is that we can use the equations to define an optimized function from an inefficient but "obvious" definition. For example:

{-@ reverseAppend :: xs:[a] -> ys:[a] -> {zs:[a] | zs = reverse xs ++ ys} @-}
reverseAppend :: [a] -> [a] -> [a]
reverseAppend [] ys = reverse [] ++ ys
  === [] ++ ys
  === ys
reverseAppend (x:xs) ys = reverse (x:xs) ++ ys
  === (reverse xs ++ [x]) ++ ys
  ==? reverse xs ++ ([x] ++ ys) ? appendAssoc (reverse xs) [x] ys
  === reverse xs ++ ([] ++ (x:ys))
  === reverse xs ++ (x:ys)
  === reverseAppend xs (x:ys)

We could have written directly

reverseAppend [] ys = ys
reverseAppend (x:xs) ys = reverseAppend xs (x:ys)

but then we would have to prove separately that it respects the desired refinement.

[ranjitjhala]

Hmm, well in this situation, I find it useful to use the withProof combinator so you just have the standard definition of revApp with the relevant extra bits asserted at the output:

{-@ LIQUID "--ple" @-}
{-@ LIQUID "--exactdc" @-}

import Language.Haskell.Liquid.NewProofCombinators

{- reflect revApp @-}

{-@ revApp :: xs:_ -> ys:_ -> {v:_ | v = app (rev xs) ys} @-}
revApp :: [a] -> [a] -> [a]
revApp []     ys = ys
revApp (x:xs) ys = revApp xs (x:ys)
                    `withProof`
                      app_assoc (rev xs) [x] ys

{-@ reflect app @-}
app :: [a] -> [a] -> [a]
app []     ys = ys
app (x:xs) ys = x : app xs ys

{-@ reflect rev @-}
rev :: [a] -> [a]
rev []     = []
rev (x:xs) = app (rev xs) [x]

{-@ app_assoc :: xs:_ -> ys:_ -> zs:_ -> { app (app xs ys) zs == app xs (app ys zs) } @-}
app_assoc :: [a] -> [a] -> [a] -> ()
app_assoc [] ys zs     = ()
app_assoc (x:xs) ys zs = app_assoc xs ys zs

Of course, I'm leaning heavily on --ple here, to first figure out the equational proof and then its shrunk/ple version:

{-@ thm :: xs:_ -> ys:_ -> { revApp xs ys = app (rev xs) ys } -}
thm :: [a] -> [a] -> ()
thm [] ys     = ()
thm (x:xs) ys =  thm xs (x:ys) &&& app_assoc (rev xs) [x] ys

(We don't need the thm xs (x:ys) at the withProof site because that fact pops out of the output refinement for revApp now...)

[ranjitjhala]

Btw, you shouldn't have had to use --prune-unsorted here. Is it because you were getting some mysterious error from fixpoint telling you to use that flag? I think that may be a variant of the issue I just saw/filed:

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

The --prune-unsorted is an unfortunate workaround a problem with the way we've implemented measures, and which will require a fair bit of work to fix properly [there's a whole tag devoted to it :-)]

[rosekunkel]

The main motivation for doing things this way is that it lets us systematically improve our definition from the obvious one to the optimized one without having to restructure the code. It's probably not a big deal if there isn't a nice way to do it like this, though. @nikivazou might have more thoughts.

Also, if I don't use --prune-unsorted, I get these errors:

:1:1-1:1: Error
  Constraint with free vars
  16
  [Example.===]
  Try using the --prune-unsorted flag
:1:1-1:1: Error
  Constraint with free vars
  17
  [Example.===]
  Try using the --prune-unsorted flag
:1:1-1:1: Error
  Constraint with free vars
  13
  [Example.===]
  Try using the --prune-unsorted flag
:1:1-1:1: Error
  Constraint with free vars
  15
  [Example.===]
  Try using the --prune-unsorted flag

instead of the error that I actually want.

[ranjitjhala]

Hmm, interesting. I suppose my worry is we'd want to make sure that the reflect-ed definition of reverseAppend is just the actual "computational" part (i.e. without the extra stuff of the proof).

It seems like it should be possible to modify CoreToLogic (i.e. the code where reflection happens) to somehow slice away the bits that have to do with proof...

[rosekunkel]

It appears that this already exists in some form, see #1247 and the eq operator added to https://github.com/ucsd-progsys/liquidhaskell/blob/develop/include/CoreToLogic.lg

Can we just reflect === instead of eq in the same way? We might want some sort of general mechanism for "inline this function when reflecting," though.