Skip to content

Commit

Permalink
Review #1
Browse files Browse the repository at this point in the history
  • Loading branch information
@jfehrle
jfehrle committed Jul 13, 2021
1 parent e1106a1 commit 44d18e9
Showing 1 changed file with 93 additions and 79 deletions.
172 changes: 93 additions & 79 deletions doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -119,13 +119,12 @@ analysis on inductive or co-inductive objects (see :ref:`variants`).

.. tacn:: destruct {+, @induction_clause } {? @induction_principle }

.. insertprodn induction_clause induction_principle
.. insertprodn induction_clause induction_arg
.. prodn::
induction_clause ::= @induction_arg {? as @or_and_intropattern } {? eqn : @naming_intropattern } {? @occurrences }
induction_arg ::= @natural
| @one_term_with_bindings
induction_principle ::= using @one_term {? with @bindings } {? @occurrences }
Performs case analysis by generating a subgoal for each constructor of the
inductive or co-inductive type in the :n:`@one_term` in :n:`@induction_arg`.
Expand Down Expand Up @@ -239,6 +238,11 @@ Induction

.. tacn:: induction {+, @induction_clause } {? @induction_principle }

.. insertprodn induction_principle induction_principle
.. prodn::
induction_principle ::= using @one_term {? with @bindings } {? @occurrences }

Applies an :term:`induction principle` to generate a subgoal for
each constructor of an inductive type.

Expand All @@ -249,83 +253,93 @@ Induction
is **IH**. The tactic is similar to :tacn:`destruct`, except that
`destruct` doesn't generate induction hypotheses.

There are several cases:
:n:`induction @one_term ...` also works when the type of :n:`@one_term` is a statement
with premises and whose conclusion is inductive. In that case the tactic
performs induction on the conclusion of the type of :n:`@one_term` and leaves the
:term:`non-dependent premises <dependent premise>` of the type as subgoals.
In the case of dependent products, the tactic tries to find an instance for
which the induction principle applies and otherwise fails.

Most parameters behave as they do in :tacn:`destruct`, with the following
differences:

