mathlib documentation

tactic.dependencies

Tactics About Dependencies

This module provides tactics to compute dependencies and reverse dependencies of hypotheses. An expression e depends on a hypothesis h if e would not be valid if h were removed from the context. For example, the expression e := x > 0 depends on x. We say that x is a dependency of e and that e is a reverse dependency of x.

It is sometimes useful to consider inclusive dependency: e inclusively depends on h iff e depends on h or e = h (so inclusive dependency is the reflexive closure of regular dependency).

Note that the standard library does not use quite the same terminology:

Local Definitions

Determining dependencies of hypotheses is usually straightforward: a hypothesis r : R depends on another hypothesis d : D if d occurs in R. The implementation is more involved, however, in the presence of local definitions. Consider this context:

n m : 
k :  := m
o :  := k
h : o > 0

h depends on o, k and m, but only the dependency on o is syntactically obvious. kdepends_on ignores this complication and claims that h does not depend on k or m. We do not follow this example but process local definitions properly. This means that if the context contains a local definition, we need to compute the syntactic dependencies of h, then their dependencies, and so on.

Direct Dependencies

If you want to ignore local definitions while computing dependencies, this module also provides tactics to find the direct dependencies of a hypothesis. These are the hypotheses that syntactically appear in the hypothesis's type (or value, if the hypothesis is a local definition).

Direct Dependencies

Checking whether hypotheses directly depend on each other

type_has_local_in_name_set h ns returns true iff the type of h contains a local constant whose unique name appears in ns.

type_has_local_in_set h hs returns true iff the type of h contains any of the local constants hs.

meta def tactic.type_has_local_in (h : expr) (hs : list expr) :

type_has_local_in h hs returns true iff the type of h contains any of the local constants hs.

local_def_value_has_local_in_name_set h ns returns true iff h is a local definition whose value contains a local constant whose unique name appears in ns.

local_def_value_has_local_in_set h hs returns true iff h is a local definition whose value contains any of the local constants hs.

local_def_value_has_local_in h hs returns true iff h is a local definition whose value contains any of the local constants hs.

hyp_directly_depends_on_local_name_set h ns is true iff the hypothesis h directly depends on a hypothesis whose unique name appears in ns.

hyp_directly_depends_on_local_set h hs is true iff the hypothesis h directly depends on any of the hypotheses hs.

hyp_directly_depends_on_locals h hs is true iff the hypothesis h directly depends on any of the hypotheses hs.

hyp_directly_depends_on_local_name_set_inclusive h ns is true iff the hypothesis h directly depends on a hypothesis whose unique name appears in ns or h's name appears in ns.

hyp_directly_depends_on_local_set_inclusive h ns is true iff the hypothesis h directly depends on any of the hypotheses hs or h appears in hs.

hyp_directly_depends_on_locals_inclusive h ns is true iff the hypothesis h directly depends on any of the hypotheses hs or h appears in hs.

Computing the direct dependencies of a hypothesis

direct_dependency_set_of_hyp h is the set of hypotheses that the hypothesis h directly depends on. These are the hypotheses that appear in h's type or value (if h is a local definition).

direct_dependency_name_set_of_hyp h is the set of unique names of hypotheses that the hypothesis h directly depends on. These are the hypotheses that appear in h's type or value (if h is a local definition).

direct_dependencies_of_hyp h is the list of hypotheses that the hypothesis h directly depends on. These are the hypotheses that appear in h's type or value (if h is a local definition). The dependencies are returned in no particular order.

direct_dependency_set_of_hyp_inclusive h is the set of hypotheses that the hypothesis h directly depends on, plus h itself.

direct_dependency_name_set_of_hyp_inclusive h is the set of unique names of hypotheses that the hypothesis h directly depends on, plus h itself.

direct_dependencies_of_hyp_inclusive h is the list of hypotheses that the hypothesis h directly depends on, plus h itself. The dependencies are returned in no particular order.

Indirect/Transitive Dependencies

Checking whether hypotheses depend on each other

hyp_depends_on_local_name_set' cache h ns is true iff h depends on any of the hypotheses whose unique names appear in ns. cache must be a set of hypotheses known not to depend (even indirectly) on any of the ns. This is a performance optimisation, so you can give an empty cache. The tactic also returns an expanded cache with hypotheses which the tactic has encountered.

You probably want to use tactic.hyp_depends_on_local_name_set or tactic.hyps_depend_on_local_name_set instead of this tactic.

hyp_depends_on_local_name_set h ns is true iff the hypothesis h depends on any of the hypotheses whose unique names appear in ns. If you need to check dependencies of multiple hypotheses, use tactic.hyps_depend_on_local_name_set.

hyp_depends_on_local_set h hs is true iff the hypothesis h depends on any of the hypotheses hs. If you need to check dependencies of multiple hypotheses, use tactic.hyps_depend_on_local_set.

