- Some experience with Functional Programming
- 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!