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: 19 May 2025).

A simple illustration¶

Consider the following data type:

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

To illustrate the [... | ... | ...] notation, let us prove that Leibniz equality is reflexive for values of type foo, as in Chapter Induction and induction proofs: a recapitulation in Week 06:

Proposition foo_identity :
  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].

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

Exercise 08¶

Prove the following property of exponentiation for an accumulator-based implementation of the exponentiation function:

Fixpoint power_acc (x i a : nat) : nat :=
  match i with
    O =>
    a
  | S i' =>
    power_acc x i' (x * a)
  end.

Definition power_alt (x n : nat) : nat :=
  power_acc x n 1.

Property about_the_power_of_a_product :
  forall x y n : nat,
    power_alt (x * y) n = power_alt x n * power_alt y n.

Solution for Exercise 08¶

The accompanying file contains the following two lemmas to prove the property about exponentiating a product:

Lemma about_power_acc :
  forall x n a : nat,
    power_acc x n a = power_acc x n 1 * a.

Lemma about_the_power_of_a_product_acc :
  forall x y n a : nat,
    power_acc (x * y) n a = power_acc x n (power_acc y n a).

Each of these two lemmas is proved using The Light of Inductil (and ;).

Proving a logical conjunction, revisited¶

In Week 03, Chapter Proving logical properties with the Coq Proof Assistant introduced how to prove logical conjunctions:

Lemma proving_a_conjunction :
  forall A B : Prop,
    A -> B -> A /\ B.
Proof.
  intros A B H_A H_B.
  intros A B H_A H_B.
  split.
  - exact H_A.
  - exact H_B.

Since the split tactic creates two subgoals, we can re-express this proof using ; and write:

  Restart.

  intros A B H_A H_B.
  split; [exact H_A | exact H_B].
Qed.

And likewise, we can prove a simpler conjunction:

Lemma proving_a_simpler_conjunction :
  forall A : Prop,
    A -> A /\ A.
Proof.
  intros A H_A.
  split; [exact H_A | exact H_A].

  Restart.

  intros A H_A.
  split; exact H_A.
Qed.

Flattening the proof of a nested conjunction¶

Using split and ;, we can also sequentialize the proof of nested conjunctions into a flat series of subgoals instead of having the structure of the proof reflect the structure of the nesting:

Lemma proving_a_nested_conjunction_revisited :
  forall A B C D : Prop,
    A -> B -> C -> D -> (A /\ B) /\ (C /\ D).
Proof.
  intros A B C D H_A H_B H_C H_D.
  split.
  - split.
    + exact H_A.
    + exact H_B.
  - split.
    + exact H_C.
    + exact H_D.

  Restart.

  intros A B C D H_A H_B H_C H_D.
  split; [split | split].
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.

  Restart.

  intros A B C D H_A H_B H_C H_D.
  split; split.
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.
Qed.

The art of writing a flat proof resides in combining split and ;.

Exercise 09¶

In the second proof, combine split and ; to enable the rest of the proof:

Lemma proving_a_conjunction_that_is_nested_on_the_left :
  forall A B C D : Prop,
    A -> B -> C -> D -> ((A /\ B) /\ C) /\ D.
Proof.
  intros A B C D H_A H_B H_C H_D.
  split.
  - split.
    + split.
      * exact H_A.
      * exact H_B.
    + exact H_C.
  - exact H_D.

  Restart.

  intros A B C D H_A H_B H_C H_D.
  ... (* <-- FIXME *)
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.
Qed.

Worked-out solution for Exercise 09¶

The inner nested part of the proof reads:

split.
+ split.
  * exact H_A.
  * exact H_B.
+ exact H_C.

We can flatten it using ;:

split; [split | ].
+ exact H_A.
+ exact H_B.
+ exact H_C.

The resulting complete proof reads as follows:

Restart.

intros A B C D H_A H_B H_C H_D.
split.
- split; [split | ].
  + exact H_A.
  + exact H_B.
  + exact H_C.
- exact H_D.

Here is the inner nested part of this proof:

split.
- split; [split | ].
  + exact H_A.
  + exact H_B.
  + exact H_C.
- exact H_D.

We can flatten it using ;:

split; [split; [split | ] | ].
- exact H_A.
- exact H_B.
- exact H_C.
- exact H_D.

The resulting complete proof reads as follows:

Restart.

intros A B C D H_A H_B H_C H_D.
split; [split; [split | ] | ].
- exact H_A.
- exact H_B.
- exact H_C.
- exact H_D.

