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≤ n and n < b (in ℕ, ℤ, ℕ+, bounds of the form a < n and n ≤ b≤ 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≤ n is automatically found).
2. call fin_cases on the synthesised hypothesis n ∈ set.Ico a b∈ 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≤ n and hu : n < b. In that case, interval_cases calls fin_cases on the resulting hypothesis h : n ∈ set.Ico a b∈ set.Ico a b.

ink

structure Mathlib.Tactic.IntervalCases.IntervalCasesSubgoal : Type

• The target expression, a numeral in the input type

  rhs : Lean.Expr

• The numeric value of the target expression

  value : ℤ

• The new subgoal, of the form ⊢ x = rhs → tgt⊢ x = rhs → tgt→ tgt

  goal : Lean.MVarId

The result of interval_cases is a list of goals, one for each integer value between the bounds.

ink

inductive Mathlib.Tactic.IntervalCases.Bound : Type

• A strictly less-than lower bound n ≱ e≱ e or upper bound e ≱ n≱ n. (interval_cases uses less-equal exclusively, so less-than bounds are actually written as not-less-equal with flipped arguments.)

  lt: ℤ → Mathlib.Tactic.IntervalCases.Bound

• A less-than-or-equal lower bound n ≤ e≤ e or upper bound e ≤ n≤ n.

  le: ℤ → Mathlib.Tactic.IntervalCases.Bound

A Bound represents the result of analyzing a lower or upper bound expression. If e is the scrutinee expression, then a lower bound expression like 3 < e is normalized to ¬e ≤ 3¬e ≤ 3≤ 3 and represented as .lt 3, and an upper bound expression like e ≤ 5≤ 5 is represented as .le 5.

ink

def Mathlib.Tactic.IntervalCases.Bound.asLower : Mathlib.Tactic.IntervalCases.Bound → ℤ

Assuming Bound represents a lower bound, this returns the (inclusive) least integer value which is allowed. So 3 ≤ e≤ e means the lower bound is 3 and 3 < e means the lower bound is 4.

Equations

• Mathlib.Tactic.IntervalCases.Bound.asLower x = match x with | Mathlib.Tactic.IntervalCases.Bound.lt n => n + 1 | Mathlib.Tactic.IntervalCases.Bound.le n => n

ink

def Mathlib.Tactic.IntervalCases.Bound.asUpper : Mathlib.Tactic.IntervalCases.Bound → ℤ

Assuming Bound represents an upper bound, this returns the (inclusive) greatest integer value which is allowed. So e ≤ 3≤ 3 means the lower bound is 3 and e < 3 means the upper bound is 2. Note that in the case of e < 0 on Nat the upper bound is -1, which is not representable as a Nat; this is why we have to treat the .lt and .le cases separately instead of normalizing everything to .le bounds.

Equations

• Mathlib.Tactic.IntervalCases.Bound.asUpper x = match x with | Mathlib.Tactic.IntervalCases.Bound.lt n => n - 1 | Mathlib.Tactic.IntervalCases.Bound.le n => n

ink

def Mathlib.Tactic.IntervalCases.parseBound (ty : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr × Bool × Bool)

Given a type ty (the type of a hypothesis in the context or a provided expression), attempt to parse it as an inequality, and return (a, b, strict, positive), where positive means it is a negated inequality and strict means it is a strict inequality (a < b or a ≱ b≱ b). a is always the lesser argument and b the greater one.

Equations

• One or more equations did not get rendered due to their size.

ink

structure Mathlib.Tactic.IntervalCases.Methods : Type

• Given e, construct (bound, n, p) where p is a proof of n ≤ e≤ e or n < e (characterized by bound), or failure if the type is not lower-bounded.

  initLB : Lean.Expr → Lean.MetaM (Mathlib.Tactic.IntervalCases.Bound × Lean.Expr × Lean.Expr)

• Given e, construct (bound, n, p) where p is a proof of e ≤ n≤ n or e < n (characterized by bound), or failure if the type is not upper-bounded.

  initUB : Lean.Expr → Lean.MetaM (Mathlib.Tactic.IntervalCases.Bound × Lean.Expr × Lean.Expr)

• Given a, b, prove a ≤ b≤ b or fail.

  proveLE : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr

