mathlib3 documentation

tactic.induction

A better tactic for induction and case analysis #

This module defines the tactics tactic.interactive.induction' and tactic.interactive.cases', which are variations on Lean's builtin induction and cases. The primed variants feature various improvements over the builtin tactics; in particular, they generate more human-friendly names and induction' deals much better with indexed inductive types. See the tactics' documentation for more details. We also provide corresponding non-interactive induction tactics tactic.eliminate_hyp and tactic.eliminate_expr.

The design and implementation of these tactics is described in a draft paper.

Tracing #

We set up two tracing functions to be used by eliminate_hyp and its supporting tactics. Their output is enabled by setting trace.eliminate_hyp to true.

source
meta def tactic.eliminate.trace_eliminate_hyp {α : Type u_1} [has_to_format α] (msg : thunk α) :
tactic unit

trace_eliminate_hyp msg traces msg if the option trace.eliminate_hyp is true.

source
meta def tactic.eliminate.trace_state_eliminate_hyp {α : Type u_1} [has_to_format α] (msg : thunk α) :
tactic unit

trace_state_eliminate_hyp msg traces msg followed by the tactic state if the option trace.eliminate_hyp is true.

Information Gathering #

We define data structures for information relevant to the induction, and functions to collect this information for a specific goal.

source
@[protected, instance]
meta def tactic.eliminate.constructor_argument_info.has_reflect  :
has_reflect tactic.eliminate.constructor_argument_info
source
meta structure tactic.eliminate.constructor_argument_info  :
Type

Information about a constructor argument. E.g. given the declaration

induction ℕ : Type
| zero : ℕ
| suc (n : ℕ) : ℕ

the zero constructor has no arguments and the suc constructor has one argument, n.

We record the following information:

  • aname: the argument's name. If the argument was not explicitly named in the declaration, the elaborator generates a name for it.
  • type : the argument's type.
  • dependent: whether the argument is dependent, i.e. whether it occurs in the remainder of the constructor type.
  • index_occurrences: the index arguments of the constructor's return type in which this argument occurs. If the constructor return type is I i₀ ... iₙ and the argument under consideration is a, and a occurs in i₁ and i₂, then the index_occurrences are 1, 2. As an additional requirement, for iⱼ to be considered an index occurrences, the type of iⱼ must match that of a according to index_occurrence_type_match.
  • recursive_leading_pis: none if this constructor is not recursive. Otherwise, the argument has type Π (x₁ : T₁) ... (xₙ : Tₙ), I ... where I is the inductive type to which this constructor belongs. In this case, recursive_leading_pis is some n with n the number of leading Π binders in the argument's type.
Instances for tactic.eliminate.constructor_argument_info
source
meta def tactic.eliminate.constructor_argument_info.is_recursive (c : tactic.eliminate.constructor_argument_info) :
bool

is_recursive c is true iff the constructor argument described by c is recursive.

source
@[protected, instance]
meta def tactic.eliminate.constructor_info.has_reflect  :
has_reflect tactic.eliminate.constructor_info
source
meta structure tactic.eliminate.constructor_info  :
Type

Information about a constructor. Contains:

  • cname: the constructor's name.
  • non_param_args: information about the arguments of the constructor, excluding the arguments induced by the parameters of the inductive type.
  • num_non_param_args: the length of non_param_args.
  • rec_args: the subset of non_param_args which are recursive constructor arguments.
  • num_rec_args: the length of rec_args.

For example, take the constructor

list.cons : ∀ {α} (x : α) (xs : list α), list α

α is a parameter of list, so non_param_args contains information about x and xs. rec_args contains information about xs.

Instances for tactic.eliminate.constructor_info
source
meta def tactic.eliminate.constructor_info.num_nameable_hypotheses (c : tactic.eliminate.constructor_info) :
ℕ

When we construct the goal for the minor premise of a given constructor, this is the number of hypotheses we must name.

source
meta structure tactic.eliminate.inductive_info  :
Type

Information about an inductive type. Contains:

  • iname: the type's name.
  • constructors: information about the type's constructors.
  • num_constructors: the length of constructors.
  • type: the type's type.
  • num_param: the type's number of parameters.
  • num_indices: the type's number of indices.
Instances for tactic.eliminate.inductive_info
source
@[protected, instance]
meta def tactic.eliminate.inductive_info.has_reflect  :
has_reflect tactic.eliminate.inductive_info
source
meta structure tactic.eliminate.major_premise_info  :
Type

