Proof by cases of finite integer

Stream: lean4

[Jeremy Salwen]

Hello all, I am trying to prove the following lemma:

lemma Nat.digitChar_is_digit (n: ℕ) (P: n < 10): Char.isDigit (Nat.digitChar n)

When I expand the two function definitions, it just becomes a large nested if statement which can be trivially evaluated to be true for n < 10. I would like to do a proof by case split on the 10 possible values for n (since this is smaller than the number of branches of the if statements). However, cases n just wants to split into zero and succ n' rather than splitting into a finite set of numbers. What is the right way to structure a proof like this?

[Kevin Buzzard]

In lean 3 the interval_cases tactic did this, but I'm not sure it's been ported to lean 4 yet. Would you like to learn how to write tactics? This is probably quite a good one to start on.

[Kevin Buzzard]

tactic#interval_cases

[Jeremy Salwen]

Sure, that sounds fun! I will take a look.

[Mario Carneiro]

I'm working on interval_cases now, should be ready soon

[Mario Carneiro]

(you probably wouldn't think it's a good tactic to start on if you discovered, as I did, that mathlib's interval_cases tactic works on any locally finite linear order, which means that you can use arguments that are sums and products of finitely supported functions on nat!)

[Mario Carneiro]

I am almost certain no one has ever made use of this "feature", but the tactic specification is very close to the implementation which is awkward since the implementation is notoriously slow

[Kevin Buzzard]

Yes I'm not sure there's ever been a use of it outside Nat and Int.

[Jeremy Salwen]

I will just leave a hole for now in my proof, let me know when you finish the tactic

[Mario Carneiro]

the cheapo method is a pattern match:

example (P : Nat → Prop) : ∀ n, n < 10 → n + 1 = 1 + n
  | 0, _ | 1, _ | 2, _ | 3, _ | 4, _ | 5, _ | 6, _ | 7, _ | 8, _ | 9, _ => rfl

[Eric Wieser]

Mario Carneiro said:

mathlib's interval_cases tactic works on any locally finite linear order, which means that you can use arguments that are sums and products of finitely supported functions on nat!)

Surely products of finsupps are not a linear order? Or do you mean under the lexicographic order?

[Mario Carneiro]

in fact, for decidable bool functions you generally don't even need to do this because there is a decidability instance for statements of the form \forall n < m, P n:

lemma Nat.digitChar_is_digit : ∀ n < 10, Char.isDigit (Nat.digitChar n) := by decide

[Mario Carneiro]

Eric Wieser said:

Mario Carneiro said:

mathlib's interval_cases tactic works on any locally finite linear order, which means that you can use arguments that are sums and products of finitely supported functions on nat!)

Surely products of finsupps are not a linear order? Or do you mean under the lexicographic order?

Actually you only need a linear order instance if there is more than one applicable hypothesis in the context (yes, the tactic does not know how to pick the best one so if you don't have a linear order then you have to be careful to not make it use the combining logic)

[Mario Carneiro]

here's the actual spec from the doc comment:

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.

[Mario Carneiro]

the fintype (set.Ico l u) thing is a bit more general than I stated but if you look in mathlib the only instance of fintype (set.Ico l u) is via the locally_finite_order class, which has instances for sums and products and finsupp and nat/int

[Jeremy Salwen]

Mario Carneiro said:

in fact, for decidable bool functions you generally don't even need to do this because there is a decidability instance for statements of the form \forall n < m, P n:

lemma Nat.digitChar_is_digit : ∀ n < 10, Char.isDigit (Nat.digitChar n) := by decide

I notice you have to revert n for the decide tactic to work. Is there a reason for that?

[Mario Carneiro]

yes, decide will only decide closed terms which can be reduced to true

[Mario Carneiro]

the instance is specifically for \forall n < m, P n, not for P n where n < m is in the context (decidability instances can't use the context because they aren't tactics)

[Mario Carneiro]

the mathlib decide! tactic is revert_all; decide which helps make this a bit more natural

[Jeremy Salwen]

ooh didn't know about decide! Thanks.

[Jeremy Salwen]

Could you clarify about how to use decide!. It doesn't seem accessible by default.

[Kevin Buzzard]

It looks to me like this tactic hasn't been ported to Lean 4 yet?

[Jeremy Salwen]

I also notice that the decide tactic will fail if revert n pulls irrelevant hypotheses into the goal that mention other variables. Is there a standard way to handle this, or do you just find any troublesome hypotheses and clear them first?