Учитывая несколько аксиом и свойство, как я могу структурировать доказательство свойства?

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