Information about a major premise (i.e. the hypothesis on which we are performing induction). Contains:

  • mpname: the major premise's name.
  • mpexpr: the major premise itself.
  • type: the type of mpexpr.
  • args: the arguments of the major premise. The major premise has type I x₀ ... xₙ, where I is an inductive type. args is the map [0 → x₀, ..., n → xₙ].
source
meta def tactic.eliminate.index_occurrence_type_match (t s : expr) :
tactic bool

index_occurrence_type_match t s is true iff t and s are definitionally equal.

source
meta def tactic.eliminate.get_index_occurrences (num_params : ℕ) (ret_type : expr) :
tactic (native.rb_lmap expr ℕ)

From the return type of a constructor C of an inductive type I, determine the index occurrences of the constructor arguments of C.

Input:

  • num_params: the number of parameters of I.
  • ret_type: the return type of C. e must be of the form I x₁ ... xₙ.

Output: A map associating each local constant c that appears in any of the xᵢ with the set of indexes j such that c appears in xⱼ and xⱼ's type matches that of c according to tactic.index_occurrence_type_match.

source
meta def tactic.eliminate.match_recursive_constructor_arg (I : name) (T : expr) :
tactic (option ℕ)

match_recursive_constructor_arg I T, given I the name of an inductive type and T the type of an argument of a constructor of I, returns none if the argument is non-recursive (i.e. I does not appear in T). If the argument is recursive, T is of the form Π (x₁ : T₁) ... (xₙ : Tₙ), I ..., in which case match_recursive_constructor_arg returns some n. Matching is performed up to WHNF with semireducible transparency.

source
meta def tactic.eliminate.get_constructor_argument_info (inductive_name : name) (num_params : ℕ) (T : expr) :
tactic (list tactic.eliminate.constructor_argument_info)

Get information about the arguments of a constructor C of an inductive type I.

Input:

  • inductive_name: the name of I.
  • num_params: the number of parameters of I.
  • T: the type of C.

Output: a constructor_argument_info structure for each argument of C.

source
meta def tactic.eliminate.get_constructor_info (iname : name) (num_params : ℕ) (c : name) :
tactic tactic.eliminate.constructor_info

Get information about a constructor C of an inductive type I.

Input:

  • iname: the name of I.
  • num_params: the number of parameters of I.
  • c : the name of C.

Output:

A constructor_info structure for C.

source
meta def tactic.eliminate.get_inductive_info (I : name) :
tactic tactic.eliminate.inductive_info

Get information about an inductive type I, given I's name.

source
meta def tactic.eliminate.get_major_premise_info (major_premise : expr) :
tactic tactic.eliminate.major_premise_info

Get information about a major premise. The given expr must be a local hypothesis.

Constructor Argument Naming #

We define the algorithm for naming constructor arguments (which is a remarkably big part of the tactic).

source
meta structure tactic.eliminate.constructor_argument_naming_info  :
Type

Information used when naming a constructor argument.

source
@[reducible]
meta def tactic.eliminate.constructor_argument_naming_rule  :
Type

A constructor argument naming rule takes a constructor_argument_naming_info structure and returns a list of suitable names for the argument. If the rule is not applicable to the given constructor argument, the returned list is empty.

source
meta def tactic.eliminate.constructor_argument_naming_rule_rec  :
tactic.eliminate.constructor_argument_naming_rule

Naming rule for recursive constructor arguments.

source
meta def tactic.eliminate.constructor_argument_naming_rule_index  :
tactic.eliminate.constructor_argument_naming_rule

Naming rule for constructor arguments associated with an index.

source
meta def tactic.eliminate.constructor_argument_naming_rule_named  :
tactic.eliminate.constructor_argument_naming_rule

Naming rule for constructor arguments which are named in the constructor declaration.

source
meta def tactic.eliminate.constructor_argument_naming_rule_type  :
tactic.eliminate.constructor_argument_naming_rule

Naming rule for constructor arguments whose type is associated with a list of typical variable names. See tactic.typical_variable_names.

source
meta def tactic.eliminate.constructor_argument_naming_rule_prop  :
tactic.eliminate.constructor_argument_naming_rule

Naming rule for constructor arguments whose type is in Prop.

source
meta def tactic.eliminate.constructor_argument_naming_rule_fallback  :
tactic.eliminate.constructor_argument_naming_rule

Fallback constructor argument naming rule. This rule never fails.