• Given a, b, prove a ≱ b≱ b or fail.

  proveLT : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr

• Given a, b, a', p where p proves a ≱ b≱ b and a' := a+1, prove a' ≤ b≤ b.

  roundUp : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr

• Given a, b, b', p where p proves a ≱ b≱ b and b' := b-1, prove a ≤ b'≤ b'.

  roundDown : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr

• Given e, return (z, n, p) where p : e = n and n is a numeral appropriate for the type denoting the integer z.

  eval : Lean.Expr → Lean.MetaM (ℤ × Lean.Expr × Lean.Expr)

• Construct the canonical numeral for integer z, or fail if z is out of range.

  mkNumeral : ℤ → Lean.MetaM Lean.Expr

A "typeclass" (not actually a class) of methods for the type-specific handling of interval_cases. To add support for a new type, you have to implement this interface and add a dispatch case for it in intervalCases.

ink

theorem Mathlib.Tactic.IntervalCases.of_not_lt_left {α : Type u_1} {a : α} {b : α} {a' : α} [inst : LinearOrder α] (h : ¬a < b) (eq : a = a') : b ≤ a'

ink

theorem Mathlib.Tactic.IntervalCases.of_not_lt_right {α : Type u_1} {a : α} {b : α} {b' : α} [inst : LinearOrder α] (h : ¬a < b) (eq : b = b') : b' ≤ a

ink

theorem Mathlib.Tactic.IntervalCases.of_not_le_left {α : Type u_1} {a : α} {b : α} {a' : α} [inst : LE α] (h : ¬a ≤ b) (eq : a = a') : ¬a' ≤ b

ink

theorem Mathlib.Tactic.IntervalCases.of_not_le_right {α : Type u_1} {a : α} {b : α} {b' : α} [inst : LE α] (h : ¬a ≤ b) (eq : b = b') : ¬a ≤ b'

ink

theorem Mathlib.Tactic.IntervalCases.of_lt_left {α : Type u_1} {a : α} {b : α} {a' : α} [inst : LinearOrder α] (h : a < b) (eq : a = a') : ¬b ≤ a'

ink

theorem Mathlib.Tactic.IntervalCases.of_lt_right {α : Type u_1} {a : α} {b : α} {b' : α} [inst : LinearOrder α] (h : a < b) (eq : b = b') : ¬b' ≤ a

ink

theorem Mathlib.Tactic.IntervalCases.of_le_left {α : Type u_1} {a : α} {b : α} {a' : α} [inst : LE α] (h : a ≤ b) (eq : a = a') : a' ≤ b

ink

theorem Mathlib.Tactic.IntervalCases.of_le_right {α : Type u_1} {a : α} {b : α} {b' : α} [inst : LE α] (h : a ≤ b) (eq : b = b') : a ≤ b'

ink

def Mathlib.Tactic.IntervalCases.Methods.getBound (m : Mathlib.Tactic.IntervalCases.Methods) (e : Lean.Expr) (pf : Lean.Expr) (lb : Bool) : Lean.MetaM (Mathlib.Tactic.IntervalCases.Bound × Lean.Expr × Lean.Expr)

