Review1Review Session for First Midterm



General Notes

Standard vs. Advanced Exams

  • 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.

Grading

  • Meaning of grades:
    • 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 : X→Y)
          (g : Y→Z)
          (a : X) ⇒
         g (f a)
(1) Z
(2) ∀ Z : Type, Z
(3) ∀ X Y Z : Type, (X→Y) → (Y → Z) → X → Z
(4) ∀ X Y Z : Type, (X→Y) → (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:nat, x + 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:nat, x + 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:nat, beq_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 : ∀n, le n n
      | le_S : ∀n m, (le n m) → (le n (S m)).
What is the type of the following expression?
      ∀x:nat, le 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 : ∀n, le 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 : ∀n, le 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 : ∀n, le 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 : nat, appears_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:Prop, A → 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 R: Prop, P → (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 (H: gorgeous 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,H2) with
    | (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
    | (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

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
    | (n, v) :: l' ⇒ override (foo l' x) n 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 [x] l
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 → Z) l,
    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 xs) x
    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 l, R 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 h, R n l → R (S n) (h :: l)
  | c3 : ∀n l, R n l → R (S 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 l h, R n l → R (S n) (h :: l)
      | c3 : ∀n l, R (S n) l → 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 l, R n l → R (S n) (n :: l)
      | c3 : ∀n l, R (S n) l → 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!