ilyasergey / pnp

Lecture notes for a short course on proving/programming in Coq via SSReflect.
https://ilyasergey.net/pnp
BSD 2-Clause "Simplified" License
159 stars 16 forks source link

complete binary trees exercise #4

Closed palmskog closed 6 years ago

palmskog commented 6 years ago

Here is a (in my opinion) fun exercise on the topic of proofs by induction that turns out to have a very succinct encoding in Ssreflect. We used this as a pen-and-paper exercise in a logic course for CS undergrads, and it worked quite well.