## 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.)

1
2
3
4

Inductive natprod : Type :=
| pair (n1 n2 : nat).
Notation "( x , y )" := (pair x y).

Proof on pair cannot simply `simpl.`

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 `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

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 upusing 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

onlypossible 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 foralllists, we can reason as follows

- First, show that
`P`

is`true`

of`l`

when`l`

is`nil`

.- 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

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