feat: remove Decidable instances from GetElem

[kim-em]

No description provided.

[david-christiansen]

Isn't this a sign that the instance doesn't quite make sense here? I'd expect there to be an Elem predicate, and that the result of getElem would not be an Option.

[david-christiansen]

(I get the pragmatic reason why we don't have that right now, of course)

[kim-em]

Yes, @TwoFX will replace this with something more sensible in the big HashMap refactor.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-4560 build failed against this PR. (2024-06-25 12:00:22) View Log
• 💥 Mathlib branch lean-pr-testing-4560 build failed against this PR. (2024-06-25 12:52:42) View Log
• 💥 Mathlib branch lean-pr-testing-4560 build failed against this PR. (2024-06-25 23:41:47) View Log
• 🟡 Mathlib branch lean-pr-testing-4560 build this PR didn't complete normally. (2024-06-25 23:44:49) View Log
• 🟡 Mathlib branch lean-pr-testing-4560 build against this PR was cancelled. (2024-06-26 00:14:07) View Log
• ✅ Mathlib branch lean-pr-testing-4560 has successfully built against this PR. (2024-06-26 01:07:03) View Log
• ✅ Mathlib branch lean-pr-testing-4560 has successfully built against this PR. (2024-06-26 06:21:08) View Log
• 💥 Mathlib branch lean-pr-testing-4560 build failed against this PR. (2024-06-26 07:28:17) View Log

[david-christiansen]

Unfortunately, it doesn't seem to let me leave suggestions for lines that weren't changed. But here's a suggestion for an updated docstring to match the code better:

The class `GetElem coll idx elem valid` implements lookup notation,
specifically `xs[i]`, `xs[i]?`, `xs[i]!`, and `xs[i]'p`.

The types `coll`, `idx`, and `elem` are the collection, the index, and the
element types. A single collection may support lookups with multiple index
types. The relation `valid` determines when the index is guaranteed to be
valid; lookups of valid indices are guaranteed not to fail.

For example, an instance for arrays looks like
`GetElem (Array α) Nat α (fun xs i => i < xs.size)`. In other words, given an
array `xs` and a natural number `i`, `xs[i]` will return an `α` when `valid xs i`
holds, which is true when `i` is less than the size of the array. `Array`
additionally supports indexing with `USize`. Because the bounds are
checked at compile time, no runtime check is required.

Given `xs[i]` with `xs : coll` and `i : idx`, Lean looks for an instance of
`GetElem coll idx elem valid` and uses this to infer the type of the return
value `elem` and side conditions `valid` required to ensure `xs[i]` yields
a valid value of type `elem`. The tactic `get_elem_tactic` is
invoked to prove validity automatically. The `xs[i]'p` notation uses the
proof `p` to satisfy the validity condition, but it is often easier to place the
proof in the context using `have`, because `get_elem_tactic` tries
`assumption`.

`xs[i]?` and `xs[i]!` do not impose a proof obligation; the former returns
an `Option elem`, with `none` signalling that the value isn't present, and
the latter returns `elem` but panics if the value isn't there, returning
`default : elem` based on the `Inhabited elem` instance.

The proof side-condition `valid xs i` is automatically dispatched by the
`get_elem_tactic` tactic; this tactic can be extended by adding more clauses to
`get_elem_tactic_trivial` using `macro_rules`.

Important instances include:
  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
    indexing with no bounds check and a proof side goal `i < arr.size`.
  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
    side goal `i < l.length`.
  * `stx[i] : Syntax` where `stx : Syntax` and `i : Nat`: get a syntax argument,
    no side goal (returns `.missing` out of range)

-/
class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
              (valid : outParam (coll → idx → Prop)) where
  /--
  The syntax `arr[i]` gets the `i`'th element of the collection `arr`. If there
  are proof side conditions to the application, they will be automatically
  inferred by the `get_elem_tactic` tactic.
  -/

What do you think?

[nomeata]

Good! Should we exclude Syntax from the docstring? The docstring is most useful to relative beginners of Lean, and I expect they are confused or at least distracted by meta-programming concepts. We can hopefully add HashMap instead soon!

[david-christiansen]

I agree!

[kim-em]

Thanks, I've adopted the doc-string, with a few minor changes.

[kim-em]

An outstanding issue here is that we no longer provide default implementations of getElem? and getElem!, adding to the implementation burden when creating GetElem instances.

@TwoFX wrote elsewhere:

It would be really cool if we could provide the class as

class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
              (valid : outParam (coll → idx → Prop)) where
  getElem (xs : coll) (i : idx) (h : valid xs i) : elem

  getElem? : coll → idx → Option elem := by
    exact fun xs i => if h : _ then some (getElem xs i h) else none

  getElem! [Inhabited elem] (xs : coll) (i : idx) : elem :=
    match getElem? xs i with | some e => e | none => outOfBounds

with the intention to defer elaboration until a user provides an instance that omits getElem? so that the elaborator can figure out the correct decidable instance at that time. This almost works, the only problem is that in the tactic block for getElem? the elaborator takes getElem to mean GetElem.getElem instead of the getElem above and then fails to synthesize the very instance we're currently defining. Can we fix this?

I propose that we merge as is for now, but keep thinking if there's a clever trick here.

Getting these Decidable instances out of the lookup functions is a big win.

[tydeu]

Below are a few GetElem instances that can be removed because of getElemOfDecidable which I imagine just slipped through.

[kim-em]

Below are a few GetElem instances that can be removed because of getElemOfDecidable which I imagine just slipped through.

The rename had already happened, so these are actually the ones that are needed!

[TwoFX]

LGTM!

[tydeu]

Looks great to me as well!