Proof schemes¶
Generation of induction principles with Scheme
¶
The Scheme
command is a highlevel tool for generating automatically
(possibly mutual) induction principles for given types and sorts. Its
syntax follows the schema:

Command
Scheme ident_{1} := Induction for ident_{2} Sort sort with ident_{i} := Induction for ident_{j} Sort sort*
¶ This command is a highlevel tool for generating automatically (possibly mutual) induction principles for given types and sorts. Each
ident_{j}
is a different inductive type identifier belonging to the same package of mutual inductive definitions. The command generates theident_{i}
s to be mutually recursive definitions. Each termident_{i}
proves a general principle of mutual induction for objects in typeident_{j}
.

Variant
Scheme ident := Minimality for ident Sort sort with ident := Minimality for ident' Sort sort*
Same as before but defines a nondependent elimination principle more natural in case of inductively defined relations.

Variant
Scheme Equality for ident
¶ Tries to generate a Boolean equality and a proof of the decidability of the usual equality. If
ident
involves some other inductive types, their equality has to be defined first.

Variant
Scheme Induction for ident Sort sort with Induction for ident Sort sort*
If you do not provide the name of the schemes, they will be automatically computed from the sorts involved (works also with Minimality).
Example
Induction scheme for tree and forest.
A mutual induction principle for tree and forest in sort
Set
can be defined using the command
 Axiom A : Set.
 A is declared
 Axiom B : Set.
 B is declared
 Inductive tree : Set := node : A > forest > tree with forest : Set := leaf : B > forest  cons : tree > forest > forest.
 tree, forest are defined tree_rect is defined tree_ind is defined tree_rec is defined forest_rect is defined forest_ind is defined forest_rec is defined
 Scheme tree_forest_rec := Induction for tree Sort Set with forest_tree_rec := Induction for forest Sort Set.
 forest_tree_rec is defined tree_forest_rec is defined tree_forest_rec, forest_tree_rec are recursively defined
You may now look at the type of tree_forest_rec:
 Check tree_forest_rec.
 tree_forest_rec : forall (P : tree > Set) (P0 : forest > Set), (forall (a : A) (f : forest), P0 f > P (node a f)) > (forall b : B, P0 (leaf b)) > (forall t : tree, P t > forall f1 : forest, P0 f1 > P0 (cons t f1)) > forall t : tree, P t
This principle involves two different predicates for trees andforests; 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
Predicates odd and even on naturals.
Let odd and even be inductively defined as:
 Inductive odd : nat > Prop := oddS : forall n:nat, even n > odd (S n) with even : nat > Prop :=  evenO : even 0  evenS : forall n:nat, odd n > even (S n).
 odd, even are defined odd_ind is defined even_ind is defined
The following command generates a powerful elimination principle:
 Scheme odd_even := Minimality for odd Sort Prop with even_odd := Minimality for even Sort Prop.
 even_odd is defined odd_even is defined odd_even, even_odd are recursively defined
The type of odd_even for instance will be:
 Check odd_even.
 odd_even : forall P P0 : nat > Prop, (forall n : nat, even n > P0 n > P (S n)) > P0 0 > (forall n : nat, odd n > P n > P0 (S n)) > forall n : nat, odd n > P n
The type of even_odd
shares the same premises but the conclusion is
(n:nat)(even n)>(P0 n)
.
Automatic declaration of schemes¶

Flag
Elimination Schemes
¶ Enables automatic declaration of induction principles when defining a new inductive type. Defaults to on.

Flag
Nonrecursive Elimination Schemes
¶ Enables automatic declaration of induction principles for types declared with the
Variant
andRecord
commands. Defaults to off.

Flag
Case Analysis Schemes
¶ This flag governs the generation of case analysis lemmas for inductive types, i.e. corresponding to the pattern matching term alone and without fixpoint.

Flag
Boolean Equality Schemes
¶ 
Flag
Decidable Equality Schemes
¶ These flags control the automatic declaration of those Boolean equalities (see the second variant of
Scheme
).
Warning
You have to be careful with this option since Coq may now reject welldefined inductive types because it cannot compute a Boolean equality for them.

Flag
Rewriting Schemes
¶ This flag governs generation of equalityrelated schemes such as congruence.
Combined Scheme¶

Command
Combined Scheme ident from ident_{i}+,
¶ This command is a tool for combining induction principles generated by the
Scheme
command. Eachident_{i}
is a different inductive principle that must belong to the same package of mutual inductive principle definitions. This command generatesident
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. In the case where all the inductive principles used are in sortProp
, the propositional conjunctionand
is used, otherwise the simple productprod
is used instead.
Example
We can define the induction principles for trees and forests using:
 Scheme tree_forest_ind := Induction for tree Sort Prop with forest_tree_ind := Induction for forest Sort Prop.
 forest_tree_ind is defined tree_forest_ind is defined tree_forest_ind, forest_tree_ind are recursively defined
Then we can build the combined induction principle which gives the conjunction of the conclusions of each individual principle:
 Combined Scheme tree_forest_mutind from tree_forest_ind,forest_tree_ind.
 tree_forest_mutind is defined tree_forest_mutind is recursively defined
