1

上下文：我正在证明有关 Haskell 快速排序实现的一些属性。以下代码是定义非确定性permute函数所需的全部内容。请注意，我使用的是LList而不是 Haskell 的基本[]类型。问题领域是permute_LCons_expansion_correct定理（它不是一个定理）。

-- Data. A list is either `LNil` or constructed with a `vhead` element and a
-- `vtail` list.
data LList a = LNil | LCons {vhead :: a, vtail :: LList a}

-- Function. Append two lists.
{-@ reflect lappend @-}
lappend :: LList a -> LList a -> LList a
lappend LNil ys = ys
lappend (LCons x xs) ys = LCons x (lappend xs ys)

-- Function. Construct a list with 1 element.
{-@ reflect llist1 @-}
llist1 :: a -> LList a
llist1 x = LCons x LNil

-- Function. Construct a list with 2 elements.
{-@ reflect llist2 @-}
llist2 :: a -> a -> LList a
llist2 x y = llist1 x `lappend` llist1 y

-- Function. Map a list-function over a list and concatenate the resulting
-- lists (i.e. list-monadic bind).
{-@ reflect lbind @-}
lbind :: LList a -> (a -> LList b) -> LList b
lbind LNil f = LNil
lbind (LCons x xs) f = f x `lappend` lbind xs f

-- Function. Map a function over a list.
{-@ reflect lmap @-}
lmap :: (a -> b) -> (LList a -> LList b)
lmap f LNil = LNil
lmap f (LCons x xs) = LCons (f x) (lmap f xs)

{-@ reflect lmap2 @-}
-- Function. Map a binary function over two lists (zipping).
lmap2 :: (a -> b -> c) -> LList a -> LList b -> LList c
lmap2 f xs ys = lbind xs (\x -> lbind ys (\y -> llist1 (f x y)))

-- Function. Nondeterministically split a list into two sublists.
{-@ reflect split @-}
split :: LList a -> LList (LList a, LList a)
split LNil = llist1 (LNil, LNil)
split (LCons x xs) =
  split xs
    `lbind` \(ys, zs) ->
      llist1 (LCons x ys, zs) `lappend` llist1 (ys, LCons x zs)

-- Function. Nondeterministically permute a list.
{-@ reflect permute @-}
permute :: LList a -> LList (LList a)
permute LNil = llist1 LNil
permute (LCons x xs) =
  split xs `lbind` \(ys, zs) ->
    lmap2
      (\ys' zs' -> ys' `lappend` llist1 x `lappend` zs')
      (permute ys)
      (permute zs)

-- Function. The expanded form of `permute` on an `LCons`.
{-@ reflect permute_LCons_expansion @-}
permute_LCons_expansion :: a -> LList a -> LList (LList a)
permute_LCons_expansion x xs =
  split xs
    `lbind` ( \(ys, zs) ->
                lmap2
                  (\ys' zs' -> ys' `lappend` llist1 x `lappend` zs')
                  (permute ys)
                  (permute zs)
            )

-- Theorem. `permute_LCons_expansion` corresponds to `permute` on an `LCons`.
{-@
permute_LCons_expansion_correct :: x:a -> xs:LList a ->
  {permute (LCons x xs) = permute_LCons_expansion x xs}
@-}
permute_LCons_expansion_correct :: a -> LList a -> Proof
permute_LCons_expansion_correct x xs =
  permute (LCons x xs)
    ==. split xs
      `lbind` ( \(ys, zs) ->
                  lmap2
                    (\ys' zs' -> ys' `lappend` llist1 x `lappend` zs')
                    (permute ys)
                    (permute zs)
              )
    ==. permute_LCons_expansion x xs
    *** QED

在permute_LCons_expansion_correct中，方程应该是正确的，因为中间的表达式只是LConscase的主体，permute也是 的定义permute_LCons_expansion。但是，当我编译时，我得到这个 LH 错误：

❯ cabal build
Build profile: -w ghc-8.10.3 -O1
{{I have removed project files info}}

**** LIQUID: UNSAFE ************************************************************

src/Test.hs:83:9: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : (Test.LList (Test.LList a))
    .
    is not a subtype of the required type
      VV : {VV : (Test.LList (Test.LList a)) | permute (LCons x xs) == VV}
    .
    in the context
      xs : (Test.LList a)

      x : a
   |
83 |     ==. split xs
   |         ^^^^^^^^...

为什么 LH 不承认隐式相等？请注意，我使用的是(==.)fromLanguage.Haskell.Equational而不是Language.Haskell.ProofCombinators.

配置：

  • ghc 版本 8.10.3
  • LiquidHaskell 版本 0.8.6.0
  • 阴谋集团 3.2.0.0 版
4

0 回答 0