Proving in Dafny: A non-empty even sequence, is the concatenation of it's two halves

Question

I would like to prove this "trivial" lemma in Dafny. A non-empty even sequence, is the concatenation of it's two halves:

lemma sequence_division(sequ:seq<int>)
    requires sequ != []
    requires even(|sequ|)
    ensures sequ[0..|sequ|] == sequ[0..(|sequ|/2)]+sequ[|sequ|/2+1..|sequ|]
    //{}

The problem is I am not used to prove inductive lemmas without the typical datatypes (using match...case...). Do I have to use if or something?

I tried:

lemma sequence_division(sequ:seq<int>)
    requires sequ != []
    requires even(|sequ|)
    ensures sequ[0..|sequ|] == sequ[0..(|sequ|/2)]+sequ[|sequ|/2+1..|sequ|]
    {
        if |sequ| == 2 { assert sequ[0..|sequ|] == sequ[0..(|sequ|/2)]+sequ[|sequ|/2+1..|sequ|]; }
        //if |sequ| == 2 { assert sequ[0..2] == sequ[0..1]+sequ[1..2];}
    }

And it marks it an assertion violation (so the if syntax seems to work), so probably I am expressing something bad. This is the last step of a full proof I am doing so this is last possibility is important.

Any help?

Answer 1

The problem is that the lemma does not hold, which makes it impossible to prove. In the right-hand side of the equality in the postcondition, you're skipping an element. Here is a correct version of the lemma's postcondition:

  ensures sequ[0..|sequ|] == sequ[0..|sequ|/2] + sequ[|sequ|/2..|sequ|]

The lower bounds default to 0 and the upper bounds default to |sequ|, so you can simplify the condition to

  ensures sequ == sequ[..|sequ|/2] + sequ[|sequ|/2..]

You can simplify the lemma further, because neither of the two preconditions is necessary for the postcondition to hold. Finally, if you care to, you can make the lemma more general by parameterizing over the sequence-element type:

lemma sequence_division<T>(sequ: seq<T>)
  ensures sequ == sequ[..|sequ|/2] + sequ[|sequ|/2..]
{
}