Dafnyにシーケンスの誘導を促すにはどうしたらいいですか？

Question

私は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

編集（私の以前の答えが不正確だった）：私は誘導がinputシーケンスを含むので、Dafnyは、それ自体で誘導を行うことができないと思います。あなたが書いたコードには、Dafnyの誘導ヒューリスティクスを誘導してinputを誘導する場所がありません。

a lemma with input as an argumentと書く必要があります。すると、Dafnyは引数の誘導が役立つかもしれないと推測し、自動的に処理を進めることができます。実際に追加した仕様は必要ありません。

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..]); 
    } 
}