Blog|Meta Topics|Advanced Topics

Software Technology: Transition to Coq

Assumed Knowledge:
  • Some experience with Functional Programming
Learning Outcomes:
  • Become familiar with the basic constructs of proofs in Coq

All the material for this topic is contained in chapters Preface and Basics of the Software Foundations text.

Some interesting points to come out of this:

  • Inductive defines new data
  • Definition defines new computation and Compute is how we invoke that computation.
  • Functions are defined in pattern matching style.
  • Example defines new goal/assertion
  • It seems like all computation over inductive data types is done with match expressions. That sounds about-right.
  • It looks like simpl might compute for us and reflexivity dispatches things that are the same on the left as they are on the right.
  • Check will tell us the type of a value.
  • Types are given in the Haskell.
  • We have enumerated types and so-called “inductive” types.
  • Constructors seem a lot like functions - they even have the same type!