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?
- 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?
- 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?