Lecture 3: Coq
==============
Goal of this lecture
Review Coq
Go over the homework assignments (Basics.v and Induction.v)
Questions about homeworks so far?
Concepts:
Inductive types
Inductive bool :=
| true
| false.
Inductive item :=
| rock
| paper
| scissors.
Inductive nat :=
| O
| S (n : nat).
Records
special case of inductive type
defines a struct with several fields
field names are accessors for those fields
Record nbpair := mkpair {
first : nat;
second : bool;
}.
Vernacular commands
Check first.
Check second.
Print nbpair.
Print first.
Search nbpair.
Definition
gives a name to a term
Definition p := mkpair 1 true.
Print p.
Eval compute in first p.
Fixpoints for recursive definitions
e.g., plus
Theorems
logical statements that refer to inductives, definitions, fixpoints, ..
theorem statement is the same kind of a term that appears in a definition
Theorem t1 : forall x y b, x = y -> mkpair x b = mkpair y b.
Theorem t2 : forall x b, mkpair (x+x-x) b = mkpair x (negb (negb b)).
Proofs
written in a language called Ltac
hypotheses: known facts (or available variables) in the current context
subgoals: proof steps can create multiple proof obligations
Global Set Default Goal Selector "!".
tactics
[intros]
[reflexivity]
simplification: [simpl]
rewriting: [rewrite], [replace]
[f_equal]
case analysis: [case_eq], [destruct]
induction: [induction]
arithmetic: [lia]
some automation: [eauto]
[apply]
https://coq.inria.fr/refman/coq-tacindex.html
Notation
1024
[+] and [*] are notation for [plus] and [mult]
Walk through [simpl] of some expressions
(S n) * (S m)
(S m) + n * (S m)
S (n + n * (S m))
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
Prop vs bool
Examples:
mult_plus_distr_r
mult_assoc