如何证明在达夫尼的普遍介绍

如何解决如何证明在达夫尼的普遍介绍

我正在尝试寻找策略来证明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的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语句的forall子句，Dafny会为您推断出来。引理introGoal如下所示：

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

Automatic induction上有一个Dafny Power User注释，该注释可能会有所帮助，或者至少会提供一些其他示例。

PS。下一个自然的问题是如何进行存在消除。您可以使用Dafny的“ assign that that”语句进行操作。这是一个示例：

type X
predicate P(x: X)

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

在此Dafny Power User note中找到了一些示例。在this paper中找到了有关:|运算符的一些高级技术信息。