Class 9: Proof by Reflection

For this class, we will read the chapter on Reflection from Adam Chlipala's Certified Programming with Dependent Types (CPDT) textbook. CPDT is a really wonderful textbook explaining many of the fundamentals of proof in Coq. The chapter on Reflection is very useful (and cited and modified excerpts from it appeared in the QED at Large reading from last week).

You can find a reading guide and the discussion questions below. Slides for this class are here, and the demo Coq file is here.

Please note that this is due the morning before class, so that we can discuss it in person. And please install the artifact before Thursday's class.

This textbook comes with Coq source files! You can find them on the landing page for the textbook. I often find it very useful to step through and try the things written in this textbook as I go. This makes them feel more real.

Please write a short paragraph as a comment in the class forum thread about any one of the following discussion questions (you need to respond to just one question of your choice to get credit, though you're free to write more if interested):

1. Do you think that proofs by reflection are a valuable approach to proofs regardless of the underlying foundations? Or are there proof assistants with foundations for which proofs by reflection may not be useful? Why or why not?
2. What tradeoffs do you perceive between proofs by reflection and other styles of proof? Which do style you find most intuitive, and why? When might you choose one you find less intuitive over one you find more intuitive?
3. If you were designing a proof assistant from scratch, would you include any special support for proof by reflection? What kind of support might you add to make proof by reflection easier?
4. Is there anything about the examples Adam goes through that you find confusing? What and why?
5. Find an answer from someone else who pointed out something confusing for the question above. If tasked with doing so, is there any way you might build interfaces, tutorials, documentation, or automation to make that thing less confusing?
6. Write a paragraph responding to someone else's comment in the discussion forum.
7. Write a paragraph about any other single interesting thought, question, or idea that you had in response to the reading.

You may want to look at other people's responses before class in order to shape the discussion. And again remember that you need to answer just one question to get credit, though you are free to answer more if interested.