# General Notes

• Unlike the homework assignments, we will make up two completely separate versions of the exam — a "standard exam" and an "advanced exam." They will share some problems, but there will be problems on each that are not on the other.
You can choose to take whichever one you want at the beginning of the exam period.

• A = mastery of all or almost all of the material
• B = good understanding of most of the material, perhaps with a few gaps
• C = some understanding of most of the material, with substantial gaps
• D = major gaps
• F = didn't show up / try
• There is no pre-determined curve. We'd be perfectly delighted to give everyone an A (for the exam, and for the course).
• Except: A+ grades will be given only for completing the advanced track.
• Standard and advanced exams will be graded relative to different expectations (i.e., "the material" is different)

### Hints

• On each version of the exam, will be at least one problem taken more or less verbatim from a homework assignment.
• On the advanced version, there will be an informal proof.

# Expressions and Their Types

Thinking about well-typed expressions and their types is a great way of reviewing many aspects of how Coq works...

What is the type of the following expression?
fun x:nat ⇒ x :: []
(1) nat
(2) list nat
(3) nat list X
(4) nat list nat
(5) nat nat
(6) Not typeable
(N.b.: On an actual exam, this might not be multiple choice!)

What is the type of the following expression?
((2 :: 3 :: []) :: []) :: []
(1) nat
(2) list list
(3) list nat
(4) list (list nat)
(5) list (list (list nat))
(6) Not typeable

What is the type of the following expression?
fun (X Y Z : Type)
(f : XY)
(g : YZ)
(a : X) ⇒
g (f a)
(1) Z
(2) Z : Type, Z
(3) X Y Z : Type, (XY) (Y Z) X Z
(4) X Y Z : Type, (XY) (Y Z) X Y
(5) X Y Z : Type, X Y Z
(6) X Y Z : Type, X Z
(7) Not typeable

What is the type of the following expression?
x:natx + 3 = 1 + x + 2
(1) nat
(2) nat nat
(3) nat Prop
(4) Prop
(5) Type
(6) True
(7) Not typeable

What is the type of the following expression?
fun x:nat ⇒ x + 3 = 1 + x + 2
(1) nat
(2) nat nat
(3) nat Prop
(4) x:nat, x + 3 = 1 + x + 2
(5) Type
(6) Not typeable

What is the type of the following expression?
x:natx + x = 5
(1) False
(2) Prop
(3) nat Prop
(4) x:nat, x + x = 5
(5) Type
(6) Not typeable

What is the type of the following expression?
nat  list nat
(1) Type
(2) nat list nat
(3) list nat
(4) x:nat, list nat
(5) nat
(6) Not typeable

What is the type of the following expression?
x:natbeq_nat x x
(1) Type
(2) nat list nat
(3) list nat
(4) x:nat, list nat
(5) x:nat, Prop
(6) Prop
(7) Not typeable

Recall the inductively defined proposition
Inductive le : nat  nat  Prop :=
| le_n : nle n n
| le_S : n m, (le n m (le n (S m)).
What is the type of the following expression?
x:natle x x
(1) Prop
(2) nat Prop
(3) fun x:nat le x x
(4) x:nat, le x x
(5) True
(6) Not typeable

Recall the inductively defined proposition
Inductive le : nat  nat  Prop :=
| le_n : nle n n
| le_S : n m, (le n m (le n (S m)).
What is the type of the following expression?
le 5
(1) Prop
(2) nat Prop
(3) nat nat Prop
(4) x:nat, le 5 x
(5) True
(6) False
(7) Not typeable

Recall the inductively defined proposition
Inductive le : nat  nat  Prop :=
| le_n : nle n n
| le_S : n m, (le n m (le n (S m)).
What is the type of the following expression?
le_S 5
(1) Prop
(2) nat Prop
(3) m:nat, le 5 m
(4) le 5 le (S 5)
(5) m:nat, (le 5 m) le 5 (S m)
(6) Not typeable

Recall the inductively defined proposition
Inductive le : nat  nat  Prop :=
| le_n : nle n n
| le_S : n m, (le n m (le n (S m)).
What is the type of the following expression?
le_n 5 5
(1) Prop
(2) nat Prop
(3) m:nat, le 5 m
(4) le 5 le (S 5)
(5) m:nat, (le 5 m) le 5 (S m)
(6) le 5 5
(7) Not typeable

(Discussion of Coq's view of the universe...)

Recall the inductively defined proposition
Inductive or (P Q : Prop) : Prop :=
| or_introl : P  or P Q
| or_intror : Q  or P Q.
What is the type of the following expression?
or_introl True
(1) Prop
(2) bool Prop
(3) Q: Prop, or True Q
(4) Q: Prop, Q
(5) Q: Prop, True or True Q
(6) Q: Prop, Q True
(7) Not typeable

Recall the inductively defined proposition
Inductive or (P Q : Prop) : Prop :=
| or_introl : P  or P Q
| or_intror : Q  or P Q.
What is the type of the following expression?
or_intror False True
(1) Prop
(2) bool bool Prop
(3) True or False True
(4) Prop, or False True
(5) Q: Prop, or True False
(6) Q: Prop, False or True False
(7) Not typeable

Recall the inductively defined proposition
Inductive and (P Q : Prop) : Prop :=
conj : P  Q  (and P Q).
What is the type of the following expression?
conj
(1) Prop
(2) bool bool
(3) P Q : Prop, P Q and P Q
(4) P Q and P Q
(5) Prop Prop Prop
(6) Not typeable

The appears_in relation expresses that an element a appears in a list l.
Inductive appears_in (X:Type) (a:X)
: list X  Prop :=
| ai_here : l,
appears_in X a (a::l)
| ai_later : b l,
appears_in X a l
appears_in X a (b::l).
Complete the definition of the following proof object:
Definition appears_example :
x y : natappears_in nat 4 [x;4;y] :=

Write an expression of the following type:
(nat  False False

Write an expression of the following type:
(A:Prop) , (A  False A  False

Write an expression of the following type:
(A:Prop),
(A  False
(A  True
A
False  True

Write an expression of the following type:
A:PropA  A  A

# Inductive Definitions

Recall that a list l3 is an ``in-order merge'' of lists l1 and l2 if it contains all the elements of l1, in the same order as l1, and all the elements of l2, in the same order as l2, with elements from l1 and l2 interleaved in any order. For example, the following lists (among others) are in-order merges of [1;2;3] and [4;5]:
[1;2;3;4;5]
[4;5;1;2;3]
[1;4;2;5;3]
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 :=

# Tactics

When is the generalize dependent tactic useful?
(Briefly explain.)

What is the difference between apply and apply ... in?
(Briefly explain.)

To prove the following proposition, which tactics will we need besides intros and reflexivity?
n:nat, 2 × n = n + n
(1) simpl, and rewrite plus_0_r
(2) induction, simpl and rewrite plus_0_r
(3) destruct, and rewrite plus_0_r
(4) only rewrite plus_0_r
(5) only induction
(6) none of the above

To prove the following proposition, which tactics will we need besides intros, rewrite, and reflexivity?
n m p : nat,
ble_nat n m = true
ble_nat (p + n) (p + m) = true.
(1) only simpl
(2) simpl, destruct p and induction n
(3) simpl, and destruct n
(4) simpl, and induction p
(5) simpl, and induction n
(6) none of the above

To prove the following proposition, which tactics will we need besides intros and apply?
P Q RPropP  (P  Q (R  P).
(1) split, inversion, left, and right
(2) inversion, left, and right
(3) inversion and one of left and right
(4) split, left, and right
(5) only right
(6) none of the above

# Proof Objects

Recall the definition of beautiful:
Inductive beautiful : nat  Prop :=
b_0   : beautiful 0
| b_3   : beautiful 3
| b_5   : beautiful 5
| b_sum : n m,
beautiful n
beautiful m
beautiful (n+m).
What is the type of this expression?
fun (n : nat) ⇒
fun (H : beautiful n) ⇒
b_sum n (n + 0) H (b_sum n 0 H b_0)
(1) n, beautiful n beautiful (n+0)
(2) beautiful n beautiful (2×n)
(3) n, beautiful n beautiful (n+(n+0))
(4) beautiful (n+(n+0))
(5) Not typeable

Recall the definition of gorgeous:
Inductive gorgeous : nat  Prop :=
g_0 :
gorgeous 0
| g_plus3 : n,
gorgeous n  gorgeous (3+n)
| g_plus5 : n,
gorgeous n  gorgeous (5+n).
What is the type of this expression?
fun (n:nat) ⇒
fun (Hgorgeous n) ⇒
g_plus5 (8+n) (g_plus5 (3+n) (g_plus3 n H)).
(1) n, gorgeous (8+n) gorgeous (13+n)
(2) n, gorgeous (8+n) gorgeous (3+n)
(3) n, gorgeous (n) gorgeous (3+n)
(4) n, gorgeous n gorgeous (13+n)
(5) Not typeable

What is the type of this expression?
fun P Q R H1 H2 ⇒
match (H1,H2with
| (conj HP _conj _ HR) ⇒ conj P R HP HR
end.
(1) P Q R, P Q Q R P R
(2) P Q R, Q P R Q P R
(3) P Q R, P R
(4) P Q R, P Q Q R P R
(5) Not typeable

What is the type of this expression?
fun P Q H ⇒
match H with
| or_introl HP ⇒ or_intror Q P HP
| or_intror HQ ⇒ or_introl Q P HQ
end.
(1) P Q H, Q P H
(2) P Q, P Q P Q
(3) P Q H, P Q Q P H
(4) P Q, P Q Q P
(5) Not typeable

# Functional Programming

Recall the definition of override:
Definition override {X} (f : nat  X) (k1 : nat) (v : X) (k2 : nat) :=
if beq_nat k1 k2 then v else f k2.
Consider the definition of the following function:
Fixpoint foo {X} (l : list (nat × X)) (x : X) :=
match l with
| [] ⇒ fun m : nat ⇒ x
| (nv) :: l' ⇒ override (foo l' xn v
end.
What does foo [(1,3), (3,4)] 20 43 evaluate to?
(1) 1
(2) 3
(3) 4
(4) 20
(5) 43

Recall the definition of override:
Definition override {X} (f : nat  X) (k1 : nat) (v : X) (k2 : nat) :=
if beq_nat k1 k2 then v else f k2.
Consider the definition of the following function:
Fixpoint foo {X} (l : list (nat × X)) (x : X) :=
match l with
| [] ⇒ fun m : nat ⇒ x
| (nv) :: l' ⇒ override (foo l' xn v
end.
What does foo [(1,3), (1,4)] 20 1 evaluate to?
(1) 1
(2) 3
(3) 4
(4) 20
(5) 43

Recall the definition of fold:
Fixpoint fold {X Y
(f : X  Y  Y
(y : Y
(l : list X) :=
match l with
| [] ⇒ y
| x :: xs ⇒ f x (fold f y xs)
end
Consider now the following function:
fun X (l : list X) (x : X) ⇒ fold cons [xl
Which of these functions does the same thing as the previous one?
(1) rev
(2) cons
(3) snoc
(4) map
(5) app

# Judging Propositions

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 : X Y Z (f : X  Y) (g : Y  Zl,
map (fun x ⇒ g (f x)) l = map g (map f l)
(1) Yes
(2) No

Recall the definition of rev:
Fixpoint rev {X} (l : list X) :=
match l with
| [] ⇒ []
| x :: xs ⇒ snoc (rev xsx
end.
Is the following proposition provable?
Theorem t1 : X (l1 l2 : list X),
rev (l1 ++ l2) = rev l1 ++ rev l2.
(1) Yes
(2) No

Is the following proposition provable?
True = False
(1) Yes
(2) No

Recall the definition of fold:
Fixpoint fold {X Y : Type
(f : X  Y  Y
(y : Y
(l : list X) :=
match l with
| [] ⇒ y
| x :: xs ⇒ f x (fold f y xs)
end
Is the following proposition provable?
Theorem foo : X (l : list (list X)),
fold (fun a b ⇒ b ++ rev a) [] l =
rev (fold (fun a b ⇒ a ++ b) [] l).
(1) Yes
(2) No

# More Type Checking

Consider the following inductive definition:
Inductive R : nat  list nat  Prop :=
| c1 : R 0 []
| c2 : n h lR n l  R (S n) (h :: l).
Which of the following propositions is not provable?
(1) R 2 [1,0]
(2) R 0 []
(3) R 10 [1,2,1,0]
(4) R 4 [3,2,1,0]

Consider the following inductive definition:
Inductive R : nat  list nat  Prop :=
| c1 : R 0 []
| c2 : n l hR n l  R (S n) (h :: l)
| c3 : n lR n l  R (S nl.
Which of the following propositions is not provable?
(1) R 2 [1,0]
(2) R 0 []
(3) R 10 [1,2,1,0]
(4) R 3 [3,2,1,0]

Consider the following inductive definition:
Inductive R : nat  list nat  Prop :=
| c1 : R 0 []
| c2 : n l hR n l  R (S n) (h :: l)
| c3 : n lR (S nl  R n l.
Which of the following propositions is not provable?
(1) R 2 [1,0]
(2) R 0 []
(3) R 10 [1,2,1,0]
(4) R 3 [3,2,1,0]

Consider the following inductive definition:
Inductive R : nat  list nat  Prop :=
| c1 : R 0 []
| c2 : n lR n l  R (S n) (n :: l)
| c3 : n lR (S nl  R n l.
Which of the following propositions is not provable?
(1) R 2 [1,0]
(2) R 1 [1,2,1,0]
(3) R 3 [3,0,1,0]
(4) R 1 [3,2,1,0]

Good luck on the exam!