source
meta def tactic.eliminate.apply_constructor_argument_naming_rules (info : tactic.eliminate.constructor_argument_naming_info) (rules : list tactic.eliminate.constructor_argument_naming_rule) :
tactic (list name)

apply_constructor_argument_naming_rules info rules applies the constructor argument naming rules in rules to the constructor argument given by info. Returns the result of the first applicable rule. Fails if no rule is applicable.

source
meta def tactic.eliminate.constructor_argument_names (info : tactic.eliminate.constructor_argument_naming_info) :
tactic (list name)

Get possible names for a constructor argument. This tactic applies all the previously defined rules in order. It cannot fail and always returns a nonempty list.

source
meta def tactic.eliminate.intron_fresh (n : ℕ) :
tactic (list expr)

intron_fresh n introduces n hypotheses with names generated by tactic.mk_fresh_name.

source
meta def tactic.eliminate.constructor_intros (generate_induction_hyps : bool) (cinfo : tactic.eliminate.constructor_info) :
tactic (list (name × tactic.eliminate.constructor_argument_info) × list (name × name × tactic.eliminate.constructor_argument_info))

Introduce the new hypotheses generated by the minor premise for a given constructor. The new hypotheses are given fresh (unique, non-human-friendly) names. They are later renamed by constructor_renames. We delay the generation of the human-friendly names because when constructor_renames is called, more names may have become unused.

Input:

  • generate_induction_hyps: whether we generate induction hypotheses (i.e. whether eliminate_hyp is in induction or cases mode).
  • cinfo: information about the constructor.

Output:

  • For each constructor argument: (1) the pretty name of the newly introduced hypothesis corresponding to the argument; (2) the argument's constructor_argument_info.
  • For each newly introduced induction hypothesis: (1) its pretty name; (2) the pretty name of the hypothesis corresponding to the constructor argument from which this induction hypothesis was derived; (3) that constructor argument's constructor_argument_info.
source
meta def tactic.eliminate.ih_name (arg_name : name) :
name

ih_name arg_name is the name ih_<arg_name>.

source
meta inductive tactic.eliminate.with_pattern  :
Type

Representation of a pattern in the with n ... syntax supported by induction' and cases'. A with_pattern can be:

  • with_pattern.auto (with _ or no with clause): use the name generated by the tactic.
  • with_pattern.clear (with -): clear this hypothesis and any hypotheses depending on it.
  • with_pattern.exact n (with n): use the name n for this hypothesis.
Instances for tactic.eliminate.with_pattern
source
@[protected, instance]
meta def tactic.eliminate.with_pattern.has_reflect  :
has_reflect tactic.eliminate.with_pattern
source
@[protected]
meta def tactic.eliminate.with_pattern.parser  :
lean.parser tactic.eliminate.with_pattern

Parser for a with_pattern.

source
meta def tactic.eliminate.with_pattern.clause_parser  :
lean.parser (list tactic.eliminate.with_pattern)

Parser for a with clause.

source
meta def tactic.eliminate.with_pattern.to_name_spec (auto_candidates : tactic (list name)) :
tactic.eliminate.with_pattern → tactic (option (name ⊕ list name))

to_name_spec auto_candidates p returns a description of how the hypothesis to which the with_pattern p applies should be named. If this function returns none, the hypothesis should be cleared. If it returns some (inl n), it should receive exactly the name n, even if this shadows other hypotheses. If it returns some (inr ns), it should receive the first unused name from ns.

If p = auto, the auto_candidates tactic is run to determine candidate names for the hypothesis (from which the first fresh one is later chosen). auto_candidates must return a nonempty list.

source
meta def tactic.eliminate.clear_dependent_if_exists (h : name) :
tactic unit

If h refers to a hypothesis, clear_dependent_if_exists h clears h and any hypotheses which depend on it. Otherwise, the tactic does nothing.

source
meta def tactic.eliminate.constructor_renames (generate_induction_hyps : bool) (mpinfo : tactic.eliminate.major_premise_info) (iinfo : tactic.eliminate.inductive_info) (cinfo : tactic.eliminate.constructor_info) (with_patterns : list tactic.eliminate.with_pattern) (args : list (name × tactic.eliminate.constructor_argument_info)) (ihs : list (name × name × tactic.eliminate.constructor_argument_info)) :
tactic (list expr × list expr)

Rename the new hypotheses in the goal for a minor premise.

