The case of proofs by cases

The goal of this lecture note is to illustrate the language support offered by Coq for proofs by cases:

• the idiom t0; [t1 | t2 | ... | tn] is used when invoking the tactic t0 creates n subgoals; t1 is then used to prove the first subgoal, t2 to prove the second subgoal, etc.; if t1, t2, etc. are the same tactic, then one writes t0; t;
• the idiom t0; (t1 || t2 || ... || tn) is used when invoking the tactic t0 creates one or more subgoals; Coq then attempts to prove each of these subgoals with t1, and then with t2, etc., until one of these successive tactics succeeds.

Resources

• The .v file for the present lecture note (latest version: 08 Mar 2024).

A silly example

Consider the following data type:

Inductive foo : Type :=
  F0 : nat -> foo
| F1 : bool -> foo
| F2 : nat -> bool -> foo.

Let us prove the following silly proposition to illustrate the [... | ... | ...] notation:

Proposition identity_over_foo :
  forall f : foo,
    f = f.
Proof.
  intros [n | b | n b].
  - reflexivity.
  - reflexivity.
  - reflexivity.

This proof is a completely canonical proof by cases where the reflexivity tactic is used in each case. We can manifest each of these uses using the first idiom:

Restart.

intros [n | b | n b]; [reflexivity | reflexivity | reflexivity].

Since in each case, the tactic is the same, we can write the proof more concisely as follows:

  Restart.

  intros [n | b | n b]; reflexivity.
Qed.

Witness Show Proof, each of these versions gives rise to the same proof tree, so the idiom is purely notational.

Soundness and completeness of an equality predicate for Booleans

The accompanying .v file revisits the soundness and completeness of the predefined equality predicate for Booleans and of a user-defined one. For each of them, the proof is first written in long hand, and then using the idioms. Again, all the successive versions of the proof give rise to the same proof tree.

About the Light of Inductil

In an induction proof that uses the Light of Inductil, instead of writing:

intro x.
induction x as ...
- intro y.
  ...AAA...
- intro y.
  ...BBB...

one can use a ; and write:

intro x.
induction x as ...; intro y.
- ...AAA...
- ...BBB...

Resources

• The .v file for the present lecture note (latest version: 08 Mar 2024).

Version

Created [08 Mar 2024]