Pair of Numbers
Q: Why name
A: Inductive means building things bottom-up, it doesn’t have to self-referencial (recursive)
induction on lists as well.)
1 2 3 4 Inductive natprod : Type := | pair (n1 n2 : nat). Notation "( x , y )" := (pair x y).
Proof on pair cannot simply
1 2 3 4 5 Theorem surjective_pairing_stuck : ∀(p : natprod), p = (fst p, snd p). Proof. simpl. (* Doesn't reduce anything! *) Abort.
We have to expose the structure:
1 2 3 4 Theorem surjective_pairing : ∀(p : natprod), p = (fst p, snd p). Proof. intros p. destruct p as [n m**. simpl. reflexivity. Qed.
It only generate one subgoal, becasue
That’s because natprods can only be constructed in one way.
My take on
S n'(inductively defined)
The prove by case analysis (exhaustive) is just an application of the idea of destruction!
the idea simply destruct the data type into its data constructors (representing ways of constructing this data)
- Java class has only 1 way to construct (via its constructor)
- Scala case class then have multiple way to construct
Lists of Numbers
Generalizing the definition of pairs
1 2 3 Inductive natlist : Type := | nil | cons (n : nat) (l : natlist).
The ability of quosiquotation using
Notation is awesome:
1 2 3 Notation "x :: l" := (cons x l) (at level 60, right associativity). Notation "[ ]" := nil. Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
It’s exactly like OCaml, even for
at level 60 means it’s tightly than
+ at level 50 .
1 Notation "x ++ y" := (app x y) (right associativity, at level 60).
Instead of SML/OCaml’s
@, Coq chooses Haskell’s
hd with default
Coq function (for some reason) has to be total, so
hd require a
default value as 1st argument:
1 2 3 4 5 Definition hd (default:nat) (l:natlist) : nat := match l with | nil ⇒ default | h :: t ⇒ h end.
Induction on Lists.
The definition of inductive defined set
Each Inductive declaration defines a set of data values that can be built up using the declared constructors:
- a boolean can be either true or false;
- a number can be either O or S applied to another number;
- a list can be either nil or cons applied to a number and a list.
The reverse: reasoning inductive defined sets
Moreover, applications of the declared constructors to one another are the only possible shapes that elements of an inductively defined set can have, and this fact directly gives rise to a way of reasoning about inductively defined sets:
- a number is either O or else it is S applied to some smaller number;
- a list is either nil or else it is cons applied to some number and some smaller list;
if we have in mind some proposition
Pthat mentions a list
land we want to argue that
Pholds for all lists, we can reason as follows
- First, show that
- Then show that
Pis true of
cons n l'for some number
nand some smaller list
l', assuming that
1 Search rev (* list all theorems of [rev] *)
Coq Conditionals (
if then else)
1 2 3 4 5 6 Fixpoint nth_error' (l:natlist) (n:nat) : natoption := match l with | nil ⇒ None | a :: l' ⇒ if n =? O then Some a else nth_error' l' (pred n) end.
One small generalization: since the boolean type in Coq is not built-in. Coq actually supports conditional expr over any inductive defined typewith two constructors. First constructor is considered true and false for second.
Stuck in Proof
could be many cases
- wrong tactics
- wrong theroem!! (might derive to counterexample)
- wrong step (most hard to figure out)
- induction on wrong things