A better tactic for induction and case analysis #
This module defines the tactics
tactic.interactive.cases', which are variations on Lean's builtin
cases. The primed variants feature various improvements over the builtin
tactics; in particular, they generate more human-friendly names and
deals much better with indexed inductive types. See the tactics' documentation
for more details. We also provide corresponding non-interactive induction
The design and implementation of these tactics is described in a draft paper.
We set up two tracing functions to be used by
eliminate_hyp and its supporting
tactics. Their output is enabled by setting
Information Gathering #
We define data structures for information relevant to the induction, and functions to collect this information for a specific goal.
Constructor Argument Naming #
We define the algorithm for naming constructor arguments (which is a remarkably big part of the tactic).
induction' can generalise the goal before performing an induction, which gives
us a more general induction hypothesis. We call this 'auto-generalisation'.
- generalize_all_except : list name → tactic.eliminate.generalization_mode
- generalize_only : list name → tactic.eliminate.generalization_mode
A value of
generalization_mode describes the behaviour of the
generalize_all_except hsmeans that the
hsremain fixed and all other hypotheses are generalised. However, there are three exceptions:
- Hypotheses depending on any
hsalso remain fixed. If we were to generalise them, we would have to generalise
- 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.
- Hypotheses depending on any
generalize_only hsmeans that only the
hsare generalised. Exception: hypotheses which depend on the major premise are generalised even if they do not appear in
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)
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.
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.
Temporary utilities #
The utility functions in this section should be removed pending certain changes to Lean's standard library.
The Elimination Tactics #
Finally, we define the tactics
cases' tactics as well as the