Finset.range and Fin too burdensome to be worth it for now

Stream: mathlib4

[Daniel Briggs]

For sums in mathlib, Finset.range and Fin are constantly recommended for everything in the documentation. I understand why this is so, but it just immediately creates a development hell where everything you're trying to do requires constantly casting back and forth between (say) natural numbers and these types. And so of course, Lean has no idea what to do with anything either; "apply?" becomes essentially worthless.

Has anyone found an efficient way to work with sums in mathlib4?

[Ruben Van de Velde]

Do you have examples of what's difficult?

[Bhavik Mehta]

I find working with Finset.range and sums very pleasant, but it is true there is not much guidance for how to make it work. And this is particularly frustrating, because it works very nicely! So I echo Ruben's question, which parts are you struggling with?

[Daniel Briggs]

Thank you both for your swift replies. I'm working on proving that you can split off the first term of a sum right now. It's a little tough since the theorems are split across different subdirectories of mathlib, but I'm sure I'll get it soon.

My eventual goal is to prove that each natural number has a unique decimal representation; I've written 150 lines of the proof of the easier half of the induction (when the previous number was not 9 mod 10) so far.

Since Lean was...fairly...good at "apply?" recommendations when I was working with Nat, Int, Rat, or Real, I got a little lazy; for Fin and Finset.range, it just seems that there's no way around committing the names of a few dozen theorems to heart.

I'll post examples of what I come up against as I work on it more.

[Bhavik Mehta]

My first guess is that you want Finset.sum_range_succ' for this

[Kyle Miller]

If this isn't for the exercise, docs#Nat.digits gives the decimal representation of a natural number, docs#Nat.ofDigits is the reverse, docs#Nat.ofDigits_digits is their relationship, and docs#Nat.digits_ofDigits is basically that the digit representation is unique.

[Daniel Briggs]

Thanks!

[Daniel Briggs]

Alright, here's an example of a related point I'm stuck on today:

The tactic fin_cases "performs case analysis on a hypothesis of the form h : A, where Fintype A is available, or h : a ∈ A, where A : Finset X, A : Multiset X or A : List X." There is one example in the documentation of its use, followed by a few paragraphs of what used to work in mathlib3 and doesn't work anymore.

I have:

msd : ℕ := (digits 10 x).getLast nonemp
msdlem : msd ≤ 9 ∧ 1 ≤ msd
xx : ¬msd ∈ {1, 2, 3, 4, 6, 8}
⊢ msd ∈ {5, 7, 9}

I'd like to use fin_cases to make this work, since cases would be an indentation headache. I've tried to do this after establishing have finny : msd ∈ Finset.range 10 or have h_msd_in_1_to_9 : msd ∈ (Finset.Icc 1 9 : Finset Nat), but I can't figure out how to go from Finset.range or Finset.Icc to Fin, and there's no relevant example in the documentation either.

[Eric Wieser]

Can you make this a #mwe ?

[Daniel Briggs]

Sorry, I had missed out one hypothesis. It should be there now.

(There's probably a better way with set unions too, but this could become an instructive example of how to use fin_cases.)

[Aaron Liu]

interval_cases is probably the better tactic to use here.

[Daniel Briggs]

Thanks! Yes, interval_cases seems to be working here. And I've used it before! I just forgot about it, since I've been encountering so many things at once.

[Sabbir Rahman]

I think loogle can most of the time do the work of apply? if you know what you're searching for. I haven't done many Finset.sum proofs, but a mental model I have realized is that converting all kinds of indices to Finset.Ico generally lessens headache