dafny - 给定几个公理和一个属性，我如何构建该属性的证明？

Question

给定以下公理：

A>=0
forall n :: n>=0 && n<N1 ==> n < A
N1 >= A

N1==A我们想用 Dafny来证明这一点。

我尝试过遵循 Dafny 程序：

function N1(n: int,A: int):bool
  requires A>=0 && n>=0 
{
  if n==0 && A<=n
  then true else
  if n>0 
    && A<=n  
    && forall k::
       (if 0<=k && k<n 
        then A>k else true) 
  then true
  else false
}

lemma Theorem(n: int,A: int)
requires A>=0 && n>=0 && N1(n,A)
ensures n==A;
{ }

但达夫尼未能证明这一点。有没有办法N1==A从给定的公理？

Answer 1

Dafny 可以证明它很好，但它需要更多帮助：

predicate P(n:int, N1:int)
{
  n >= 0 && n < N1
}

lemma Lem(A:int, N1:int)
  requires A>=0
  requires forall n :: P(n, N1) ==> n < A
  requires  N1 >= A
  ensures N1 == A 
{ 
  if(N1 > A)
  {
    assert A >= 0 && A < N1;
    assert P(A, N1);
    assert A < A;
    assert false;
  }
  assert N1 <= A;  
}

证明是矛盾的，是相当标准的。唯一的 Dafny 特定证明部分是我们必须为n >= 0 && n < N1. P我们通过将其作为谓词引入来给属性命名。引入 P 的要求来自 Dafny 与量词实例化（触发匹配）如何在底层 SMT 求解器（Z3）中工作的一些细节的交互。

您可能更喜欢这样写引理：

lemma Lem(A:int, N1:int)
  requires A>=0
  requires forall n :: P(n, N1) ==> n < A
  requires  N1 >= A
  ensures N1 == A 
{ 
   calc ==>
   {
     N1 > A;
        {assert P(A, N1);}
     A < A;
     false;
   }  
   assert N1 <= A;
}