hyp_depends_on_locals h hs is true iff the hypothesis h depends on any of the hypotheses hs. If you need to check dependencies of multiple hypotheses, use tactic.hyps_depend_on_locals.

hyps_depend_on_local_name_set hs ns returns, for each h ∈ hs, whether h depends on a hypothesis whose unique name appears in ns. This is the same as (but more efficient than) calling tactic.hyp_depends_on_local_name_set for every h ∈ hs.

hyps_depend_on_local_set hs is returns, for each h ∈ hs, whether h depends on any of the hypotheses is. This is the same as (but more efficient than) calling tactic.hyp_depends_on_local_set for every h ∈ hs.

hyps_depend_on_locals hs is returns, for each h ∈ hs, whether h depends on any of the hypotheses is. This is the same as (but more efficient than) calling tactic.hyp_depends_on_locals for every h ∈ hs.

hyp_depends_on_local_name_set_inclusive' cache h ns is true iff the hypothesis h inclusively depends on a hypothesis whose unique name appears in ns. cache must be a set of hypotheses known not to depend (even indirectly) on any of the ns. This is a performance optimisation, so you can give an empty cache. The tactic also returns an expanded cache with hypotheses which the tactic has encountered. Note that the cache records exclusive, not inclusive dependencies.

You probably want to use tactic.hyp_depends_on_local_name_set_inclusive or tactic.hyps_depend_on_local_name_set_inclusive instead of this tactic.

hyp_depends_on_local_name_set_inclusive h ns is true iff the hypothesis h inclusively depends on any of the hypotheses whose unique names appear in ns. If you need to check the dependencies of multiple hypotheses, use tactic.hyps_depend_on_local_name_set_inclusive.

hyp_depends_on_local_set_inclusive h hs is true iff the hypothesis h inclusively depends on any of the hypotheses hs. If you need to check dependencies of multiple hypotheses, use tactic.hyps_depend_on_local_set_inclusive.

hyp_depends_on_locals_inclusive h hs is true iff the hypothesis h inclusively depends on any of the hypotheses hs. If you need to check dependencies of multiple hypotheses, use tactic.hyps_depend_on_locals_inclusive.

hyps_depend_on_local_name_set_inclusive hs ns returns, for each h ∈ hs, whether h inclusively depends on a hypothesis whose unique name appears in ns. This is the same as (but more efficient than) calling tactic.hyp_depends_on_local_name_set_inclusive for every h ∈ hs.

hyps_depend_on_local_set_inclusive hs is returns, for each h ∈ hs, whether h depends inclusively on any of the hypotheses is. This is the same as (but more efficient than) calling tactic.hyp_depends_on_local_set_inclusive for every h ∈ hs.

hyps_depend_on_locals_inclusive hs is returns, for each h ∈ hs, whether h depends inclusively on any of the hypotheses is. This is the same as (but more efficient than) calling tactic.hyp_depends_on_locals_inclusive for every h ∈ hs.

Computing the dependencies of a hypothesis

dependency_set_of_hyp' cache h is the set of dependencies of the hypothesis h. cache is a map from hypotheses to all their dependencies (including indirect dependencies). This is a performance optimisation, so you can give an empty cache. The tactic also returns an expanded cache with hypotheses which the tactic has encountered.

You probably want to use tactic.dependency_set_of_hyp or tactic.dependency_sets_of_hyps instead of this tactic.

dependency_set_of_hyp h is the set of dependencies of the hypothesis h. If you need the dependencies of multiple hypotheses, use tactic.dependency_sets_of_hyps.

dependency_name_set_of_hyp h is the set of unique names of the dependencies of the hypothesis h. If you need the dependencies of multiple hypotheses, use tactic.dependency_name_sets_of_hyps.

dependencies_of_hyp h is the list of dependencies of the hypothesis h. The dependencies are returned in no particular order. If you need the dependencies of multiple hypotheses, use tactic.dependencies_of_hyps.

dependency_sets_of_hyps hs returns, for each h ∈ hs, the set of dependencies of h. This is the same as (but more performant than) using tactic.dependency_set_of_hyp on every h ∈ hs.

dependency_name_sets_of_hyps hs returns, for each h ∈ hs, the set of unique names of the dependencies of h. This is the same as (but more performant than) using tactic.dependency_name_set_of_hyp on every h ∈ hs.

dependencies_of_hyps hs returns, for each h ∈ hs, the dependencies of h. The dependencies appear in no particular order in the returned lists. This is the same as (but more performant than) using tactic.dependencies_of_hyp on every h ∈ hs.

dependency_set_of_hyp_inclusive' cache h is the set of dependencies of the hypothesis h, plus h itself. cache is a map from hypotheses to all their dependencies (including indirect dependencies). This is a performance optimisation, so you can give an empty cache. The tactic also returns an expanded cache with hypotheses which the tactic has encountered. Note that the cache records exclusive, not inclusive dependencies.

