mathlib3 documentation

tactic.interval_cases

Case bash on variables in finite intervals #

This file provides the tactic interval_cases. interval_cases n will:

  1. inspect hypotheses looking for lower and upper bounds of the form a ≤ n and n < b (in , , ℕ+, bounds of the form a < n and n ≤ b are also allowed), and also makes use of lower and upper bounds found via le_top and bot_le (so for example if n : ℕ, then the bound 0 ≤ n is automatically found).
  2. call fin_cases on the synthesised hypothesis n ∈ set.Ico a b, assuming an appropriate fintype instance can be found for the type of n.

The variable n can belong to any type α, with the following restrictions:

You can also explicitly specify a lower and upper bound to use, as interval_cases using hl hu, where the hypotheses should be of the form hl : a ≤ n and hu : n < b. In that case, interval_cases calls fin_cases on the resulting hypothesis h : n ∈ set.Ico a b.

If e easily implies (%%n < %%b) for some explicit b, return that proof.

If e easily implies (%%n ≥ %%b) for some explicit b, return that proof.

Inspect a given expression, using it to update a set of upper and lower bounds on n.

Attempt to find a lower bound for the variable n, by evaluating bot_le n.

Attempt to find an upper bound for the variable n, by evaluating le_top n.

Inspect the local hypotheses for upper and lower bounds on a variable n.

def tactic.interval_cases.set_elems {α : Type u_1} [decidable_eq α] (s : set α) [fintype s] :

The finset of elements of a set s for which we have fintype s.

Equations
theorem tactic.interval_cases.mem_set_elems {α : Type u_1} [decidable_eq α] (s : set α) [fintype s] {a : α} (h : a s) :

Each element of s is a member of set_elems s.

meta def tactic.interval_cases_using (hl hu : expr) (n : option name) :

Call fin_cases on membership of the finset built from an Ico interval corresponding to a lower and an upper bound.

Here hl should be an expression of the form a ≤ n, for some explicit a, and hu should be of the form n < b, for some explicit b.

By default interval_cases_using automatically generates a name for the new hypothesis. The name can be specified via the optional argument n.

interval_cases n searches for upper and lower bounds on a variable n, and if bounds are found, splits into separate cases for each possible value of n.

As an example, in

example (n : ) (w₁ : n  3) (w₂ : n < 5) : n = 3  n = 4 :=
begin
  interval_cases n,
  all_goals {simp}
end

after interval_cases n, the goals are 3 = 3 ∨ 3 = 4 and 4 = 3 ∨ 4 = 4.

You can also explicitly specify a lower and upper bound to use, as interval_cases using hl hu. The hypotheses should be in the form hl : a ≤ n and hu : n < b, in which case interval_cases calls fin_cases on the resulting fact n ∈ set.Ico a b.

You can specify a name h for the new hypothesis, as interval_cases n with h or interval_cases n using hl hu with h.

interval_cases n searches for upper and lower bounds on a variable n, and if bounds are found, splits into separate cases for each possible value of n.

As an example, in

example (n : ) (w₁ : n  3) (w₂ : n < 5) : n = 3  n = 4 :=
begin
  interval_cases n,
  all_goals {simp}
end

after interval_cases n, the goals are 3 = 3 ∨ 3 = 4 and 4 = 3 ∨ 4 = 4.

You can also explicitly specify a lower and upper bound to use, as interval_cases using hl hu. The hypotheses should be in the form hl : a ≤ n and hu : n < b, in which case interval_cases calls fin_cases on the resulting fact n ∈ set.Ico a b.

You can also explicitly specify a name to use for the hypothesis added, as interval_cases n with hn or interval_cases n using hl hu with hn.

In particular, interval_cases n

  1. inspects hypotheses looking for lower and upper bounds of the form a ≤ n and n < b (although in , , and ℕ+ bounds of the form a < n and n ≤ b are also allowed), and also makes use of lower and upper bounds found via le_top and bot_le (so for example if n : ℕ, then the bound 0 ≤ n is found automatically), then
  2. calls fin_cases on the synthesised hypothesis n ∈ set.Ico a b, assuming an appropriate fintype instance can be found for the type of n.

The variable n can belong to any type α, with the following restrictions:

  • only bounds on which expr.to_rat succeeds will be considered "explicit" (TODO: generalise this?)
  • an instance of decidable_eq α is available,
  • an explicit lower bound can be found amongst the hypotheses, or from bot_le n,
  • an explicit upper bound can be found amongst the hypotheses, or from le_top n,
  • if multiple bounds are located, an instance of linear_order α is available, and
  • an instance of fintype set.Ico l u is available for the relevant bounds.