The type of tree_forest_mutind will be:
 Check tree_forest_mutind.
 tree_forest_mutind : forall (P : tree > Prop) (P0 : forest > Prop), (forall (a : A) (f : forest), P0 f > P (node a f)) > (forall b : B, P0 (leaf b)) > (forall t : tree, P t > forall f1 : forest, P0 f1 > P0 (cons t f1)) > (forall t : tree, P t) /\ (forall f2 : forest, P0 f2)
Example
We can also combine schemes at sortType
:
 Scheme tree_forest_rect := Induction for tree Sort Type with forest_tree_rect := Induction for forest Sort Type.
 forest_tree_rect is defined tree_forest_rect is defined tree_forest_rect, forest_tree_rect are recursively defined
 Combined Scheme tree_forest_mutrect from tree_forest_rect, forest_tree_rect.
 tree_forest_mutrect is defined tree_forest_mutrect is recursively defined
 Check tree_forest_mutrect.
 tree_forest_mutrect : forall (P : tree > Type) (P0 : forest > Type), (forall (a : A) (f : forest), P0 f > P (node a f)) > (forall b : B, P0 (leaf b)) > (forall t : tree, P t > forall f1 : forest, P0 f1 > P0 (cons t f1)) > (forall t : tree, P t) * (forall f2 : forest, P0 f2)
Generation of induction principles with Functional
Scheme
¶

Command
Functional Scheme ident_{0} := Induction for ident' Sort sort with ident_{i} := Induction for ident_{i}' Sort sort*
¶ This command is a highlevel experimental tool for generating automatically induction principles corresponding to (possibly mutually recursive) functions. First, it must be made available via
Require Import FunInd
. Eachident_{i}
is a different mutually defined function name (the names must be in the same order as when they were defined). This command generates the induction principle for eachident_{i}
, following the recursive structure and case analyses of the corresponding functionident_{i}'
.
Warning
There is a difference between induction schemes generated by the command
Functional Scheme
and these generated by the Function
. Indeed,
Function
generally produces smaller principles that are closer to how
a user would implement them. See Advanced recursive functions for details.
Example
Induction scheme for div2.
We define the function div2 as follows:
 Require Import FunInd.
 [Loading ML file extraction_plugin.cmxs ... done] [Loading ML file recdef_plugin.cmxs ... done]
 Require Import Arith.
 [Loading ML file newring_plugin.cmxs ... done]
 Fixpoint div2 (n:nat) : nat := match n with  O => 0  S O => 0  S (S n') => S (div2 n') end.
 div2 is defined div2 is recursively defined (decreasing on 1st argument)
The definition of a principle of induction corresponding to the
recursive structure of div2
is defined by the command:
 Functional Scheme div2_ind := Induction for div2 Sort Prop.
 div2_equation is defined div2_ind is defined
You may now look at the type of div2_ind:
 Check div2_ind.
 div2_ind : forall P : nat > nat > Prop, (forall n : nat, n = 0 > P 0 0) > (forall n n0 : nat, n = S n0 > n0 = 0 > P 1 0) > (forall n n0 : nat, n = S n0 > forall n' : nat, n0 = S n' > P n' (div2 n') > P (S (S n')) (S (div2 n'))) > forall n : nat, P n (div2 n)
We can now prove the following lemma using this principle:
 Lemma div2_le' : forall n:nat, div2 n <= n.
 1 subgoal ============================ forall n : nat, div2 n <= n
 intro n.
 1 subgoal n : nat ============================ div2 n <= n
 pattern n, (div2 n).
 1 subgoal n : nat ============================ (fun n0 n1 : nat => n1 <= n0) n (div2 n)
 apply div2_ind; intros.
 3 subgoals n, n0 : nat e : n0 = 0 ============================ 0 <= 0 subgoal 2 is: 0 <= 1 subgoal 3 is: S (div2 n') <= S (S n')
 auto with arith.
 2 subgoals n, n0, n1 : nat e : n0 = S n1 e0 : n1 = 0 ============================ 0 <= 1 subgoal 2 is: S (div2 n') <= S (S n')
 auto with arith.
 1 subgoal n, n0, n1 : nat e : n0 = S n1 n' : nat e0 : n1 = S n' H : div2 n' <= n' ============================ S (div2 n') <= S (S n')
 simpl; auto with arith.
 No more subgoals.
 Qed.
 div2_le' is defined
