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.