「SF-LC」3 List

Pair of Numbers

Q: Why name inductive?
A: Inductive means building things bottom-up, it doesn’t have to self-referencial (recursive)
(see below induction on lists as well.)

Inductive natprod : Type :=
  | pair (n1 n2 : nat).

Notation "( x , y )" := (pair x y).

Proof on pair cannot simply simpl.

Theorem surjective_pairing_stuck : ∀(p : natprod),
  p = (fst p, snd p).
Proof.
  simpl. (* Doesn't reduce anything! *)
Abort.

We have to expose the structure:

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 destruct

destruct

• destruct bool to true and false
• destruct nat to O and S n' (inductively defined)
• destruct pair to (n, m)

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

Inductive natlist : Type :=
  | nil
  | cons (n : nat) (l : natlist).

The ability of quosiquotation using Notation is awesome:

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 .

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:

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;

Reasoning lists

if we have in mind some proposition P that mentions a list l and we want to argue that P holds for all lists,
we can reason as follows

1. First, show that P is true of l when l is nil.
2. Then show that P is true of l when l is cons n l' for some number n and some smaller list l', assuming that P is true for l'.

Search

Search rev  (* list all theorems of [rev] *)

Coq Conditionals (if then else)

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