Recitation 23

1. Explain in your own words how defining recursive functions in Coq is different than in OCaml. What additional restriction does Coq make? Why is it necessary?

2. Here is the induction principle on Coq lists:

   list_ind
     : forall (A : Type) (P : list A -> Prop),
       P nil ->
       (forall (a : A) (l : list A), P l -> P (a :: l)) ->
       forall l : list A, P l
   

   Explain each piece of this proposition. How does it correspond to structural induction as you learned it in CS 2800?

3. The notes for today say, “An inductive proof is a recursive program.” How would you explain that idea to someone who has not taken 3110?