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を削除し、それを証明したいと言うはずです

content(without(x,l)) == content(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

クラスに関しては、BuiltInNames現在 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 式

最後に 1 点。Inox で利用可能なさまざまな構造の完全なリストを探している場合は、Inox のExpressionsファイルを参照してください。

于 2017-03-25T07:34:08.320 に答える