feat: let get_elem_tactic_trivial handle [a]'h.2

[nomeata]

The pattern

    for h : i in [:xs.size] do
      let x := xs[i]'h.2

is occassionally useful to iterate over an array with the index in
hand. This PR extends the get_elem_tactic_trivial so that one can
simply write

    for h : i in [:xs.size] do
      let x := xs[i]

fixes #3032.

[nomeata]

Hmm, the tactic

exact Membership.mem.upper (by assumption)

I wrote doesn’t work as well as I thought; the by assumption can pick the wrong one. #mwe:

macro_rules
  | `(tactic| get_elem_tactic_trivial) => `(tactic| exact Membership.mem.upper (by assumption))


def withTwoRanges (xs : Array Nat) : Option Nat := Id.run do
  for h1 : i in [:xs.size] do
    for h2 : j in [i + 1:xs.size] do
      if xs[i] == xs[j] then
        return i
  return none

Is it possible to say “apply Membership.mem.upper with the assumption that fits”? Or does that need something like solveByElim?

NB: Simply apply fails with

tactic 'apply' failed, failed to unify
  ?i < ?r.stop
with
  i < size a

[leodemoura]

@nomeata What about the following?

theorem helper {r : Std.Range} (h₁ : i ∈ r) (h₂ : r.stop = n) : i < n := by
  have := h₁.2
  rw [h₂] at this
  assumption

macro_rules
  | `(tactic| get_elem_tactic_trivial) => `(tactic| apply helper; assumption; rfl)

def withTwoRanges (xs : Array Nat) : Option Nat := Id.run do
  for h1 : i in [:xs.size] do
    for h2 : j in [i + 1:xs.size] do
      if xs[i] == xs[j] then
        return i
  return none

BTW, we will be working on better automation this year.

[nomeata]

I thought about something in that direction, good to know that it was a reasonable direction :-)

[leanprover-community-mathlib4-bot]

• ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-12-31' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2024-01-03 13:04:14)