Search code examples
coqlogical-foundations

Logic: In_example_2

Here is the code from the book:

Example In_example_2 :
  forall n, In n [2; 4] ->
  exists n', n = 2 * n'.
Proof.
  (* WORKED IN CLASS *)
  simpl.
  intros n [H | [H | []]].
  - exists 1. rewrite <- H. reflexivity.
  - exists 2. rewrite <- H. reflexivity.
Qed.

After simpl. In is transformed into a disjunction of 3 elements:

============================
forall n : nat, 2 = n \/ 4 = n \/ False -> exists n' : nat, n = n' + (n' + 0)

But I totally don't understand how to read this:

intros n [H | [H | []]].

It produced this:

n : nat
H : 2 = n
============================
exists n' : nat, n = n' + (n' + 0)

subgoal 2 (ID 229) is:
 exists n' : nat, n = n' + (n' + 0)

What I understood:

  1. It put n from forall into the context.
  2. It split disjunction of 3 elements into 2 subgoals, ignoring False:
  3. Created 2 subgoals according to the number of splits.

There is also a notice at the bottom:

(** (Notice the use of the empty pattern to discharge the last case
    _en passant_.) *)

En passant (French: [ɑ̃ paˈsɑ̃], lit. in passing) is a move in chess. It is a special pawn capture that can only occur immediately after a pawn makes a move of two squares from its starting square, and when it could have been captured by an enemy pawn had it advanced only one square.

Looking at this:

intros n [H | [H | []]].

Can somebody explain me:

  1. Should command of this form be used for destructing forall? Is there something else for this task?
  2. How to read this command in English?
  3. Why [H | []] was put into another pair of brackets?
  4. How [] told coq to ignore the False statement?
  5. When this command should be used in general?
Solution

  • The intros n [H | [H | []]] form is a shorthand for 

    intros n H. destruct H as [H | [H | []]].

    You can further rewrite the proof as

    intros n H. destruct H as [H2 | H4F].
- (* H2 : 2 = n *)
  exists 1. rewrite <- H2. reflexivity.
- (* H4F : 4 = n \/ False *)
  destruct H4F as [H4 | HF].
  + (* H4 : 4 = n *)
    exists 2. rewrite <- H4. reflexivity.
  + (* HF : False *)
    destruct HF. (* No more subgoals here *)

    The two proofs are logically equivalent, but the first one is shorter (and easier to read, once you get used to the syntax).

    Generally speaking, the tactic destruct x as [...] takes the expression x and generates one subgoal for each constructor that could have been used to produce x. The arguments to the constructors are named according to the pattern [...], and the parts corresponding to the different constructors are separated by vertical bars.

    A proposition of the form A \/ B \/ C should be read as A \/ (B \/ C). Thus, when you call destruct for the first time in the expanded form above, you get two cases: when for when A holds, the other one for when B \/ C holds. You need to call destruct a second time to analyze the inner or, which is why you had nested brackets in the original expression. As for the last branch, False is defined as a proposition with no constructors, so once you destruct a hypothesis HF : False, the proof is complete.

    (Here, "en passant" is equivalent to the English "in passing", roughly meaning "incidentally". It refers to the fact that we are discharging the last case as a by-product of doing a case analysis on the or hypothesis.)