在 Inox/Welder 中证明集合的属性

Question

我想在 Inox/Welder 上证明集合的一些性质，但我缺少帮助我弄清楚如何去做的例子。假设我要证明：

content(y::xs).contains(x) && x != y ==> content(xs).contains(x)

我定义了属性:

def property(xs: Expr) =
  forall("x"::A,"y"::A){case (x,y) 
    content(ConsA(y,xs)).contains(x) && x !== y ==> content(xs).contains(x)
  }

但事实证明，这个属性不会编译，因为它没有很好地表述（显然错误的部分是.contains、&&、!==...）

那么，制定属性的正确方法是什么？这里我假设我有一个内容函数定义为：

val contentFunction = mkFunDef(contentID)("A") { case Seq(aT) => (
    Seq("l" :: T(list)(aT)), SetType(aT), { case Seq(l) =>
      if_ (l.isInstOf(T(cons)(aT))) {
        SetAdd(E(contentID)(aT)(l.asInstOf(T(cons)(aT)).getField(tail)), l.asInstOf(T(cons)(aT)).getField(head))
        } else_ {
          FiniteSet(Seq.empty, aT)
        }
    })
  }

关于证明部分，假设我得到了函数：

def without(x: A, xs: List[A]) = xs match{
   case Nil() => Nil()
   case y :: ys if(x == y) => without(x,ys)
   case y :: ys if(x != y) => y :: without(x,ys)  
}

应该从列表 xs 中删除 x 并说我想证明

content(without(x,l)) == content(l) -- Set(x)

你能给出一个如何做的草图吗？我应该使用 BuiltInNames 例如 SetDifference 吗？

Answer 1

编译错误

您看到的编译错误可能是由于属性公式中 case 后缺少的箭头所致。此外，请务必为 content.

使用正确的标识符

def property(xs: Expr) =
  forall("x"::A,"y"::A) { case (x,y) =>
    contentID(ConsA(y,xs)).contains(x) && x !== y ==> contentID(xs).contains(x)
  }

否则，属性使用 Inox DSL 编码看起来正确。

属性

的证明

关于证明本身，它认为without功能不是完全必要的。通过列表 xs.

上的结构归纳，证明应该会顺利进行

structuralInduction(property(_), "xs" :: T(List)(A)) { case (ihs, goal) =>
  ihs.expression match {
    case C(`Cons`, head, tail) => // Your case for Cons here.
    case C(`Nil`)              => // Your case for Nil here.
  }
}

ListAndTrees 展示了许多这样的证明。

`BuiltInName`

关于BuiltInNames class，它用于目前正在Welder中开发的Inox表达式的解析器。这很可能很快就会被放在一个单独的项目中。

此解析器在 Welder 中使用，因此您可以使用更友好的语法编写 Inox 表达式。例如，您的属性可以表示为：

def property(xs: Expr) =
  e"forall x, y. contains(content(Cons(y, $xs)), x) && x != y ==> contains(content($xs), x)"

Inox 表达式

最后一点。如果您正在寻找 Inox 中可用的不同构造的详尽列表，请查看 Inox 中的 Expressions 文件。

在 Inox/Welder 中证明集合的属性

Proving properties of sets in Inox/Welder

formal-verification

scala

leon

编译错误

属性

`BuiltInName`

Inox 表达式