Index bounds proof

Stream: Is there code for X?

[Vlad]

Is there a better way to handle index bound proofs in this example?
Ideally, index bounds would be derived from the set membership.
Here, I'm forced to use a dependent type for the index, and then convert it to Finset.attach and back, which makes the proof more complicated.
I like how using Fin index automatically derives the boundary proof, but Fin ranges from 0, which is not the case here.

import Mathlib

open BigOperators Finset

variable (i: ℕ)(xs: Array ℤ)
example (h₁: i < xs.size)
 : xs[i] + ∑i : Ico (i+1) xs.size, xs[i.1]'(by aesop) = ∑i : Ico i xs.size, xs[i.1]'(by aesop)
 := calc xs[i] + ∑i : Ico (i+1) xs.size, xs[i.1]'(by aesop)
    _ = ∑i : Ico i xs.size, xs[i.1]'(by aesop) := by simp_rw[univ_eq_attach, sum_attach (Ico (i+1) xs.size) (xs[·]'sorry)]
                                                     rw [←Finset.sum_eq_sum_Ico_succ_bot _ (xs[·]'sorry)];
                                                     rw [sum_attach (Ico i xs.size) (xs[·]'sorry)];
                                                     assumption

[Daniel Weber]

Perhaps you can make a set of Fin xs.size?

[Vlad]

Unfortunately, that only works for indices starting from 0.

[Vlad]

Here's another attempt at this (if I understood the suggestion right)

variable (xs: Array ℤ)
#check ((Ico 0 xs.size): Finset (Fin xs.size))

This results in an error:

failed to synthesize instance
  OfNat (Fin (Array.size xs)) 0

Any Nat literal coercion (like in ∑i : Ico (i+1) xs.size) will trigger this error.

[Ruben Van de Velde]

Isn't that just Finset.univ?

[Vlad]

Not sure I understand. Could you show how to use Finset.univ in the first example?

[Vlad]

My goal is to remove (by aesop) and sorry in all instances, including rw applications. It would be great if Lean could derive those proofs automatically or at least make them as side goals instead of proving them "in-line".

[Ruben Van de Velde]

I was only looking at your latest message. Maybe this is a start for your first question:

import Mathlib

open BigOperators Finset

variable (xs : Array ℤ)
example (i : Fin (xs.size)) :
    xs.get i + ∑ j in Ioi i, xs.get j = ∑ j in Ici i, xs.get j := by
  sorry

[Ruben Van de Velde]

(and then the proof is add_sum_Ioi_eq_sum_Ici ..)

[A.]

The docs say

From the point of view of proofs Array α is just a wrapper around List α.

Doesn't that suggest that this sort of work might better be carried out on the underlying list?

[Vlad]

Thank you @Ruben Van de Velde. While your example is equivalent to my problem, it's less applicable for my use case. I'm using Lean for program refinement, which requires a series of transformation of the original boolean expression.
In this context, I need to handle expressions in their original form regardless of their structure. For instance, if the expression includes a quantifier with range Ico 0 n, and the transformation increments n, then I would like to preserve the original Ico construct at least in the initial transformation step. I hope this clarifies my situation.

As a separate question for my own understanding, why does replacing xs.get with square brackets in your example require proof of index boundaries?

[Vlad]

@Alistair Tucker Just tried replacing Array with List, no significant difference. Index bounds proofs still needed.

[Yaël Dillies]

Alistair Tucker said:

The docs say

From the point of view of proofs Array α is just a wrapper around List α.

Doesn't that suggest that this sort of work might better be carried out on the underlying list?

The Array vs List difference is completely orthogonal to Vlad's issue

[A.]

Obviously I meant to suggest that he might not face that particular issue if he were able to reformulate the problem. Am I wrong?

[Yaël Dillies]

I believe so, yes. The List API uses the same mechanisms to check indices are in-bound

[A.]

Working with lists it is not so natural to use indices at all.

[Vlad]

Thanks for the suggestion, Alistair. Now I understand better what you mean. Unfortunately, I do need to use indexed access for my problem.