0

我想证明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 并说我想证明

内容（没有（x，l））==内容（l）--设置（x）

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

4

1 回答 1

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

Regarding the BuiltInNames class, it is used in the parser of Inox expressions that is currently being developed within Welder. This very likely will be put in a separate project very soon.

This parser is used within Welder so that you can write Inox expressions using a somewhat friendlier syntax. For instance, your property could be stated as:

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

Inox Expressions

One last point. If you are looking for an exhaustive list of the different constructs available in Inox, have a look at the Expressions file in Inox.

于 2017-03-25T07:34:08.320 回答