L03: Coq
Done: Basics.v and Induction.v
Questions?
Concepts:
Inductive types
Booleans (a simple enumerated type)
Nats (defined by a collection of inductive rules)
Definition
gives a name to a term
Fixpoints for recursive definitions
e.g. plus
Proofs
simplification
rewriting
case analysis
induction
Some notation
1024
plus, mult
Why is termination important?
Let's say we can write:
Fixpoint loop (x:nat) : ? := loop x
[Coq will reject this]
What is the return type?
Every function must have a return type
Nat? Bool? False?
Fixpoint loop (x:nat) : False := loop x.
What is loop 0?
False
Oops, we can proof False without hypothesis
Example: mult_plus_distr_r, mult_assoc