时间戳

首页 > 解决方案 > 如何在 Dafny 中证明通用引入

dafny - 如何在 Dafny 中证明通用引入

问题描述

我正在尝试寻找策略来证明 Dafny 中普遍量化的断言。我看到 Dafny 很容易证明普遍消除：

predicate P<X>(k:X)
 lemma unElim<X>(x:X)    
 ensures  (forall a:X  :: P(a)) ==> P(x)
 {  }
lemma elimHyp<H> () 
  ensures forall k:H :: P(k)
 lemma elimGoal<X> (x:X)
    ensures P(x)
  { elimHyp<X>(); }

但我找不到如何证明引入规则：

//lemma unInto<X>(x:X)    
// ensures  P(x) ==> (forall a:X :: P(a))
// this definition is wrong 

lemma introHyp<X> (x:X)
    ensures P(x)
lemma introGoal<H> () 
  ensures forall k:H :: P(k)
{ }

所有想法都表示赞赏

标签： dafny

解决方案

通用介绍是使用 Dafny 的forall语句完成的。

lemma introHyp<X>(x: X)
  ensures P(x)

lemma introGoal<H>() 
  ensures forall k: H :: P(k)
{
  forall k: H
    ensures P(k)
  {
    introHyp<H>(k);
  }
}

一般来说，它看起来像这样：

forall x: X | R(x)
  ensures P(x)
{
  // for x of type X and satisfying R(x), prove P(x) here
  // ...
}

所以，在花括号内，你证明P(x)了一个x。在forall陈述之后，您可以假设全称量词

forall x: X :: R(x) ==> P(x)

如果像introGoal上面我所说的那样，语句的主体forall恰好是一个引理调用，并且该引理的后置条件是您在语句ensures子句中的内容forall，那么您可以省略该语句的ensures子句，forallDafny 会为您推断. 引理introGoal看起来像这样：

lemma introGoal<H>() 
  ensures forall k: H :: P(k)
{
  forall k: H {
    introHyp(k);
  }
}

有一个关于自动感应的 Dafny 高级用户说明可能会有所帮助，或者至少给出了一些额外的例子。

PS。一个自然的下一个问题是如何进行存在主义消除。您可以使用 Dafny 的“assign such that”语句来完成。这是一个例子：

type X
predicate P(x: X)

lemma ExistentialElimination() returns (y: X)
  requires exists x :: P(x)
  ensures P(y)
{
  y :| P(y);
}

此Dafny 高级用户说明中提供了一些示例。本文:|提供了一些关于运营商的先进技术信息。

推荐阅读