This proof is flat.

Exercise 10¶

In the second proof, combine split and ; to enable the rest of the proof:

Lemma proving_a_conjunction_that_is_nested_on_the_right :
  forall A B C D : Prop,
    A -> B -> C -> D -> A /\ (B /\ (C /\ D)).
Proof.
  intros A B C D H_A H_B H_C H_D.
  split.
  - exact H_A.
  - split.
    + exact H_B.
    + split.
      * exact H_C.
      * exact H_D.

  Restart.

  intros A B C D H_A H_B H_C H_D.
  ... (* <-- FIXME *)
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.
Qed.

Worked-out solution for Exercise 10¶

The inner nested part of the proof reads:

split.
+ exact H_B.
+ split.
  * exact H_C.
  * exact H_D.

We can flatten it using ;:

split; [ | split].
+ exact H_B.
+ exact H_C.
+ exact H_D.

The resulting complete proof reads as follows:

Restart.

intros A B C D H_A H_B H_C H_D.
split.
- exact H_A.
- split; [ | split].
  + exact H_B.
  + exact H_C.
  + exact H_D.

The inner nested part of this proof reads:

split.
- exact H_A.
- split; [ | split].
  + exact H_B.
  + exact H_C.
  + exact H_D.

We can flatten it using ;:

split; [ | split; [ | split]].
- exact H_A.
- exact H_B.
- exact H_C.
- exact H_D.

The resulting complete proof reads as follows:

Restart.

intros A B C D H_A H_B H_C H_D.
split; [ | split; [ | split]].
- exact H_A.
- exact H_B.
- exact H_C.
- exact H_D.

This proof is flat.

Exercise 11¶

The following lemma requires proving a conjunction A /\ ... whose right conjunct is a conjunction ... /\ G whose left conjunct is a conjunction B /\ ... whose right conjunct is a conjunction ... /\ F whose left conjunct is a conjunction C /\ ... whose right conjunct is a conjunction ... /\ E whose left conjunct is D:

Lemma proving_a_deeper_conjunction_of_conjunctions :
  forall A B C D E F G : Prop,
    A -> B -> C -> D -> E ->  F ->  G ->
    A /\ ((B /\ ((C /\ (D /\ E)) /\ F)) /\ G).

Prove this lemma with a flat proof, using a combination of split and ;.

Worked-out solution for Exercise 11¶

Here is a succession of proofs where each successive sub-conjunct is admitted:

intros A B C D E F G.
intros H_A H_B H_C H_D H_E H_F H_G.
split.
- exact H_A.
- admit.

Restart.

intros A B C D E F G.
intros H_A H_B H_C H_D H_E H_F H_G.
split.
- exact H_A.
- split.
  + admit.
  + exact H_G.

Restart.

intros A B C D E F G.
intros H_A H_B H_C H_D H_E H_F H_G.
split.
- exact H_A.
- split.
  + split.
    * exact H_B.
    * admit.
  + exact H_G.

Restart.

intros A B C D E F G.
intros H_A H_B H_C H_D H_E H_F H_G.
split.
- exact H_A.
- split.
  + split.
    * exact H_B.
    * split.
      ** admit.
      ** exact H_F.
  + exact H_G.

Restart.

intros A B C D E F G.
intros H_A H_B H_C H_D H_E H_F H_G.
split.
- exact H_A.
- split.
  + split.
    * exact H_B.
    * split.
      ** split.
         *** exact H_C.
         *** admit.
      ** exact H_F.
  + exact H_G.

Restart.

intros A B C D E F G.
intros H_A H_B H_C H_D H_E H_F H_G.
split.
- exact H_A.
- split.
  + split.
    * exact H_B.
    * split.
      ** split.
         *** exact H_C.
         *** split.
             **** exact H_D.
             **** exact H_E.
      ** exact H_F.
  + exact H_G.

The last proof is complete. Its tree structure corresponds to the abstract-syntax tree structure of the nested conjunctions.

Here is the inner nested part of this proof:

split.
*** exact H_C.
*** split.
    **** exact H_D.
    **** exact H_E.

We can flatten it using ;:

split; [ | split].
*** exact H_C.
*** exact H_D.
*** exact H_E.

The resulting complete proof reads as follows:

Restart.

