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.

source
meta def tactic.interval_cases.gives_upper_bound (n e : expr) :
tactic expr

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

source
meta def tactic.interval_cases.gives_lower_bound (n e : expr) :
tactic expr

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

source
meta def tactic.interval_cases.combine_upper_bounds  :
option expr → option expr → tactic (option expr)

Combine two upper bounds.

source
meta def tactic.interval_cases.combine_lower_bounds  :
option expr → option expr → tactic (option expr)

Combine two lower bounds.

source
meta def tactic.interval_cases.update_bounds (n : expr) (bounds : option expr × option expr) (e : expr) :
tactic (option expr × option expr)

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

source
meta def tactic.interval_cases.initial_lower_bound (n : expr) :
tactic expr

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

source
meta def tactic.interval_cases.initial_upper_bound (n : expr) :
tactic expr

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

source
meta def tactic.interval_cases.get_bounds (n : expr) :
tactic (expr × expr)

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

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

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

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

Each element of s is a member of set_elems s.

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

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.

source
meta def tactic.interactive.interval_cases (n : interactive.parse (optional interactive.types.texpr)) (bounds : interactive.parse (optional (lean.parser.tk "using" *> (prod.mk <$> lean.parser.ident <*> lean.parser.ident)))) (lname : interactive.parse (optional (lean.parser.tk "with" *> lean.parser.ident))) :
tactic unit

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.

source
def tactic_doc.tactic.interval_cases  :
tactic_doc_entry

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.