## Review (only in slide)

1
2

Theorem review2: ∀b, (orb true b) = true.
Theorem review3: ∀b, (orb b true) = true.

Whether or not it can be just `simpl.`

depending on the definition of `orb`

.

In *Proof Engineering*, we probably won’t need to include `review2`

but need to include `review3`

in library.

Why we have

`simpl.`

but not`refl.`

?

## Proving `0`

is a “neutral element” for `+`

(additive identity)

### Proving `0 + n = n`

1
2
3

Theorem plus_O_n : forall n : nat, 0 + n = n.
Proof.
intros n. simpl. reflexivity. Qed.

This can be simply proved by *simplication* bcuz the definition of `+`

is defined by pattern matching against 1st operand:

1
2
3
4
5

Fixpoint plus (n : nat) (m : nat) : nat :=
match n with
| O ⇒ m
| S n' ⇒ S (plus n' m)
end.

We can observe that if `n`

is `0`

(`O`

), no matter `m`

is, it returns `m`

as is.

### Proving `n + 0 = n`

#### 1st try: Simplication

1
2
3
4
5

Theorem plus_O_n_1 : forall n : nat, n + 0 = n.
Proof.
intros n.
simpl. (* Does nothing! *)
Abort.

This cannot be proved by *simplication* bcuz `n`

is unknown so *unfold* the definition `+`

won’t be able to simplify anything.

#### 2nd try: Case Analysis

1
2
3
4
5
6
7
8
9

Theorem plus_n_O_2 : ∀n:nat,
n = n + 0.
Proof.
intros n. destruct n as [| n'] eqn:E.
- (* n = 0 *)
reflexivity. (* so far so good... *)
- (* n = S n' *)
simpl. (* ...but here we are stuck again *)
Abort.

Our 2nd try is to use *case analysis* (`destruct`

), but the proof stucks in *inductive case* since `n`

can be infinitely large (destructed)

#### Induction to the resucue

To prove interesting facts about numbers, lists, and other inductively defined sets, we usually need a more powerful reasoning principle: induction.

Princeple of induction over natural numbers (i.e. *mathematical induction*)

1

P(0); ∀n' P(n') → P(S n') ====> P(n)

In Coq, like `destruct`

, `induction`

break `P(n)`

into 2 subgoals:

1
2
3
4
5

Theorem plus_n_O : ∀n:nat, n = n + 0.
Proof.
intros n. induction n as [| n' IHn'].
- (* n = 0 *) reflexivity.
- (* n = S n' *) simpl. rewrite <- IHn'. reflexivity. Qed.

## Proving `n - n = 0`

1
2
3
4
5
6
7
8
9

Theorem minus_diag : ∀n,
minus n n = 0.
Proof.
(* WORKED IN CLASS *)
intros n. induction n as [| n' IHn'].
- (* n = 0 *)
simpl. reflexivity.
- (* n = S n' *)
simpl. rewrite → IHn'. reflexivity. Qed

Noticed that the definition of `minus`

:

1
2
3
4
5
6

Fixpoint minus (n m:nat) : nat :=
match n, m with
| O , _ => O
| S _ , O => n
| S n', S m' => minus n' m'
end.

`rewrite`

`rewrite`

would do a (DFS) preorder traversal in the syntax tree.