You probably want to use tactic.dependency_set_of_hyp_inclusive or tactic.dependency_sets_of_hyps_inclusive instead of this tactic.

dependency_set_of_hyp_inclusive h is the set of dependencies of the hypothesis h, plus h itself. If you need the dependencies of multiple hypotheses, use tactic.dependency_sets_of_hyps_inclusive.

dependency_name_set_of_hyp_inclusive h is the set of unique names of the dependencies of the hypothesis h, plus the unique name of h itself. If you need the dependencies of multiple hypotheses, use tactic.dependency_name_sets_of_hyps_inclusive.

dependencies_of_hyp_inclusive h is the list of dependencies of the hypothesis h, plus h itself. The dependencies are returned in no particular order. If you need the dependencies of multiple hypotheses, use tactic.dependencies_of_hyps_inclusive.

dependency_sets_of_hyps_inclusive hs returns, for each h ∈ hs, the dependencies of h, plus h itself. This is the same as (but more performant than) using tactic.dependency_set_of_hyp_inclusive on every h ∈ hs.

dependency_name_sets_of_hyps_inclusive hs returns, for each h ∈ hs, the unique names of the dependencies of h, plus the unique name of h itself. This is the same as (but more performant than) using tactic.dependency_name_set_of_hyp_inclusive on every h ∈ hs.

dependencies_of_hyps_inclusive hs returns, for each h ∈ hs, the dependencies of h, plus h itself. The dependencies appear in no particular order in the returned lists. This is the same as (but more performant than) using tactic.dependencies_of_hyp_inclusive on every h ∈ hs.

Computing the reverse dependencies of a hypothesis

reverse_dependencies_of_hyp_name_set hs is the list of reverse dependencies of the hypotheses whose unique names appear in hs, excluding the hs themselves. The reverse dependencies are returned in the order in which they appear in the context.

reverse_dependencies_of_hyp_set hs is the list of reverse dependencies of the hypotheses hs, excluding the hs themselves. The reverse dependencies are returned in the order in which they appear in the context.

reverse_dependencies_of_hyps hs is the list of reverse dependencies of the hypotheses hs, excluding the hs themselves. The reverse dependencies are returned in the order in which they appear in the context.

reverse_dependencies_of_hyp_name_set_inclusive hs is the list of reverse dependencies of the hypotheses whose unique names appear in hs, including the hs themselves. The reverse dependencies are returned in the order in which they appear in the context.

reverse_dependencies_of_hyp_set_inclusive hs is the list of reverse dependencies of the hypotheses hs, including the hs themselves. The inclusive reverse dependencies are returned in the order in which they appear in the context.

reverse_dependencies_of_hyps_inclusive hs is the list of reverse dependencies of the hypotheses hs, including the hs themselves. The reverse dependencies are returned in the order in which they appear in the context.

Reverting a hypothesis and its reverse dependencies

revert_name_set hs reverts the hypotheses whose unique names appear in hs, as well as any hypotheses that depend on them. Returns the number of reverted hypotheses and a list containing these hypotheses. The reverted hypotheses are returned in the order in which they used to appear in the context and are guaranteed to store the correct type (see tactic.update_type).

revert_set hs reverts the hypotheses hs, as well as any hypotheses that depend on them. Returns the number of reverted hypotheses and a list containing these hypotheses. The reverted hypotheses are returned in the order in which they used to appear in the context and are guaranteed to store the correct type (see tactic.update_type).

meta def tactic.revert_lst' (hs : list expr) :

revert_lst' hs reverts the hypotheses hs, as well as any hypotheses that depend on them. Returns the number of reverted hypotheses and a list containing these hypotheses. The reverted hypotheses are returned in the order in which they used to appear in the context and are guaranteed to store the correct type (see tactic.update_type).

This is a more informative version of tactic.revert_lst.

revert_reverse_dependencies_of_hyp h reverts all the hypotheses that depend on the hypothesis h, including the local definitions that have h in their value. This fixes a bug in tactic.revert_kdependencies that does not revert local definitions for which h only appears in the value. Returns the number of reverted hypotheses.

revert_reverse_dependencies_of_hyp_name_set hs reverts all the hypotheses that depend on a hypothesis whose unique name appears in hs. The hs themselves are not reverted, unless they depend on each other. Returns the number of reverted hypotheses.

revert_reverse_dependencies_of_hyp_set hs reverts all the hypotheses that depend on a hypothesis in hs. The hs themselves are not reverted, unless they depend on each other. Returns the number of reverted hypotheses.

revert_reverse_dependencies_of_hyp hs reverts all the hypotheses that depend on a hypothesis in hs. The hs themselves are not reverted, unless they depend on each other. Returns the number of reverted hypotheses.