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≤ n
andn < b
(inℕ
,ℤ
,ℕ+
, bounds of the forma < n
andn ≤ b≤ b
are also allowed), and also makes use of lower and upper bounds found viale_top
andbot_le
(so for example ifn : ℕ
, then the bound0 ≤ n≤ n
is automatically found). - call
fin_cases
on the synthesised hypothesisn ∈ set.Ico a b∈ set.Ico a b
, assuming an appropriatefintype
instance can be found for the type ofn
.
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
.
The target expression, a numeral in the input type
rhs : Lean.ExprThe 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.
Instances For
- lt: ℤ → Mathlib.Tactic.IntervalCases.Bound
A strictly less-than lower bound
n ≱ e≱ e
or upper bounde ≱ n≱ n
. (interval_cases
uses less-equal exclusively, so less-than bounds are actually written as not-less-equal with flipped arguments.) - le: ℤ → Mathlib.Tactic.IntervalCases.Bound
A less-than-or-equal lower bound
n ≤ e≤ e
or upper bounde ≤ n≤ n
.
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
.
Instances For
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
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
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.
Given
e
, construct(bound, n, p)
wherep
is a proof ofn ≤ e≤ e
orn < e
(characterized bybound
), orfailure
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)
wherep
is a proof ofe ≤ n≤ n
ore < n
(characterized bybound
), orfailure
if the type is not upper-bounded.initUB : Lean.Expr → Lean.MetaM (Mathlib.Tactic.IntervalCases.Bound × Lean.Expr × Lean.Expr)Given
a, b
, provea ≤ b≤ b
or fail.proveLE : Lean.Expr → Lean.Expr → Lean.MetaM Lean.ExprGiven
a, b
, provea ≱ b≱ b
or fail.proveLT : Lean.Expr → Lean.Expr → Lean.MetaM Lean.ExprGiven
a, b, a', p
wherep
provesa ≱ b≱ b
anda' := a+1
, provea' ≤ b≤ b
.Given
a, b, b', p
wherep
provesa ≱ b≱ b
andb' := b-1
, provea ≤ b'≤ b'
.Given
e
, return(z, n, p)
wherep : e = n
andn
is a numeral appropriate for the type denoting the integerz
.Construct the canonical numeral for integer
z
, or fail ifz
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
.
Instances For
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.
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.
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
.
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.
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.
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 integerse'
: a version ofe
used for error messages. (This is used by theinterval_cases
frontend tactic because it uses a fresh variable fore
, 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 givenubs
orlbs
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 overNat
orFin n
).
Returns an array of IntervalCasesSubgoal
, one per subgoal. A subgoal has the following fields:
rhs
: the numeral expression for this casevalue
: the integral value ofrhs
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.
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.