Applying add iSup lemmas

Stream: Is there code for X?

[Vlad]

Is there a relevant lemma that could be helpful in proving example below? I found lemmas about supremum of an (bounded) indexed family in the Real, Language, and Cardinality packages, but I haven't been able to connect them directly to this problem.

import Lean
import Mathlib.Tactic
open Lean Finset Algebra

example {i : ℕ} {xs: Array ℤ}
  (h0: 0 < i)
  (hi: i < xs.size)
  := calc xs[i] + (⨆ a ∈ range i, xs[a]'sorry)
        _ = ⨆ a ∈ range i, (xs[i] + xs[a]'sorry)   := sorry -- by rw [add_ciSup]

[Yury G. Kudryashov]

What do you want to prove?

[Yury G. Kudryashov]

Since you're talking about a finite iSup, you may want to use docs#Finset.sup' with s = (Finset.univ : Finset (Fin i))

[Yury G. Kudryashov]

If you want to use docs#iSup, then what's wrong with docs#add_ciSup ?

[Eric Wieser]

Your code above has a syntax error when I try to run it

[Eric Wieser]

Yury G. Kudryashov said:

If you want to use docs#iSup, then what's wrong with docs#add_ciSup ?

#12113 is one problem with it

[Vlad]

@Yury G. Kudryashov perhaps there's a way to make add_ciSup work, but when I apply it as a rewrite rule (as in the commented section), then the goal changes to
⊢ ⨆ i_1, xs[i] + ⨆ (_ : i_1 ∈ range i), xs[i_1] = ⨆ a ∈ range i, xs[i] + xs[a]
which is not the same as the RHS.

This is the kind of transformations I often deal with when solving programming problems (e.g. finding min/max of segment/pairs of elements of an array etc.).
I would appreciate if someone could show how apply iSup lemmas for the example above just as a learning exercise.

[Eric Wieser]

You need to apply the lemma twice, but unfortunately you need the correction from #12113 first

[Eric Wieser]

Using ⨆ a : Fin i, instead should fix that, and will make your sorrys easier

[Vlad]

Thank you @Eric Wieser!

[Vlad]

I'm still missing something. Here's a revised example

import Lean
import Mathlib.Tactic
open Lean Finset Algebra

example {i : ℕ} {xs: Array ℤ}
  (h0: 0 < i)
  (hi: i < xs.size)
  := calc xs[i] + (⨆ a: Fin i, xs[a])
        _ = ⨆ a: Fin i, (xs[i] + xs[a])   := by rw [add_ciSup]; sorry;  existsi 0; exact h0

which results in error

failed to synthesize instance
  Nonempty (Fin i)

[Edward van de Meent]

@loogle Nonempty (Fin ?i)

[loogle]

:search: Fin.size_pos', Fin.pos_iff_nonempty, and 1 more

[Edward van de Meent]

you can supply the instance manually using docs#Fin.pos_iff_nonempty

[Vlad]

That's a nice trick with loogle. Thanks!

[Matt Diamond]

on a side note, how does that syntax work? is the type of the example implicit? a def with an implicit return type makes sense to me, but a proof with an implicit return type is confusing... like your goal is to just prove anything

[Eric Wieser]

The secret is that example is really a def