missing cases in auto_cases?

Stream: general

[Lucas Allen]

Auto_cases seems to miss some possible induction hypotheses. One example of this is

lemma test_one (n a : ℕ) (h : 1 ≤ n) : n * a = a * n :=
begin
  --auto_cases,
  induction h,
  sorry,
  sorry,
end

Here auto_cases says that it "did not find any hypotheses to apply cases or induction to", but induction h works.

Another example is

lemma test_three (n : ℕ) : n = n :=
begin
  --auto_cases,
  induction n,
  sorry,
  sorry,
end

auto_cases gives the same message, but induction n works, I don't know if this is what it's supposed to do though.

[Reid Barton]

auto_cases isn't really intended for the end user

[Reid Barton]

It's part of tidy. It has a list of known types for which it's usually a good idea to apply cases (or occasionally induction, I don't really understand why induction is even necessary)

[Lucas Allen]

I see. If I wanted something like this for the end user, would it make more sense to just run cases and induction on each hypothesis and report the ones which work?

[Reid Barton]

I assumed you were the end user

[Reid Barton]

What are you really trying to do?

[Lucas Allen]

I'm writing a tactic called check which goes through a list of tactics (an extended version of the list from tidy) and reports which ones succeed without modifying the tactic state. The idea is that this might be helpful when I get stuck proving something. Would something like this be suitable for mathlib?

[Scott Morrison]

@Lucas Allen, look for case_bash, hiding somewhere in mathlib.

[Lucas Allen]

II found it, it's in core.lean. A few modifications and it'll do what I want it to. Thanks.