如何证明Dafny中的通用介绍

Question

我正在努力寻找策略来证明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)
{ }

感谢所有的想法

Answer 1

通用介绍是使用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
  // ...
}

因此，在大括号内，您可以证明一个x的P(x)。在forall语句之后，您可以假定通用量词

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

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

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

在Automatic induction上有一篇Dafny Power用户笔记，可能会有帮助，或者至少给出一些额外的例子。

PS。一个自然的下一个问题是如何进行存在消除法。你可以使用Dafny的"assign 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中可以找到有关:|运算符的一些高级技术信息。