Chapter 13  Proof schemes

• 13.1  Generation of induction principles with Scheme
• 13.2  Generation of induction principles with Functional Scheme
• 13.3  Generation of inversion principles with Derive Inversion

13.1  Generation of induction principles with Scheme

The Scheme command is a high-level tool for generating automatically (possibly mutual) induction principles for given types and sorts. Its syntax follows the schema:

Scheme ident₁ := Induction for ident’₁ Sort sort₁
with
…
with ident_m := Induction for ident’_m Sort sort_m

where ident’₁ … ident’_m are different inductive type identifiers belonging to the same package of mutual inductive definitions. This command generates ident₁… ident_m to be mutually recursive definitions. Each term ident_i proves a general principle of mutual induction for objects in type term_i.

Variants:

1. Scheme ident₁ := Minimality for ident’₁ Sort sort₁
   with
   …
   with ident_m := Minimality for ident’_m Sort sort_m

   Same as before but defines a non-dependent elimination principle more natural in case of inductively defined relations.

2. Scheme Equality for ident₁

   Tries to generate a Boolean equality and a proof of the decidability of the usual equality. If ident_i involves some other inductive types, their equality has to be defined first.

3. Scheme Induction for ident₁ Sort sort₁
   with
   …
   with Induction for ident_m Sort sort_m

   If you do not provide the name of the schemes, they will be automatically computed from the sorts involved (works also with Minimality).

Example 1: Induction scheme for tree and forest

The definition of principle of mutual induction for tree and forest over the sort Set is defined by the command:

You may now look at the type of tree_forest_rec:

This principle involves two different predicates for trees and forests; it also has three premises each one corresponding to a constructor of one of the inductive definitions.

The principle forest_tree_rec shares exactly the same premises, only the conclusion now refers to the property of forests.

Example 2: Predicates odd and even on naturals

Let odd and even be inductively defined as:

The following command generates a powerful elimination principle:

The type of odd_even for instance will be:

The type of even_odd shares the same premises but the conclusion is (n:nat)(even n)->(Q n).

13.1.1  Automatic declaration of schemes

It is possible to deactivate the automatic declaration of the induction principles when defining a new inductive type with the Unset Elimination Schemes command. It may be reactivated at any time with Set Elimination Schemes.
You can also activate the automatic declaration of those Boolean equalities and their proof (see the second variant of Scheme) with respectively the commands Set Boolean Equality Schemes and Set Decidable Equality Schemes. However you have to be careful with this option since Coq  may now reject well-defined inductive types because it cannot compute a Boolean equality for them.

13.1.2  Combined Scheme

The Combined Scheme command is a tool for combining induction principles generated by the Scheme command. Its syntax follows the schema :

Combined Scheme ident₀ from ident₁, .., ident_n

where ident₁ …ident_n are different inductive principles that must belong to the same package of mutual inductive principle definitions. This command generates ident₀ to be the conjunction of the principles: it is built from the common premises of the principles and concluded by the conjunction of their conclusions.

Example: We can define the induction principles for trees and forests using:

Then we can build the combined induction principle which gives the conjunction of the conclusions of each individual principle:

The type of tree_forest_mutrec will be:

13.2  Generation of induction principles with Functional Scheme

The Functional Scheme command is a high-level experimental tool for generating automatically induction principles corresponding to (possibly mutually recursive) functions. Its syntax follows the schema:

Functional Scheme ident₁ := Induction for ident’₁ Sort sort₁
with
…
with ident_m := Induction for ident’_m Sort sort_m

where ident’₁ … ident’_m are different mutually defined function names (they must be in the same order as when they were defined). This command generates the induction principles ident₁…ident_m, following the recursive structure and case analyses of the functions ident’₁ … ident’_m.

Remark: There is a difference between obtaining an induction scheme by using Functional Scheme on a function defined by Function or not. Indeed Function generally produces smaller principles, closer to the definition written by the user.

Example 1: Induction scheme for div2

We define the function div2 as follows:

The definition of a principle of induction corresponding to the recursive structure of div2 is defined by the command:

You may now look at the type of div2_ind:

We can now prove the following lemma using this principle:

We can use directly the functional induction (8.5.5) tactic instead of the pattern/apply trick:

Remark: There is a difference between obtaining an induction scheme for a function by using Function (see Section 2.3) and by using Functional Scheme after a normal definition using Fixpoint or Definition. See 2.3 for details.

Example 2: Induction scheme for tree_size

We define trees by the following mutual inductive type:

We define the function tree_size that computes the size of a tree or a forest. Note that we use Function which generally produces better principles.

Remark: Function generates itself non mutual induction principles tree_size_ind and forest_size_ind:

The definition of mutual induction principles following the recursive structure of tree_size and forest_size is defined by the command:

You may now look at the type of tree_size_ind2:

13.3  Generation of inversion principles with Derive Inversion

The syntax of Derive Inversion follows the schema:

Derive Inversion ident with forall (x : T), I t Sort sort

This command generates an inversion principle for the inversion … using tactic. Let I be an inductive predicate and x the variables occurring in t. This command generates and stocks the inversion lemma for the sort sort  corresponding to the instance ∀ (x:T), I t with the name ident in the global environment. When applied, it is equivalent to having inverted the instance with the tactic inversion.

Variants:

1. Derive Inversion_clear ident with forall (x:T), I t Sort sort
   When applied, it is equivalent to having inverted the instance with the tactic inversion replaced by the tactic inversion_clear.
2. Derive Dependent Inversion ident with forall (x:T), I t Sort sort
   When applied, it is equivalent to having inverted the instance with the tactic dependent inversion.
3. Derive Dependent Inversion_clear ident with forall (x:T), I t Sort sort
   When applied, it is equivalent to having inverted the instance with the tactic dependent inversion_clear.

Example:

Let us consider the relation Le over natural numbers and the following variable:

To generate the inversion lemma for the instance (Le (S n) m) and the sort Prop, we do:

Then we can use the proven inversion lemma: