\[\begin{split}\newcommand{\alors}{\textsf{then}} \newcommand{\alter}{\textsf{alter}} \newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\bool}{\textsf{bool}} \newcommand{\case}{\kw{case}} \newcommand{\conc}{\textsf{conc}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\conshl}{\textsf{cons\_hl}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\EqSt}{\textsf{EqSt}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\false}{\textsf{false}} \newcommand{\filter}{\textsf{filter}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\from}{\textsf{from}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\haslength}{\textsf{has\_length}} \newcommand{\hd}{\textsf{hd}} \newcommand{\ident}{\textsf{ident}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\lb}{\lambda} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\Nat}{\mathbb{N}} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\Prod}{\textsf{prod}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\si}{\textsf{if}} \newcommand{\sinon}{\textsf{else}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\true}{\textsf{true}} \newcommand{\Type}{\textsf{Type}} \newcommand{\unfold}{\textsf{unfold}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \newcommand{\zeros}{\textsf{zeros}} \end{split}\]

Proof schemes

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:

Command Scheme ident1 := Induction for ident2 Sort sort with identi := Induction for identj Sort sort*

This command is a high-level tool for generating automatically (possibly mutual) induction principles for given types and sorts. Each identj is a different inductive type identifier belonging to the same package of mutual inductive definitions. The command generates the identis to be mutually recursive definitions. Each term identi proves a general principle of mutual induction for objects in type identj.

Variant Scheme ident := Minimality for ident Sort sort with ident := Minimality for ident' Sort sort*

Same as before but defines a non-dependent 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

Inductive tree : Set := node : A -> forest -> tree
with forest : Set :=
    leaf : B -> forest
  | cons : tree -> forest -> forest.

Scheme tree_forest_rec := Induction for tree Sort Set
  with forest_tree_rec := Induction for forest Sort Set.

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).

The following command generates a powerful elimination principle:

Scheme odd_even := Minimality for odd Sort Prop
with even_odd := Minimality for even Sort Prop.

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 and Record 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 well-defined inductive types because it cannot compute a Boolean equality for them.

Flag Rewriting Schemes

This flag governs generation of equality-related schemes such as congruence.

Combined Scheme

Command Combined Scheme ident from identi+,

This command is a tool for combining induction principles generated by the Scheme command. Each identi is a different inductive principle 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. In the case where all the inductive principles used are in sort Prop, the propositional conjunction and is used, otherwise the simple product prod 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.

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.

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 sort Type:

Scheme tree_forest_rect := Induction for tree Sort Type
with forest_tree_rect := Induction for forest Sort Type.

Combined Scheme tree_forest_mutrect from tree_forest_rect, forest_tree_rect.

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 ident0 := Induction for ident' Sort sort with identi := Induction for identi' Sort sort*

This command is a high-level experimental tool for generating automatically induction principles corresponding to (possibly mutually recursive) functions. First, it must be made available via Require Import FunInd. Each identi 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 each identi, following the recursive structure and case analyses of the corresponding function identi'.

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.
Require Import Arith.

Fixpoint div2 (n:nat) : nat :=
match n with
| O => 0
| S O => 0
| S (S n') => S (div2 n')
end.

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.

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.
forall n : nat, div2 n <= n
intro n.
n:nat
div2 n <= n
pattern n, (div2 n).
n:nat
(fun n0 n1 : nat => n1 <= n0) n (div2 n)
apply div2_ind; intros.
n, n0:nat
e:n0 = 0
0 <= 0
n, n0, n1:nat
e:n0 = S n1
e0:n1 = 0
0 <= 1
n, n0, n1:nat
e:n0 = S n1
n':nat
e0:n1 = S n'
H:div2 n' <= n'
S (div2 n') <= S (S n')
auto with arith.
n, n0, n1:nat
e:n0 = S n1
e0:n1 = 0
0 <= 1
n, n0, n1:nat
e:n0 = S n1
n':nat
e0:n1 = S n'
H:div2 n' <= n'
S (div2 n') <= S (S n')
auto with arith.
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.
Qed.

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.
forall n : nat, div2 n <= n
intro n.
n:nat
div2 n <= n
functional induction (div2 n).
0 <= 0
0 <= 1
n':nat
IHn0:div2 n' <= n'
S (div2 n') <= S (S n')
auto with arith.
0 <= 1
n':nat
IHn0:div2 n' <= n'
S (div2 n') <= S (S n')
auto with arith.
n':nat
IHn0:div2 n' <= n'
S (div2 n') <= S (S n')
auto with arith.
Qed.

Example

Induction scheme for tree_size.

We define trees by the following mutual inductive type:

Axiom A : Set.

Inductive tree : Set :=
node : A -> forest -> tree
with forest : Set :=
| empty : forest
| cons : tree -> forest -> forest.

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.

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.

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 first ident is the name of the generated principle. The second ident should be an inductive predicate, and binders the variables occurring in the term term. This command generates the inversion lemma for the sort sort corresponding to the instance forall binders, ident term. When applied, it is equivalent to having inverted the instance with the tactic inversion.

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).

Parameter P : nat -> nat -> Prop.

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:

Show.
1 subgoal

  n, m : nat
  H : Le (S n) m
  ============================
  P n m
n, m:nat
H:Le (S n) m
P n m

inversion H using leminv.
n, m:nat
H:Le (S n) m
forall m0 : nat, Le n m0 -> P n (S m0)