Writing Proofs

Formulating Proofs

Can use Check to check that formal statement is well-formed:

Check 3 = 3.
(* 3 = 3 : Prop *)

Check forall n : nat, 0 + n = n.
(* ∀ n : ℕ, 0 + n = n : Prop *)

Should be a well-formed term of type Prop for proposition.

Check does not check the provability of the statement → use keywords such as Lemma (or Theorem, Remark, Corollary, etc.) to express the start of a statement is going to be proved.

Use keyword Proof to start proof text and end it with either Qed or Admitted.

Lemma addnA (m n k : nat) : m + (n + k) = m + n + k.
Proof. Admitted.

Type annotation is not necessary if it can be inferred from the statement.

Use -> for implication:

Lemma leq_pmull m n : n > 0 -> m <= n * m.
Proof. Admitted.

Proof by Simplification

strategy for proving identities
use simpl to simplify both sides of the equation
use reflexivity to check that both sides contain identical values
use Theorem which works the same as (@see: Example)
note use of \(\forall\) i.e. forall to include all natural numbers
intros moves n from goal to context of current assumptions
tactics - commands used between Theorem and Qed to guide the process of checking claim we are making e.g. intros, simpl, reflexivity → (@see: tactics)

Simple example

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

None: this example can be written without simpl because reflexivity performs simplification automatically. Adding simpl allows seeing intermediate state → use simpl when interested in the new goal it creates.

More examples

Theorem plus_1_l : forall n:nat, 1 + n = S n.
Proof.
  intros n. reflexivity. Qed.

Theorem mult_0_l : forall n:nat, 0 * n = 0.
Proof.
  intros n. reflexivity. Qed.

(* _l means on the left *)

Proof by Rewriting

Tactic called rewrite replaces expression in the goal state

Theorem plus_id_example : forall n m:nat,
  n = m -> n + n = m + m.
Proof.
  (* move both quantifiers into the context: *)
  intros n m.
  (* move the hypothesis n = m into the context and name it H: *)
  intros H.
  (* rewrite the goal using the hypothesis: *)
  rewrite -> H.
  reflexivity. Qed.

writing -> says: replace left side of the equality hypothesis H with the right side
<- used to replace in the opposite direction

Theorem plus_id_exercise : forall n m o : nat,
  n = m -> m = o -> n + m = m + o.
Proof.
  intros n m o.   (* intros n m o H I. works also *)
  intros H I.
  rewrite H.
  rewrite I.
  reflexivity. Qed.

Can use Check to examine previously declared lemmas and theorems. These are from and proven in the standard library:

Check mult_n_O.
(*  mult_n_O : forall n : nat, 0 = n * 0  *)

Check mult_n_Sm.
(*  mult_n_Sm : forall n m : nat, n * m + n = n * S m  *)

Can use rewrite with a previously proven theorem instead of hypothesis from context
if theorem involves quantified variables, Coq tries to instantiate them by matching with the current goal

Theorem mult_n_0_m_0 : forall p q : nat,
  (p * 0) + (q * 0) = 0.
Proof.
  intros p q.
  rewrite <- mult_n_O.
  rewrite <- mult_n_O.
  reflexivity. Qed.

Proof by Case Analysis

sometimes must consider possible forms separately → simplification or rewrite is not an option
destruct tactic says to consider cases separately

Simple examples

Theorem dbl_neg: forall b: bool, negb (negb b) = b.
  Proof.
    intros b. destruct b eqn:E.
    - reflexivity.
    - reflexivity. Qed.

Theorem plus_1_neq_0 : forall n : nat,
  (n + 1) == 0 = false.
Proof.
  (*  destruct to cases where n = O and n = S n' *)
  (*  generates two subgoals which must be proven separately *)
  intros n. destruct n as [| n'] eqn:E.
  - reflexivity.
  - reflexivity. Qed.

Introduction Pattern and Bullets

as [| n'] is an introduction pattern
- tells Coq what variable names to use
- between square brackets: list of lists of names, separated by |
- in example:
  - first component is empty since the O constructor is nullary
  - second component gives a single name, n', since S is unary constructor
In each subgoal, Coq remembers the assumption about n that is relevant for this subgoal → either n = 0 or n = S n' for some n'.
eqn:E tells destruct to give the name E to this equation (optional)

Example: negation is its own inverse

Theorem negb_involutive : forall b : bool,
  negb (negb b) = b.
Proof.
  (* no as clause because none of the subcases of
    destruct need to bind any variables *)
  intros b. destruct b eqn:E.
  - reflexivity.
  - reflexivity. Qed.

- signs before reflexivity are called bullets - after a bullet is the entire proof for the corresponding subgoal - in example: each of the subgoals is easily proved by reflexivity - using bullets is optional but more readable if used - can use other symbols (*, +, --, ***, etc.) or curly braces

Nested Destruct

Can invoke destruct inside subgoal → use different bullets at different levels

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

Theorem andb3_exchange :
  forall b c d, andb (andb b c) d = andb (andb b d) c.
Proof.
  intros b c d. destruct b eqn:Eb.
  - destruct c eqn:Ec.
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
  - destruct c eqn:Ec.
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
Qed.

Destruct Shorthand

Destructing after intros has a shorthand:

Theorem plus_1_neq_0' : forall n : nat,
  (n + 1) == 0 = false.
Proof.
  intros [|n].
  - reflexivity.
  - reflexivity. Qed.

If there are no constructor arguments that need names, can just write [] to get the case analysis.

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

Proof by Induction

Goal - show that \(P(0)\) holds - show that, for any \(n'\), if \(P(n')\) holds, then so does \(P(S n')\); - conclude that \(P(n)\) holds for all n

Steps 1. begin with the goal of proving \(P(n)\) for all \(n\) 2. break it down by applying the induction tactic into two separate subgoals - one where we must show \(P(O)\) - one where we must show \(P(n') → P(S n')\)

Example

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

Note: use of the intros here is redundant. When applied to a goal that contains quantified variables, the induction tactic will automatically move them into the context.

Use as to specify the names of the variables to be introduced in the subgoals. Since there are two subgoals the as clause has two parts separated by |:

in first subgoal n is replaced by 0 (first part is empty)
- goal becomes \(0 = 0 + 0\)
in second subgoal n is replaced by S n' (specified in second part)
- assumption \(n' + 0 = n'\) is added to the context with name IHn'
- goal becomes \(S n' = (S n') + 0\) which simplifies to \(S n' = S (n' + 0)\) which follows from IHn'.

Another simple example

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

Using Assert

Sometimes need to break large proofs into sequence of theorems, with later proofs referring to earlier theorems. Some proofs include parts that are too trivial for top-level name → use assert to state and prove a needed sub-theorem at point of use.

Example

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 tactic introduces two sub-goals: 1. assertion itself, which we name H
→ alternative syntax using as: assert (0 + n = n) as H 2. second goal is the same as the one at the point where assert is invoked, except now we have assumption H that 0 + n = n

Prove the first goal and use the second to make progress.