# NOTE: Coq tactics

Quickly note some Coq.

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

`intros`

introduces variable from environment, here introduce bound`n`

from`forall`

.`simpl`

would try to reduce both sides of equation, in case`0 + n`

should become`n`

`reflexivity`

check`n = n`

which is true, put`Qed`

in the end.

Theorem plus_id : forall n m:nat, (* -> constructs a function type, means implies *) m = n -> n + n = m + m. Proof. (* introduce n m from forall first *) intros n m. (* introduce m = n as H*) intros H. (* rewrite n + n = m + m with m = n, got n + n = m + m *) rewrite -> H. reflexivity. Qed.

`rewrite`

do substitution, without it we would get
`Unable to unify "m + m" with "n + n".`

.

Theorem negb_involutive : forall b : bool, negb (negb b) = b. Proof. intros b. destruct b [] eqn : B. (* b = true *) - reflexivity. (* b = false *) - reflexivity. Qed.

`destruct`

makes subgoals, in this case `bool`

constructors `true`

and
`false`

has no arguments, therefore use `[]`

since no identifiers has to
bind. In fact, we can totally remove it: `destruct b eqn : B.`

. `eqn`

gives `destruct`

equation a name, also can omit: `destruct b.`

. We can
make it even simpler: `intros [].`

and remove `destruct`

. `-`

handles
subgoals.

Theorem andb_commutative : forall b c, andb b c = andb c b. Proof. intros [] []. - reflexivity. - reflexivity. - reflexivity. - reflexivity. Qed

This case shows how to handle combinations: `true true`

, `true false`

,
`false true`

, `false false`

. To make `destruct`

deeper, can use `--`

,
`---`

and so on:

Theorem andb_commutative : forall b c, andb b c = andb c b. Proof. intros b c. destruct b. - destruct c. -- reflexivity. -- reflexivity. - destruct c. -- reflexivity. -- reflexivity. Qed.

To prove `n + 0`

, at first we might think it's easy.

Theorem plus_n_0 : forall n : nat, n = n + 0. Proof. intros [| n']. (* n = 0 | S n'*) - reflexivity. - reflexivity. Qed

We get two subgoals:

`n = 0`

,`reflexivity`

is enough here.`n = S n'`

, but we have no idea what`n'`

is, to prove it requires proving`plus_n_0`

first! First we might think we can`destruct n'`

, but`n`

can be infinite, we run out of ideas. Unless we have`induction`

.

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

As we learn at before, prove `P(0)`

, suppose `P(n)`

is true then check
`P(S n)`

works.

Theorem mult_0_plus' : forall n m : nat, (0 + n) * m = n * m. Proof. intros n m. assert (H : 0 + n = n). { reflexivity. } rewrite -> H. reflexivity. Qed.

`assert`

proves a sub theorem, here is `0 + n = n`

, `{ reflexivity. }`

is the proof of the sub theorem. Later we `rewrite`

equation:
`(0 + n) * m = n * m`

with `0 + n = n`

, then get `n * m = n * m`

,
finally, use `reflexivity`

.