// 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))
}

// Here is an example of how to prove by induction an interesting property about Length and Append
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);
    }
  }
}

// Use an inductive argument to prove the following lemma:
lemma {:induction false} AppendAssoc<T>(l1: List<T>, l2: List<T>, l3: List<T>)
  ensures Append(Append(l1, l2), l3) == Append(l1, Append(l2, l3))
{
  assume false;
}

// Here is a tail-recursive function computing the length of a list, which uses an auxiliary function for the tail calls
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)
}

// Try to prove that Length and Length' return the same result and understand why you fail
lemma {:induction false} LengthSameFail<T>(l : List<T>)
  ensures Length<T>(l) == Length'(l)
{
  assume false;
}

// Prove by induction the following more general property:
lemma {:induction false} LengthSameAux<T>(l : List<T>, acc : nat)
  ensures Length<T>(l) + acc == LengthAux<T>(l, acc)
{
  assume false;
}

// Now the proof is simple:
lemma {:induction false} LengthSame<T>(l : List<T>)
  ensures Length<T>(l) == Length'(l)
{
  LengthSameAux(l, 0);
}