Zulip Chat Archive

Stream: general

Topic: finset_cases and nat_cases


Scott Morrison (Feb 27 2019 at 22:15):

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 (Feb 27 2019 at 22:15):

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 (Feb 27 2019 at 22:16):

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

Kenny Lau (Feb 27 2019 at 22:20):

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

Chris Hughes (Feb 27 2019 at 22:22):

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 (Feb 27 2019 at 22:23):

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

Kenny Lau (Feb 27 2019 at 22:24):

bingo:

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

Kenny Lau (Feb 27 2019 at 22:24):

(used in tactic.fin_cases)

Kenny Lau (Feb 27 2019 at 22:26):

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 (Feb 27 2019 at 22:26):

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

Rob Lewis (Feb 27 2019 at 22:30):

(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 (Feb 27 2019 at 22:31):

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

Kenny Lau (Feb 27 2019 at 22:31):

eval_expr can tell just fine

Scott Morrison (Mar 02 2019 at 22:34):

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 (Mar 02 2019 at 22:34):

nat_cases and int_cases are still in progress.


Last updated: Dec 20 2023 at 11:08 UTC