intros A B C D E F G.
intros H_A H_B H_C H_D H_E H_F H_G.
split.
- exact H_A.
- split.
  + split.
    * exact H_B.
    * split.
      ** split; [ | split].
         *** exact H_C.
         *** exact H_D.
         *** exact H_E.
      ** exact H_F.
  + exact H_G.

Here is the inner nested part of this proof:

split.
** split; [ | split].
   *** exact H_C.
   *** exact H_D.
   *** exact H_E.
** exact H_F.

We can flatten it using ;:

split; [split; [ | split] | ].
** exact H_C.
** exact H_D.
** exact H_E.
** exact H_F.

The resulting complete proof reads as follows:

Restart.

intros A B C D E F G.
intros H_A H_B H_C H_D H_E H_F H_G.
split.
- exact H_A.
- split.
  + split.
    * exact H_B.
    * split; [split; [ | split] | ].
      ** exact H_C.
      ** exact H_D.
      ** exact H_E.
      ** exact H_F.
  + exact H_G.

Here is the inner nested part of this proof:

split.
* exact H_B.
* split; [split; [ | split] | ].
  ** exact H_C.
  ** exact H_D.
  ** exact H_E.
  ** exact H_F.

We can flatten it using ;:

split; [ | split; [split; [ | split] | ]].
* exact H_B.
* exact H_C.
* exact H_D.
* exact H_E.
* exact H_F.

The resulting complete proof reads as follows:

Restart.

intros A B C D E F G.
intros H_A H_B H_C H_D H_E H_F H_G.
split.
- exact H_A.
- split.
  + split; [ | split; [split; [ | split] | ]].
    * exact H_B.
    * exact H_C.
    * exact H_D.
    * exact H_E.
    * exact H_F.
  + exact H_G.

Here is the inner nested part of this proof:

split.
+ split; [ | split; [split; [ | split] | ]].
  * exact H_B.
  * exact H_C.
  * exact H_D.
  * exact H_E.
  * exact H_F.
+ exact H_G.

We can flatten it using ;:

split; [split; [ | split; [split; [ | split] | ]] | ].
+ exact H_B.
+ exact H_C.
+ exact H_D.
+ exact H_E.
+ exact H_F.
+ exact H_G.

The resulting complete proof reads as follows:

Restart.

intros A B C D E F G.
intros H_A H_B H_C H_D H_E H_F H_G.
split.
- exact H_A.
- split; [split; [ | split; [split; [ | split] | ]] | ].
  + exact H_B.
  + exact H_C.
  + exact H_D.
  + exact H_E.
  + exact H_F.
  + exact H_G.

Here is the inner nested part of this proof:

split.
- exact H_A.
- split; [split; [ | split; [split; [ | split] | ]] | ].
  + exact H_B.
  + exact H_C.
  + exact H_D.
  + exact H_E.
  + exact H_F.
  + exact H_G.

We can flatten it using ;:

split; [ | split; [split; [ | split; [split; [ | split] | ]] | ]].
- exact H_A.
- exact H_B.
- exact H_C.
- exact H_D.
- exact H_E.
- exact H_F.
- exact H_G.

The resulting complete proof reads as follows:

Restart.

intros A B C D E F G.
intros H_A H_B H_C H_D H_E H_F H_G.
split; [ | split; [split; [ | split; [split; [ | split] | ]] | ]].
- exact H_A.
- exact H_B.
- exact H_C.
- exact H_D.
- exact H_E.
- exact H_F.
- exact H_G.

This proof is flat.

Exercise 12¶

In each of the following proofs, combine split and ; to enable the rest of the proof:

Lemma proving_a_more_complicated_conjunction_of_conjunctions :
  forall A B C D E F G H I J K L : Prop,
    A -> B -> C -> D -> E ->  F ->  G ->  H ->  I ->  J ->  K ->  L ->
    A
    /\
    B
    /\
    (C /\ D)
    /\
    (E /\ F)
    /\
    (G /\ H /\ I)
    /\
    (J /\ K /\ L).
