Dafny.Невозможно установить существование LHS ... для последовательностей

Question

Для следующего кода я получаю, что он не может установить существование значений LHS, которые удовлетворяют такому предикату.Как я могу доказать, что правая сторона верна и такой х существует?

method Main() {
  var n : int := 10;
  var x : seq<int> :| n == |x| && forall i :: 0 <= i < |x| ==> -1 <= x[i] <= 1; 
}

https://rise4fun.com/Dafny/TiO5

Answer 1

Кажется, что даже что-то тривиальное, подобное этому, в данный момент не поддерживается:

method Main() {
  var n : int := 10;
  var y : seq<int> :|  y  == [3];
  var x : seq<int> :|  x  ==  y;
  var z : seq<int> :| |z| == |y|;
}

Дафни удается создать экземпляр x, но не z.Может опубликовать его в своих GitHub / Issues ?

Answer 2

Вы должны предоставить свидетеля. Следующее утверждение помогает:

method Main() {
  var n : int := 10;
  assert |[0, 0, 0, 0, 0, 0, 0, 0, 0, 0]| == 10;
  var x : seq<int> :| n == |x| && forall i :: 0 <= i < |x| ==> -1 <= x[i] <= 1; 
}

Однако, это подводит вас к следующему пункту, а именно: