Extensional reasoning on Values

[AlecsFerra]

The extensionality flag fails when a function used as argument of a data constructor, take this as an example:

fixpoint "--rewrite"
fixpoint "--allowho"

constant f : (func(0 , [int; int; int]))
define f (x : int, y: int) : int = {(x + y)}

constant g : (func(0 , [int; int; int]))
define g (a : int, b: int) : int = {(b + a)}

data Ty 0 = [
    | Cons {mkCons : func(0 , [int; int; int])}
]

constant Cons : (func(0 , [func(0 , [int; int; int]); Ty]))

expand [1 : True; 2 : True]

constraint:
  env []
  lhs {VV1 : Tuple | true }
  rhs {VV2 : Tuple | (Cons f = Cons g) }
  id 2 tag []

it cannot prove that f and g are the same function since it cannot add the ext$... variable on the functions (and then cause their unfolding by PLE) since they would make the program ill-typed, the solution is eta-expanding the definitions of f and g to (\x:Int -> \y:Int -> f x y) (\x:Int -> \y:Int -> g x y) to let PLE then unfold the definitions in the body of the lambda and prove the equality.

DO NOT MERGE: This feature is exposing another LF bug in some tests in the liquidhaskell repo related to lambdas in the refinements.

[AlecsFerra]

The issue on the liquid haskell main repo is related to programs like this:

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

module Example where

{-@ reflect idu @-}
{-@ idu :: Int -> Int @-}
idu :: Int -> Int
idu x = x

{-@ proof :: {(\x:Int -> x) = idu } @-}
proof = ()

As it throws crash: SMTLIB2 respSat = Error "line 3 column 18650: unknown constant lam_arg$35$$35$1" whenever a lambda is used this way in the refinements

This error is already present is not caused by this patch

[nikivazou]

Yes, right now there is no real support for lambdas in LH :)

[AlecsFerra]

Uhm ok then I'm stuck

[AlecsFerra]

Right now It's verifying the example but it's also making some tests in the LH repo fail because it's unfolding some types and inserting lambdas

[AlecsFerra]

I think I fixed the bug regarding lambdas, I'll run the tests on the main repo to double check

[AlecsFerra]

The tests on the liquidhaskell are passing!

But I still have to fix a minor bug for my tests

[AlecsFerra]

Can confirm that it's passing all the test on the main LH repo, now I'm running the benchmarks

[AlecsFerra]

Benchmarks:

On average we are not extremely slower than then original PLE

[AlecsFerra]

Still in todo:

• Check if all the equations are actually needed
• Find a more solid way to write `validVar' here
• Decide if the feature will be hidden by a flag and if yes which
• Think if this is enough

[AlecsFerra]

Ops forgot about the tests on liquid-fixpoint

[AlecsFerra]

[AlecsFerra]

I can open a PR on LH when we are done here https://github.com/AlecsFerra/liquidhaskell/commits/develop/ I've also added two tests to showcase the feature:

• The famous STLC to SKI proof that started the whole thing here
• Automatic proof of the monad axiom of the reader monad here

[AlecsFerra]

Btw I think that now we can allow lambdas in reflected functions definitions, at least for the reader monad example it works

[AlecsFerra]

I will squash the commits at the end

[AlecsFerra]

Following some discussion in private I decided to remove the code relating to make PLE aware of dependent pattern matching / unification

The code of the reader monad still passes, the SKI calculus instead will require some extra lemmas

[facundominguez]

The only open discussion that I could catch is about making a comment more instructive. Update: oh, I asked about a couple other things in comments later.

Regarding performance, if the verification times worsen when enabling extensionality and --etabeta I'd say it is fine to merge. If verification worsens even when not enabling the flags, then I'd prefer to understand why before merging.

[AlecsFerra]

[AlecsFerra]

[AlecsFerra]

Looks way better I guess the slowdowns were actually caused by the elaboration

[facundominguez]

Also, note the comment edits that I just contributed. Feel free to adjust them if you see anything amiss.

[AlecsFerra]

Ops

[AlecsFerra]

Ok now It's ok to merge