Input:

  • generate_induction_hyps: whether we generate induction hypotheses (i.e. whether eliminate_hyp is in induction or cases mode).
  • mpinfo: information about the major premise.
  • iinfo: information about the inductive type.
  • cinfo: information about the constructor whose minor premise we are processing.
  • with_patterns: a list of with patterns given by the user. These are used to name constructor arguments and induction hypotheses. If the list does not contain enough patterns for all introduced hypotheses, the remaining ones are treated as if the user had given with_pattern.auto (_).
  • args and ihs: the output of constructor_intros.

Output:

  • The newly introduced hypotheses corresponding to constructor arguments.
  • The newly introduced induction hypotheses.

Generalisation #

induction' can generalise the goal before performing an induction, which gives us a more general induction hypothesis. We call this 'auto-generalisation'.

source
inductive tactic.eliminate.generalization_mode  :
Type

A value of generalization_mode describes the behaviour of the auto-generalisation functionality:

  • generalize_all_except hs means that the hs remain fixed and all other hypotheses are generalised. However, there are three exceptions:

    • Hypotheses depending on any h in hs also remain fixed. If we were to generalise them, we would have to generalise h as well.
    • Hypotheses which do not occur in the target and which do not mention the major premise or its dependencies are never generalised. Generalising them would not lead to a more general induction hypothesis.
    • Local definitions (hypotheses of the form h : T := t) and their dependencies are not generalised. This is due to limitations of the implementation; local definitions could in principle be generalised.

  • generalize_only hs means that only the hs are generalised. Exception: hypotheses which depend on the major premise are generalised even if they do not appear in hs.

Instances for tactic.eliminate.generalization_mode
source
@[protected, instance]
meta def tactic.eliminate.generalization_mode.has_reflect  :
has_reflect tactic.eliminate.generalization_mode
source
@[protected, instance]
def tactic.eliminate.generalization_mode.inhabited  :
inhabited tactic.eliminate.generalization_mode
Equations
source
meta def tactic.eliminate.generalization_mode.to_generalize (major_premise : expr) :
tactic.eliminate.generalization_mode → tactic name_set

Given the major premise and a generalization_mode, this function returns the unique names of the hypotheses that should be generalized. See generalization_mode for what these are.

source
meta def tactic.eliminate.generalize_hyps (major_premise : expr) (gm : tactic.eliminate.generalization_mode) :
tactic ℕ

Generalize hypotheses for the given major premise and generalization mode. See generalization_mode and to_generalize.

Complex Index Generalisation #

A complex expression is any expression that is not merely a local constant. When such a complex expression appears as an argument of the major premise, and when that argument is an index of the inductive type, we must generalise the complex expression. E.g. when we operate on the major premise fin (2 + n) (assuming that fin is encoded as an inductive type), the 2 + n is a complex index argument. To generalise it, we replace it with a new hypothesis index : ℕ and add an equation induction_eq : index = 2 + n.

source
meta def tactic.eliminate.generalize_complex_index_args (major_premise : expr) (num_params : ℕ) (generate_induction_hyps : bool) :
tactic (expr × ℕ × list name × ℕ)

Generalise the complex index arguments.

Input:

  • major premise: the major premise.
  • num_params: the number of parameters of the inductive type.
  • generate_induction_hyps: whether we generate induction hypotheses (i.e. whether eliminate_hyp is in induction or cases mode).

Output:

  • The new major premise. This procedure may change the major premise's type signature, so the old major premise hypothesis is invalidated.
  • The number of index placeholder hypotheses we introduced.
  • The index placeholder hypotheses we introduced.
  • The number of hypotheses which were reverted because they contain complex indices.

Simplification of Induction Hypotheses #

Auto-generalisation and complex index generalisation may produce unnecessarily complex induction hypotheses. We define a simplification algorithm that recovers understandable induction hypotheses in many practical cases.

source
meta def tactic.eliminate.process_index_equation  :
expr → tactic (expr × option expr)

Process one index equation for simplify_ih.

Input: a local constant h : x = y or h : x == y.

Output: A proof of x = y or x == y and possibly a local constant of type x = y or x == y used in the proof. More specifically:

  • For h : x = y and x defeq y, we return the proof of x = y by reflexivity and none.
  • For h : x = y and x not defeq y, we return h and h.
  • For h : x == y where x and y have defeq types:
    • If x defeq y, we return the proof of x == y by reflexivity and none.
    • If x not defeq y, we return heq_of_eq h' and a fresh local constant h' : x = y.
  • For h : x == y where x and y do not have defeq types, we return h and h.

