いくつかの公理とプロパティが与えられている場合、プロパティの証明をどのように構造化するのですか？

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; 
{ } 

しかしDafnyはそれを証明するために失敗しました。与えられた公理から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; 
}