\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \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{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#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}{\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{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \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{\Type}{\textsf{Type}} \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}]} \end{split}\]

# Reasoning with inductive types

## Applying constructors

The tactics presented here specialize `apply` and `eapply` to constructors of inductive types.

Tactic constructor nat_or_var? with bindings?

  First does `repeat intro; hnf` on the goal. If the result is an inductive type `I`, then apply the appropriate constructor(s), and otherwise fail. If `nat_or_var` is specified and has the value `i`, it uses `apply ci`, where `ci` is the i-th constructor of `I`. If not specified, the tactic tries all the constructors, which can result in more than one success (e.g. for `\/`) when using backtracking tactics such as `constructor; ...`. See `ltac-seq`.

  `with bindings?`

    If specified, the `apply` is done as `apply … with bindings`.

    Warning

    The terms in `bindings` are checked in the context where constructor is executed and not in the context where `apply` is executed (the introductions are not taken into account).

  Error Not an inductive product.
  Error Not enough constructors.
  Error The type has no constructors.

Tactic split with bindings?

  Equivalent to `constructor 1 with bindings?` when the conclusion is an inductive type with a single constructor. The `bindings` specify any parameters required for the constructor. It is typically used to split conjunctions in the conclusion such as `A /\ B` into two new goals `A` and `B`.

  To `split` a hypothesis `H` that begins with `and`, use `destruct` `H`. See example.

Tactic exists bindings*,

  Equivalent to `constructor 1 with bindingsi` for each set of bindings (or just `constructor 1` if there are no `bindings`) when the conclusion is an inductive type with a single constructor. It is typically used on existential quantifications in the form `exists x, P x.`

  Error Not an inductive goal with 1 constructor.

Tactic left with bindings?
Tactic right with bindings?

  These tactics apply only if `I` has two constructors, for instance in the case of a disjunction `A \/ B`. Then they are respectively equivalent to `constructor 1 with bindings?` and `constructor 2 with bindings?`.

  Error Not an inductive goal with 2 constructors.

Tactic econstructor nat_or_var with bindings??
Tactic eexists bindings*,
Tactic esplit with bindings?
Tactic eleft with bindings?
Tactic eright with bindings?

  These tactics behave like `constructor`, `exists`, `split`, `left` and `right`, but they introduce existential variables instead of failing when a variable can't be instantiated (cf. `eapply` and `apply`).

Example: `constructor`, `left` and `right`

Print or. (* or, represented by \/, has two constructors, or_introl and or_intror *)
  Inductive or (A B : Prop) : Prop := or_introl : A -> A \/ B | or_intror : B -> A \/ B. Arguments or (A B)%_type_scope Arguments or_introl [A B]%_type_scope _, [_] _ _ Arguments or_intror [A B]%_type_scope _, _ [_] _
Goal forall P1 P2 : Prop, P1 -> P1 \/ P2.
  1 goal ============================ forall P1 P2 : Prop, P1 -> P1 \/ P2
constructor 1. (* equivalent to "left" *)
  1 goal P1, P2 : Prop H : P1 ============================ P1
apply H. (* success *)
  No more goals.

In contrast, we won't be able to complete the proof if we select constructor 2:

Goal forall P1 P2 : Prop, P1 -> P1 \/ P2.
  1 goal ============================ forall P1 P2 : Prop, P1 -> P1 \/ P2

constructor 2. (* equivalent to "right" *)
  1 goal P1, P2 : Prop H : P1 ============================ P2

You can also apply a constructor by name:

Goal forall P1 P2 : Prop, P1 -> P1 \/ P2.
  1 goal ============================ forall P1 P2 : Prop, P1 -> P1 \/ P2

intros; apply or_introl. (* equivalent to "left" *)
  1 goal P1, P2 : Prop H : P1 ============================ P1

## Case analysis

The tactics in this section implement case analysis on inductive or coinductive objects (see Variants and the match construct).

Tactic destruct induction_clause+, induction_principle?
  induction_clause`::=`induction_arg as or_and_intropattern? eqn : naming_intropattern? occurrences?``induction_arg`::=`one_term_with_bindings`````|`natural``

  Performs case analysis by generating a subgoal for each constructor of the inductive or coinductive type selected by `induction_arg`. The selected subterm, after possibly doing an `intros`, must have an inductive or coinductive type. Unlike `induction`, `destruct` generates no induction hypothesis (see `induction` example).

  In each new subgoal, the tactic replaces the selected subterm with the associated constructor applied to its arguments, if any.

  Applying `destruct` to a hypothesis beginning with `and` such as `A /\ B` or `A <-> B` splits the hypothesis into multiple hypotheses without creating new subgoals. Example here.

  `induction_clause+,`

    Giving multiple `induction_clause`s is equivalent to applying `destruct` serially on each `induction_clause`.

  `induction_arg`

    - If `one_term` (in `one_term_with_bindings`) is an identifier `ident`:

      - If `ident` denotes a `forall` variable in the goal, then `destruct ident` behaves like `intros` `until ident; destruct ident`.

      - If `ident` is not referenced directly or indirectly in the goal or unselected hypotheses after application of `destruct`, it is erased (unless it is a section variable). To avoid erasure, parenthesize the argument to make it a `term` rather than an `ident`, as in `destruct (ident)`.

    - `one_term` may contain holes that are denoted by “_”. In this case, the tactic selects the first subterm that matches the pattern and performs case analysis using that subterm.

    - If `induction_arg` is a `natural`, then `destruct natural` behaves like `intros until natural` followed by `destruct` applied to the last introduced premise.

  `as or_and_intropattern`

    Provides names for (or applies further transformations to) the variables and hypotheses introduced in each new subgoal. The `or_and_intropattern` must have one `intropattern*` for each constructor, given in the order in which the constructors are defined. If there are not enough names, Rocq picks fresh names. Inner `intropattern`s can also split introduced hypotheses into multiple hypotheses or subgoals.

  `eqn : naming_intropattern`

    Generates a new hypothesis in each new subgoal that is an equality between the term being case-analyzed and the associated constructor (applied to its arguments). The name of the new item may be specified in the `naming_intropattern`.

  `with bindings` (in `one_term_with_bindings`)

    Provides explicit instances for the dependent premises of the type of `one_term`.

  `occurrences`

    Selects specific subterms of the goal and/or hypotheses to apply the tactic to. See Occurrence clauses. If it occurs in the `induction_principle`, then there can only be one `induction_clause`, which can't have its own `occurrences` clause.

  `induction_principle`

    Makes the tactic equivalent to `induction` `induction_clause+, induction_principle`.

  Example: Using `destruct`

  Creates a subgoal for each constructor, substituting the constructor into the hypotheses and conclusion.

  Goal forall m n: nat, n = n -> m + n = n + m.
    1 goal ============================ forall m n : nat, n = n -> m + n = n + m
  intros.
    1 goal m, n : nat H : n = n ============================ m + n = n + m
  destruct n.
    2 goals m : nat H : 0 = 0 ============================ m + 0 = 0 + m goal 2 is: m + S n = S n + m
  2: { (* no induction hypothesis created *)
    1 goal m, n : nat H : S n = S n ============================ m + S n = S n + m

  Example: `induction` creating an induction hypotheses

  Like `destruct`, creates a subgoal for each constructor, substituting the constructor into the hypotheses and conclusion. In addition, `induction` creates induction hypotheses in appropriate subgoals (compare to the previous example).

  Goal forall m n: nat, n = n -> m + n = n + m.
    1 goal ============================ forall m n : nat, n = n -> m + n = n + m
  intros.
    1 goal m, n : nat H : n = n ============================ m + n = n + m
  induction n.
    2 goals m : nat H : 0 = 0 ============================ m + 0 = 0 + m goal 2 is: m + S n = S n + m
  2: { (* IHn is the induction hypothesis *)
    1 goal m, n : nat H : S n = S n IHn : n = n -> m + n = n + m ============================ m + S n = S n + m

  Example: Using `destruct` on a hypothesis beginning with `and`

  Goal forall A B: Prop, A /\ B -> True.
    1 goal ============================ forall A B : Prop, A /\ B -> True
  intros.
    1 goal A, B : Prop H : A /\ B ============================ True
  destruct H.
    1 goal A, B : Prop H : A H0 : B ============================ True

  Example: Using `destruct` on an argument with premises

  Parameter A B C D : Prop.
    A is declared B is declared C is declared D is declared
  Goal (A -> B \/ C) -> D.
    1 goal ============================ (A -> B \/ C) -> D
  intros until 1.
    1 goal H : A -> B \/ C ============================ D
  destruct H.
    3 goals ============================ A goal 2 is: D goal 3 is: D
  Show 2.
    goal 2 is: H : B ============================ D
  Show 3.
    goal 3 is: H : C ============================ D

  The single tactic `destruct 1` is equivalent to the `intros` and `destruct` used here.

  Tactic edestruct induction_clause+, induction_principle?

    If the type of `one_term` (in `induction_arg`) has dependent premises whose values can't be inferred from the `with bindings` clause, `edestruct` turns them into existential variables to be resolved later on.

Tactic case induction_clause+, induction_principle?

  An older, more basic tactic to perform case analysis without recursion. We recommend using `destruct` instead where possible. `case` only modifies the goal; it does not modify the local context.

  Tactic ecase induction_clause+, induction_principle?

    If the type of `one_term` (in `induction_arg`) has dependent premises whose values can't be inferred from the `with bindings` clause, `ecase` turns them into existential variables to be resolved later on.

  Tactic case_eq one_term

    A variant of the `case` tactic that allows performing case analysis on a term without completely forgetting its original form. This is done by generating equalities between the original form of the term and the outcomes of the case analysis. We recommend using the `destruct` tactic with an `eqn:` clause instead.

Tactic simple destruct ident​natural

  Equivalent to `intros` `until ident​natural; case ident` where `ident` is a `forall` variable in the goal and otherwise fails.

Tactic dependent destruction ident generalizing ident+? using one_term?

  Note

  This tactic requires the Stdlib library.

  There is a long example of `dependent destruction` and an explanation of the underlying technique here.

Tactic decompose [ one_term+ ] one_term

  Recursively decomposes a complex proposition in order to obtain atomic ones.

  Example

  Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C.
    1 goal ============================ forall A B C : Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C
  intros A B C H; decompose [and or] H.
    3 goals A, B, C : Prop H : A /\ B /\ C \/ B /\ C \/ C /\ A H1 : A H0 : B H3 : C ============================ C goal 2 is: C goal 3 is: C
  all: assumption.
    No more goals.
  Qed.

  Note

  `decompose` does not work on right-hand sides of implications or products.

  Tactic decompose sum one_term

    This decomposes sum types (like `or`).

  Tactic decompose record one_term

    This decomposes record types (inductive types with one constructor, like `and` and `exists` and those defined with the `Record` command.

## Induction

Tactic induction induction_clause+, induction_principle?
  induction_principle`::=`using one_term_with_bindings occurrences?``

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

  If the argument is dependent in the conclusion or some hypotheses of the goal, the argument is replaced by the appropriate constructor in each of the resulting subgoals and induction hypotheses are added to the local context using names whose prefix is IH. The tactic is similar to `destruct`, except that `destruct` doesn't generate induction hypotheses.

  `induction` and `destruct` are very similar. Aside from the following differences, please refer to the description of `destruct` while mentally substituting `induction` for `destruct`.

  `induction_clause+,`

    If no `induction_principle` clause is provided, this is equivalent to doing `induction` on the first `induction_clause` followed by `destruct` on any subsequent clauses.

  `induction_principle`

    `one_term` specifies which induction principle to use. The optional `with bindings` gives any values that must be substituted into the induction principle. The number of `bindings` must be the same as the number of parameters of the induction principle.

    If unspecified, the tactic finds the appropriate induction principle using the "scheme" registration. The scheme kind depends on the sort of the goal: `sind` for `SProp`, `ind` for `Prop`, `rec` for `Set` and `rect` for `Type`. It also has a `_dep` or `_nodep` suffix indicating whether it is dependent in the eliminated value (i.e. in `Scheme`, `Induction` is `_dep` and `Minimality` is `_nodep`). When both `_dep` and `_nodep` schemes are registered for the eliminated inductive and goal sort, the `_dep` scheme is used unless the inductive type was explicitly declared in `Prop`.

    Automatically generated schemes and schemes produced by `Scheme` are automatically registered. Constants may also be registered using `Register Scheme`, e.g. `Register Scheme my_foo_elim as rect_dep for foo` where `my_foo_elim` is a dependent elimination scheme for inductive `foo` at sort `Type`.

    If no scheme is registered for the eliminated inductive and goal sort, `induction` attempts to find a constant from the same module as the inductive whose name is the inductive's name suffixed by `sind` / `ind` / `rec` / `rect`. This name-based lookup is deprecated.

  Error Cannot recognize a statement based on reference.

    The type of the `induction_arg` (in an `induction_clause`) must reduce to the `reference` which was inferred as the type the induction principle operates on. Note that it is not enough to be convertible, but you can work around that with `change`:

    Definition N := nat.
      N is defined
    Axiom strong : forall P, (forall n:N, (forall m:N, m < n -> P m) -> P n) -> forall n, P n.
      strong is declared
    Axiom P : N -> Prop.
      P is declared
    Goal forall n:nat, P n.
      1 goal ============================ forall n : nat, P n
    intros.
      1 goal n : nat ============================ P n
    Fail induction n using strong.
      The command has indeed failed with message: Cannot recognize a statement based on N.
    change N in n.
      1 goal n : N ============================ P n
    (* n is now of type N, matching the inferred type that strong operates on *) induction n using strong.
      1 goal n : N H : forall m : N, m < n -> P m ============================ P n
  Error Unable to find an instance for the variables ident … ident.

    Use the `with bindings` clause or the `einduction` tactic instead.

  Example

  Lemma induction_test : forall n:nat, n = n -> n <= n.
    1 goal ============================ forall n : nat, n = n -> n <= n
  intros n H.
    1 goal n : nat H : n = n ============================ n <= n
  induction n.
    2 goals H : 0 = 0 ============================ 0 <= 0 goal 2 is: S n <= S n
  exact (le_n 0).
    1 goal n : nat H : S n = S n IHn : n = n -> n <= n ============================ S n <= S n

  Example: `induction` with `occurrences`

  `induction in` is useful to generalize over other variables:

  Lemma induction_test2 : forall n m:nat, n = m -> n <= m.
    1 goal ============================ forall n m : nat, n = m -> n <= m
  intros n m H.
    1 goal n, m : nat H : n = m ============================ n <= m
  induction n in m, H |- *.
    2 goals m : nat H : 0 = m ============================ 0 <= m goal 2 is: S n <= m
  Show 2.
    goal 2 is: n, m : nat H : S n = m IHn : forall m : nat, n = m -> n <= m ============================ S n <= m
  Tactic einduction induction_clause+, induction_principle?

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

Tactic elim one_term_with_bindings using one_term_with_bindings?

  An older, more basic induction tactic. Unlike `induction`, `elim` only modifies the goal; it does not modify the local context. We recommend using `induction` instead where possible.

  `with bindings` (in `one_term_with_bindings`)

    Explicitly gives instances to the premises of the type of `one_term` (see Bindings).

  `using one_term_with_bindings?`

    Allows explicitly giving an induction principle `one_term` that is not the standard one for the underlying inductive type of `one_term`. The `bindings` clause allows instantiating premises of the type of `one_term`.

  Tactic eelim one_term_with_bindings using one_term_with_bindings?

    If the type of `one_term` has dependent premises, this turns them into existential variables to be resolved later on.

Tactic simple induction ident​natural

  Behaves like `intros until ident​natural; elim ident` when `ident` is a `forall` variable in the goal.

Tactic dependent induction ident generalizing​in ident+? using one_term?

  Note

  This tactic requires the Stdlib library.

  The experimental tactic `dependent induction` performs induction-inversion on an instantiated inductive predicate. One needs to first `Require` the `Stdlib.Program.Equality` module to use this tactic. The tactic is based on the BasicElim tactic by Conor McBride [McB00] and the work of Cristina Cornes around inversion [CT95]. From an instantiated inductive predicate and a goal, it generates an equivalent goal where the hypothesis has been generalized over its indexes which are then constrained by equalities to be the right instances. This permits to state lemmas without resorting to manually adding these equalities and still get enough information in the proofs.

  `generalizing​in ident+`

    First generalizes the goal by the given variables so that they are universally quantified in the goal. This is generally what one wants to do with variables that are inside constructors in the induction hypothesis. The other ones need not be further generalized.

  There is a long example of `dependent induction` and an explanation of the underlying technique here.

  Example

  Lemma lt_1_r : forall n:nat, n < 1 -> n = 0.
    1 goal ============================ forall n : nat, n < 1 -> n = 0
  intros n H ; induction H.
    2 goals n : nat ============================ n = 0 goal 2 is: n = 0

  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 Stdlib.Program.Equality.
    Toplevel input, characters 15-38: > Require Import Stdlib.Program.Equality. > ^^^^^^^^^^^^^^^^^^^^^^^ Error: Cannot find a physical path bound to logical path Stdlib.Program.Equality.
  Lemma lt_1_r : forall n:nat, n < 1 -> n = 0.
    1 goal ============================ forall n : nat, n < 1 -> n = 0
  intros n H ; dependent induction H.
    Toplevel input, characters 13-34: > intros n H ; dependent induction H. > ^^^^^^^^^^^^^^^^^^^^^ Error: Tactic failure: To use dependent induction, first [Require Import Stdlib.Program.Equality.].

  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.
    Toplevel input, characters 0-11: > reflexivity. > ^^^^^^^^^^^ Error: In environment n : nat H : n < 1 Unable to unify "0" with "n".

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

  inversion H.
    Toplevel input, characters 0-11: > inversion H. > ^^^^^^^^^^^ Error: No such hypothesis: H

  This technique works with any inductive predicate. In fact, the `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 `Stdlib.Program.Equality`.

  See also

  `functional induction`

Tactic fix ident natural with ( ident simple_binder* { struct name }? : type )+?

  A primitive tactic that starts a proof by induction. Generally, higher-level tactics such as `induction` or `elim` are easier to use.

  The `ident`s (including the first one before the `with` clause) are the names of the induction hypotheses. `natural` tells on which premise of the current goal the induction acts, starting from 1, counting both dependent and non-dependent products, but skipping local definitions. The current lemma must be composed of at least `natural` products.

  As in a fix expression, induction hypotheses must be used on structurally smaller arguments. The verification that inductive proof 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 `Guarded`.

  `with ( ident simple_binder* { struct name }? : type )+`

    Starts a proof by mutual induction. The statements to be proven are `forall simple_binderi, typei`. The identifiers `ident` (including the first one before the `with` clause) are the names of the induction hypotheses. The identifiers `name` (in the `{ struct ... }` clauses) are the respective names of the premises on which the induction is performed in the statements to be proved (if not given, Rocq guesses what they are).

Tactic cofix ident with ( ident simple_binder* : type )+?

  Starts a proof by coinduction. The `ident`s (including the first one before the `with` clause) are the names of the coinduction hypotheses. As in a cofix expression, the use of induction hypotheses must be guarded by a constructor. The verification that the use of coinductive hypotheses is correct is done only at the time of registering the lemma in the global environment. To know if the use of coinduction hypotheses is correct at some time of the interactive development of a proof, use the command `Guarded`.

  `with ( ident simple_binder* : type )+`

    Starts a proof by mutual coinduction. The statements to be proven are `forall simple_binderi, typei`. The identifiers `ident` (including the first one before the `with` clause) are the names of the coinduction hypotheses.

## Equality of inductive types

This section describes some special purpose tactics to work with Leibniz equality of inductive sets or types.

Tactic discriminate induction_arg?

  Proves goals for which a hypothesis or a premise in the goal that is convertible to the form `term1 = term2` has inconsistent constructors between the two sides of the equality (i.e., a contradiction). The tactic also works for goals in the form `term1 <> term2` that are inconsistent (example).

  If `induction_arg` is provided, only the provided proof term or hypothesis is checked for inconsistency. If `induction_arg` is not given, the tactic does an `intro` for each premise in the goal, then it checks all the resulting hypotheses for impossible equalities.

  The tactic relies on the fact that constructors of inductive types are injective and disjoint, i.e. if `C1` and `C2` are distinct constructors of an inductive type then `C1 term1 = C1 term2` implies that `term1 = term2` (injectivity) and `C1 term1 = C2 term2` is a contradiction (disjointedness). For example, `S (S O) = S O` is a contradiction: while the outermost constructors are both `S`, the next ones differ (`S` versus `O`).

  The tactic traverses the normal forms of `term1` and `term2`, looking for subterms placed in the same positions whose head symbols are different constructors. If such subterms are present, the equality is impossible and the current goal is completed. Otherwise the tactic fails. Note that opaque constants are not expanded by δ reductions while computing the head normal form.

  Note that `discriminate` doesn't handle contradictory equalities such as `n = S n`. In this case you must use `induction` (see example).

  `ident` (as `induction_arg`)

    Checks the hypothesis `ident` for impossible equalities. If `ident` is not already in the context, this is equivalent to `intros until ident; discriminate ident`.

  `natural` (as `induction_arg`)

    Equivalent to `intros` `until natural; discriminate ident`, where `ident` is the identifier for the last introduced hypothesis.

  `one_term with bindings` (in `induction_arg`)

    Equivalent to `discriminate one_term` but uses the given bindings to instantiate parameters or hypotheses of `one_term`. `one_term` must be a proof of `term1 = term2`.

  Error No primitive equality found.
  Error Not a discriminable equality.
  Tactic ediscriminate induction_arg?

    Works the same as `discriminate` but if the type of `one_term`, or the type of the hypothesis referred to by `natural`, has uninstantiated parameters, these parameters are left as existential variables.

> Example: Proving `1 <> 2`

> Goal 1 <> 2.
>   1 goal ============================ 1 <> 2
> discriminate.
>   No more goals.
> Qed.

> This works because `1 <> 2` is represented internally as `not (1 = 2)`, which is just `(1 = 2) -> False` from the definition of `not`:

> Print not.
>   not = fun A : Prop => A -> False : Prop -> Prop Arguments not A%_type_scope

> You can see this better by doing the `intro` explicitly:

> Goal 1 <> 2.
>   1 goal ============================ 1 <> 2
> intro. (* if omitted, "discriminate" does an intro *)
>   1 goal H : 1 = 2 ============================ False
> discriminate.
>   No more goals.
> Qed.

> Example: `discriminate` limitation: proving `n <> S n`

> Goal forall n:nat, n <> S n.
>   1 goal ============================ forall n : nat, n <> S n
> intro n.
>   1 goal n : nat ============================ n <> S n
> induction n.
>   2 goals ============================ 0 <> 1 goal 2 is: S n <> S (S n)
> - discriminate. (* works: O and (S O) start with different constructors *)
>   1 goal ============================ 0 <> 1 This subproof is complete, but there are some unfocused goals. Focus next goal with bullet -. 1 goal goal 1 is: S n <> S (S n)
> - Fail discriminate. (* fails: discriminate doesn't handle this case *)
>   1 goal n : nat IHn : n <> S n ============================ S n <> S (S n) The command has indeed failed with message: No primitive equality found.
> injection.
>   1 goal n : nat IHn : n <> S n H : S n = S (S n) ============================ n = S n -> False
> assumption.
>   No more goals.
> Qed.

Tactic injection induction_arg? as simple_intropattern*?

  Exploits the property that constructors of inductive types are injective, i.e. that if `c` is a constructor of an inductive type and `c t1 = c t2` then `t1 = t2` are equal too.

  If there is a hypothesis `H` in the form `term1 = term2`, then `injection H` applies the injectivity of constructors as deep as possible to derive the equality of subterms of `term1` and `term2` wherever the subterms start to differ. For example, from `(S p, S n) = (q, S (S m))` we may derive `S p = q` and `n = S m`. The terms must have inductive types and the same head constructor, but must not be convertible. If so, the tactic derives the equalities and adds them to the current goal as premises (except if the `as` clause is used).

  If no `induction_arg` is provided and the current goal is of the form `term <> term`, `injection` is equivalent to `intro ident; injection ident`.

  `ident` (in `induction_arg`)

    Derives equalities based on constructor injectivity for the hypothesis `ident`. If `ident` is not already in the context, this is equivalent to `intros until ident; injection ident`.

  `natural` (in `induction_arg`)

    Equivalent to `intros` `until natural` followed by `injection ident` where `ident` is the identifier for the last introduced hypothesis.

  `one_term with bindings` (in `induction_arg`)

    Like `injection one_term` but uses the given bindings to instantiate parameters or hypotheses of `one_term`.

  `as [= intropattern* ]`

    Specifies names to apply after the injection so that all generated equalities become hypotheses, which (unlike `intros`) may replace existing hypotheses with same name. The number of provided names must not exceed the number of newly generated equalities. If it is smaller, fresh names are generated for the unspecified items. The original equality is erased if it corresponds to a provided name or if the list of provided names is incomplete.

    Note that, as a convenience for users, specifying `simple_intropattern+` is treated as if `[= simple_intropattern+ ]` was specified.

  Example

  Consider the following goal:

  Inductive list : Set := | nil : list | cons : nat -> list -> list.
    list is defined list_rect is defined list_ind is defined list_rec is defined list_sind is defined
  Parameter P : list -> Prop.
    P is declared
  Goal forall l n, P nil -> cons n l = cons 0 nil -> P l.
    1 goal ============================ forall (l : list) (n : nat), P nil -> cons n l = cons 0 nil -> P l
  intros.
    1 goal l : list n : nat H : P nil H0 : cons n l = cons 0 nil ============================ P l
  injection H0.
    1 goal l : list n : nat H : P nil H0 : cons n l = cons 0 nil ============================ l = nil -> n = 0 -> P l

  Note

  Beware that injection yields an equality in a sigma type whenever the injected object has a dependent type `P` with its two instances in different types `(P t1 … tn)` and `(P u1 … un)`. If `t1` and `u1` are the same and have for type an inductive type for which a decidable equality has been declared using `Scheme Equality`, the use of a sigma type is avoided.

  Error No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop. You can try to use option Set Keep Proof Equalities.
  Error Not a negated primitive equality

    When `induction_arg` is not provided, the goal must be in the form `term <> term`.

  Error Nothing to inject.

    Generated when one side of the equality is not a constructor.

  Tactic einjection induction_arg? as simple_intropattern*?

    Works the same as `injection` but if the type of `one_term`, or the type of the hypothesis referred to by `natural` has uninstantiated parameters, these parameters are left as existential variables.

  Tactic simple injection induction_arg?

    Similar to `injection`, but always adds the derived equalities as new premises in the current goal (instead of as new hypotheses) even if the `Structural Injection` flag is set.

  Flag Structural Injection

    When this flag is set, `injection term` erases the original hypothesis and adds the generated equalities as new hypotheses rather than adding them to the current goal as premises, as if giving `injection term as` (with an empty list of names). This flag is off by default.

  Flag Keep Proof Equalities

    By default, `injection` only creates new equalities between `term`s whose type is in sort `Type` or `Set`, thus implementing a special behavior for objects that are proofs of a statement in `Prop`. This flag controls this behavior.

  Table Keep Equalities qualid

    This table specifies a set of inductive types for which proof equalities are always kept by `injection`. This overrides the `Keep Proof Equalities` flag for those inductive types. Use the `Add` and `Remove` commands to update this set manually.

Tactic simplify_eq induction_arg?

  Examines a hypothesis that has the form `term1 = term2`. If the terms are structurally different, the tactic does a `discriminate`. Otherwise, it does an `injection` to simplify the equality, if possible. If `induction_arg` is not provided, the tactic examines the goal, which must be in the form `term1 <> term2`.

  See the description of `induction_arg` in `injection` for an explanation of the parameters.

  Tactic esimplify_eq induction_arg?

    Works the same as `simplify_eq` but if the type of `one_term` or the type of the hypothesis referred to by `natural` has uninstantiated parameters, these parameters are left as existential variables.

Tactic inversion ident​natural as or_and_intropattern? in ident+?
Tactic inversion ident​natural using one_term in ident+?

  For a hypothesis whose type is a (co)inductively defined proposition, the tactic introduces a goal for each constructor of the proposition that isn't self-contradictory. Each such goal includes the hypotheses needed to deduce the proposition. (Co)inductively defined propositions are those defined with the `Inductive` or `CoInductive` commands whose contructors yield a `Prop`, as in this example.

  `ident`

    The name of the hypothesis to invert. If `ident` does not denote a hypothesis in the local context but refers to a hypothesis quantified in the goal, then the latter is first introduced in the local context using `intros until ident`.

  `natural`

    Equivalent to `intros until natural; inversion ident` where `ident` is the identifier for the last introduced hypothesis.

  `in ident+?`

    When `ident+` are identifiers in the local context, this does a `generalize` `ident+` as the initial step of `inversion`.

  `as or_and_intropattern`

    Provides names for the variables introduced in each new subgoal. The `or_and_intropattern` must have one `intropattern*` for each constructor of the (co)inductive predicate, given in the order in which the constructors are defined. If there are not enough names, Rocq picks fresh names.

    If an equation splits into several equations (because `inversion` applies `injection` on the equalities it generates), the corresponding `intropattern` should be in the form `[ intropattern* ]` (or the equivalent `( simple_intropattern )*,`), with the number of entries equal to the number of subequalities obtained from splitting the original equation. Example here.

  Note

  The `inversion … as` variant of `inversion` generally behaves in a slightly more expected way than `inversion` (no artificial duplication of some hypotheses referring to other hypotheses). To take advantage of these improvements, it is enough to use `inversion … as []`, letting Rocq choose fresh names.

  Note

  As `inversion` proofs may be large, we recommend creating and using lemmas whenever the same instance needs to be inverted several times. See Generation of inversion principles with Derive Inversion.

  Note

  Part of the behavior of the `inversion` tactic is to generate equalities between expressions that appeared in the hypothesis that is being processed. By default, no equalities are generated if they relate two proofs (i.e. equalities between `term`s whose type is in sort `Prop`). This behavior can be turned off by using the `Keep Proof Equalities` setting.

> Example: `inversion` with `as or_and_intropattern`

> Inductive contains0 : list nat -> Prop := | in_hd : forall l, contains0 (0 :: l) | in_tl : forall l b, contains0 l -> contains0 (b :: l).
>   contains0 is defined contains0_ind is defined contains0_sind is defined
> Goal forall l:list nat, contains0 (1 :: l) -> contains0 l.
>   1 goal ============================ forall l : list nat, contains0 (1 :: l) -> contains0 l
> intros l H.
>   1 goal l : list nat H : contains0 (1 :: l) ============================ contains0 l
> inversion H as [ | l' p Hl' [Heqp Heql'] ].
>   1 goal l : list nat H : contains0 (1 :: l) l' : list nat p : nat Hl' : contains0 l Heqp : p = 1 Heql' : l' = l ============================ contains0 l
> Tactic inversion_clear ident​natural as or_and_intropattern? in ident+?

>   Does an `inversion` and then erases the hypothesis that was used for the inversion.

> Tactic simple inversion ident​natural as or_and_intropattern? in ident+?

>   A very simple inversion tactic that derives all the necessary equalities but does not simplify the constraints as `inversion` does.

> Tactic dependent inversion ident​natural as or_and_intropattern? with one_term?

>   For use when the inverted hypothesis appears in the current goal. Does an `inversion` and then substitutes the name of the hypothesis where the corresponding term appears in the goal.

> Tactic dependent inversion_clear ident​natural as or_and_intropattern? with one_term?

>   Does a `dependent inversion` and then erases the hypothesis that was used for the dependent inversion.

> Tactic dependent simple inversion ident​natural as or_and_intropattern? with one_term?

Tactic inversion_sigma ident as simple_intropattern??

  Note

  This tactic requires the Stdlib library.

  Turns equalities of dependent pairs (e.g., `existT P x p = existT P y q`, frequently left over by `inversion` on a dependent type family) into pairs of equalities (e.g., a hypothesis `H : x = y` and a hypothesis of type `rew H in p = q`); these hypotheses can subsequently be simplified using `subst`, without ever invoking any kind of axiom asserting uniqueness of identity proofs. If you want to explicitly specify the hypothesis to be inverted, you can pass it as an argument to `inversion_sigma`. This tactic also works for `sig`, `sigT2`, `sig2`, `ex`, and `ex2` and there are similar `eq_sig` `***_rect` induction lemmas.

  Error Type of ident is not an equality of recognized Σ types: expected one of sig sig2 sigT sigT2 sigT2 ex or ex2 but got term

    When applied to a hypothesis, `inversion_sigma` can only handle equalities of the listed sigma types.

  Error ident is not an equality of Σ types

    When applied to a hypothesis, `inversion_sigma` can only be called on hypotheses that are equalities using `Stdlib.Logic.Init.eq`.

Example: Non-dependent inversion

Let us consider the relation `Le` over natural numbers:

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 Le_sind is defined

Let us consider the following goal:

Section Section.
Variable P : nat -> nat -> Prop.
  P is declared
Variable Q : forall n m:nat, Le n m -> Prop.
  Q is declared
Goal forall n m, Le (S n) m -> P n m.
  1 goal P : nat -> nat -> Prop Q : forall n m : nat, Le n m -> Prop ============================ forall n m : nat, Le (S n) m -> P n m

intros.
  1 goal P : nat -> nat -> Prop Q : forall n m : nat, Le n m -> Prop n, m : nat H : Le (S n) m ============================ P n m

To prove the goal, we may need to reason by cases on `H` and to derive that `m` is necessarily of the form `(S m0)` for certain `m0` and that `(Le n m0)`. Deriving these conditions corresponds to proving that the only possible constructor of `(Le (S n) m)` is `LeS` and that we can invert the arrow in the type of `LeS`. This inversion is possible because `Le` is the smallest set closed by the constructors `LeO` and `LeS`.

inversion_clear H.
  1 goal P : nat -> nat -> Prop Q : forall n m : nat, Le n m -> Prop n, m, m0 : nat H0 : Le n m0 ============================ P n (S m0)

Note that `m` has been substituted in the goal for `(S m0)` and that the hypothesis `(Le n m0)` has been added to the context.

Sometimes it is interesting to have the equality `m = (S m0)` in the context to use it after. In that case we can use `inversion` that does not clear the equalities:

intros.
  1 goal P : nat -> nat -> Prop Q : forall n m : nat, Le n m -> Prop n, m : nat H : Le (S n) m ============================ P n m

inversion H.
  1 goal P : nat -> nat -> Prop Q : forall n m : nat, Le n m -> Prop n, m : nat H : Le (S n) m n0, m0 : nat H1 : Le n m0 H0 : n0 = n H2 : S m0 = m ============================ P n (S m0)

Example: Dependent inversion

Let us consider the following goal:

Abort.
Goal forall n m (H:Le (S n) m), Q (S n) m H.
  1 goal P : nat -> nat -> Prop Q : forall n m : nat, Le n m -> Prop ============================ forall (n m : nat) (H : Le (S n) m), Q (S n) m H

intros.
  1 goal P : nat -> nat -> Prop Q : forall n m : nat, Le n m -> Prop n, m : nat H : Le (S n) m ============================ Q (S n) m H

As `H` occurs in the goal, we may want to reason by cases on its structure and so, we would like inversion tactics to substitute `H` by the corresponding term in constructor form. Neither `inversion` nor `inversion_clear` do such a substitution. To have such a behavior we use the dependent inversion tactics:

dependent inversion_clear H.
  1 goal P : nat -> nat -> Prop Q : forall n m : nat, Le n m -> Prop n, m, m0 : nat l : Le n m0 ============================ Q (S n) (S m0) (LeS n m0 l)

Note that `H` has been substituted by `(LeS n m0 l)` and `m` by `(S m0)`.

Example: Using `inversion_sigma`

Let us consider the following inductive type of length-indexed lists, and a lemma about inverting equality of cons:

Require Import Stdlib.Logic.Eqdep_dec.
  Toplevel input, characters 15-37: > Require Import Stdlib.Logic.Eqdep_dec. > ^^^^^^^^^^^^^^^^^^^^^^ Error: Cannot find a physical path bound to logical path Stdlib.Logic.Eqdep_dec.
Inductive vec A : nat -> Type := | nil : vec A O | cons {n} (x : A) (xs : vec A n) : vec A (S n).
  vec is defined vec_rect is defined vec_ind is defined vec_rec is defined vec_sind is defined
Lemma invert_cons : forall A n x xs y ys, @cons A n x xs = @cons A n y ys -> xs = ys.
  1 goal ============================ forall (A : Type) (n : nat) (x : A) (xs : vec A n) (y : A) (ys : vec A n), cons A x xs = cons A y ys -> xs = ys
Proof.
intros A n x xs y ys H.
  1 goal A : Type n : nat x : A xs : vec A n y : A ys : vec A n H : cons A x xs = cons A y ys ============================ xs = ys

After performing inversion, we are left with an equality of existTs:

inversion H.
  1 goal A : Type n : nat x : A xs : vec A n y : A ys : vec A n H : cons A x xs = cons A y ys H1 : x = y H2 : existT (fun n : nat => vec A n) n xs = existT (fun n : nat => vec A n) n ys ============================ xs = ys

We can turn this equality into a usable form with inversion_sigma:

inversion_sigma.
  1 goal A : Type n : nat x : A xs : vec A n y : A ys : vec A n H : cons A x xs = cons A y ys H1 : x = y H2_ : n = n H2_0 : eq_rect n (fun n : nat => vec A n) xs n H2_ = ys ============================ xs = ys

To finish cleaning up the proof, we will need to use the fact that that all proofs of n = n for n a nat are eq_refl:

let H := match goal with H : n = n |- _ => H end in pose proof (Eqdep_dec.UIP_refl_nat _ H); subst H.
  Toplevel input, characters 64-86: > let H := match goal with H : n = n |- _ => H end in pose proof (Eqdep_dec.UIP_refl_nat _ H); subst H. > ^^^^^^^^^^^^^^^^^^^^^^ Error: The reference Eqdep_dec.UIP_refl_nat was not found in the current environment.
simpl in *.
  1 goal A : Type n : nat x : A xs : vec A n y : A ys : vec A n H : cons A x xs = cons A y ys H1 : x = y H2_ : n = n H2_0 : eq_rect n (fun n : nat => vec A n) xs n H2_ = ys ============================ xs = ys

Finally, we can finish the proof:

assumption.
  Toplevel input, characters 0-10: > assumption. > ^^^^^^^^^^ Error: No such assumption.
Qed.
  Toplevel input, characters 0-4: > Qed. > ^^^^ Error: (in proof invert_cons): Attempt to save an incomplete proof (there are remaining open goals).

See also

`functional inversion`

### Helper tactics

Tactic decide one_term1 with one_term2

  Replaces occurrences of `one_term1` in the form `{P}+{~P}` in the goal with `(left _)` or `(right _)`, depending on `one_term2`. `one_term2` must be of type either `P` or `~P`, and `P` must be of type `Prop`.

  Example: Using `decide` to rewrite the goal

  Goal forall (P Q : Prop) (Hp : {P} + {~P}) (Hq : {Q} + {~Q}), P -> ~Q -> (if Hp then true else false) = (if Hq then false else true).
    Toplevel input, characters 0-137: > Goal forall (P Q : Prop) (Hp : {P} + {~P}) (Hq : {Q} + {~Q}), P -> ~Q -> (if Hp then true else false) = (if Hq then false else true). > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Nested proofs are discouraged and not allowed by default. This error probably means that you forgot to close the last "Proof." with "Qed." or "Defined.". If you really intended to use nested proofs, you can do so by turning the "Nested Proofs Allowed" flag on.
  intros P Q Hp Hq p nq.
    Toplevel input, characters 0-21: > intros P Q Hp Hq p nq. > ^^^^^^^^^^^^^^^^^^^^^ Error: No product even after head-reduction.
  decide Hp with p.
    Toplevel input, characters 7-9: > decide Hp with p. > ^^ Error: The variable Hp was not found in the current environment.
  decide Hq with nq.
    Toplevel input, characters 7-9: > decide Hq with nq. > ^^ Error: The variable Hq was not found in the current environment.
  reflexivity.
    Toplevel input, characters 0-11: > reflexivity. > ^^^^^^^^^^^ Error: In environment A : Type n : nat x : A xs : vec A n y : A ys : vec A n H : cons A x xs = cons A y ys H1 : x = y H2_ : n = n H2_0 : eq_rect n (fun n : nat => vec A n) xs n H2_ = ys Unable to unify "ys" with "xs".
  Qed.
    Toplevel input, characters 0-4: > Qed. > ^^^^ Error: (in proof invert_cons): Attempt to save an incomplete proof (there are remaining open goals).

Tactic decide equality

  Solves a goal of the form `forall x y : R,? {x = y} + {~ x = y}` or `forall x y : R,? (x = y) \/ (~ x = y)`, where `R` is an inductive type whose constructors do not take proofs or functions as arguments, nor objects in dependent types.

Tactic compare one_term1 one_term2

  Compares two `one_term`s of an inductive datatype. If `G` is the current goal, it leaves the sub-goals `one_term1 = one_term2 -> G` and `~ one_term1 = one_term2 -> G`. The type of the `one_term`s must satisfy the same restrictions as in the tactic `decide equality`.

Tactic dependent rewrite ->​<-? one_term in ident?

  If `ident` has type `(existT B a b)=(existT B a' b')` in the local context (i.e. each term of the equality has a sigma type `{ a:A & (B a)}`) this tactic rewrites `a` into `a'` and `b` into `b'` in the current goal. This tactic works even if `B` is also a sigma type. This kind of equalities between dependent pairs may be derived by the `injection` and `inversion` tactics.

  `->​<-?`

    By default, the equality is applied from left to right. Specify `<-` to apply the equality from right to left.

## Generation of induction principles with `Scheme`

Command Scheme ident :=? scheme_kind with ident :=? scheme_kind*
  scheme_kind`::=`scheme_type for reference Sort sort_quality_or_set``scheme_type`::=`Induction`````|`Minimality`````|`Elimination`````|`Case``sort_quality_or_set`::=`Prop`````|`SProp`````|`Set`````|`Type``

  Generates induction principles with given `scheme_type`s and `sort_quality_or_set`s for an inductive type. In the case where the inductive definition is a mutual inductive definition, the `with` clause is used to generate a mutually recursive inductive scheme for each clause of the mutual inductive type.

  `ident`

    The name of the scheme. If not provided, the name will be determined automatically from the `scheme_type` and `sort_quality_or_set`.

  `scheme_type`

    Generate induction principles with given properties:

    `scheme_type` | Recursive | Dependent
    --- | --- | ---
    `Induction` | Yes | Yes
    `Minimality` | Yes | No
    `Elimination` | No | Yes
    `Case` | No | No

    See examples of the `scheme_type`s.

  Unless attribute `register=no` is used, the scheme is automatically registered for use by tactics (for instance `induction` uses `Induction` schemes). Use `Register Scheme` to manually register a scheme.

Example: Induction scheme for tree and forest

> Currently the automatically-generated induction principles such as `odd_ind` are not useful for mutually-inductive types such as `odd` and `even`. You can define a mutual induction principle for tree and forest in sort `Set` with the `Scheme` 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 tree_sind is defined forest_rect is defined forest_ind is defined forest_rec is defined forest_sind is defined
> > Scheme tree_forest_rec := Induction for tree Sort Set with forest_tree_rec := Induction for forest Sort Set.
> >   tree_forest_rec is defined forest_tree_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 f : forest, P0 f -> P0 (cons t f)) -> forall t : tree, P t

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: 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 odd_sind is defined even_ind is defined even_sind 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.
>   odd_even is defined even_odd 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 `forall n : nat, even n -> P0 n`.

Example: `Scheme` commands with various `scheme_type`s

Let us demonstrate the difference between the Scheme commands.

Unset Elimination Schemes.
Inductive Nat := | z : Nat | s : Nat -> Nat.
  Nat is defined
(* dependent, recursive *) Scheme Induction for Nat Sort Set.
  Nat_rec is defined Nat_rec is recursively defined
About Nat_rec.
  Nat_rec : forall P : Nat -> Set, P z -> (forall n : Nat, P n -> P (s n)) -> forall n : Nat, P n Nat_rec is not universe polymorphic Arguments Nat_rec P%_function_scope z s%_function_scope n Nat_rec is transparent Expands to: Constant Top.Nat_rec Declared in toplevel input, characters 6614-6648
(* non-dependent, recursive *) Scheme Minimality for Nat Sort Set.
  Nat_rec_nodep is defined Nat_rec_nodep is recursively defined
About Nat_rec_nodep.
  Nat_rec_nodep : forall P : Set, P -> (Nat -> P -> P) -> Nat -> P Nat_rec_nodep is not universe polymorphic Arguments Nat_rec_nodep P%_type_scope z s%_function_scope n Nat_rec_nodep is transparent Expands to: Constant Top.Nat_rec_nodep Declared in toplevel input, characters 6695-6730
(* dependent, non-recursive *) Scheme Elimination for Nat Sort Set.
  Nat_case is defined Nat_case is recursively defined
About Nat_case.
  Nat_case : forall P : Nat -> Set, P z -> (forall n : Nat, P (s n)) -> forall n : Nat, P n Nat_case is not universe polymorphic Arguments Nat_case P%_function_scope z s%_function_scope n Nat_case is transparent Expands to: Constant Top.Nat_case Declared in toplevel input, characters 6783-6819
(* non-dependent, non-recursive *) Scheme Case for Nat Sort Set.
  Nat_case_nodep is defined Nat_case_nodep is recursively defined
About Nat_case_nodep.
  Nat_case_nodep : forall P : Set, P -> (Nat -> P) -> Nat -> P Nat_case_nodep is not universe polymorphic Arguments Nat_case_nodep P%_type_scope z s%_function_scope n Nat_case_nodep is transparent Expands to: Constant Top.Nat_case_nodep Declared in toplevel input, characters 6871-6900

### Eliminators for Nested Inductive Types

When generating eliminators for a predicate `P`, if an argument is nested with `reference`, the `All` predicate and its theorem will be looked up with the key `All` and `AllForall`, and used to enforce `P` holds on the nested argument.

> Warning reference is nested using reference. No Lemma for reference is registered for ident. It can be generated using command "Scheme All" e.g. "Scheme All for ident.".

>   The `All` and `AllForall` predicate need to be defined and registered before the definition of the nested inductive type. They are not generated on the fly if they are not found. If they are not registered, no induction hypothesis is created for the nested argument.

Command Scheme All for reference over ident+,?

  For an inductive type `ind`, it generates the sort and universe polymorphic inductive predicate `ind_all` and its theorem `ind_all_forall`, and register them with the keys `All` and `AllForall` (see command `Register Scheme`).

  Option Depth Scheme All natural

    The `All` predicate for an inductive type is itself an inductive type. Consequently, generating automatically the `All` predicate at the definition of an inductive type would create an infinite loop. To prevent this, `Depth Scheme All` controls to which depth should the `All` predicate be generated. For instance, at depth `1`, the `All` predicate for `prod` will be generated, `prod_all`, but the `All` predicate for `prod_all` will not be generated. Its default value is `0`.

    The depth for nested inductive types is `Depth Scheme All -1` as if `X` is nested with `Y`, then `X_all` is nested with `Y_all`, and the eliminator for `X_all` requires `Y_all_all`.

  The `All` predicate features a predicate `PA : A -> Type@{s;u}` for each strictly positive uniform-parameter `A : Type` (or more generally an arity), and enforces they hold for each subterm of type `A` in the body of `ind`. The theorem `AllForall` then states that if all the predicates `PA` hold, that is `forall a, PA a`, then `ind_all` holds. The definitions must be sort polymorphic to generate eliminators for the different sorts `Prop`, `Type`, etc. The `AllForall` theorem must also be transparent to ensure termination checking. The corresponding theory can found in [LFST25].

  Wen used to generate eliminators, the type `unit` is used to instantiate the predicates if some parameters are not nested on. For instance, if `prod A B` is nested on `A` but not on `B`, then the predicate for `B` is instantiated with `fun _ => unit`.

  To provide better eliminators, the `over` clause enables to generate partial version of the `All` predicate, with predicates only for strictly positive uniform-parameter specified. The partial versions of `All` and `AllForall` are looked up first, and the implementation fallbacks on the general ones if they are not found.

  Partial versions can be registered by hand using the key with `All_s` and `AllForall_s` where `s` is a list of `1` and `0` specifying which parameters can be nested or not. For instance, to register a partial version of `All` for `prod A B` with a predicate on `A` but not on `B`, one should use `All_10`.

Example: Nesting With Prod

The inductive type `prod` has two uniform-parameters `A, B : Type` that are strictly positive, and hence nestable.

Inductive prod (A B : Type) : Type := | pair : A -> B -> prod A B.
  prod is defined prod_rect is defined prod_ind is defined prod_rec is defined prod_sind is defined

The `All` predicate should then be a predicate with additional parameters `PA : A -> Type@{s;u}` and `PB : B -> Type@{s';u'}`, and requires `PA a` and `PB b` for `prod A PA B PB (pair a b)` to hold. Its theorem will then state that if `PA` and `PB` hold, then `prod_all` holds. They can be generated with `Scheme All` command.

Scheme All for prod.
  prod_all is defined prod_all_rect is defined prod_all_ind is defined prod_all_rec is defined prod_all_sind is defined prod_all_forall is defined
Print prod_all.
  Inductive prod_all@{α α0 ; u u0 u1 u2} (A : Type) (PA : A -> Type@{α ; _}) (B : Type) (PB : B -> Type@{α0 ; _}) : prod A B -> Type := pair_all : forall a : A, PA a -> forall b : B, PB b -> prod_all A PA B PB (pair A B a b). Arguments prod_all A%_type_scope PA%_function_scope B%_type_scope PB%_function_scope p Arguments pair_all A%_type_scope PA%_function_scope B%_type_scope PB%_function_scope a _ b _
About prod_all_forall.
  prod_all_forall@{α α0 ; u u0 u1 u2} : forall (A : Type) (PA : A -> Type@{α ; _}), (forall a : A, PA a) -> forall (B : Type) (PB : B -> Type@{α0 ; _}), (forall b : B, PB b) -> forall p : prod A B, prod_all A PA B PB p prod_all_forall is universe polymorphic Arguments prod_all_forall A%_type_scope (PA HPA)%_function_scope B%_type_scope (PB HPB)%_function_scope p prod_all_forall is transparent Expands to: Constant Top.prod_all_forall Declared in toplevel input, characters 7057-7077

When generating eliminators for a predicate `P`, if an argument is nested with `prod`, the `prod_all` predicate and its theorem will be looked up, and used to enforce `P` holds on the argument. The type `unit` is used to instantiate the predicates if some parameters are not nested on. For instance, if `prod` is nested on `A` but not on `B`, then `PB` is instantiated with `fun _ => unit`.

Inductive LeftTree A : Type := | Lleaf (a : A) : LeftTree A | Lnode (p : prod (LeftTree A) nat) : LeftTree A.
  LeftTree is defined LeftTree_rect is defined LeftTree_ind is defined LeftTree_rec is defined LeftTree_sind is defined
About LeftTree_ind.
  LeftTree_ind : forall (A : Type) (P : LeftTree A -> Prop), (forall a : A, P (Lleaf A a)) -> (forall p : prod (LeftTree A) nat, prod_all (LeftTree A) P nat (fun _ : nat => unit) p -> P (Lnode A p)) -> forall l : LeftTree A, P l LeftTree_ind is not universe polymorphic Arguments LeftTree_ind A%_type_scope (P Lleaf Lnode)%_function_scope l LeftTree_ind is transparent Expands to: Constant Top.LeftTree_ind Declared in toplevel input, characters 7117-7226

To provide better eliminators for partially nesting like `LeftTree`, it is possible to generate partial version of `prod_all`

Scheme All for prod over A.
  prod_all_10 is defined prod_all_10_rect is defined prod_all_10_ind is defined prod_all_10_rec is defined prod_all_10_sind is defined prod_all_forall_10 is defined
Print prod_all_10.
  Inductive prod_all_10@{α ; u u0 u1} (A : Type) (PA : A -> Type@{α ; _}) (B : Type) : prod A B -> Type := pair_all_10 : forall a : A, PA a -> forall b : B, prod_all_10 A PA B (pair A B a b). Arguments prod_all_10 A%_type_scope PA%_function_scope B%_type_scope p Arguments pair_all_10 A%_type_scope PA%_function_scope B%_type_scope a _ b
About prod_all_forall_10.
  prod_all_forall_10@{α ; u u0 u1} : forall (A : Type) (PA : A -> Type@{α ; _}), (forall a : A, PA a) -> forall (B : Type) (p : prod A B), prod_all_10 A PA B p prod_all_forall_10 is universe polymorphic Arguments prod_all_forall_10 A%_type_scope (PA HPA)%_function_scope B%_type_scope p prod_all_forall_10 is transparent Expands to: Constant Top.prod_all_forall_10 Declared in toplevel input, characters 7247-7274

This partial verion of the `All` predicate will then be used in priority, falling back on the general version if it is not found. For instance, if we generate an eliminator for `LeftTree` after the generation of `prod_all_10`, `prod_all_10` will be used instead of `prod_all`.

Scheme LeftTree_ind_partial := Induction for LeftTree Sort Prop.
  LeftTree_ind_partial is defined LeftTree_ind_partial is recursively defined
About LeftTree_ind_partial.
  LeftTree_ind_partial : forall (A : Type) (P : LeftTree A -> Prop), (forall a : A, P (Lleaf A a)) -> (forall p : prod (LeftTree A) nat, prod_all_10 (LeftTree A) P nat p -> P (Lnode A p)) -> forall l : LeftTree A, P l LeftTree_ind_partial is not universe polymorphic Arguments LeftTree_ind_partial A%_type_scope (P Lleaf Lnode)%_function_scope l LeftTree_ind_partial is transparent Expands to: Constant Top.LeftTree_ind_partial Declared in toplevel input, characters 7320-7384

### Scheme Equality, and Rewriting

Command Scheme Boolean? Equality for reference

  Tries to generate a Boolean equality for `reference`. If `Boolean` is not specified, the command also tries to generate a proof of the decidability of propositional equality over `reference`. If `reference` involves independent constants or other inductive types, we recommend defining their equality first.

Command Scheme Rewriting for reference

  Tries to generate rewriting schemes such as congruence for `reference`. Equivalent to setting `Rewriting Schemes` before declaring `reference`.

### Automatic declaration of schemes

Attribute schemes = default​none

  When this attribute is not provided or provided with value `default`, schemes are automatically declared according to the following flags.

  When it is provided with value `none`, no schemes are automatically declared.

Flag Elimination Schemes

  This flag enables automatic declaration of induction principles when defining a new inductive type. Defaults to on.

Flag Nonrecursive Elimination Schemes

  This flag 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 these flags since Rocq 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 identdef from ident+,

  Combines induction principles generated by the `Scheme` command. Each `ident` is a different inductive principle that must belong to the same package of mutual inductive principle definitions. This command generates `identdef` as 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:

> 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 tree_sind is defined forest_rect is defined forest_ind is defined forest_rec is defined forest_sind is defined

Scheme tree_forest_ind := Induction for tree Sort Prop with forest_tree_ind := Induction for forest Sort Prop.
  tree_forest_ind is defined forest_tree_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 f : forest, P0 f -> P0 (cons t f)) -> (forall t : tree, P t) /\ (forall f : forest, P0 f)

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.
  tree_forest_rect is defined forest_tree_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 f : forest, P0 f -> P0 (cons t f)) -> (forall t : tree, P t) * (forall f : forest, P0 f)

See also

Generation of induction principles with Functional Scheme

## Generation of inversion principles with `Derive` `Inversion`

Command Derive Inversion ident with one_term Sort sort_quality_or_set?

  Generates an inversion lemma for the `inversion` tactic. `ident` is the name of the generated lemma. `one_term` should be in the form `qualid` or `(forall binder+, qualid one_term+)` where `qualid` is the name of an inductive predicate and `binder+` binds the variables occurring in `one_term+`. The lemma is generated for the sort `sort_quality_or_set` corresponding to `one_term`. Applying the lemma is equivalent to inverting the instance with the `inversion` tactic.

Command Derive Inversion_clear ident with one_term Sort sort_quality_or_set?

  When applied, it is equivalent to having inverted the instance with the tactic inversion replaced by the tactic `inversion_clear`.

Command Derive Dependent Inversion ident with one_term Sort sort_quality_or_set

  When applied, it is equivalent to having inverted the instance with the tactic `dependent inversion`.

Command Derive Dependent Inversion_clear ident with one_term Sort sort_quality_or_set

  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 Le_sind 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.
  leminv is defined
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 goal ============================ forall n m : nat, Le (S n) m -> P n m
intros.
  1 goal n, m : nat H : Le (S n) m ============================ P n m

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

## Examples of `dependent destruction` / `dependent induction`

Note

These tactics require the Stdlib library.

The tactics `dependent induction` and `dependent destruction` are another solution for inverting inductive predicate instances and potentially doing induction at the same time. It is based on the `BasicElim` tactic of Conor McBride which works by abstracting each argument of an inductive instance by a variable and constraining it by equalities afterwards. This way, the usual induction and destruct tactics can be applied to the abstracted instance and after simplification of the equalities we get the expected goals.

The abstracting tactic is called generalize_eqs and it takes as argument a hypothesis to generalize. It uses the JMeq datatype defined in Stdlib.Logic.JMeq, hence we need to require it before. For example, revisiting the first example of the inversion documentation:

Require Import Stdlib.Logic.JMeq.
  Toplevel input, characters 15-32: > Require Import Stdlib.Logic.JMeq. > ^^^^^^^^^^^^^^^^^ Error: Cannot find a physical path bound to logical path Stdlib.Logic.JMeq.
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 Le_sind is defined
Parameter P : nat -> nat -> Prop.
  P is declared
Goal forall n m:nat, Le (S n) m -> P n m.
  1 goal ============================ forall n m : nat, Le (S n) m -> P n m
intros n m H.
  1 goal n, m : nat H : Le (S n) m ============================ P n m

generalize_eqs H.
  Toplevel input, characters 0-16: > generalize_eqs H. > ^^^^^^^^^^^^^^^^ Error: Library Stdlib.Logic.JMeq has to be required first.

The index `S n` gets abstracted by a variable here, but a corresponding equality is added under the abstract instance so that no information is actually lost. The goal is now almost amenable to do induction or case analysis. One should indeed first move `n` into the goal to strengthen it before doing induction, or `n` will be fixed in the inductive hypotheses (this does not matter for case analysis). As a rule of thumb, all the variables that appear inside constructors in the indices of the hypothesis should be generalized. This is exactly what the `generalize_eqs_vars` variant does:

generalize_eqs_vars H.
  Toplevel input, characters 0-21: > generalize_eqs_vars H. > ^^^^^^^^^^^^^^^^^^^^^ Error: Library Stdlib.Logic.JMeq has to be required first.
induction H.
  2 goals n, n0 : nat ============================ P n n0 goal 2 is: P n (S m)

As the hypothesis itself did not appear in the goal, we did not need to use an heterogeneous equality to relate the new hypothesis to the old one (which just disappeared here). However, the tactic works just as well in this case, e.g.:

Require Import Stdlib.Program.Equality.
  Toplevel input, characters 15-38: > Require Import Stdlib.Program.Equality. > ^^^^^^^^^^^^^^^^^^^^^^^ Error: Cannot find a physical path bound to logical path Stdlib.Program.Equality.

Parameter Q : forall (n m : nat), Le n m -> Prop.
  Q is declared
Goal forall n m (p : Le (S n) m), Q (S n) m p.
  1 goal ============================ forall (n m : nat) (p : Le (S n) m), Q (S n) m p

intros n m p.
  1 goal n, m : nat p : Le (S n) m ============================ Q (S n) m p
generalize_eqs_vars p.
  Toplevel input, characters 0-21: > generalize_eqs_vars p. > ^^^^^^^^^^^^^^^^^^^^^ Error: Library Stdlib.Logic.JMeq has to be required first.

One drawback of this approach is that in the branches one will have to substitute the equalities back into the instance to get the right assumptions. Sometimes injection of constructors will also be needed to recover the needed equalities. Also, some subgoals should be directly solved because of inconsistent contexts arising from the constraints on indexes. The nice thing is that we can make a tactic based on discriminate, injection and variants of substitution to automatically do such simplifications (which may involve the axiom K). This is what the `simplify_dep_elim` tactic from `Stdlib.Program.Equality` does. For example, we might simplify the previous goals considerably:

induction p ; simplify_dep_elim.
  Toplevel input, characters 14-31: > induction p ; simplify_dep_elim. > ^^^^^^^^^^^^^^^^^ Error: The reference simplify_dep_elim was not found in the current environment.

The higher-order tactic `do_depind` defined in `Stdlib.Program.Equality` takes a tactic and combines the building blocks we have seen with it: generalizing by equalities calling the given tactic with the generalized induction hypothesis as argument and cleaning the subgoals with respect to equalities. Its most important instantiations are `dependent induction` and `dependent destruction` that do induction or simply case analysis on the generalized hypothesis. For example we can redo what we've done manually with dependent destruction:

Lemma ex : forall n m:nat, Le (S n) m -> P n m.
  1 goal ============================ forall n m : nat, Le (S n) m -> P n m

intros n m H.
  1 goal n, m : nat H : Le (S n) m ============================ P n m

dependent destruction H.
  Toplevel input, characters 0-23: > dependent destruction H. > ^^^^^^^^^^^^^^^^^^^^^^^ Error: Tactic failure: To use dependent destruction, first [Require Import Stdlib.Program.Equality.].

This gives essentially the same result as inversion. Now if the destructed hypothesis actually appeared in the goal, the tactic would still be able to invert it, contrary to dependent inversion. Consider the following example on vectors:

Set Implicit Arguments.

Parameter A : Set.
  A is declared

Inductive vector : nat -> Type := | vnil : vector 0 | vcons : A -> forall n, vector n -> vector (S n).
  vector is defined vector_rect is defined vector_ind is defined vector_rec is defined vector_sind is defined

Goal forall n, forall v : vector (S n), exists v' : vector n, exists a : A, v = vcons a v'.
  1 goal ============================ forall (n : nat) (v : vector (S n)), exists (v' : vector n) (a : A), v = vcons a v'

intros n v.
  1 goal n : nat v : vector (S n) ============================ exists (v' : vector n) (a : A), v = vcons a v'

dependent destruction v.
  Toplevel input, characters 0-23: > dependent destruction v. > ^^^^^^^^^^^^^^^^^^^^^^^ Error: Tactic failure: To use dependent destruction, first [Require Import Stdlib.Program.Equality.].

In this case, the `v` variable can be replaced in the goal by the generalized hypothesis only when it has a type of the form `vector (S n)`, that is only in the second case of the destruct. The first one is dismissed because `S n <> 0`.

### A larger example

Let's see how the technique works with induction on inductive predicates on a real example. We will develop an example application to the theory of simply-typed lambda-calculus formalized in a dependently-typed style:

Inductive type : Type := | base : type | arrow : type -> type -> type.
  type is defined type_rect is defined type_ind is defined type_rec is defined type_sind is defined

Notation " t --> t' " := (arrow t t') (at level 20, right associativity).

Inductive ctx : Type := | empty : ctx | snoc : ctx -> type -> ctx.
  ctx is defined ctx_rect is defined ctx_ind is defined ctx_rec is defined ctx_sind is defined

Notation " G , tau " := (snoc G tau) (at level 21, left associativity).

Fixpoint conc (G D : ctx) : ctx := match D with | empty => G | snoc D' x => snoc (conc G D') x end.
  conc is defined conc is recursively defined (guarded on 2nd argument)

Notation " G ; D " := (conc G D) (at level 21).

Inductive term : ctx -> type -> Type := | ax : forall G tau, term (G, tau) tau | weak : forall G tau, term G tau -> forall tau', term (G, tau') tau | abs : forall G tau tau', term (G , tau) tau' -> term G (tau --> tau') | app : forall G tau tau', term G (tau --> tau') -> term G tau -> term G tau'.
  term is defined term_rect is defined term_ind is defined term_rec is defined term_sind is defined

We have defined types and contexts which are snoc-lists of types. We also have a `conc` operation that concatenates two contexts. The `term` datatype represents in fact the possible typing derivations of the calculus, which are isomorphic to the well-typed terms, hence the name. A term is either an application of:

- the axiom rule to type a reference to the first variable in a context

- the weakening rule to type an object in a larger context

- the abstraction or lambda rule to type a function

- the application to type an application of a function to an argument

Once we have this datatype we want to do proofs on it, like weakening:

Lemma weakening : forall G D tau, term (G ; D) tau -> forall tau', term (G , tau' ; D) tau.
  1 goal ============================ forall (G D : ctx) (tau : type), term (G; D) tau -> forall tau' : type, term ((G, tau'); D) tau

The problem here is that we can't just use induction on the typing derivation because it will forget about the `G ; D` constraint appearing in the instance. A solution would be to rewrite the goal as:

Lemma weakening' : forall G' tau, term G' tau -> forall G D, (G ; D) = G' -> forall tau', term (G, tau' ; D) tau.
  1 goal ============================ forall (G' : ctx) (tau : type), term G' tau -> forall G D : ctx, G; D = G' -> forall tau' : type, term ((G, tau'); D) tau

With this proper separation of the index from the instance and the right induction loading (putting `G` and `D` after the inducted-on hypothesis), the proof will go through, but it is a very tedious process. One is also forced to make a wrapper lemma to get back the more natural statement. The `dependent induction` tactic alleviates this trouble by doing all of this plumbing of generalizing and substituting back automatically. Indeed we can simply write:

Require Import Stdlib.Program.Tactics.
  Toplevel input, characters 15-37: > Require Import Stdlib.Program.Tactics. > ^^^^^^^^^^^^^^^^^^^^^^ Error: Cannot find a physical path bound to logical path Stdlib.Program.Tactics.
Require Import Stdlib.Program.Equality.
  Toplevel input, characters 15-38: > Require Import Stdlib.Program.Equality. > ^^^^^^^^^^^^^^^^^^^^^^^ Error: Cannot find a physical path bound to logical path Stdlib.Program.Equality.

Lemma weakening : forall G D tau, term (G ; D) tau -> forall tau', term (G , tau' ; D) tau.
  1 goal ============================ forall (G D : ctx) (tau : type), term (G; D) tau -> forall tau' : type, term ((G, tau'); D) tau

Proof with simpl in * ; simpl_depind ; auto.
  Toplevel input, characters 24-36: > Proof with simpl in * ; simpl_depind ; auto. > ^^^^^^^^^^^^ Error: The reference simpl_depind was not found in the current environment.

intros G D tau H. dependent induction H generalizing G D ; intros.
  1 goal G, D : ctx tau : type H : term (G; D) tau ============================ forall tau' : type, term ((G, tau'); D) tau Toplevel input, characters 40-52: > intros G D tau H. dependent induction H generalizing G D ; intros. > ^^^^^^^^^^^^ Error: Syntax error: [ltac_use_default] expected after [tactic] (in [tactic_command]).

This call to `dependent induction` has an additional arguments which is a list of variables appearing in the instance that should be generalized in the goal, so that they can vary in the induction hypotheses. By default, all variables appearing inside constructors (except in a parameter position) of the instantiated hypothesis will be generalized automatically but one can always give the list explicitly.

Show.
  1 goal G, D : ctx tau : type H : term (G; D) tau ============================ forall tau' : type, term ((G, tau'); D) tau

The `simpl_depind` tactic includes an automatic tactic that tries to simplify equalities appearing at the beginning of induction hypotheses, generally using trivial applications of `reflexivity`. In cases where the equality is not between constructor forms though, one must help the automation by giving some arguments, using the `specialize` tactic for example.

destruct D; simpl in * ; simpl_depind ; auto. apply weak; apply ax. apply ax.
  Toplevel input, characters 25-37: > destruct D; simpl in * ; simpl_depind ; auto. > ^^^^^^^^^^^^ Error: The reference simpl_depind was not found in the current environment. Toplevel input, characters 52-56: > destruct D; simpl in * ; simpl_depind ; auto. apply weak; apply ax. > ^^^^ Error: In environment G, D : ctx tau : type H : term (G; D) tau tau' : type Unable to unify "term (?G, tau') ?tau" with "term ((G, tau'); D) tau". Toplevel input, characters 74-76: > destruct D; simpl in * ; simpl_depind ; auto. apply weak; apply ax. apply ax. > ^^ Error: In environment G, D : ctx tau : type H : term (G; D) tau tau0 : type Unable to unify "term (?G@{tau0:=tau; tau:=tau0}, tau0) tau0" with "term ((G, tau0); D) tau".

destruct D; simpl in * ; simpl_depind ; auto.
  Toplevel input, characters 25-37: > destruct D; simpl in * ; simpl_depind ; auto. > ^^^^^^^^^^^^ Error: The reference simpl_depind was not found in the current environment.

Show.
  1 goal G, D : ctx tau : type H : term (G; D) tau ============================ forall tau' : type, term ((G, tau'); D) tau

specialize (IHterm G0 empty eq_refl).
  Toplevel input, characters 12-18: > specialize (IHterm G0 empty eq_refl). > ^^^^^^ Error: The variable IHterm was not found in the current environment.

Once the induction hypothesis has been narrowed to the right equality, it can be used directly.

apply weak, IHterm.
  Toplevel input, characters 6-10: > apply weak, IHterm. > ^^^^ Error: In environment G, D : ctx tau : type H : term (G; D) tau tau' : type Unable to unify "term (?G, tau') ?tau" with "term ((G, tau'); D) tau".

Now concluding this subgoal is easy.

constructor; apply IHterm; reflexivity.
  Toplevel input, characters 0-11: > constructor; apply IHterm; reflexivity. > ^^^^^^^^^^^ Error: Unable to find an instance for the variable tau.

Other versions v: 9.2

Versions
  dev
  stable
  9.2
  9.1
  9.0
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF