assignment1.v

Require Import Arith.
Require Import List.

(* This is the definition of insertion sort from "Coq in a Hurry": *)

Fixpoint insert n l :=
  match l with
    | nil     => n :: nil
    | a :: l' => if leb n a then n :: l else a :: insert n l'
  end.

Fixpoint sort l :=
  match l with
    | nil     => nil
    | a :: l' => insert a (sort l')
  end.

(* Solve one of the following exercises and hand in your solution via
   Moodle before Monday the 3rd of April 2017. *)

(* Exercise 1.  Coq has a built-in function `length` to compute the
   length of a list.  Use this function to prove that `sort` preserves
   the length of the input list.  That is, show that for any list `l`,
   it holds that

     length l = length (sort l)

   Hints.  (1) You probably need a lemma showing that for any value
   `a` and list `l`,
 
     S (length l) = length (insert a l)

   where `S` is Coq's successor function.  (2) If you have a goal
   containing ... if B then E1 else E2 ... and you don't care about
   the value of the boolean expression B, then you can get rid of the
   if-expression by the tactic

     destruct (B).

   This generates two goals, namely ... E_1 ... and ... E_2 ...
*)

(* Exercise 2. Coq has a built-in predicate `In` such that `In a l`
   holds if `a` is an element of the list `l`.  Use this predicate to
   prove that to prove that all elements in the input list to `sort`
   are also elements in the output list. That is, for all `l`

      In a l -> In a (sort l).

   Hint. You may need two auxiliary lemmas: On that states that `a`
   must be a member of `insert a l` and another that states that if
   `a` is an element of `l` then `a` is also an element of `insert b
   l:

   Theorem insert_In_this : forall a l, In a (insert a l).
   admit. Qed.

   Theorem insert_In_other : forall a b l, In a l -> In a (insert b l).
   admit. Qed.
*)