+ If :n:`@one_term` (in :n:`@induction_arg`)
is an identifier :n:`@ident` denoting a quantified variable of the
conclusion of the goal, then :n:`induction @ident` behaves like :tacn:`intros` :n:`until
@ident; induction @ident`. If :n:`@ident` is no longer dependent in the
@ident; induction @ident`. :n:`@one_term` must have an inductive type.
If :n:`@ident` is no longer dependent in the
goal after application of :n:`induction`, it is erased. To avoid erasure,
use parentheses, as in :n:`induction (@ident)`.
+ If :n:`@induction_arg` is a :n:`@natural`, then :n:`induction @natural` behaves like
:n:`intros until @natural` followed by :n:`induction` applied to the last
introduced hypothesis.

.. note::
For simple induction on a number, use the form `induction (number)`
For induction on a number, use the form `induction (number)`
(which is not very interesting).

+ If :n:`@one_term` is a hypothesis :n:`@ident` of the context, and :n:`@ident`
is no longer dependent in the goal after application of :n:`induction`,
it is erased (to avoid erasure, use parentheses, as in
:n:`induction (@ident)`).
+ The argument :n:`@one_term` can also be a pattern in which holes are denoted
by “_”. In this case, the tactic checks that all subterms matching the
pattern in the conclusion and the hypotheses are compatible and
performs induction using this subterm.

:n:`{+, @induction_clause }`
If no using clause is provided, this is equivalent to doing :n:`induction` on the
first :n:`@induction_clause` followed by :n:`destruct` on any subsequent clauses.
If no :n:`induction_principle` clause is provided, this is equivalent to doing
:n:`induction` on the first :n:`@induction_clause` followed by :n:`destruct`
on any subsequent clauses.

:n:`using @one_term {? with @bindings }`
Specifies which :term:`induction principle` to use and, optionally, what bindings
:n:`@induction_principle`
:n:`one_term` specifies which :term:`induction principle` to use and, optionally,
what bindings
to apply to the induction principle. The number of :n:`@induction_clause`\s
must be the same as the number of parameters of the induction principle.

Other parameters behave as they do in :tacn:`destruct`.
If unspecified, the tactic applies the appropriate :term:`induction principle`
that was automatically generated when the inductive type was declared based
on the type of the goal.

.. example::
.. exn:: Not an inductive product.
:undocumented:

.. coqtop:: reset all
.. exn:: Unable to find an instance for the variables @ident … @ident.

Lemma induction_test : forall n:nat, n = n -> n <= n.
intros n H.
induction n.
exact (le_n 0).
Use the :n:`with @bindings` clause or the :tacn:`einduction` tactic instead.

.. example:: :tacn:`induction` with :n:`@occurrences`
.. example::

.. coqtop:: reset all
.. coqtop:: reset all

Lemma comm x y : x + y = y + x.
induction y in x |- *.
Show 2.
Lemma induction_test : forall n:nat, n = n -> n <= n.
intros n H.
induction n.
exact (le_n 0).

.. exn:: Not an inductive product.
:undocumented:
.. example:: :tacn:`induction` with :n:`@occurrences`

.. exn:: Unable to find an instance for the variables @ident … @ident.
.. coqtop:: reset all

Use the variant :tacn:`elim` `… with …` instead.
Lemma induction_test2 : forall n:nat, n = n -> n <= n.
intros.
induction n in H |-.
Show 2.
.. tacn:: einduction {+, @induction_clause } {? @induction_principle }
.. tacn:: einduction {+, @induction_clause } {? @induction_principle }

Behaves like :tacn:`induction` except that it does not fail if
some dependent premise of the type of :n:`@one_term` is not inferrable. Instead,
the unresolved premises are posed as existential variables to be inferred
later, in the same way as :tacn:`eapply` does.
Behaves like :tacn:`induction` except that it does not fail if
some dependent premise of the type of :n:`@one_term` is not inferrable. Instead,
the unresolved premises are posed as existential variables to be inferred
later, in the same way as :tacn:`eapply` does.

.. tacn:: elim @one_term_with_bindings {? using @one_term {? with @bindings } }

An older, more basic induction tactic. We recommend using :tacn:`induction`
instead where possible. :n:`@one_term` must have an inductive
An older, more basic induction tactic. Unlike :tacn:`induction`, ``elim`` only
modifies the goal; it does not modify the :term:`local context`. We recommend
using :tacn:`induction` instead where possible. :n:`@one_term` must have an inductive
type. The tactic applies the appropriate :term:`induction principle` based
on the type of the goal. (For example, if the local context
contains :g:`n : nat` and the current goal is :g:`T` of type :g:`Prop`, then
:n:`elim k` is equivalent to :tacn:`apply` :n:`nat_ind with (n:=k)` since
`nat_ind` is for `Prop` goals.)
``elim`` only modifies the goal; it does not modify the :term:`local context`.

More generally,
:n:`elim @one_term` also works when the type of :n:`@one_term` is a statement
Expand All @@ -335,7 +349,7 @@ Induction
In the case of dependent products, the tactic tries to find an instance for
which the induction principle applies and otherwise fails.

:n:`with @bindings`
:n:`with @bindings` (in :n:`@one_term_with_bindings`)
Explicitly gives instances to the premises of the type of :n:`@one_term`
(see :ref:`bindings`).

Expand All @@ -357,7 +371,7 @@ Induction
hypothesis :g:`Hn` will not appear in the context(s) of the subgoal(s).
Conversely, if :g:`t` is a :n:`@one_term` of (inductive) type :g:`I` that does
not occur in the goal, then :n:`elim t` is equivalent to
:n:`elimtype I; 2:` :tacn:`exact` `t.`
:n:`elimtype I; only 2:` :tacn:`exact` `t.`

.. tacn:: simple induction {| @ident | @natural }

Expand All @@ -366,9 +380,9 @@ Induction

.. tacn:: dependent induction @ident {? {| generalizing | in } {+ @ident } } {? using @one_term }

The *experimental* tactic :tacn:`dependent induction` performs induction-
inversion on an instantiated inductive predicate. One needs to first
:cmd:`Require` the Coq.Program.Equality module to use this tactic. The tactic
The *experimental* tactic :tacn:`dependent induction` performs
induction-inversion on an instantiated inductive predicate. One needs to first
:cmd:`Require` the `Coq.Program.Equality` module to use this tactic. The tactic
is based on the BasicElim tactic by Conor McBride
:cite:`DBLP:conf/types/McBride00` and the work of Cristina Cornes around
inversion :cite:`DBLP:conf/types/CornesT95`. From an instantiated
Expand All @@ -387,46 +401,45 @@ Induction
There is a long example of :tacn:`dependent induction` and an explanation
of the underlying technique :ref:`here <dependent-induction-examples>`.

.. example::

.. coqtop:: reset all
.. example::

Lemma lt_1_r : forall n:nat, n < 1 -> n = 0.
intros n H ; induction H.
.. coqtop:: reset all

Here we did not get any information on the indexes to help fulfill
this proof. The problem is that, when we use the ``induction`` tactic, we
lose information on the hypothesis instance, notably that the second
argument is 1 here. Dependent induction solves this problem by adding
the corresponding equality to the context.
Lemma lt_1_r : forall n:nat, n < 1 -> n = 0.
intros n H ; induction H.

.. coqtop:: reset all
Here we did not get any information on the indexes to help fulfill
this proof. The problem is that, when we use the ``induction`` tactic, we
lose information on the hypothesis instance, notably that the second
argument is 1 here. Dependent induction solves this problem by adding
the corresponding equality to the context.

Require Import Coq.Program.Equality.
Lemma lt_1_r : forall n:nat, n < 1 -> n = 0.
intros n H ; dependent induction H.
.. coqtop:: reset all

The subgoal is cleaned up as the tactic tries to automatically
simplify the subgoals with respect to the generated equalities. In
this enriched context, it becomes possible to solve this subgoal.
Require Import Coq.Program.Equality.
Lemma lt_1_r : forall n:nat, n < 1 -> n = 0.
intros n H ; dependent induction H.

.. coqtop:: all
The subgoal is cleaned up as the tactic tries to automatically
simplify the subgoals with respect to the generated equalities. In
this enriched context, it becomes possible to solve this subgoal.

reflexivity.
.. coqtop:: all

Now we are in a contradictory context and the proof can be solved.
reflexivity.

.. coqtop:: all abort
Now we are in a contradictory context and the proof can be solved.

inversion H.
.. coqtop:: all abort

This technique works with any inductive predicate. In fact, the
:tacn:`dependent induction` tactic is just a wrapper around the ``induction``
tactic. One can make its own variant by just writing a new tactic
based on the definition found in ``Coq.Program.Equality``.
inversion H.

.. seealso:: :tacn:`functional induction`
This technique works with any inductive predicate. In fact, the
:tacn:`dependent induction` tactic is just a wrapper around the :tacn:`induction`
tactic. One can make its own variant by just writing a new tactic
based on the definition found in ``Coq.Program.Equality``.

.. seealso:: :tacn:`functional induction`

.. tacn:: fix @ident @natural {? with {+ ( @ident {* @simple_binder } {? %{ struct @name %} } : @type ) } }

Expand All @@ -452,33 +465,34 @@ Induction
arguments are correct is done only when registering the
lemma in the global environment. To know if the use of induction hypotheses
is correct during the interactive development of a proof, use
the command :cmd:`Guarded` (see Section :ref:`requestinginformation`).
the command :cmd:`Guarded`.

:n:`with {+ ( @ident {* @simple_binder } {? %{ struct @name %} } : @type ) }`
Starts a proof by mutual induction. The statements to be proven
are :n:`forall @simple_binder__i, @type__i`.
The identifiers :n:`@ident` are the names of the induction hypotheses. The identifiers
:n:`@ident` are the respective names of the premises on which the induction
The identifiers :n:`@ident` (including the first one before the `with` clause)
are the names of the induction hypotheses. The identifiers
:n:`@name` are the respective names of the premises on which the induction
is performed in the statements to be proved (if not given, Coq
guesses what they are).

.. tacn:: cofix @ident {? with {+ ( @ident {* @simple_binder } : @type ) } }

.. todo:
Starts a proof by co-induction. The first :n:`@ident` is the
name of the co-induction hypothesis. As in a cofix expression,
Starts a proof by co-induction. The :n:`@ident`\s (including the first one
before the `with` clause) are the
names of the co-induction hypothesis. As in a cofix expression,
the use of induction hypotheses must be guarded by a constructor. The
verification that the use of co-inductive hypotheses is correct is
done only at the time of registering the lemma in the global environment. To
know if the use of co-induction hypotheses is correct at some time of
the interactive development of a proof, use the command ``Guarded``
(see Section :ref:`requestinginformation`).
the interactive development of a proof, use the command :cmd`Guarded`.


:n:`with {+ ( @ident {* @simple_binder } : @type ) }`
Starts a proof by mutual co-induction. The statements to be
proven are :n:`forall @simple_binder__i, @type__i`.
The identifiers :n:`@ident` are the names of the co-induction hypotheses.
The identifiers :n:`@ident` (including the first one before the `with` clause)
are the names of the co-induction hypotheses.

.. _equality-inductive_types:

Expand Down

0 comments on commit 44d18e9

Please sign in to comment.