IndProp

We have seen several ways of writing propositions (conjunction, disjunction, and existential quantification) In this chapter, we bring yet another new tool in to the mix: inductive definitions.

Uses an inductive definition of "evenness" as a running example.

In past chapters, we have two ways to say [n] is even:

1. [evenb n = true]
2. [exists k, n = double k]

Yet another possibility is to say that [n] is even if we can establish its evenness from the following rules:

• Rule [ev_0]: The number [0] is even.
• Rule [ev_SS]: If [n] is even, then [S (S n)] is even.

Inductive Definition of Evenness

Inductive ev : nat -> Prop :=
  | ev_0 : ev 0
  | ev_SS (n : nat) (H : ev n) : ev (S (S n)).

Different from previous uses of [Inductive]. Neither a [Type] (like [nat]) nor a function yielding a [Type] (like [list]).

We define a function from [nat] to [Prop]. That is, a property of numbers!

In contrast, recall the definition of [list]:

Inductive list (X:Type) : Type :=
  | nil
  | cons (x : X) (l : list X).

Notice the "parameter" on the left of the colon and "index" (or "annotation") on the right.

Inversion on Evidence

destruct [ev n] directly.

destruct E as [|n' E'] eqn:EE

When the goal relates to [n] but we destruct H with S(n) or S(S(n)), we can two ways to prove.

• with the help of [ev_inversion] theorem proven before.
• use [remember] tactic.

Note how both proofs produce two subgoals, which correspond to the two ways of proving [ev]. The first subgoal is a contradiction that is discharged with [discriminate]. The second subgoal makes use of [injection] and [rewrite]. Coq provides a handy tactic called [inversion] that factors out that common pattern.

The [inversion] tactic can detect:

1. that the first case ([n = 0]) does not apply and 2 .that the [n'] that appears in the [ev_SS] case must be the same as [n].

It has an "[as]" variant similar to [destruct], allowing us to assign names rather than have Coq choose them.

Theorem evSS_ev' : forall n,
  ev (S (S n)) -> ev n.
Proof.
  intros n E.
  inversion E as [| n' E' Heq].
  (* We are in the [E = ev_SS n' E'] case now. *)
  apply E'.
Qed.

The [inversion] tactic does quite a bit of work. destruct, injection ...

When [inversion H]. Generate subgoals which [H] has been replaced by exact contexts. Then [inversion] will throw those self-contradictionory subgoals away. Details follows:

Here's how [inversion] works in general. Suppose the name [H] refers to an assumption [P] in the current context, where [P] has been defined by an [Inductive] declaration. Then, for each of the constructors of [P], [inversion H] generates a subgoal in which [H] has been replaced by the exact, specific conditions under which this constructor could have been used to prove [P]. Some of these subgoals will be self-contradictory; [inversion] throws these away. The ones that are left represent the cases that must be proved to establish the original goal. For those, [inversion] adds all equations into the proof context that must hold of the arguments given to [P] (e.g., [S (S n') = n] in the proof of [evSS_ev]).

Induction on Evidence

Just as induction on data, when we inversion construct evidence and get stuck like prove another instance of the same theorem we set out to prove, we can consider use induction on evidence.

This time we can get a useful hypothesis related to the other instance of n.

Lemma ev_even : forall n,
  ev n -> even n.
Proof.
  intros n E.
  induction E as [| n' E' IH].
  - (* E = ev_0 *)
    exists 0. reflexivity.
  - (* E = ev_SS n' E'
       with IH : even E' *)
    unfold even in IH.
    destruct IH as [k Hk].
    rewrite Hk. exists (S k). simpl. reflexivity.
Qed.

(** Here, we can see that Coq produced an [IH] that corresponds
    to [E'], the single recursive occurrence of [ev] in its own
    definition.  Since [E'] mentions [n'], the induction hypothesis
    talks about [n'], as opposed to [n] or some other number. *)

(** The equivalence between the second and third definitions of
    evenness now follows. *)

Theorem ev_even_iff : forall n,
  ev n <-> even n.
Proof.
  intros n. split.
  - (* -> *) apply ev_even.
  - (* <- *) unfold even. intros [k Hk]. rewrite Hk.
    Check ev_double.
    apply ev_double.
Qed.

Inductive Relations

A one-argument proposition can be thought of as a property. A two-argument proposition can be thought of as a relation.

Inductive le : nat -> nat -> Prop :=
  | le_n (n : nat)                : le n n
  | le_S (n m : nat) (H : le n m) : le n (S m).