These are sample questions that likely reflect the level of difficulty
and style of questions on the actual exam.  The number of questions
and topics may, of course, differ.
--------------------------------------------------------------------


(1) Complete the following inductively defined relation in such a way that merge
l1 l2 l3 is provable exactly when l3 is an in-order merge of l1 and l2 .

Inductive merge {X:Type}
    : list X -> list X -> list X -> Prop :=

(2) True or false - induction is necessary to prove the following proposition?

              forall n:nat, 2 * n = n + n

(3) Consider the following definitions:

    Definition override {X} (f : nat -> X) (k1 : nat) (v : X) (k2 : nat) :=
      if beq_nat k1 k2 then v else f k2.

    Fixpoint foo {X} (l : list (nat * X)) (x : X) :=
       match l with
       | [] => fun m : nat => x
       | (n, v) :: l' => override (foo l' x) n v
       end.

    What does foo [(1,3), (3,4)] 20 43 evaluate to?

    (1) 1
 
    (2) 3

    (3) 4

    (4) 20

    (5) 43

(4) Recall the definition of map :

    Fixpoint map {X Y} (f : X -> Y) (l : list X) :=
      match l with
      | [] => []
      | x :: xs => f x :: map f xs
    end.

    Is the following proposition provable?

    Theorem map_comp : forall X Y Z (f : X -> Y) (g : Y -> Z) l,
        map (fun x => g (f x)) l = map g (map f l)


    (1) Yes

    (2) No

    Justify your answer.  

(5)  What is the type of the following expression?

        exists x:nat, x + x = 5


(6) Consider the following definition:

    Inductive gorgeous : nat -> Prop :=
     | g_0 : gorgeous 0
     | g_plus3 : forall n, gorgeous n -> gorgeous (3+n)
     | g_plus5 : forall n, gorgeous n -> gorgeous (5+n).

   What is the type of this expression?

   fun (n:nat) => fun (H: gorgeous n) =>
                     g_plus5 (8+n) (g_plus5 (3+n) (g_plus3 n H)).


(7) How many elements inhabit this type?

    Inductive baz : Type :=
      | x : baz -> baz
      | y : baz -> bool -> baz.


(8) Consider the following:

    Inductive mumble : Type :=
      | a : mumble
      | b : mumble -> nat -> mumble
      | c : mumble.

    Inductive grumble (X:Type) : Type :=
      | d : mumble -> grumble X
      | e : X -> grumble X.

    Which of the following are well-typed?

    1. d (b a 5)
    2. d mumble (b a 5)}
    3. d bool (b a 5)}
    4. e bool true}
    5. e mumble (b c 0)}
    6. e bool (b c 0)}
    7. c


(9) Write an inductively defined proposition "appears_in" that holds whenever value "a"
    appears at least once as a member of a list "l".

       Inductive appears in X:Type (a:X) : list X -> Prop :=

    Now, use appears_in to define an inductive proposition "no_repeats X
    l", which should be provable exactly when "l" is a list (with elements
    of type "X") where every member is different from every other. For
    example, no_repeats nat [1,2,3,4] and no_repeats bool [] should be
    provable, while no_repeats nat [1,2,1] and no_repeats bool [true,true]
    should not be.

(10) Decorate the following definition so that it would be considered well-typed:

     Fixpoint fold f l b :=
       match l with
        | nil => b
        | h :: t => f h (fold f t b)
       end.