Equational reasoning on higher order expressions

[josedusol]

Im trying to write some proofs in point free style, but it seems i can't convince LH of my work. I present a simple example next.

Let f:b->c, g:a->b, h:a->c and f1 be the inverse of f. Let's say we want to prove the following "shunting" rule:
f.g = h implies g = f1.h

So we assume f.g = h and prove g = f1.h. The natural thing to do would be to start on the rhs f1.h to reach lhs g. If we try to express this idea in code:

{-@ shuntingWrong :: f:(b -> c) -> g:(a -> b) -> h:(a -> c) 
                  -> f1:(c -> b) -> ({ f . f1 = id }, { f1 . f = id })
                  -> ({ f . g = h }) -> { g = f1 . h } @-}
shuntingWrong f g h f1 (f1_pf1, f1_pf2) hyp =
      f1 . h                   ? hyp   
  ==. f1 . (f . g)             ? compAssoc f1 f g
  ==. (f1 . f) . g             ? f1_pf2  
  ==. id . g                   ? compIdLeft g
  ==. g 
  *** QED                      -- ERROR, not what LH expected, why?
  
{-@ assume compIdLeft :: f:(a -> b) -> { id . f = f } @-}
compIdLeft _ = ()
{-@ assume compAssoc :: f:(c -> d) -> g:(b -> c) -> h:(a -> b) 
                     -> { (f . g) . h = f . (g . h) } @-}
compAssoc _ _ _ = ()

we get:

The inferred type
VV : a -> b
.
is not a subtype of the required type
VV : a -> b

I can't understand the error here because clearly the inferred and required type are actually the same... so there may be another thing going on, what?. BTW, i am using --extensionality and --higherorder.

Interestingly, we can do the proof in a more verbose fashion working over equality and reducing to True as follows:

{-@ shuntingOk :: Eq (a -> b)
             => f:(b -> c) -> g:(a -> b) -> h:(a -> c) 
             -> f1:(c -> b) -> ({ f . f1 = id }, { f1 . f = id })
             -> ({ f . g = h }) -> { g = f1 . h } @-}
shuntingOk f g h f1 (f1_pf1, f1_pf2) hyp =
      g == f1 . h                   ? hyp   
  ==. g == f1 . (f . g)             ? compAssoc f1 f g
  ==. g == (f1 . f) . g             ? f1_pf2  
  ==. g == id . g                   ? compIdLeft g
  ==. g == g                        -- well, obvius
  ==. True
  *** QED

One problem with this approach (besides verbosity) is that working explicitly with == forces the inclusion of special type constraints like Eq (a -> b). Then, derived proofs inheriting lot of these constraints could get expensive to type check, i.e. not scalable.

[facundominguez]

Hello @josedusol. Thanks for the report. I tried this example but I got different errors. Please, could you share the complete source code of the example, and also the stack/cabal configuration that you are using?

[josedusol]

Hello @facundominguez !. Of course:

{-# LANGUAGE FlexibleContexts #-}
{-@ LIQUID "--extensionality" @-}
{-@ LIQUID "--reflection"     @-}
{-@ LIQUID "--higherorder"    @-}
{-@ LIQUID "--short-names"    @-}

module Test where

import Language.Haskell.Liquid.Equational
import Prelude hiding (id)

{-@ reflect id @-}         -- couldn't reflect predefined id, so introduced my own here
{-@ id :: a -> a @-}
id :: a -> a 
id x = x

{-@ assume compIdLeft :: f:(a -> b) -> { id . f = f } @-}
compIdLeft :: (a -> b) -> Proof
compIdLeft _ = ()

{-@ assume compAssoc :: f:(c -> d) -> g:(b -> c) -> h:(a -> b) 
                     -> { (f . g) . h = f . (g . h) } @-}
compAssoc :: (c -> d) -> (b -> c) -> (a -> b) -> Proof
compAssoc _ _ _ = ()

{-@ shuntingWrong :: f:(b -> c) -> g:(a -> b) -> h:(a -> c) 
                  -> f1:(c -> b) -> ({ f . f1 = id }, { f1 . f = id })
                  -> ({ f . g = h }) -> { g = f1 . h } @-}
shuntingWrong :: (b -> c) -> (a -> b) -> (a -> c)            
              -> (c -> b) -> (Proof, Proof)           
              -> Proof -> Proof
shuntingWrong f g h f1 (f1_prp1, f1_prp2) hyp =
      f1 . h                   ? hyp   
  ==. f1 . (f . g)             ? compAssoc f1 f g
  ==. (f1 . f) . g             ? f1_prp2  
  ==. id . g                   ? compIdLeft g
  ==. g 
  *** QED                     -- ERROR, not what LH expected, why?

{-@ shuntingOk :: Eq (a -> b)
             => f:(b -> c) -> g:(a -> b) -> h:(a -> c) 
             -> f1:(c -> b) -> ({ f . f1 = id }, { f1 . f = id })
             -> ({ f . g = h }) -> { g = f1 . h } @-}
shuntingOk :: Eq (a -> b)
         => (b -> c) -> (a -> b) -> (a -> c)            
         -> (c -> b) -> (Proof, Proof)           
         -> Proof -> Proof
shuntingOk f g h f1 (f1_prp1, f1_prp2) hyp =
      g == f1 . h                   ? hyp   
  ==. g == f1 . (f . g)             ? compAssoc f1 f g
  ==. g == (f1 . f) . g             ? f1_prp2  
  ==. g == id . g                   ? compIdLeft g
  ==. g == g 
  ==. True
  *** QED

cabal-version:  2.4

name:           test-lh
version:        0.1.0.0
build-type:     Simple

library
  exposed-modules:
      Test
  hs-source-dirs:
      src
  build-depends:
      liquidhaskell,
      liquid-base,
      liquid-prelude
  default-language: Haskell2010
  ghc-options: -fplugin=LiquidHaskell

Im using ghc-9.0.2, liquidhaskell-0.9.0.2.1 and liquid-base-0.4.15.1. Also, im using Z3 v4.12.2.
Thanks!

[josedusol]

Tested also with ghc-9.2.5 and liquidhaskell-0.9.2.5.0, same result.