We can use directly the functional induction (function induction
) tactic instead
of the pattern/apply trick:
 Reset div2_le'.
 Lemma div2_le : forall n:nat, div2 n <= n.
 1 subgoal ============================ forall n : nat, div2 n <= n
 intro n.
 1 subgoal n : nat ============================ div2 n <= n
 functional induction (div2 n).
 3 subgoals ============================ 0 <= 0 subgoal 2 is: 0 <= 1 subgoal 3 is: S (div2 n') <= S (S n')
 auto with arith.
 2 subgoals ============================ 0 <= 1 subgoal 2 is: S (div2 n') <= S (S n')
 auto with arith.
 1 subgoal n' : nat IHn0 : div2 n' <= n' ============================ S (div2 n') <= S (S n')
 auto with arith.
 No more subgoals.
 Qed.
 div2_le is defined
Example
Induction scheme for tree_size.
We define trees by the following mutual inductive type:
 Axiom A : Set.
 A is declared
 Inductive tree : Set := node : A > forest > tree with forest : Set :=  empty : forest  cons : tree > forest > forest.
 tree, forest are defined tree_rect is defined tree_ind is defined tree_rec is defined forest_rect is defined forest_ind is defined forest_rec is defined
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.
 Require Import FunInd.
 Function tree_size (t:tree) : nat := match t with  node A f => S (forest_size f) end with forest_size (f:forest) : nat := match f with  empty => 0  cons t f' => (tree_size t + forest_size f') end.
 tree_size is defined forest_size is defined tree_size, forest_size are recursively defined (decreasing respectively on 1st, 1st arguments) tree_size_equation is defined tree_size_ind is defined tree_size_rec is defined tree_size_rect is defined forest_size_equation is defined forest_size_ind is defined forest_size_rec is defined forest_size_rect is defined R_tree_size_correct is defined R_forest_size_correct is defined R_tree_size_complete is defined R_forest_size_complete is defined
Notice that the induction principles tree_size_ind
and forest_size_ind
generated by Function
are not mutual.
 Check tree_size_ind.
 tree_size_ind : forall P : tree > nat > Prop, (forall (t : tree) (A : A) (f : forest), t = node A f > P (node A f) (S (forest_size f))) > forall t : tree, P t (tree_size t)
Mutual induction principles following the recursive structure of tree_size
and forest_size
can be generated by the following command:
 Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop with forest_size_ind2 := Induction for forest_size Sort Prop.
 tree_size_ind2 is defined forest_size_ind2 is defined
You may now look at the type of tree_size_ind2
:
 Check tree_size_ind2.
 tree_size_ind2 : forall (P : tree > nat > Prop) (P0 : forest > nat > Prop), (forall (t : tree) (A : A) (f : forest), t = node A f > P0 f (forest_size f) > P (node A f) (S (forest_size f))) > (forall f0 : forest, f0 = empty > P0 empty 0) > (forall (f1 : forest) (t : tree) (f' : forest), f1 = cons t f' > P t (tree_size t) > P0 f' (forest_size f') > P0 (cons t f') (tree_size t + forest_size f')) > forall t : tree, P t (tree_size t)
Generation of inversion principles with Derive
Inversion
¶

Command
Derive Inversion ident with ident Sort sort
¶ 
Command
Derive Inversion ident with (forall binders, ident term) Sort sort
This command generates an inversion principle for the
inversion ... using ...
tactic. The firstident
is the name of the generated principle. The secondident
should be an inductive predicate, andbinders
the variables occurring in the termterm
. This command generates the inversion lemma for the sortsort
corresponding to the instanceforall binders, ident term
. When applied, it is equivalent to having inverted the instance with the tacticinversion
.

Variant
Derive Inversion_clear ident with ident Sort sort

Variant
Derive Inversion_clear ident with (forall binders, ident term) Sort sort
When applied, it is equivalent to having inverted the instance with the tactic inversion replaced by the tactic
inversion_clear
.

Variant
Derive Dependent Inversion ident with ident Sort sort

Variant
Derive Dependent Inversion ident with (forall binders, ident term) Sort sort
When applied, it is equivalent to having inverted the instance with the tactic
dependent inversion
.

Variant
Derive Dependent Inversion_clear ident with ident Sort sort

Variant
Derive Dependent Inversion_clear ident with (forall binders, ident term) Sort sort
When applied, it is equivalent to having inverted the instance with the tactic
dependent inversion_clear
.
Example
Consider the relation Le
over natural numbers and the following
parameter P
:
 Inductive Le : nat > nat > Set :=  LeO : forall n:nat, Le 0 n  LeS : forall n m:nat, Le n m > Le (S n) (S m).
 Le is defined Le_rect is defined Le_ind is defined Le_rec is defined
 Parameter P : nat > nat > Prop.
 P is declared
To generate the inversion lemma for the instance (Le (S n) m)
and the
sort Prop
, we do:
 Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort Prop.
 Check leminv.
 leminv : forall (n m : nat) (P : nat > nat > Prop), (forall m0 : nat, Le n m0 > P n (S m0)) > Le (S n) m > P n m
Then we can use the proven inversion lemma:
 Goal forall (n m : nat) (H : Le (S n) m), P n m.
 1 subgoal ============================ forall n m : nat, Le (S n) m > P n m
 intros.
 1 subgoal n, m : nat H : Le (S n) m ============================ P n m
 Show.
 1 subgoal n, m : nat H : Le (S n) m ============================ P n m
 inversion H using leminv.
 1 subgoal n, m : nat H : Le (S n) m ============================ forall m0 : nat, Le n m0 > P n (S m0)