From 8182f83929df4bcafe0558f69eb2d96dab2b79cc Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 16 Aug 2022 22:49:42 -0400 Subject: [PATCH] doc: documentation for Init.Tactics --- src/Init/Prelude.lean | 21 +- src/Init/Tactics.lean | 559 +++++++++++++----- tests/lean/interactive/1403.lean.expected.out | 2 +- 3 files changed, 425 insertions(+), 157 deletions(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 1052fcb67e..1e77419d6e 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -2414,7 +2414,26 @@ The proof side-condition `dom xs i` is automatically dispatched by the `get_elem_tactic_trivial`. -/ class GetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) where - /-- The implementation of `xs[i]`. `h` is discharged by `get_elem_tactic`. -/ + /-- + 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. + + The actual behavior of this class is type-dependent, + but here are some important implementations: + * `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) + + There are other variations on this syntax: + * `arr[i]`: proves the proof side goal by `get_elem_tactic` + * `arr[i]!`: panics if the side goal is false + * `arr[i]?`: returns `none` if the side goal is false + * `arr[i]'h`: uses `h` to prove the side goal + -/ getElem (xs : cont) (i : idx) (h : dom xs i) : elem export GetElem (getElem) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 4936ab13fd..90b95e458f 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -1,25 +1,37 @@ /- Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura +Authors: Leonardo de Moura, Mario Carneiro -/ prelude import Init.Notation +set_option linter.missingDocs true -- keep it documented namespace Lean +/-- +`binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding +position, where `_` means that the value should be left unnamed and inaccessible. +-/ syntax binderIdent := ident <|> hole namespace Parser.Tactic -/-- `with_annotate_state stx t` annotates the lexical range of `stx : Syntax` with the initial and final state of running tactic `t`. -/ -scoped syntax (name := withAnnotateState) "with_annotate_state " rawStx ppSpace tactic : tactic +/-- +`with_annotate_state stx t` annotates the lexical range of `stx : Syntax` with +the initial and final state of running tactic `t`. +-/ +scoped syntax (name := withAnnotateState) + "with_annotate_state " rawStx ppSpace tactic : tactic /-- -Introduce one or more hypotheses, optionally naming and/or pattern-matching them. -For each hypothesis to be introduced, the remaining main goal's target type must be a `let` or function type. -* `intro` by itself introduces one anonymous hypothesis, which can be accessed by e.g. `assumption`. -* `intro x y` introduces two hypotheses and names them. Individual hypotheses can be anonymized via `_`, - or matched against a pattern: +Introduces one or more hypotheses, optionally naming and/or pattern-matching them. +For each hypothesis to be introduced, the remaining main goal's target type must +be a `let` or function type. + +* `intro` by itself introduces one anonymous hypothesis, which can be accessed + by e.g. `assumption`. +* `intro x y` introduces two hypotheses and names them. Individual hypotheses + can be anonymized via `_`, or matched against a pattern: ```lean -- ... ⊢ α × β → ... intro (a, b) @@ -33,29 +45,49 @@ For each hypothesis to be introduced, the remaining main goal's target type must ``` -/ syntax (name := intro) "intro " notFollowedBy("|") (colGt term:max)* : tactic -/-- `intros x...` behaves like `intro x...`, but then keeps introducing (anonymous) hypotheses until goal is not of a function type. -/ + +/-- +`intros x...` behaves like `intro x...`, but then keeps introducing (anonymous) +hypotheses until goal is not of a function type. +-/ syntax (name := intros) "intros " (colGt (ident <|> hole))* : tactic + /-- -`rename t => x` renames the most recent hypothesis whose type matches `t` (which may contain placeholders) to `x`, -or fails if no such hypothesis could be found. -/ +`rename t => x` renames the most recent hypothesis whose type matches `t` +(which may contain placeholders) to `x`, or fails if no such hypothesis could be found. +-/ syntax (name := rename) "rename " term " => " ident : tactic -/-- `revert x...` is the inverse of `intro x...`: it moves the given hypotheses into the main goal's target type. -/ + +/-- +`revert x...` is the inverse of `intro x...`: it moves the given hypotheses +into the main goal's target type. +-/ syntax (name := revert) "revert " (colGt term:max)+ : tactic -/-- `clear x...` removes the given hypotheses, or fails if there are remaining references to a hypothesis. -/ + +/-- +`clear x...` removes the given hypotheses, or fails if there are remaining +references to a hypothesis. +-/ syntax (name := clear) "clear " (colGt term:max)+ : tactic + /-- -`subst x...` substitutes each `x` with `e` in the goal if there is a hypothesis of type `x = e` or `e = x`. -If `x` is itself a hypothesis of type `y = e` or `e = y`, `y` is substituted instead. -/ +`subst x...` substitutes each `x` with `e` in the goal if there is a hypothesis +of type `x = e` or `e = x`. +If `x` is itself a hypothesis of type `y = e` or `e = y`, `y` is substituted instead. +-/ syntax (name := subst) "subst " (colGt term:max)+ : tactic + /-- -Apply `subst` to all hypotheses of the form `h : x = t` or `h : t = x`. +Applies `subst` to all hypotheses of the form `h : x = t` or `h : t = x`. -/ syntax (name := substVars) "subst_vars" : tactic /-- `assumption` tries to solve the main goal using a hypothesis of compatible type, or else fails. -Note also the `‹t›` term notation, which is a shorthand for `show t by assumption`. -/ +Note also the `‹t›` term notation, which is a shorthand for `show t by assumption`. +-/ syntax (name := assumption) "assumption" : tactic + /-- `contradiction` closes the main goal if its hypotheses are "trivially contradictory". - Inductive type/family with no applicable constructors @@ -80,87 +112,142 @@ example (x : Nat) (h : x ≠ x) : p := by contradiction ``` -/ syntax (name := contradiction) "contradiction" : tactic + /-- `apply e` tries to match the current goal against the conclusion of `e`'s type. If it succeeds, then the tactic returns as many subgoals as the number of premises that have not been fixed by type inference or type class resolution. Non-dependent premises are added before dependent ones. -The `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types. +The `apply` tactic uses higher-order pattern matching, type class resolution, +and first-order unification with dependent types. -/ syntax (name := apply) "apply " term : tactic + /-- `exact e` closes the main goal if its target type matches that of `e`. -/ syntax (name := exact) "exact " term : tactic + /-- -`refine e` behaves like `exact e`, except that named (`?x`) or unnamed (`?_`) holes in `e` that are not solved -by unification with the main goal's target type are converted into new goals, using the hole's name, if any, as the goal case name. +`refine e` behaves like `exact e`, except that named (`?x`) or unnamed (`?_`) +holes in `e` that are not solved by unification with the main goal's target type +are converted into new goals, using the hole's name, if any, as the goal case name. -/ syntax (name := refine) "refine " term : tactic -/-- `refine' e` behaves like `refine e`, except that unsolved placeholders (`_`) and implicit parameters are also converted into new goals. -/ -syntax (name := refine') "refine' " term : tactic -/-- If the main goal's target type is an inductive type, `constructor` solves it with the first matching constructor, or else fails. -/ -syntax (name := constructor) "constructor" : tactic + /-- -`case tag => tac` focuses on the goal with case name `tag` and solves it using `tac`, or else fails. -`case tag x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with inaccessible names to the given names. -/ +`refine' e` behaves like `refine e`, except that unsolved placeholders (`_`) +and implicit parameters are also converted into new goals. +-/ +syntax (name := refine') "refine' " term : tactic + +/-- +If the main goal's target type is an inductive type, `constructor` solves it with +the first matching constructor, or else fails. +-/ +syntax (name := constructor) "constructor" : tactic + +/-- +* `case tag => tac` focuses on the goal with case name `tag` and solves it using `tac`, + or else fails. +* `case tag x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses + with inaccessible names to the given names. +-/ syntax (name := case) "case " binderIdent binderIdent* " => " tacticSeq : tactic /-- -`case'` is similar to the `case tag => tac` tactic, but does not ensure the goal has been solved after applying `tac`, nor -admits the goal if `tac` failed. Recall that `case` closes the goal using `sorry` when `tac` fails, and +`case'` is similar to the `case tag => tac` tactic, but does not ensure the goal +has been solved after applying `tac`, nor admits the goal if `tac` failed. +Recall that `case` closes the goal using `sorry` when `tac` fails, and the tactic execution is not interrupted. -/ syntax (name := case') "case' " binderIdent binderIdent* " => " tacticSeq : tactic /-- -`next => tac` focuses on the next goal solves it using `tac`, or else fails. -`next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with inaccessible names to the given names. -/ +`next => tac` focuses on the next goal and solves it using `tac`, or else fails. +`next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with +inaccessible names to the given names. +-/ macro "next " args:binderIdent* " => " tac:tacticSeq : tactic => `(tactic| case _ $args* => $tac) /-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/ syntax (name := allGoals) "all_goals " tacticSeq : tactic -/-- `any_goals tac` applies the tactic `tac` to every goal, and succeeds if at least one application succeeds. -/ + +/-- +`any_goals tac` applies the tactic `tac` to every goal, and succeeds if at +least one application succeeds. +-/ syntax (name := anyGoals) "any_goals " tacticSeq : tactic + /-- `focus tac` focuses on the main goal, suppressing all other goals, and runs `tac` on it. -Usually `· tac`, which enforces that the goal is closed by `tac`, should be preferred. -/ +Usually `· tac`, which enforces that the goal is closed by `tac`, should be preferred. +-/ syntax (name := focus) "focus " tacticSeq : tactic + /-- `skip` does nothing. -/ syntax (name := skip) "skip" : tactic + /-- `done` succeeds iff there are no remaining goals. -/ syntax (name := done) "done" : tactic + /-- `trace_state` displays the current state in the info view. -/ syntax (name := traceState) "trace_state" : tactic + /-- `trace msg` displays `msg` in the info view. -/ syntax (name := traceMessage) "trace " str : tactic + /-- `fail_if_success t` fails if the tactic `t` succeeds. -/ syntax (name := failIfSuccess) "fail_if_success " tacticSeq : tactic -/-- `(tacs)` executes a list of tactics in sequence, without requiring that + +/-- +`(tacs)` executes a list of tactics in sequence, without requiring that the goal be closed at the end like `· tacs`. Like `by` itself, the tactics -can be either separated by newlines or `;`. -/ +can be either separated by newlines or `;`. +-/ syntax (name := paren) "(" tacticSeq ")" : tactic -/-- `with_reducible tacs` excutes `tacs` using the reducible transparency setting. -In this setting only definitions tagged as `[reducible]` are unfolded. -/ + +/-- +`with_reducible tacs` excutes `tacs` using the reducible transparency setting. +In this setting only definitions tagged as `[reducible]` are unfolded. +-/ syntax (name := withReducible) "with_reducible " tacticSeq : tactic -/-- `with_reducible_and_instances tacs` excutes `tacs` using the `.instances` transparency setting. -In this setting only definitions tagged as `[reducible]` or type class instances are unfolded. -/ + +/-- +`with_reducible_and_instances tacs` excutes `tacs` using the `.instances` transparency setting. +In this setting only definitions tagged as `[reducible]` or type class instances are unfolded. +-/ syntax (name := withReducibleAndInstances) "with_reducible_and_instances " tacticSeq : tactic -/-- `with_unfolding_all tacs` excutes `tacs` using the `.all` transparency setting. -In this setting all definitions that are not opaque are unfolded. -/ + +/-- +`with_unfolding_all tacs` excutes `tacs` using the `.all` transparency setting. +In this setting all definitions that are not opaque are unfolded. +-/ syntax (name := withUnfoldingAll) "with_unfolding_all " tacticSeq : tactic + /-- `first | tac | ...` runs each `tac` until one succeeds, or else fails. -/ syntax (name := first) "first " withPosition((colGe "|" tacticSeq)+) : tactic -/-- `rotate_left n` rotates goals to the left by `n`. That is, `rotate_left 1` + +/-- +`rotate_left n` rotates goals to the left by `n`. That is, `rotate_left 1` takes the main goal and puts it to the back of the subgoal list. -If `n` is omitted, it defaults to `1`. -/ +If `n` is omitted, it defaults to `1`. +-/ syntax (name := rotateLeft) "rotate_left" (num)? : tactic -/-- Rotate the goals to the right by `n`. That is, take the goal at the back -and push it to the front `n` times. If `n` is omitted, it defaults to `1`. -/ + +/-- +Rotate the goals to the right by `n`. That is, take the goal at the back +and push it to the front `n` times. If `n` is omitted, it defaults to `1`. +-/ syntax (name := rotateRight) "rotate_right" (num)? : tactic + /-- `try tac` runs `tac` and succeeds even if `tac` failed. -/ macro "try " t:tacticSeq : tactic => `(first | $t | skip) -/-- `tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal, concatenating all goals produced by `tac'`. -/ + +/-- +`tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal, +concatenating all goals produced by `tac'`. +-/ macro:1 x:tactic tk:" <;> " y:tactic:0 : tactic => `(tactic| focus $x:tactic @@ -179,11 +266,13 @@ for new reflexive relations. macro "rfl" : tactic => `(eq_refl) /-- - `rfl'` is similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions, - theorems included (relevant for declarations defined by well-founded recursion). -/ +`rfl'` is similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions, +theorems included (relevant for declarations defined by well-founded recursion). +-/ macro "rfl'" : tactic => `(set_option smartUnfolding false in with_unfolding_all rfl) -/-- `ac_rfl` proves equalities up to application of an associative and commutative operator. +/-- +`ac_rfl` proves equalities up to application of an associative and commutative operator. ``` instance : IsAssociative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩ instance : IsCommutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩ @@ -193,19 +282,46 @@ example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by ac_rfl -/ syntax (name := acRfl) "ac_rfl" : tactic +/-- +The `sorry` tactic closes the goal using `sorryAx`. This is intended for stubbing out incomplete +parts of a proof while still having a syntactically correct proof skeleton. Lean will give +a warning whenever a proof uses `sorry`, so you aren't likely to miss it, but +you can double check if a theorem depends on `sorry` by using +`#print axioms my_thm` and looking for `sorryAx` in the axiom list. +-/ +macro "sorry" : tactic => `(exact @sorryAx _ false) + /-- `admit` is a shorthand for `exact sorry`. -/ macro "admit" : tactic => `(exact @sorryAx _ false) -/-- The `sorry` tactic is a shorthand for `exact sorry`. -/ -macro "sorry" : tactic => `(exact @sorryAx _ false) -/-- `infer_instance` is an abbreviation for `exact inferInstance` -/ + +/-- +`infer_instance` is an abbreviation for `exact inferInstance`. +It synthesizes a value of any target type by typeclass inference. +-/ macro "infer_instance" : tactic => `(exact inferInstance) /-- Optional configuration option for tactics -/ syntax config := atomic("(" &"config") " := " term ")" +/-- The `*` location refers to all hypotheses and the goal. -/ syntax locationWildcard := "*" -syntax locationHyp := (colGt term:max)+ ("⊢" <|> "|-")? -syntax location := withPosition(" at " (locationWildcard <|> locationHyp)) + +/-- +A hypothesis location specification consists of 1 or more hypothesis references +and optionally `⊢` denoting the goal. +-/ +syntax locationHyp := (colGt term:max)+ ("⊢" <|> "|-")? + +/-- +Location specifications are used by many tactics that can operate on either the +hypotheses or the goal. It can have one of the forms: +* 'empty' is not actually present in this syntax, but most tactics use + `(location)?` matchers. It means to target the goal only. +* `at h₁ ... hₙ`: target the hypotheses `h₁`, ..., `hₙ` +* `at h₁ h₂ ⊢`: target the hypotheses `h₁` and `h₂`, and the goal +* `at *`: target all hypotheses and the goal +-/ +syntax location := withPosition(" at " (locationWildcard <|> locationHyp)) /-- * `change tgt'` will change the goal from `tgt` to `tgt'`, @@ -222,15 +338,24 @@ syntax (name := change) "change " term (location)? : tactic -/ syntax (name := changeWith) "change " term " with " term (location)? : tactic +/-- +If `thm` is a theorem `a = b`, then as a rewrite rule, +* `thm` means to replace `a` with `b`, and +* `← thm` means to replace `b` with `a`. +-/ syntax rwRule := ("← " <|> "<- ")? term +/-- A `rwRuleSeq` is a list of `rwRule` in brackets. -/ syntax rwRuleSeq := "[" rwRule,*,? "]" /-- `rewrite [e]` applies identity `e` as a rewrite rule to the target of the main goal. If `e` is preceded by left arrow (`←` or `<-`), the rewrite is applied in the reverse direction. -If `e` is a defined constant, then the equational theorems associated with `e` are used. This provides a convenient way to unfold `e`. +If `e` is a defined constant, then the equational theorems associated with `e` are used. +This provides a convenient way to unfold `e`. - `rewrite [e₁, ..., eₙ]` applies the given rules sequentially. -- `rewrite [e] at l` rewrites `e` at location(s) `l`, where `l` is either `*` or a list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-` can also be used, to signify the target of the goal. +- `rewrite [e] at l` rewrites `e` at location(s) `l`, where `l` is either `*` or a + list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-` + can also be used, to signify the target of the goal. -/ syntax (name := rewriteSeq) "rewrite " (config)? rwRuleSeq (location)? : tactic @@ -245,12 +370,16 @@ macro (name := rwSeq) "rw " c:(config)? s:rwRuleSeq l:(location)? : tactic => | _ => Macro.throwUnsupported /-- -The `injection` tactic is based on the fact that constructors of inductive data types are injections. -That means that if `c` is a constructor of an inductive datatype, and if `(c t₁)` and `(c t₂)` are two terms that are equal then `t₁` and `t₂` are equal too. -If `q` is a proof of a statement of conclusion `t₁ = t₂`, then injection applies injectivity to derive the equality of all arguments of `t₁` and `t₂` -placed in the same positions. For example, from `(a::b) = (c::d)` we derive `a=c` and `b=d`. To use this tactic `t₁` and `t₂` -should be constructor applications of the same constructor. -Given `h : a::b = c::d`, the tactic `injection h` adds two new hypothesis with types `a = c` and `b = d` to the main goal. +The `injection` tactic is based on the fact that constructors of inductive data +types are injections. +That means that if `c` is a constructor of an inductive datatype, and if `(c t₁)` +and `(c t₂)` are two terms that are equal then `t₁` and `t₂` are equal too. +If `q` is a proof of a statement of conclusion `t₁ = t₂`, then injection applies +injectivity to derive the equality of all arguments of `t₁` and `t₂` placed in +the same positions. For example, from `(a::b) = (c::d)` we derive `a=c` and `b=d`. +To use this tactic `t₁` and `t₂` should be constructor applications of the same constructor. +Given `h : a::b = c::d`, the tactic `injection h` adds two new hypothesis with types +`a = c` and `b = d` to the main goal. The tactic `injection h with h₁ h₂` uses the names `h₁` and `h₂` to name the new hypotheses. -/ syntax (name := injection) "injection " term (" with " (colGt (ident <|> hole))+)? : tactic @@ -261,62 +390,100 @@ constructor equalities like `(a::b::c) = (d::e::f)`. -/ -- TODO: add with syntax (name := injections) "injections" : tactic +/-- +The discharger clause of `simp` and related tactics. +This is a tactic used to discharge the side conditions on conditional rewrite rules. +-/ syntax discharger := atomic("(" (&"discharger" <|> &"disch")) " := " tacticSeq ")" +/-- Use this rewrite rule before entering the subterms -/ syntax simpPre := "↓" +/-- Use this rewrite rule after entering the subterms -/ syntax simpPost := "↑" +/-- +A simp lemma specification is: +* optional `↑` or `↓` to specify use before or after entering the subterm +* optional `←` to use the lemma backward +* `thm` for the theorem to rewrite with +-/ syntax simpLemma := (simpPre <|> simpPost)? ("← " <|> "<- ")? term +/-- An erasure specification `-thm` says to remove `thm` from the simp set -/ syntax simpErase := "-" term:max +/-- The simp lemma specification `*` means to rewrite with all hypotheses -/ syntax simpStar := "*" /-- -The `simp` tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses. It has many variants. +The `simp` tactic uses lemmas and hypotheses to simplify the main goal target or +non-dependent hypotheses. It has many variants: - `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`. -- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions. If an `hᵢ` is a defined constant `f`, then the equational lemmas associated with `f` are used. This provides a convenient way to unfold `f`. -- `simp [*]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and all hypotheses. -- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas -- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`, but removes the ones named `idᵢ`. -- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis `hᵢ` is introduced, but the old one remains in the local context. +- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged + with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions. + If an `hᵢ` is a defined constant `f`, then the equational lemmas associated with + `f` are used. This provides a convenient way to unfold `f`. +- `simp [*]` simplifies the main goal target using the lemmas tagged with the + attribute `[simp]` and all hypotheses. +- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas. +- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged + with the attribute `[simp]`, but removes the ones named `idᵢ`. +- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If + the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis + `hᵢ` is introduced, but the old one remains in the local context. - `simp at *` simplifies all the hypotheses and the target. -- `simp [*] at *` simplifies target and all (propositional) hypotheses using the other hypotheses. +- `simp [*] at *` simplifies target and all (propositional) hypotheses using the + other hypotheses. -/ -syntax (name := simp) "simp " (config)? (discharger)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic +syntax (name := simp) "simp " (config)? (discharger)? (&"only ")? + ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic /-- -`simp_all` is a stronger version of `simp [*] at *` where the hypotheses and target are simplified -multiple times until no simplication is applicable. +`simp_all` is a stronger version of `simp [*] at *` where the hypotheses and target +are simplified multiple times until no simplication is applicable. Only non-dependent propositional hypotheses are considered. -/ -syntax (name := simpAll) "simp_all " (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? : tactic +syntax (name := simpAll) "simp_all " (config)? (discharger)? (&"only ")? + ("[" (simpErase <|> simpLemma),* "]")? : tactic /-- -The `dsimp` tactic is the definitional simplifier. It is similar to `simp` but only applies theorems that hold by -reflexivity. Thus, the result is guaranteed to be definitionally equal to the input. +The `dsimp` tactic is the definitional simplifier. It is similar to `simp` but only +applies theorems that hold by reflexivity. Thus, the result is guaranteed to be +definitionally equal to the input. -/ -syntax (name := dsimp) "dsimp " (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? (location)? : tactic +syntax (name := dsimp) "dsimp " (config)? (discharger)? (&"only ")? + ("[" (simpErase <|> simpLemma),* "]")? (location)? : tactic /-- - `delta id` delta-expands the definition `id`. - This is a low-level tactic, it will expose how recursive definitions have been compiled by Lean. -/ +`delta id` delta-expands the definition `id`. +This is a low-level tactic, it will expose how recursive definitions have been +compiled by Lean. +-/ syntax (name := delta) "delta " ident (location)? : tactic + /-- - `unfold id,+` unfolds definition `id`. For non-recursive definitions, this tactic is identical to `delta`. - For recursive definitions, it hides the encoding tricks used by the Lean frontend to convince the - kernel that the definition terminates. -/ +`unfold id,+` unfolds definition `id`. For non-recursive definitions, this tactic +is identical to `delta`. +For definitions by pattern matching, it uses "equation lemmas" which are +autogenerated for each match arm. +-/ syntax (name := unfold) "unfold " ident,+ (location)? : tactic -/-- Auxiliary macro for lifting have/suffices/let/... - It makes sure the "continuation" `?_` is the main goal after refining. -/ +/-- +Auxiliary macro for lifting have/suffices/let/... +It makes sure the "continuation" `?_` is the main goal after refining. +-/ macro "refine_lift " e:term : tactic => `(focus (refine no_implicit_lambda% $e; rotate_right)) /-- -`have h : t := e` adds the hypothesis `h : t` to the current goal if `e` a term of type `t`. If `t` is omitted, it will be inferred. -If `h` is omitted, the name `this` is used. -The variant `have pattern := e` is equivalent to `match e with | pattern => _`, and it is convenient for types that have only applicable constructor. -Example: given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`. +`have h : t := e` adds the hypothesis `h : t` to the current goal if `e` a term +of type `t`. +* If `t` is omitted, it will be inferred. +* If `h` is omitted, the name `this` is used. +* The variant `have pattern := e` is equivalent to `match e with | pattern => _`, + and it is convenient for types that have only one applicable constructor. + For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the + hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`. -/ macro "have " d:haveDecl : tactic => `(refine_lift have $d:haveDecl; ?_) /-- -Given a main goal `ctx |- t`, `suffices h : t' from e` replaces the main goal with `ctx |- t'`, +Given a main goal `ctx ⊢ t`, `suffices h : t' from e` replaces the main goal with `ctx ⊢ t'`, `e` must have type `t` in the context `ctx, h : t'`. The variant `suffices h : t' by tac` is a shorthand for `suffices h : t' from by tac`. @@ -326,8 +493,10 @@ macro "suffices " d:sufficesDecl : tactic => `(refine_lift suffices $d; ?_) /-- `let h : t := e` adds the hypothesis `h : t := e` to the current goal if `e` a term of type `t`. If `t` is omitted, it will be inferred. -The variant `let pattern := e` is equivalent to `match e with | pattern => _`, and it is convenient for types that have only applicable constructor. -Example: given `h : p ∧ q ∧ r`, `let ⟨h₁, h₂, h₃⟩ := h` produces the hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`. +The variant `let pattern := e` is equivalent to `match e with | pattern => _`, +and it is convenient for types that have only applicable constructor. +Example: given `h : p ∧ q ∧ r`, `let ⟨h₁, h₂, h₃⟩ := h` produces the hypotheses +`h₁ : p`, `h₂ : q`, and `h₃ : r`. -/ macro "let " d:letDecl : tactic => `(refine_lift let $d:letDecl; ?_) /-- @@ -350,42 +519,88 @@ macro (priority := high) "have'" x:ident " := " p:term : tactic => `(have' $x : /-- Similar to `let`, but using `refine'` -/ macro "let' " d:letDecl : tactic => `(refine_lift' let $d:letDecl; ?_) -syntax inductionAltLHS := "| " (("@"? ident) <|> hole) (ident <|> hole)* -syntax inductionAlt := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> syntheticHole <|> tacticSeq) -syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+) /-- -Assuming `x` is a variable in the local context with an inductive type, `induction x` applies induction on `x` to the main goal, -producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor -and an inductive hypothesis is added for each recursive argument to the constructor. -If the type of an element in the local context depends on `x`, that element is reverted and reintroduced afterward, -so that the inductive hypothesis incorporates that hypothesis as well. -For example, given `n : Nat` and a goal with a hypothesis `h : P n` and target `Q n`, `induction n` produces one goal -with hypothesis `h : P 0` and target `Q 0`, and one goal with hypotheses `h : P (Nat.succ a)` and `ih₁ : P a → Q a` and target `Q (Nat.succ a)`. -Here the names `a` and `ih₁` are chosen automatically and are not accessible. You can use `with` to provide the variables names for each constructor. -- `induction e`, where `e` is an expression instead of a variable, generalizes `e` in the goal, and then performs induction on the resulting variable. -- `induction e using r` allows the user to specify the principle of induction that should be used. Here `r` should be a theorem whose result type must be of the form `C t`, where `C` is a bound variable and `t` is a (possibly empty) sequence of bound variables -- `induction e generalizing z₁ ... zₙ`, where `z₁ ... zₙ` are variables in the local context, generalizes over `z₁ ... zₙ` before applying the induction but then introduces them in each goal. In other words, the net effect is that each inductive hypothesis is generalized. -- Given `x : Nat`, `induction x with | zero => tac₁ | succ x' ih => tac₂` uses tactic `tac₁` for the `zero` case, and `tac₂` for the `succ` case. +The left hand side of an induction arm, `| foo a b c` or `| @foo a b c` +where `foo` is a constructor of the inductive type and `a b c` are the arguments +to the contstructor. -/ -syntax (name := induction) "induction " term,+ (" using " ident)? ("generalizing " (colGt term:max)+)? (inductionAlts)? : tactic - -syntax generalizeArg := atomic(ident " : ")? term:51 " = " ident +syntax inductionAltLHS := "| " (("@"? ident) <|> hole) (ident <|> hole)* /-- -`generalize ([h :] e = x),+` replaces all occurrences `e`s in the main goal with a fresh hypothesis `x`s. -If `h` is given, `h : e = x` is introduced as well. -/ +In induction alternative, which can have 1 or more cases on the left +and `_`, `?_`, or a tactic sequence after the `=>`. +-/ +syntax inductionAlt := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> syntheticHole <|> tacticSeq) +/-- +After `with`, there is an optional tactic that runs on all branches, and +then a list of alternatives. +-/ +syntax inductionAlts := "with " (tactic)? withPosition((colGe inductionAlt)+) + +/-- +Assuming `x` is a variable in the local context with an inductive type, +`induction x` applies induction on `x` to the main goal, +producing one goal for each constructor of the inductive type, +in which the target is replaced by a general instance of that constructor +and an inductive hypothesis is added for each recursive argument to the constructor. +If the type of an element in the local context depends on `x`, +that element is reverted and reintroduced afterward, +so that the inductive hypothesis incorporates that hypothesis as well. + +For example, given `n : Nat` and a goal with a hypothesis `h : P n` and target `Q n`, +`induction n` produces one goal with hypothesis `h : P 0` and target `Q 0`, +and one goal with hypotheses `h : P (Nat.succ a)` and `ih₁ : P a → Q a` and target `Q (Nat.succ a)`. +Here the names `a` and `ih₁` are chosen automatically and are not accessible. +You can use `with` to provide the variables names for each constructor. +- `induction e`, where `e` is an expression instead of a variable, + generalizes `e` in the goal, and then performs induction on the resulting variable. +- `induction e using r` allows the user to specify the principle of induction that should be used. + Here `r` should be a theorem whose result type must be of the form `C t`, + where `C` is a bound variable and `t` is a (possibly empty) sequence of bound variables +- `induction e generalizing z₁ ... zₙ`, where `z₁ ... zₙ` are variables in the local context, + generalizes over `z₁ ... zₙ` before applying the induction but then introduces them in each goal. + In other words, the net effect is that each inductive hypothesis is generalized. +- Given `x : Nat`, `induction x with | zero => tac₁ | succ x' ih => tac₂` + uses tactic `tac₁` for the `zero` case, and `tac₂` for the `succ` case. +-/ +syntax (name := induction) "induction " term,+ (" using " ident)? + ("generalizing " (colGt term:max)+)? (inductionAlts)? : tactic + +/-- A `generalize` argument, of the form `term = x` or `h : term = x`. -/ +syntax generalizeArg := atomic(ident " : ")? term:51 " = " ident + +/-- +`generalize ([h :] e = x),+` replaces all occurrences `e`s in the main goal +with a fresh hypothesis `x`s. If `h` is given, `h : e = x` is introduced as well. +-/ syntax (name := generalize) "generalize " generalizeArg,+ : tactic +/-- +A `cases` argument, of the form `e` or `h : e` (where `h` asserts that +`e = cᵢ a b` for each constructor `cᵢ` of the inductive). +-/ syntax casesTarget := atomic(ident " : ")? term /-- -Assuming `x` is a variable in the local context with an inductive type, `cases x` splits the main goal, -producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor. -If the type of an element in the local context depends on `x`, that element is reverted and reintroduced afterward, -so that the case split affects that hypothesis as well. `cases` detects unreachable cases and closes them automatically. -For example, given `n : Nat` and a goal with a hypothesis `h : P n` and target `Q n`, `cases n` produces one goal with hypothesis `h : P 0` and target `Q 0`, -and one goal with hypothesis `h : P (Nat.succ a)` and target `Q (Nat.succ a)`. Here the name `a` is chosen automatically and are not accessible. You can use `with` to provide the variables names for each constructor. -- `cases e`, where `e` is an expression instead of a variable, generalizes `e` in the goal, and then cases on the resulting variable. -- Given `as : List α`, `cases as with | nil => tac₁ | cons a as' => tac₂`, uses tactic `tac₁` for the `nil` case, and `tac₂` for the `cons` case, and `a` and `as'` are used as names for the new variables introduced. -- `cases h : e`, where `e` is a variable or an expression, performs cases on `e` as above, but also adds a hypothesis `h : e = ...` to each hypothesis, where `...` is the constructor instance for that particular case. +Assuming `x` is a variable in the local context with an inductive type, +`cases x` splits the main goal, producing one goal for each constructor of the +inductive type, in which the target is replaced by a general instance of that constructor. +If the type of an element in the local context depends on `x`, +that element is reverted and reintroduced afterward, +so that the case split affects that hypothesis as well. +`cases` detects unreachable cases and closes them automatically. + +For example, given `n : Nat` and a goal with a hypothesis `h : P n` and target `Q n`, +`cases n` produces one goal with hypothesis `h : P 0` and target `Q 0`, +and one goal with hypothesis `h : P (Nat.succ a)` and target `Q (Nat.succ a)`. +Here the name `a` is chosen automatically and is not accessible. +You can use `with` to provide the variables names for each constructor. +- `cases e`, where `e` is an expression instead of a variable, generalizes `e` in the goal, + and then cases on the resulting variable. +- Given `as : List α`, `cases as with | nil => tac₁ | cons a as' => tac₂`, + uses tactic `tac₁` for the `nil` case, and `tac₂` for the `cons` case, + and `a` and `as'` are used as names for the new variables introduced. +- `cases h : e`, where `e` is a variable or an expression, + performs cases on `e` as above, but also adds a hypothesis `h : e = ...` to each hypothesis, + where `...` is the constructor instance for that particular case. -/ syntax (name := cases) "cases " casesTarget,+ (" using " ident)? (inductionAlts)? : tactic @@ -401,7 +616,8 @@ macro_rules | `(tactic| repeat $seq) => `(tactic| first | ($seq); repeat $seq | skip) /-- -`trivial` tries different simple tactics (e.g., `rfl`, `contradiction`, ...) to close the current goal. +`trivial` tries different simple tactics (e.g., `rfl`, `contradiction`, ...) +to close the current goal. You can use the command `macro_rules` to extend the set of tactics used. Example: ``` macro_rules | `(tactic| trivial) => `(tactic| simp) @@ -426,15 +642,21 @@ example : False ∨ True := by -/ syntax (name := dbgTrace) "dbg_trace " str : tactic -/-- `stop` is a helper tactic for "discarding" the rest of a proof. It is useful when working on the middle of a complex proofs, - and less messy than commenting the remainder of the proof. -/ +/-- +`stop` is a helper tactic for "discarding" the rest of a proof: +it is defined as `repeat sorry`. +It is useful when working on the middle of a complex proofs, +and less messy than commenting the remainder of the proof. +-/ macro "stop" tacticSeq : tactic => `(repeat sorry) /-- The tactic `specialize h a₁ ... aₙ` works on local hypothesis `h`. -The premises of this hypothesis, either universal quantifications or non-dependent implications, -are instantiated by concrete terms coming either from arguments `a₁` ... `aₙ`. -The tactic adds a new hypothesis with the same name `h := h a₁ ... aₙ` and tries to clear the previous one. +The premises of this hypothesis, either universal quantifications or +non-dependent implications, are instantiated by concrete terms coming +from arguments `a₁` ... `aₙ`. +The tactic adds a new hypothesis with the same name `h := h a₁ ... aₙ` +and tries to clear the previous one. -/ syntax (name := specialize) "specialize " term : tactic @@ -445,7 +667,8 @@ macro_rules | `(tactic| trivial) => `(tactic| decide) macro_rules | `(tactic| trivial) => `(tactic| apply True.intro) macro_rules | `(tactic| trivial) => `(tactic| apply And.intro <;> trivial) -/-- `unhygienic tacs` runs `tacs` with name hygiene disabled. +/-- +`unhygienic tacs` runs `tacs` with name hygiene disabled. This means that tactics that would normally create inaccessible names will instead make regular variables. **Warning**: Tactics may change their variable naming strategies at any time, so code that depends on autogenerated names is brittle. @@ -458,10 +681,11 @@ example : ∀ x : Nat, x = x := by unhygienic -/ macro "unhygienic " t:tacticSeq : tactic => `(set_option tactic.hygienic false in $t) -/-- `fail msg` is a tactic that always fail and produces an error using the given message. -/ +/-- `fail msg` is a tactic that always fails, and produces an error using the given message. -/ syntax (name := fail) "fail " (str)? : tactic -/-- `checkpoint tac` acts the same as `tac`, but it caches the input and output of `tac`, +/-- +`checkpoint tac` acts the same as `tac`, but it caches the input and output of `tac`, and if the file is re-elaborated and the input matches, the tactic is not re-run and its effects are reapplied to the state. This is useful for improving responsiveness when working on a long tactic proof, by wrapping expensive tactics with `checkpoint`. @@ -469,31 +693,41 @@ when working on a long tactic proof, by wrapping expensive tactics with `checkpo See the `save` tactic, which may be more convenient to use. (TODO: do this automatically and transparently so that users don't have to use -this combinator explicitly.) -/ +this combinator explicitly.) +-/ syntax (name := checkpoint) "checkpoint " tacticSeq : tactic -/-- `save` is defined to be the same as `skip`, but the elaborator has +/-- +`save` is defined to be the same as `skip`, but the elaborator has special handling for occurrences of `save` in tactic scripts and will transform `by tac1; save; tac2` to `by (checkpoint tac1); tac2`, meaning that the effect of `tac1` will be cached and replayed. This is useful for improving responsiveness when working on a long tactic proof, by using `save` after expensive tactics. (TODO: do this automatically and transparently so that users don't have to use -this combinator explicitly.) -/ +this combinator explicitly.) +-/ macro (name := save) "save" : tactic => `(skip) -/-- The tactic `sleep ms` sleeps for `ms` milliseconds and does nothing. It is used for debugging purposes only. -/ +/-- +The tactic `sleep ms` sleeps for `ms` milliseconds and does nothing. +It is used for debugging purposes only. +-/ syntax (name := sleep) "sleep" num : tactic -/-- `exists e₁, e₂, ...` is shorthand for `refine ⟨e₁, e₂, ...⟩; try trivial`. It is useful for existential goals. -/ +/-- +`exists e₁, e₂, ...` is shorthand for `refine ⟨e₁, e₂, ...⟩; try trivial`. +It is useful for existential goals. +-/ macro "exists " es:term,+ : tactic => `(tactic| (refine ⟨$es,*, ?_⟩; try trivial)) /-- Apply congruence (recursively) to goals of the form `⊢ f as = f bs` and `⊢ HEq (f as) (f bs)`. -The optional parameter is the depth of the recursive applications. This is useful when `congr` is too aggressive -in breaking down the goal. -For example, given `⊢ f (g (x + y)) = f (g (y + x))`, `congr` produces the goals `⊢ x = y` and `⊢ y = x`, +The optional parameter is the depth of the recursive applications. +This is useful when `congr` is too aggressive in breaking down the goal. +For example, given `⊢ f (g (x + y)) = f (g (y + x))`, +`congr` produces the goals `⊢ x = y` and `⊢ y = x`, while `congr 2` produces the intended `⊢ x + y = y + x`. -/ syntax (name := congr) "congr " (num)? : tactic @@ -502,40 +736,46 @@ end Tactic namespace Attr /-- -Theorems tagged with the `simp` attribute are by the simplifier (i.e., the `simp` tactic, and its variants) to simplify -expressions occurring in your goals. +Theorems tagged with the `simp` attribute are by the simplifier +(i.e., the `simp` tactic, and its variants) to simplify expressions occurring in your goals. We call theorems tagged with the `simp` attribute "simp theorems" or "simp lemmas". Lean maintains a database/index containing all active simp theorems. Here is an example of a simp theorem. ```lean @[simp] theorem ne_eq (a b : α) : (a ≠ b) = Not (a = b) := rfl ``` -This simp theorem instructs the simplifier to replace instances of the term `a ≠ b` (e.g. `x + 0 ≠ y`) with `Not (a = b)` -(e.g., `Not (x + 0 = y)`). -The simplifier applies simp theorems in one direction only: if `A = B` is a simp theorem, then `simp` -replaces `A`s with `B`s, but it doesn't replace `B`s with `A`s. Hence a simp theorem should have the +This simp theorem instructs the simplifier to replace instances of the term +`a ≠ b` (e.g. `x + 0 ≠ y`) with `Not (a = b)` (e.g., `Not (x + 0 = y)`). +The simplifier applies simp theorems in one direction only: +if `A = B` is a simp theorem, then `simp` replaces `A`s with `B`s, +but it doesn't replace `B`s with `A`s. Hence a simp theorem should have the property that its right-hand side is "simpler" than its left-hand side. In particular, `=` and `↔` should not be viewed as symmetric operators in this situation. The following would be a terrible simp theorem (if it were even allowed): ```lean @[simp] lemma mul_right_inv_bad (a : G) : 1 = a * a⁻¹ := ... ``` -Replacing 1 with a * a⁻¹ is not a sensible default direction to travel. Even worse would be a theorem -that causes expressions to grow without bound, causing simp to loop forever. +Replacing 1 with a * a⁻¹ is not a sensible default direction to travel. +Even worse would be a theorem that causes expressions to grow without bound, +causing simp to loop forever. -By default the simplifier applies `simp` theorems to an expression `e` after its sub-expressions have been simplified. -We say it performs a bottom-up simplification. You can instruct the simplifier to apply a theorem before its sub-expressions +By default the simplifier applies `simp` theorems to an expression `e` +after its sub-expressions have been simplified. +We say it performs a bottom-up simplification. +You can instruct the simplifier to apply a theorem before its sub-expressions have been simplified by using the modifier `↓`. Here is an example ```lean @[simp↓] theorem not_and_eq (p q : Prop) : (¬ (p ∧ q)) = (¬p ∨ ¬q) := ``` -When multiple simp theorems are applicable, the simplifier uses the one with highest priority. If there are several with -the same priority, it is uses the "most recent one". Example: +When multiple simp theorems are applicable, the simplifier uses the one with highest priority. +If there are several with the same priority, it is uses the "most recent one". Example: ```lean @[simp high] theorem cond_true (a b : α) : cond true a b = a := rfl -@[simp low+1] theorem or_true (p : Prop) : (p ∨ True) = True := propext <| Iff.intro (fun _ => trivial) (fun _ => Or.inr trivial) -@[simp 100] theorem ite_self {d : Decidable c} (a : α) : ite c a a = a := by cases d <;> rfl +@[simp low+1] theorem or_true (p : Prop) : (p ∨ True) = True := + propext <| Iff.intro (fun _ => trivial) (fun _ => Or.inr trivial) +@[simp 100] theorem ite_self {d : Decidable c} (a : α) : ite c a a = a := by + cases d <;> rfl ``` -/ syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? (prio)? : attr @@ -545,26 +785,33 @@ end Parser end Lean /-- -`‹t›` resolves to an (arbitrary) hypothesis of type `t`. It is useful for referring to hypotheses without accessible names. -`t` may contain holes that are solved by unification with the expected type; in particular, `‹_›` is a shortcut for `by assumption`. -/ +`‹t›` resolves to an (arbitrary) hypothesis of type `t`. +It is useful for referring to hypotheses without accessible names. +`t` may contain holes that are solved by unification with the expected type; +in particular, `‹_›` is a shortcut for `by assumption`. +-/ macro "‹" type:term "›" : term => `((by assumption : $type)) -/-- `get_elem_tactic_trivial` is an extensible tactic automatically called +/-- +`get_elem_tactic_trivial` 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` -(for doing linear arithmetic in the index). -/ +(for doing linear arithmetic in the index). +-/ syntax "get_elem_tactic_trivial" : tactic macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| trivial) macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp (config := { arith := true }); done) -/-- `get_elem_tactic` is the tactic automatically called by the notation `arr[i]` +/-- +`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. -/ +users are encouraged to extend `get_elem_tactic_trivial` instead of this tactic. +-/ macro "get_elem_tactic" : tactic => `(first | get_elem_tactic_trivial @@ -575,10 +822,12 @@ macro "get_elem_tactic" : tactic => - Use `a[i]'h` notation instead, where `h` is a proof that index is valid" ) +@[inheritDoc getElem] macro:max x:term noWs "[" i:term "]" : term => `(getElem $x $i (by get_elem_tactic)) /-- Helper declaration for the unexpander -/ @[inline] def getElem' [GetElem cont idx elem dom] (xs : cont) (i : idx) (h : dom xs i) : elem := getElem xs i h +@[inheritDoc getElem] macro x:term noWs "[" i:term "]'" h:term:max : term => `(getElem' $x $i $h) diff --git a/tests/lean/interactive/1403.lean.expected.out b/tests/lean/interactive/1403.lean.expected.out index d2c5e00720..a00fbddf06 100644 --- a/tests/lean/interactive/1403.lean.expected.out +++ b/tests/lean/interactive/1403.lean.expected.out @@ -4,5 +4,5 @@ {"start": {"line": 1, "character": 2}, "end": {"line": 1, "character": 12}}, "contents": {"value": - "`rewrite [e]` applies identity `e` as a rewrite rule to the target of the main goal.\nIf `e` is preceded by left arrow (`←` or `<-`), the rewrite is applied in the reverse direction.\nIf `e` is a defined constant, then the equational theorems associated with `e` are used. This provides a convenient way to unfold `e`.\n- `rewrite [e₁, ..., eₙ]` applies the given rules sequentially.\n- `rewrite [e] at l` rewrites `e` at location(s) `l`, where `l` is either `*` or a list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-` can also be used, to signify the target of the goal.\n", + "`rewrite [e]` applies identity `e` as a rewrite rule to the target of the main goal.\nIf `e` is preceded by left arrow (`←` or `<-`), the rewrite is applied in the reverse direction.\nIf `e` is a defined constant, then the equational theorems associated with `e` are used.\nThis provides a convenient way to unfold `e`.\n- `rewrite [e₁, ..., eₙ]` applies the given rules sequentially.\n- `rewrite [e] at l` rewrites `e` at location(s) `l`, where `l` is either `*` or a\n list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-`\n can also be used, to signify the target of the goal.\n", "kind": "markdown"}}