Induction with relatively complicated constrained input gives an error.

[notcome]

I am trying to do induction of the following form: theorem :: x : Type1 -> { y : Type2 | condition x y = BTrue } -> { some proposition } where data BBool = BTrue = BFalse is my own version of boolean values. Any recursive call to the theorem (i.e. induction) will give an error of the following form:

:1:1-1:1: Error
  elaborate symbolic evaluation failed on:
      lqdc##is##O VV##F##19
  with error
      Unbound Symbol VV##F##19
 Perhaps you meant: y##a2iK, VV, x##a2iJ
  in environment
      lqdc##is##O := func(0, [A.Peano; bool])

I manage to reduce the problem to the following minimal pair:

{-@ reflect nonzero @-}
nonzero :: Peano -> BBool
nonzero O = BFalse
nonzero _ = BTrue

{-@ thm' :: { x : Peano | toNat x > 0 }
         -> { y : Peano | toNat y > 0 }
         -> { toNat (plus x y) > 0 } @-}
thm' :: Peano -> Peano -> Proof
thm' (S O) _ = trivial
thm' _ (S O) = trivial
thm' (S x@(S _)) (S y@(S _)) = (thm' x y, trivial) *** QED

{-@ thm :: { x : Peano | nonzero x = BTrue }
        -> { y : Peano | nonzero y = BTrue }
        -> { nonzero (plus x y) = BTrue } @-}
thm :: Peano -> Peano -> Proof
thm (S O) _ = trivial
thm _ (S O) = trivial
thm (S x@(S _)) (S y@(S _)) = (thm x y, trivial) *** QED

thm' uses the measure and the recursive call is fine. On the other hand, thm gives the unbound symbol error as illustrated above. (Note the proof itself is wrong, but that is of little concern here.)

Here is an minimal file that reproduces the issue. The two theorems of concern is at the bottom of the file.

[notcome]

In fact, induction is not necessary. Theorems with refined types have the same issue. Consider the following code:

{-@ thmRevInvolutive :: l : NatList
                     -> { reverse (reverse l) = l }
@-}
-- unimportant proofs

{-@ thmRevInjective :: l1 : NatList
                    -> { l2 : NatList | reverse l1 = reverse l2 }
                    -> { l1 = l2 }
@-}
thmRevInjective l1 l2 = l1
               `safeEq` (reverse (reverse l1) `since` thmRevInvolutive l1)
               `safeEq` reverse (reverse l2)
               `safeEq` (l2 `since` thmRevInvolutive l2)
                   ***  QED

There is no recursive call but a use of the refinement on l2, and LH crashes with the same unbound symbol error.

[ranjitjhala]

Can you submit the complete source so we can reproduce?

[ranjitjhala]

oops just saw link above...

[ranjitjhala]

@atondwal and @nikivazou this is a nasty bug, esp. in that I don't know what triggers it. (I had to keep doing random trial and error till it goes away...)

Still, its unlikely we will fix it before the upcoming deadline. More likely, we can use this (and other similar examples) for the regressions in the eventual PBE rewrite...

@notcome in the meantime, here is a version of your code that does work. Note that if you want to use a binder x in the OUT, you need to write x:{Peano | ...} -> OUT (as opposed to {x:Peano | ...} -> OUT.

{-@ LIQUID "--exact-data-con"                      @-}
{-@ LIQUID "--higherorder"                         @-}
{-@ LIQUID "--totality"                            @-}
{-@ LIQUID "--automatic-instances=liquidinstances" @-}

module A where

import qualified Prelude
import           Prelude ((+), Char, Int, Bool (..))
import Language.Haskell.Liquid.ProofCombinators

-- TODO: import Basics and Induction

{-@ data Peano [toNat] = O | S Peano @-}
data Peano = O | S Peano

{-@ measure toNat @-}
{-@ toNat :: Peano -> Nat @-}
toNat :: Peano -> Int
toNat O     = 0
toNat (S n) = 1 Prelude.+ toNat n

{-@ reflect plus @-}
plus :: Peano -> Peano -> Peano
plus O     n = n
plus (S m) n = S (plus m n)

{-@ safeEq :: x : a -> { y : a | x = y } -> a @-}
safeEq :: a -> a -> a
safeEq x y = x

{-@ data BBool = BTrue | BFalse @-}
data BBool = BTrue | BFalse

{-@ reflect negb @-}
negb :: BBool -> BBool
negb BTrue  = BFalse
negb BFalse = BTrue

{-@ reflect evenb @-}
evenb :: Peano -> BBool
evenb O         = BTrue
evenb (S O)     = BFalse
evenb (S (S n)) = evenb n

{-@ reflect nonzero @-}
nonzero :: Peano -> BBool
nonzero O = BFalse
nonzero _ = BTrue

{-@ test :: { plus (S O) (S O) = S (S O) } @-}
test = plus (S O) (S O)
   `safeEq` S (plus O (S O))
   `safeEq` S (S O)
   *** QED

{-@ lem :: n:Peano -> { toNat (S n) > 0 } @-}
lem :: Peano -> Proof
lem O     = trivial
lem (S n) = trivial

{-@ thm' :: x : {Peano | toNat x > 0 }
         -> y : {Peano | toNat y > 0 }
         -> { toNat (plus x y) > 0 } @-}
thm' :: Peano -> Peano -> Proof
thm' O     m = trivial
thm' (S n) m = lem (plus n m)

{-@ thm :: x:{Peano | nonzero x = BTrue }
        -> y:{Peano | nonzero y = BTrue }
        -> { nonzero (plus x y) = BTrue } @-}
thm :: Peano -> Peano -> Proof
thm O     m = trivial
thm (S n) m = trivial