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