finset_cases and nat_cases

Stream: general

[Scott Morrison]

I was thinking while walking the dog this morning about how to implement a nat_cases tactic.

It seems best to do something more general first, and write a finset_cases tactic, so that finset_cases h takes a hypothesis of the form h : x \mem A, where A is an "explicitly known" finset, and explodes into multiple goals, one for each element of A.

After that, I'd write a nat_cases n a b, which gives you a goal with the hypothesis n < a, individual goals for each value of n \mem Ico a b (implemented using finset_cases), and another goal with n \geq b.

Finally we'd add nat_cases n, which collects hypotheses which are "obviously" linear inequalities solely in n, and calculates the relevant lower and upper bounds a and b. Now we'll call nat_cases n a b, and follow up by discharging the two goals with inequalities using linarith (passing to linarith just the collected relevant hypotheses, and the new hypothesis, so it should be fast).

[Scott Morrison]

I haven't yet thought too hard about what it means for a tactic to decide that a finset is "explicitly known", so maybe there is a problem here.

[Scott Morrison]

Any criticisms before I get started (maybe not today), welcome!

[Kenny Lau]

I think there is a tactic to determine if a formula is "closed", i.e. "explicitly known"

[Chris Hughes]

Let's say you've got some horrible finset like (univ : finset (perm (fin 2 -> fin 2))). You have to do some clever unfolding to work out what the expression for each element is I think. Maybe if the type has a has_reflect instance it will be easier.

[Chris Hughes]

In fact a has_reflect instance is probably a good definition of "explicitly known"

[Kenny Lau]

bingo:

/-- (eval_expr α e) evaluates 'e' IF 'e' has type 'α'. -/
meta constant eval_expr (α : Type u) [reflected α] : expr → tactic α

[Kenny Lau]

(used in tactic.fin_cases)

[Kenny Lau]

case in point:

example : true :=
begin
  have : ∀ n, ∀ k : fin n, true,
  { intros n k, fin_cases k,
/-
invalid eval_expr, expression must be closed
state:
n : ℕ,
k : fin n
⊢ true
-/ },
end

[Rob Lewis]

Yeah, I suspect eval_expr on finset.sort will be the way to get your hands on the underlying list.

[Rob Lewis]

(Note, "closed" and "explicitly known" aren't quite synonyms. Closed means something like it has no local constants, which isn't enough to guarantee that it evaluates to a value. E.g. (λ x : ℝ, if x = 0 then 0 else 1) 0 is a closed nat that won't evaluate.)

[Kenny Lau]

invalid eval_expr, expression must be closed
state:
_inst : Π (a : Prop), decidable a,
k : fin (ite (ℕ = ℤ) 0 1)
⊢ true

[Kenny Lau]

eval_expr can tell just fine

[Scott Morrison]

Just following up here: it turns out eval_expr and finset.sort aren't even needed; cases is already awesome enough. https://github.com/leanprover-community/mathlib/pull/775 has an implemenation of fin_cases.

[Scott Morrison]

nat_cases and int_cases are still in progress.