Checking for definitional equality of the left- and right-hand sides may assign metavariables.

source
meta def tactic.eliminate.assign_local_to_unassigned_mvar (mv : expr) (pp_name : name) (binfo : binder_info) :
tactic (option expr)

assign_local_to_unassigned_mvar mv pp_name binfo, where mv is a metavariable, acts as follows:

  • If mv is assigned, it is not changed and the tactic returns none.
  • If mv is not assigned, it is assigned a fresh local constant with the type of mv, pretty name pp_name and binder info binfo. This local constant is returned.
source
meta def tactic.eliminate.assign_locals_to_unassigned_mvars (mvars : list (expr × name × binder_info)) :
tactic (list expr)

Apply assign_local_to_unassigned_mvar to a list of metavariables. Returns the newly created local constants.

source
meta def tactic.eliminate.simplify_ih (num_leading_pis num_generalized num_index_vars : ℕ) (ih : expr) :
tactic expr

Simplify an induction hypothesis.

Input: a local constant

ih : ∀ (a₁ : A₁) ... (aₙ : Aₙ) (b₁ : B₁) ... (bₘ : Bₘ)
       (eq₁ : y₁ = z₁) ... (eqₖ : yₒ = zₒ), P

where n = num_leading_pis, m = num_generalized and o = num_index_vars. The aᵢ are arguments of the type of the constructor argument to which this induction hypothesis belongs (usually zero). The xᵢ are hypotheses that we generalised over before performing induction. The eqᵢ are index equations.

Output: a new local constant

