Как я могу побудить Дафни выполнить индукцию последовательности?

Мне интересно, что мне нужно добавить к следующему, чтобы он прошел дафни?

function mapper (input: seq<int>) : seq<(int, int)>
ensures |mapper(input)| == |input|
{
  if |input| == 0 then []
  else [(0,input[0])] + mapper(input[1..])   
}

// given [(0,n1), (0,n2) ... ] recovers [n1, n2, ...]
function retList (input: seq<(int, int)>, v : int) : seq<int>
ensures |input| >= |retList(input, v)|
ensures forall i :: 0 <= i < |input| && input[i].0 == v ==> input[i].1 in retList(input, v)
ensures forall x,y : int :: (x,y) in input && x == v ==> y in retList(input, v)
{
  if input == [] then []
  else if input[0].0 == v then [input[0].1] + retList(input[1..], v)
  else retList(input[1..], v)
}


method test (input: seq<int>)
requires |input| > 0 
{   
  assert retList(mapper(input), 0) == input;  
}

person JRR    schedule 16.04.2016    source источник


Ответы (1)


Редактировать (мой предыдущий ответ был неточным): я думаю, что, поскольку индукция включает последовательность input, Дафни не может провести индукцию сама по себе. В написанном вами коде нет места, которое побудило бы эвристику индукции Дафни попробовать индукцию на input.

Итак, вам нужно написать лемму с input в качестве аргумента, когда вы это сделаете, Дафни догадается, что индукция по аргумент может быть полезен, и тогда он сможет продолжить работу автоматически. На самом деле вам не нужна никакая спецификация, которую вы добавили.

function mapper (input: seq<int>) : seq<(int, int)>
{
  if |input| == 0 then []
  else [(0,input[0])] + mapper(input[1..])   
}

lemma allKeysRetainsInput(input: seq<int>)
   ensures retList(mapper(input), 0) == input
{ }  

// given [(v,n1), (v+1,n2), (v,n3), ... ] recovers [n1, n3,...]
function retList (input: seq<(int, int)>, v : int) : seq<int>
{
  if input == [] then []
  else if input[0].0 == v then [input[0].1] + retList(input[1..], v)
  else retList(input[1..], v)
}

method test (input: seq<int>)
  requires |input| > 0 
{   
  allKeysRetainsInput(input);
  assert retList(mapper(input), 0) == input;  
}

Если вы хотите увидеть немного больше доказательств, вы можете отключить автоматическую индукцию для этой леммы. Затем вам нужно будет вызвать гипотезу индукции вручную

lemma {:induction false} allKeysRetainsInput(input: seq<int>)
   ensures retList(mapper(input), 0) == input
{ 
  if input != [] {
    allKeysRetainsInput(input[1..]);
  }
}
person lexicalscope    schedule 18.04.2016