Given a proof pf, attempts to parse it as an upper (lb = false) or lower (lb = true) bound on n. If successful, it returns (bound, n, pf') where n is a numeral and pf' proves n ≤ e≤ e or n ≱ e≱ e (as described by bound).

Equations

• One or more equations did not get rendered due to their size.

ink

theorem Mathlib.Tactic.IntervalCases.le_of_not_le_of_le {α : Type u_1} {hi : α} {n : α} {lo : α} [inst : LinearOrder α] (h1 : ¬hi ≤ n) (h2 : hi ≤ lo) : n ≤ lo

ink

def Mathlib.Tactic.IntervalCases.Methods.inconsistentBounds (m : Mathlib.Tactic.IntervalCases.Methods) (z1 : Mathlib.Tactic.IntervalCases.Bound) (z2 : Mathlib.Tactic.IntervalCases.Bound) (e1 : Lean.Expr) (e2 : Lean.Expr) (p1 : Lean.Expr) (p2 : Lean.Expr) (e : Lean.Expr) : Lean.MetaM Lean.Expr

Given (z1, e1, p1) a lower bound on e and (z2, e2, p2) an upper bound on e, such that the distance between the bounds is negative, returns a proof of False.

Equations

• One or more equations did not get rendered due to their size.

ink

partial def Mathlib.Tactic.IntervalCases.Methods.bisect (m : Mathlib.Tactic.IntervalCases.Methods) (g : Lean.MVarId) (cases : Subarray Mathlib.Tactic.IntervalCases.IntervalCasesSubgoal) (z1 : Mathlib.Tactic.IntervalCases.Bound) (z2 : Mathlib.Tactic.IntervalCases.Bound) (e1 : Lean.Expr) (e2 : Lean.Expr) (p1 : Lean.Expr) (p2 : Lean.Expr) (e : Lean.Expr) : Lean.MetaM Unit

Given (z1, e1, p1) a lower bound on e and (z2, e2, p2) an upper bound on e, such that the distance between the bounds matches the number of cases in the subarray (which must be positive), proves the goal g using the metavariables in the array by recursive bisection. This is the core of the tactic, producing a case tree of if statements which bottoms out at the cases.

ink

def Mathlib.Tactic.IntervalCases.natMethods : Mathlib.Tactic.IntervalCases.Methods

A Methods implementation for ℕ. This tells interval_cases how to work on natural numbers.

Equations

• One or more equations did not get rendered due to their size.

ink

theorem Int.add_one_le_of_not_le {a : ℤ} {b : ℤ} (h : ¬b ≤ a) : a + 1 ≤ b

ink

theorem Int.le_sub_one_of_not_le {a : ℤ} {b : ℤ} (h : ¬b ≤ a) : a ≤ b - 1

ink

def Mathlib.Tactic.IntervalCases.intMethods : Mathlib.Tactic.IntervalCases.Methods

A Methods implementation for ℤ. This tells interval_cases how to work on integers.

Equations

• One or more equations did not get rendered due to their size.

ink

def Mathlib.Tactic.IntervalCases.intervalCases (g : Lean.MVarId) (e : Lean.Expr) (e' : Lean.Expr) (lbs : Array Lean.Expr) (ubs : Array Lean.Expr) (mustUseBounds : optParam Bool false) : Lean.MetaM (Array Mathlib.Tactic.IntervalCases.IntervalCasesSubgoal)

intervalCases proves goal g by splitting into cases for each integer between the given bounds.

Parameters:

• g: the goal, which can have any type ⊢ tgt⊢ tgt (it works in both proofs and programs)
• e: the scrutinee, the expression we are proving is bounded between integers
• e': a version of e used for error messages. (This is used by the interval_cases frontend tactic because it uses a fresh variable for e, so it is more helpful to show the pre-generalized expression in error messages.)
• lbs: A list of candidate lower bound expressions. The tactic will automatically pick the best lower bound it can find from the list.
• ubs: A list of candidate upper bound expressions. The tactic will automatically pick the best upper bound it can find from the list.
• mustUseBounds: If true, the tactic will fail if it is unable to parse any of the given ubs or lbs into bounds. If false (the default), these will be silently skipped and an error message is only produced if we could not find any bounds (including those supplied by the type itself, e.g. if we are working over Nat or Fin n).

Returns an array of IntervalCasesSubgoal, one per subgoal. A subgoal has the following fields:

• rhs: the numeral expression for this case
• value: the integral value of rhs
• goal: the subgoal of type ⊢ e = rhs → tgt⊢ e = rhs → tgt→ tgt

Note that this tactic does not perform any substitution or introduction steps - all subgoals are in the same context as goal itself.

Equations

• One or more equations did not get rendered due to their size.

ink

def Mathlib.Tactic.intervalCases : Lean.ParserDescr

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 := by
  interval_cases n
  all_goals simp
≥ 3) (w₂ : n < 5) : n = 3 ∨ n = 4 := by
  interval_cases n
  all_goals simp
∨ n = 4 := by
  interval_cases n
  all_goals simp

after interval_cases n, the goals are 3 = 3 ∨ 3 = 4∨ 3 = 4 and 4 = 3 ∨ 4 = 4∨ 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≤ n and hu : n < b, in which case interval_cases calls fin_cases on the resulting fact n ∈ set.Ico a b∈ set.Ico a b.

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

Equations

• One or more equations did not get rendered due to their size.