Case bash on variables in finite intervals #

This file provides the tactic interval_cases. interval_cases n will:

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).
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:

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 among the hypotheses, or from bot_le n,
an explicit upper bound can be found among 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.

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

tactic.interval_cases.set_elems s = finset.image subtype.val (fintype.elems ↥s)

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 interactive.types.texpr ?) (bounds : interactive.parse (lean.parser.tk "using" *> (prod.mk <$> lean.parser.ident <*> lean.parser.ident))?) (lname : interactive.parse (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.