ih' : ∀ (a'₁ : A'₁) ... (b'ₖ : B'ₖ) (eq'₁ : y'₁ = z'₁) ... (eq'ₗ : y'ₗ = z'ₗ), P'

This new induction hypothesis is derived from ih by removing those eqᵢ whose left- and right-hand sides can be unified. This unification may also determine some of the aᵢ and bᵢ. The a'ᵢ, b'ᵢ and eq'ᵢ are those aᵢ, bᵢ and eqᵢ that were not removed by this process.

Some of the eqᵢ may be heterogeneous: eqᵢ : yᵢ == zᵢ. In this case, we proceed as follows:

  • If yᵢ and zᵢ are defeq, then eqᵢ is removed.
  • If yᵢ and zᵢ are not defeq but their types are, then eqᵢ is replaced by eq'ᵢ : x = y.
  • Otherwise eqᵢ remains unchanged.

Temporary utilities #

The utility functions in this section should be removed pending certain changes to Lean's standard library.

source
meta def tactic.eliminate.set_cases_tags (in_tag : tactic.tag) (rs : list (name × list expr)) :
tactic unit

Updates the tags of new subgoals produced by cases or induction. in_tag is the initial tag, i.e. the tag of the goal on which cases/induction was applied. rs should contain, for each subgoal, the constructor name associated with that goal and the hypotheses that were introduced.

The Elimination Tactics #

Finally, we define the tactics induction' and cases' tactics as well as the non-interactive variant eliminate_hyp.

source
meta def tactic.eliminate_hyp (generate_ihs : bool) (major_premise : expr) (gm : tactic.eliminate.generalization_mode := tactic.eliminate.generalization_mode.generalize_all_except list.nil) (with_patterns : list tactic.eliminate.with_pattern := list.nil) :
tactic unit

eliminate_hyp generate_ihs h gm with_patterns performs induction or case analysis on the hypothesis h. If generate_ihs is true, the tactic performs induction, otherwise case analysis.

In case analysis mode, eliminate_hyp is very similar to tactic.cases. The only differences (assuming no bugs in eliminate_hyp) are that eliminate_hyp can do case analysis on a slightly larger class of hypotheses and that it generates more human-friendly names.

In induction mode, eliminate_hyp is similar to tactic.induction, but with more significant differences:

  • If h (the hypothesis we are performing induction on) has complex indices, eliminate_hyp 'remembers' them. A complex expression is any expression that is not merely a local hypothesis. A hypothesis h : I p₁ ... pₙ j₁ ... jₘ, where I is an inductive type with n parameters and m indices, has a complex index if any of the jᵢ are complex. In this situation, standard induction effectively forgets the exact values of the complex indices, which often leads to unprovable goals. eliminate_hyp 'remembers' them by adding propositional equalities. As a result, you may find equalities named induction_eq in your goal, and the induction hypotheses may also quantify over additional equalities.

  • eliminate_hyp generalises induction hypotheses as much as possible by default. This means that if you eliminate n in the goal

    n m : ℕ
⊢ P n m

    the induction hypothesis is ∀ m, P n m instead of P n m.

    You can modify this behaviour by giving a different generalisation mode gm; see tactic.eliminate.generalization_mode.

  • eliminate_hyp generates much more human-friendly names than induction. It also clears more redundant hypotheses.

  • eliminate_hyp currently does not support custom induction principles a la induction using.

The with_patterns can be used to give names for the hypotheses introduced by eliminate_hyp. See tactic.eliminate.with_pattern for details.

To debug this tactic, use

set_option trace.eliminate_hyp true
source
meta def tactic.eliminate_expr (generate_induction_hyps : bool) (major_premise : expr) (eq_name : option name := option.none) (gm : tactic.eliminate.generalization_mode := tactic.eliminate.generalization_mode.generalize_all_except list.nil) (with_patterns : list tactic.eliminate.with_pattern := list.nil) :
tactic unit

A variant of tactic.eliminate_hyp which performs induction or case analysis on an arbitrary expression. eliminate_hyp requires that the major premise is a hypothesis. eliminate_expr lifts this restriction by generalising the goal over the major premise before calling eliminate_hyp. The generalisation replaces the major premise with a new hypothesis x everywhere in the goal. If eq_name is some h, an equation h : major_premise = x is added to remember the value of the major premise.

source
meta def tactic.interactive.generalisation_mode_parser  :
lean.parser tactic.eliminate.generalization_mode

Parse a fixing or generalizing clause for induction' or cases'.

source
meta def tactic.interactive.induction' (major_premise : interactive.parse tactic.interactive.cases_arg_p) (gm : interactive.parse tactic.interactive.generalisation_mode_parser) (with_patterns : interactive.parse tactic.eliminate.with_pattern.clause_parser) :
tactic unit

A variant of tactic.interactive.induction, with the following differences:

  • If the major premise (the hypothesis we are performing induction on) has complex indices, induction' 'remembers' them. A complex expression is any expression that is not merely a local hypothesis. A major premise h : I p₁ ... pₙ j₁ ... jₘ, where I is an inductive type with n parameters and m indices, has a complex index if any of the jᵢ are complex. In this situation, standard induction effectively forgets the exact values of the complex indices, which often leads to unprovable goals. induction' 'remembers' them by adding propositional equalities. As a result, you may find equalities named induction_eq in your goal, and the induction hypotheses may also quantify over additional equalities.
  • induction' generalises induction hypotheses as much as possible by default. This means that if you eliminate n in the goal 
    n m : ℕ
⊢ P n m
    the induction hypothesis is ∀ m, P n m instead of P n m.
  • induction' generates much more human-friendly names than induction. It also clears redundant hypotheses more aggressively.
  • induction' currently does not support custom induction principles a la induction using.

Like induction, induction' supports some modifiers:

induction' e with n₁ ... nₘ uses the names nᵢ for the new hypotheses. Instead of a name, you can also give an underscore (_) to have induction' generate a name for you, or a hyphen (-) to clear the hypothesis and any hypotheses that depend on it.

induction' e fixing h₁ ... hₙ fixes the hypotheses hᵢ, so the induction hypothesis is not generalised over these hypotheses.

induction' e fixing * fixes all hypotheses. This disables the generalisation functionality, so this mode behaves like standard induction.

induction' e generalizing h₁ ... hₙ generalises only the hypotheses hᵢ. This mode behaves like induction e generalizing h₁ ... hₙ.

induction' t, where t is an arbitrary term (rather than a hypothesis), generalises the goal over t, then performs induction on the generalised goal.

induction' h : t = x is similar, but also adds an equation h : t = x to remember the value of t.

To debug this tactic, use

set_option trace.eliminate_hyp true
source
meta def tactic.interactive.cases' (major_premise : interactive.parse tactic.interactive.cases_arg_p) (with_patterns : interactive.parse tactic.eliminate.with_pattern.clause_parser) :
tactic unit

A variant of tactic.interactive.cases, with minor changes:

  • cases' can perform case analysis on some (rare) goals that cases does not support.
  • cases' generates much more human-friendly names for the new hypotheses it introduces.

This tactic supports the same modifiers as cases, e.g.

cases' H : e = x with n _ o

This is almost exactly the same as tactic.interactive.induction', only that no induction hypotheses are generated.

To debug this tactic, use

set_option trace.eliminate_hyp true