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:
- [evenb n = true]
- [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  is even.
- Rule [ev_SS]: If [n] is even, then [S (S n)] is even.
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]:
Notice the “parameter” on the left of the colon and “index” (or “annotation”) on the right.
destruct [ev n] directly.
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:
- 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.
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]).
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.
A one-argument proposition can be thought of as a property. A two-argument proposition can be thought of as a relation.