Proof.
  intros A B C D E F G H I J K L.
  intros H_A H_B H_C H_D H_E H_F H_G H_H H_I H_J H_K H_L.
  ... (* <-- FIXME *)
  - exact H_A.
  - exact H_B.
  - ... (* <-- FIXME *)
    + exact H_C.
    + exact H_D.
  - ... (* <-- FIXME *)
    + exact H_E.
    + exact H_F.
  - ... (* <-- FIXME *)
    + exact H_G.
    + exact H_H.
    + exact H_I.
  - ... (* <-- FIXME *)
    + exact H_J.
    + exact H_K.
    + exact H_L.

  Restart.

  intros A B C D E F G H I J K L.
  intros H_A H_B H_C H_D H_E H_F H_G H_H H_I H_J H_K H_L.
  ... (* <-- FIXME *)
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.
  - ... (* <-- FIXME *)
    + exact H_E.
    + exact H_F.
  - ... (* <-- FIXME *)
    + exact H_G.
    + exact H_H.
    + exact H_I.
  - ... (* <-- FIXME *)
    + exact H_J.
    + exact H_K.
    + exact H_L.

  Restart.

  intros A B C D E F G H I J K L.
  intros H_A H_B H_C H_D H_E H_F H_G H_H H_I H_J H_K H_L.
  ... (* <-- FIXME *)
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.
  - exact H_E.
  - exact H_F.
  - ... (* <-- FIXME *)
    + exact H_G.
    + exact H_H.
    + exact H_I.
  - ... (* <-- FIXME *)
    + exact H_J.
    + exact H_K.
    + exact H_L.

  Restart.

  intros A B C D E F G H I J K L.
  intros H_A H_B H_C H_D H_E H_F H_G H_H H_I H_J H_K H_L.
  ... (* <-- FIXME *)
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.
  - exact H_E.
  - exact H_F.
  - ... (* <-- FIXME *)
    + exact H_G.
    + exact H_H.
    + exact H_I.
  - exact H_J.
  - exact H_K.
  - exact H_L.

  Restart.

  intros A B C D E F G H I J K L.
  intros H_A H_B H_C H_D H_E H_F H_G H_H H_I H_J H_K H_L.
  ... (* <-- FIXME *)
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.
  - exact H_E.
  - exact H_F.
  - exact H_G.
  - exact H_H.
  - exact H_I.
  - ... (* <-- FIXME *)
    + exact H_J.
    + exact H_K.
    + exact H_L.

  Restart.

  intros A B C D E F G H I J K L.
  intros H_A H_B H_C H_D H_E H_F H_G H_H H_I H_J H_K H_L.
  ... (* <-- FIXME *)
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.
  - exact H_E.
  - exact H_F.
  - exact H_G.
  - exact H_H.
  - exact H_I.
  - exact H_J.
  - exact H_K.
  - exact H_L.
Qed.

Solution for Exercise 12¶

Here is a winning combination for the last proof:

split; [ | split; [ | split; [split | split; [split | split; [split; [ | split] | split; [ | split]]]]]].

The progressive solutions are available in the accompanying file.

Exercise 13¶

In the manner of the previous exercises, state a nested conjunction and prove it in a flat way, using split and ;. Explain your solution in the manner of the previous solutions.

Resources¶

The .v file for the present lecture note (latest version: 19 May 2025).

Version¶

Expanded this chapter with proofs for conjunctions and with Exercise 09, Exercise 10, Exercise 11, Exercise 12 and Exercise 13 [19 May 2025]

Added Exercise 08 and its solution [18 May 2025]

Created [21 Mar 2025]

The case of proofs by cases¶

Resources¶

A simple illustration¶

Soundness and completeness of an equality predicate for Booleans¶

About the Light of Inductil¶

Exercise 08¶

Solution for Exercise 08¶

Proving a logical conjunction, revisited¶

Flattening the proof of a nested conjunction¶

Exercise 09¶

Worked-out solution for Exercise 09¶

Exercise 10¶

Worked-out solution for Exercise 10¶

Exercise 11¶

Worked-out solution for Exercise 11¶

Exercise 12¶

Solution for Exercise 12¶

Exercise 13¶

Resources¶

Version¶

Table Of Contents

Previous topic

Next topic

Navigation

The case of proofs by cases¶

Resources¶

A simple illustration¶

Soundness and completeness of an equality predicate for Booleans¶

About the Light of Inductil¶

Exercise 08¶

Solution for Exercise 08¶

Proving a logical conjunction, revisited¶

Flattening the proof of a nested conjunction¶

Exercise 09¶

Worked-out solution for Exercise 09¶

Exercise 10¶

Worked-out solution for Exercise 10¶

Exercise 11¶

Worked-out solution for Exercise 11¶

Exercise 12¶

Solution for Exercise 12¶

Exercise 13¶

Resources¶

Version¶

Table Of Contents

Previous topic

Next topic

Quick search

Navigation