在不锈钢中使用构造构造

问题描述：

我试图在不锈钢中证明如果两个列表具有相同的内容并且一个列表由x界定，那么另一个列表也由x界定。这样做，我被告知可以使用结构：在不锈钢中使用构造构造

forall(x => list.content.contains(x) ==> p(x))

引理将被写入（在松散的方式）为：

def lowerBoundLemma(l1: List[BigInt],l2: List[BigInt],x:BigInt) : Boolean = { 
    require(l1.content == l2.content && forall(y => l1.content.contains(y) ==> y <= x)) 
    forall(z => l2.content.contains(z) ==> z <= x) because{ 
     forall(z => l2.content.contains(z) ==> z <= x) ==| l1.content == l2.content | 
     forall(z => l1.content.contains(z) ==> z <= x) ==| trivial     | 
     forall(y => l1.content.contains(z) ==> y <= x) 
    } 
    }.holds

的问题是，我收到以下错误：

exercise.scala:12:48: error: missing parameter type 
require(l1.content == l2.content && forall(y => l1.content.contains(y) ==> y <= x))

有一次，我的类型添加到y我得到这个错误（指向的左括号包含括号）：

exercise.scala:12:81: error: ')' expected but '(' found. 
require(l1.content == l2.content && forall(y : BigInt => l1.content.contains(y) ==> y <= x))

任何想法为什么会发生这种情况？

我也尝试过的语法l.forall(_ <= x)但与像because和类型的==|结构结合我得到的错误：因为不是布尔的成员。

答

您面临的问题是来自Scala编译器前端的不锈钢。在Scala中，对于一个封闭的语法（与指定的参数类型）为(x: Type) => body（注意额外的括号！）

如果你想使用because和==|，你必须在你的源文件的开头添加import stainless.proof._ 。

在不锈钢中使用构造构造

相关推荐