How can I prompt Dafny to perform induction on a sequence?

Question

I'm wondering what I need to add to the following to make it pass dafny?

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

Answer 1

Edit (my earlier answer was inaccurate): I think that because the induction involves the input sequence, that Dafny can't do the induction by itself. There isn't a place in the code you have written that would prompt Dafny's induction heuristics to try induction on input.

So you need to write a lemma with input as an argument, when you do that Dafny will guess that induction on the argument might be helpful, and then will be able to proceed automatically. You don't actually need any of the specification you have added.

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

If you want to see a bit more of the proof, you can turn automatic induction off for that lemma. Then you will need to call the induction hypothesis manually

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