Тривиальная лемма не доказана - PullRequest
Новая
       46

Тривиальная лемма не доказана

1 голос
/ 27 марта 2020

Я определил следующие datatype, function и lemma для σ-алгебры в Дафни. Мне кажется, что лемма должна доказать, но я получаю нарушение утверждения при последнем утверждении assert. 

datatype Alg = Empty | Complement(a: Alg) | Union(b: Alg, c: Alg)

const S : set<int>

function eval(X: Alg) : set<int>
    decreases X;
{
    match X
    case Empty => {}
    case Complement(a) => S - eval(X.a)
    case Union(b,c) => eval(X.b) + eval(X.c)
}

lemma algebra()
    ensures forall x :: exists y :: eval(y) == S - eval(x);
{
    var l : Alg;
    var c :| c == Complement(l);
    assert eval(c) == S - eval(l);
    assert exists a {:induction false} :: eval(a) == S - eval(l);
    assert forall x :: exists y :: eval(y) == S - eval(x);   // this statement does not prove
}

Мое доказательство следует этой логике c: пусть l будет произвольным Alg ( σ-алгебра) и пусть c будет дополнением к l. Таким образом, для l существует c, который оценивается как S - оценка l. Поскольку l был произвольным Alg, разве это не должно обобщать для всех Alg?

Обратите внимание, я также попытался выписать последнее утверждение assert следующим образом, но все же получил нарушение. 

assert forall x {:induction false} :: exists y {:induction false} :: eval(y) == S - eval(x);

Есть идеи, почему это не доказывает, или есть предложение, которое я мог бы попробовать?

...