path: root/doc/sphinx/user-extensions/proof-schemes.rst

.. _proofschemes:

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:

.. cmd:: Scheme ident := Induction for ident' Sort sort {* with ident := Induction for ident' Sort sort}

where each `ident'ᵢ` is a different inductive type identifier 
belonging to the same package of mutual inductive definitions. This
command generates the `identᵢ`s to be mutually recursive
definitions. Each term `identᵢ` proves a general principle of mutual
induction for objects in type `identᵢ`.

.. cmdv:: 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.

.. cmdv:: 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.

.. cmdv:: 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.

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

    .. coqtop:: none

     Axiom A : Set.	       
     Axiom B : Set.	       
   
    .. coqtop:: all

     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:

  .. coqtop:: all

    Check tree_forest_rec.

  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:

   .. coqtop:: all

      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:

   .. coqtop:: all

    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:

  .. coqtop:: all

    Check odd_even.

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


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

The types declared with the keywords ``Variant`` (see :ref:`TODO-1.3.3`) and ``Record``
(see :ref:`Record Types <record-types>`) do not have an automatic declaration of the induction
principles. It can be activated with the command
``Set Nonrecursive Elimination Schemes``. It can be deactivated again with
``Unset Nonrecursive Elimination Schemes``.

In addition, the ``Case Analysis Schemes`` flag governs the generation of
case analysis lemmas for inductive types, i.e. corresponding to the
pattern-matching term alone and without fixpoint.
You can also activate the automatic declaration of those Boolean
equalities (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.

.. opt:: Rewriting Schemes

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

Combined Scheme
~~~~~~~~~~~~~~~~~~~~~~

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

.. cmd:: Combined Scheme ident from {+, ident}

where each identᵢ after the ``from`` is a different inductive principle that must
belong to the same package of mutual inductive principle definitions.
This command generates the leftmost `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:

  .. coqtop:: all

    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:

  .. coqtop:: all

    Combined Scheme tree_forest_mutind from tree_forest_ind,forest_tree_ind.

  The type of tree_forest_mutrec will be:

  .. coqtop:: all

    Check tree_forest_mutind.

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. First, it must be made
available via ``Require Import FunInd``. Its syntax then follows the
schema:

.. cmd:: Functional Scheme ident := Induction for ident' Sort sort {* with ident := Induction for ident' Sort sort}

where each `ident'ᵢ` 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 `identᵢ`, following
the recursive structure and case analyses of the corresponding function 
identᵢ’.

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

  Induction scheme for div2.

  We define the function div2 as follows:

  .. coqtop:: all

   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:

  .. coqtop:: all

    Functional Scheme div2_ind := Induction for div2 Sort Prop.

  You may now look at the type of div2_ind:

  .. coqtop:: all

    Check div2_ind.

  We can now prove the following lemma using this principle:

  .. coqtop:: all

    Lemma div2_le' : forall n:nat, div2 n <= n.
    intro n.
    pattern n, (div2 n).
    apply div2_ind; intros.
    auto with arith.
    auto with arith.
    simpl; auto with arith.
    Qed.

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

  .. coqtop:: all

    Reset div2_le'.

    Lemma div2_le : forall n:nat, div2 n <= n.
    intro n.
    functional induction (div2 n).
    auto with arith.
    auto with arith.
    auto with arith.
    Qed.

  Remark: There is a difference between obtaining an induction scheme
  for a function by using ``Function`` (see :ref:`advanced-recursive-functions`) and by using
  ``Functional Scheme`` after a normal definition using ``Fixpoint`` or
  ``Definition``. See :ref:`advanced-recursive-functions` for details.

.. example::

  Induction scheme for tree_size.

  We define trees by the following mutual inductive type:

  .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning
   
  .. coqtop:: reset all

     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.

  .. coqtop:: all

    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.

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

  .. coqtop:: all

    Check tree_size_ind.

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

  .. coqtop:: all

    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`:

  .. coqtop:: all

    Check tree_size_ind2.
     
Generation of inversion principles with ``Derive`` ``Inversion``
-----------------------------------------------------------------

The syntax of ``Derive`` ``Inversion`` follows the schema:

.. cmd:: 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`.

.. cmdv:: 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`.

.. cmdv:: 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`.

.. cmdv:: 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:

  .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning
  
  .. coqtop:: all

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

    Axiom P : nat -> nat -> Prop.

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

  .. coqtop:: all

    Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort Prop.
    Check leminv.

  Then we can use the proven inversion lemma:

  .. the original LaTeX did not have any Coq code to setup the goal

  .. coqtop:: none

    Goal forall (n m : nat) (H : Le (S n) m), P n m.			  
    intros.
  
  .. coqtop:: all

    Show.

    inversion H using leminv.