feat: rename get_elem_tactic_trivial to get_elem_tactic_extensible

Author: kim-em

src/Init/Data/Range/Basic.lean

@@ -84,5 +84,8 @@ theorem Membership.mem.step {i : Nat} {r : Std.Range} (h : i ∈ r) : (i - r.sta
 theorem Membership.get_elem_helper {i n : Nat} {r : Std.Range} (h₁ : i ∈ r) (h₂ : r.stop = n) :
     i < n := h₂ ▸ h₁.2.1
 
+macro_rules
+  | `(tactic| get_elem_tactic_extensible) => `(tactic| apply Membership.get_elem_helper; assumption; rfl)
+
 macro_rules
   | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Membership.get_elem_helper; assumption; rfl)

src/Init/GetElem.lean

@@ -47,7 +47,7 @@ proof in the context using `have`, because `get_elem_tactic` tries
 
 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`.
+`get_elem_tactic_extensible` using `macro_rules`.
 
 `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
@@ -280,6 +280,9 @@ instance [GetElem? cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
 
 @[simp, grind =] theorem getElem!_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) [Inhabited Elem] : a[i]! = a[i.1]! := rfl
 
+macro_rules
+  | `(tactic| get_elem_tactic_extensible) => `(tactic| (with_reducible apply Fin.val_lt_of_le); get_elem_tactic_extensible; done)
+
 macro_rules
   | `(tactic| get_elem_tactic_trivial) => `(tactic| (with_reducible apply Fin.val_lt_of_le); get_elem_tactic_trivial; done)
 

src/Init/Tactics.lean

@@ -1917,30 +1917,37 @@ syntax "‹" withoutPosition(term) "›" : term
 macro_rules | `(‹$type›) => `((by assumption : $type))
 
 /--
-`get_elem_tactic_trivial` is an extensible tactic automatically called
+`get_elem_tactic_extensible` is an extensible tactic automatically called
 by the notation `arr[i]` to prove any side conditions that arise when
 constructing the term (e.g. the index is in bounds of the array).
-The default behavior is to just try `trivial` (which handles the case
-where `i < arr.size` is in the context) and `simp +arith` and `omega`
+The default behavior is to try `simp +arith` and `omega`
 (for doing linear arithmetic in the index).
+
+(Note that the core tactic `get_elem_tactic` has already tried
+`done` and `assumption` before the extensible tactic is called.)
 -/
+syntax "get_elem_tactic_extensible" : tactic
+
+/-- `get_elem_tactic_trivial` has been deprecated in favour of `get_elem_tactic_extensible`. -/
 syntax "get_elem_tactic_trivial" : tactic
 
+macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| omega)
+macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| simp +arith; done)
+
 macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| omega)
 macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp +arith; done)
-macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| trivial)
 
 /--
 `get_elem_tactic` is the tactic automatically called by the notation `arr[i]`
 to prove any side conditions that arise when constructing the term
 (e.g. the index is in bounds of the array). It just delegates to
-`get_elem_tactic_trivial` and gives a diagnostic error message otherwise;
-users are encouraged to extend `get_elem_tactic_trivial` instead of this tactic.
+`get_elem_tactic_extensible` and gives a diagnostic error message otherwise;
+users are encouraged to extend `get_elem_tactic_extensible` instead of this tactic.
 -/
 macro "get_elem_tactic" : tactic =>
   `(tactic| first
       /-
-      Recall that `macro_rules` (namely, for `get_elem_tactic_trivial`) are tried in reverse order.
+      Recall that `macro_rules` (namely, for `get_elem_tactic_extensible`) are tried in reverse order.
       We first, however, try `done`, since the necessary proof may already have been
       found during unification, in which case there is no goal to solve (see #6999).
       If a goal is present, we want `assumption` to be tried first.
@@ -1953,15 +1960,15 @@ macro "get_elem_tactic" : tactic =>
       If `omega` is used to "fill" this proof, we will have a more complex proof term that
       cannot be inferred by unification.
       We hardcoded `assumption` here to ensure users cannot accidentally break this IF
-      they add new `macro_rules` for `get_elem_tactic_trivial`.
+      they add new `macro_rules` for `get_elem_tactic_extensible`.
 
       TODO: Implement priorities for `macro_rules`.
-      TODO: Ensure we have **high-priority** macro_rules for `get_elem_tactic_trivial` which are
+      TODO: Ensure we have **high-priority** macro_rules for `get_elem_tactic_extensible` which are
             just `done` and `assumption`.
       -/
     | done
     | assumption
-    | get_elem_tactic_trivial
+    | get_elem_tactic_extensible
     | fail "failed to prove index is valid, possible solutions:
   - Use `have`-expressions to prove the index is valid
   - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid

src/Lean/Elab/Tactic.lean

@@ -51,3 +51,6 @@ import Lean.Elab.Tactic.TreeTacAttr
 import Lean.Elab.Tactic.ExposeNames
 import Lean.Elab.Tactic.SimpArith
 import Lean.Elab.Tactic.Lets
+
+elab "get_elem_tactic_trivial" : tactic => do
+  throwError "`get_elem_tactic_trivial` has been renamed to `get_elem_tactic_extensible`"

tests/lean/run/grind_heapsort.lean

@@ -4,7 +4,7 @@ set_option grind.warning false
 /-
 Use `grind` as one of the tactics for array-element access and termination proofs.
 -/
-macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| grind)
+macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| grind)
 /-
 Note: We disable model-based theory combination (-mbtc) here because `grind` can
 exhaust heartbeats when exploring certain "bad" termination checker scenarios.