// Consider the following algebraic data type:
datatype List<T> = Empty | Cons(head : T, tail : List<T>)

// And two recursively defined functions:
function Length<T>(l : List<T>) : nat
{
  if l.Empty? then
    0
  else
    1 + Length<T>(l.tail)
}

function Append<T>(l1 : List<T>, l2 : List<T>) : List<T>
{
  if l1.Empty? then
    l2
  else
    Cons(l1.head, Append<T>(l1.tail, l2))
}

/*
   Consider the following lemma in the previous lab.
 */
lemma {:induction false} AppendLength<T>(l1 : List<T>, l2 : List<T>)
  ensures Length(Append(l1, l2)) == Length(l1) + Length(l2)
{
  match l1
  {
  case Empty =>
  case Cons(head, tail) =>
    calc {
      Length(Append(l1, l2));
      == 
        Length(Append(Cons(head, tail), l2));
        == 
          Length(Cons(head, Append(tail, l2)));
          ==
            1 + Length(Append(tail, l2));
            ==
              {
                AppendLength<T>(tail, l2); // bring induction hypothesis into scope
              }
              1 + Length(tail) + Length(l2);
              ==
                Length(Cons(head, tail)) + Length(l2);
                ==
                  Length(l1) + Length(l2);
    }
  }
}

// You can instead add the lemma statement as a postcondition to the function (intrinsec verification)
function Append'<T>(l1 : List<T>, l2 : List<T>) : List<T>
  ensures Length(Append'(l1, l2)) == Length(l1) + Length(l2)
{
  if l1.Empty? then
    l2
  else
    Cons(l1.head, Append'<T>(l1.tail, l2))
}

// Exercise 1: try to add the associativity property to Append' (and fail). Explain why.

// Exercise 2: prove that Length' computes the same value as Length using an intrinsec property to the auxilliary function.

function LengthAux<T>(l : List<T>, acc : nat) : nat
{
  match l
  {
  case Empty => acc
  case Cons(head, tail) => LengthAux(tail, acc + 1)
  }
}

function Length'<T>(l : List<T>) : nat
{
  LengthAux(l, 0)
}