From e3420c08f1823e8e2f6733520f4b4b9361bb3e6f Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Fri, 8 Nov 2024 10:17:46 -0800 Subject: [PATCH] feat: `decide +revert` and improvements to `native_decide` (#5999) This PR adds configuration options for `decide`/`decide!`/`native_decide` and refactors the tactics to be frontends to the same backend. Adds a `+revert` option that cleans up the local context and reverts all local variables the goal depends on, along with indirect propositional hypotheses. Makes `native_decide` fail at elaboration time on failure without sacrificing performance (the decision procedure is still evaluated just once). Now `native_decide` supports universe polymorphism. Closes #2072 --- src/Init/Prelude.lean | 36 +- src/Init/Tactics.lean | 133 ++- src/Lean/Elab/Tactic/ElabTerm.lean | 152 +++- src/Lean/Parser/Tactic.lean | 84 -- tests/lean/1825.lean.expected.out | 9 +- .../completionTactics.lean.expected.out | 833 +++--------------- tests/lean/run/4306.lean | 9 +- tests/lean/run/decideBang.lean | 25 + tests/lean/run/decideNative.lean | 130 +++ tests/lean/run/decideTactic.lean | 27 +- 10 files changed, 571 insertions(+), 867 deletions(-) create mode 100644 tests/lean/run/decideNative.lean diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 28cd71a30700..2f34e230a517 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1951,7 +1951,7 @@ def UInt8.decEq (a b : UInt8) : Decidable (Eq a b) := instance : DecidableEq UInt8 := UInt8.decEq instance : Inhabited UInt8 where - default := UInt8.ofNatCore 0 (by decide) + default := UInt8.ofNatCore 0 (of_decide_eq_true rfl) /-- The size of type `UInt16`, that is, `2^16 = 65536`. -/ abbrev UInt16.size : Nat := 65536 @@ -1992,7 +1992,7 @@ def UInt16.decEq (a b : UInt16) : Decidable (Eq a b) := instance : DecidableEq UInt16 := UInt16.decEq instance : Inhabited UInt16 where - default := UInt16.ofNatCore 0 (by decide) + default := UInt16.ofNatCore 0 (of_decide_eq_true rfl) /-- The size of type `UInt32`, that is, `2^32 = 4294967296`. -/ abbrev UInt32.size : Nat := 4294967296 @@ -2038,7 +2038,7 @@ def UInt32.decEq (a b : UInt32) : Decidable (Eq a b) := instance : DecidableEq UInt32 := UInt32.decEq instance : Inhabited UInt32 where - default := UInt32.ofNatCore 0 (by decide) + default := UInt32.ofNatCore 0 (of_decide_eq_true rfl) instance : LT UInt32 where lt a b := LT.lt a.toBitVec b.toBitVec @@ -2105,7 +2105,7 @@ def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) := instance : DecidableEq UInt64 := UInt64.decEq instance : Inhabited UInt64 where - default := UInt64.ofNatCore 0 (by decide) + default := UInt64.ofNatCore 0 (of_decide_eq_true rfl) /-- The size of type `USize`, that is, `2^System.Platform.numBits`. -/ abbrev USize.size : Nat := (hPow 2 System.Platform.numBits) @@ -2113,8 +2113,8 @@ abbrev USize.size : Nat := (hPow 2 System.Platform.numBits) theorem usize_size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) := show Or (Eq (hPow 2 System.Platform.numBits) 4294967296) (Eq (hPow 2 System.Platform.numBits) 18446744073709551616) from match System.Platform.numBits, System.Platform.numBits_eq with - | _, Or.inl rfl => Or.inl (by decide) - | _, Or.inr rfl => Or.inr (by decide) + | _, Or.inl rfl => Or.inl (of_decide_eq_true rfl) + | _, Or.inr rfl => Or.inr (of_decide_eq_true rfl) /-- A `USize` is an unsigned integer with the size of a word @@ -2156,8 +2156,8 @@ instance : DecidableEq USize := USize.decEq instance : Inhabited USize where default := USize.ofNatCore 0 (match USize.size, usize_size_eq with - | _, Or.inl rfl => by decide - | _, Or.inr rfl => by decide) + | _, Or.inl rfl => of_decide_eq_true rfl + | _, Or.inr rfl => of_decide_eq_true rfl) /-- Upcast a `Nat` less than `2^32` to a `USize`. @@ -2170,7 +2170,7 @@ def USize.ofNat32 (n : @& Nat) (h : LT.lt n 4294967296) : USize where BitVec.ofNatLt n ( match System.Platform.numBits, System.Platform.numBits_eq with | _, Or.inl rfl => h - | _, Or.inr rfl => Nat.lt_trans h (by decide) + | _, Or.inr rfl => Nat.lt_trans h (of_decide_eq_true rfl) ) /-- @@ -2197,8 +2197,8 @@ structure Char where private theorem isValidChar_UInt32 {n : Nat} (h : n.isValidChar) : LT.lt n UInt32.size := match h with - | Or.inl h => Nat.lt_trans h (by decide) - | Or.inr ⟨_, h⟩ => Nat.lt_trans h (by decide) + | Or.inl h => Nat.lt_trans h (of_decide_eq_true rfl) + | Or.inr ⟨_, h⟩ => Nat.lt_trans h (of_decide_eq_true rfl) /-- Pack a `Nat` encoding a valid codepoint into a `Char`. @@ -2216,7 +2216,7 @@ Convert a `Nat` into a `Char`. If the `Nat` does not encode a valid unicode scal def Char.ofNat (n : Nat) : Char := dite (n.isValidChar) (fun h => Char.ofNatAux n h) - (fun _ => { val := ⟨BitVec.ofNatLt 0 (by decide)⟩, valid := Or.inl (by decide) }) + (fun _ => { val := ⟨BitVec.ofNatLt 0 (of_decide_eq_true rfl)⟩, valid := Or.inl (of_decide_eq_true rfl) }) theorem Char.eq_of_val_eq : ∀ {c d : Char}, Eq c.val d.val → Eq c d | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl @@ -2239,9 +2239,9 @@ instance : DecidableEq Char := /-- Returns the number of bytes required to encode this `Char` in UTF-8. -/ def Char.utf8Size (c : Char) : Nat := let v := c.val - ite (LE.le v (UInt32.ofNatCore 0x7F (by decide))) 1 - (ite (LE.le v (UInt32.ofNatCore 0x7FF (by decide))) 2 - (ite (LE.le v (UInt32.ofNatCore 0xFFFF (by decide))) 3 4)) + ite (LE.le v (UInt32.ofNatCore 0x7F (of_decide_eq_true rfl))) 1 + (ite (LE.le v (UInt32.ofNatCore 0x7FF (of_decide_eq_true rfl))) 2 + (ite (LE.le v (UInt32.ofNatCore 0xFFFF (of_decide_eq_true rfl))) 3 4)) /-- `Option α` is the type of values which are either `some a` for some `a : α`, @@ -3480,7 +3480,7 @@ def USize.toUInt64 (u : USize) : UInt64 where let ⟨⟨n, h⟩⟩ := u show LT.lt n _ from match System.Platform.numBits, System.Platform.numBits_eq, h with - | _, Or.inl rfl, h => Nat.lt_trans h (by decide) + | _, Or.inl rfl, h => Nat.lt_trans h (of_decide_eq_true rfl) | _, Or.inr rfl, h => h ) @@ -3549,9 +3549,9 @@ with /-- A hash function for names, which is stored inside the name itself as a computed field. -/ @[computed_field] hash : Name → UInt64 - | .anonymous => .ofNatCore 1723 (by decide) + | .anonymous => .ofNatCore 1723 (of_decide_eq_true rfl) | .str p s => mixHash p.hash s.hash - | .num p v => mixHash p.hash (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatCore v h) (fun _ => UInt64.ofNatCore 17 (by decide))) + | .num p v => mixHash p.hash (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatCore v h) (fun _ => UInt64.ofNatCore 17 (of_decide_eq_true rfl))) instance : Inhabited Name where default := Name.anonymous diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 0117ec495349..78c9959b338b 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -990,13 +990,6 @@ and tries to clear the previous one. -/ syntax (name := specialize) "specialize " term : tactic -macro_rules | `(tactic| trivial) => `(tactic| assumption) -macro_rules | `(tactic| trivial) => `(tactic| rfl) -macro_rules | `(tactic| trivial) => `(tactic| contradiction) -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. This means that tactics that would normally create inaccessible names will instead @@ -1156,6 +1149,132 @@ macro "haveI" d:haveDecl : tactic => `(tactic| refine_lift haveI $d:haveDecl; ?_ /-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/ macro "letI" d:haveDecl : tactic => `(tactic| refine_lift letI $d:haveDecl; ?_) +/-- +Configuration for the `decide` tactic family. +-/ +structure DecideConfig where + /-- If true (default: false), then use only kernel reduction when reducing the `Decidable` instance. + This is more efficient, since the default mode reduces twice (once in the elaborator and again in the kernel), + however kernel reduction ignores transparency settings. The `decide!` tactic is a synonym for `decide +kernel`. -/ + kernel : Bool := false + /-- If true (default: false), then uses the native code compiler to evaluate the `Decidable` instance, + admitting the result via the axiom `Lean.ofReduceBool`. This can be significantly more efficient, + but it is at the cost of increasing the trusted code base, namely the Lean compiler + and all definitions with an `@[implemented_by]` attribute. + The instance is only evaluated once. The `native_decide` tactic is a synonym for `decide +native`. -/ + native : Bool := false + /-- If true (default: true), then when preprocessing the goal, do zeta reduction to attempt to eliminate free variables. -/ + zetaReduce : Bool := true + /-- If true (default: false), then when preprocessing reverts free variables. -/ + revert : Bool := false + +/-- +`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p` +and then reducing that instance to evaluate the truth value of `p`. +If it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal. + +The target is not allowed to contain local variables or metavariables. +If there are local variables, you can first try using the `revert` tactic with these local variables to move them into the target, +or you can use the `+revert` option, described below. + +Options: +- `decide +revert` begins by reverting local variables that the target depends on, + after cleaning up the local context of irrelevant variables. + A variable is *relevant* if it appears in the target, if it appears in a relevant variable, + or if it is a proposition that refers to a relevant variable. +- `decide +kernel` uses kernel for reduction instead of the elaborator. + It has two key properties: (1) since it uses the kernel, it ignores transparency and can unfold everything, + and (2) it reduces the `Decidable` instance only once instead of twice. +- `decide +native` uses the native code compiler (`#eval`) to evaluate the `Decidable` instance, + admitting the result via the `Lean.ofReduceBool` axiom. + This can be significantly more efficient than using reduction, but it is at the cost of increasing the size + of the trusted code base. + Namely, it depends on the correctness of the Lean compiler and all definitions with an `@[implemented_by]` attribute. + Like with `+kernel`, the `Decidable` instance is evaluated only once. + +Limitation: In the default mode or `+kernel` mode, since `decide` uses reduction to evaluate the term, +`Decidable` instances defined by well-founded recursion might not work because evaluating them requires reducing proofs. +Reduction can also get stuck on `Decidable` instances with `Eq.rec` terms. +These can appear in instances defined using tactics (such as `rw` and `simp`). +To avoid this, create such instances using definitions such as `decidable_of_iff` instead. + +## Examples + +Proving inequalities: +```lean +example : 2 + 2 ≠ 5 := by decide +``` + +Trying to prove a false proposition: +```lean +example : 1 ≠ 1 := by decide +/- +tactic 'decide' proved that the proposition + 1 ≠ 1 +is false +-/ +``` + +Trying to prove a proposition whose `Decidable` instance fails to reduce +```lean +opaque unknownProp : Prop + +open scoped Classical in +example : unknownProp := by decide +/- +tactic 'decide' failed for proposition + unknownProp +since its 'Decidable' instance reduced to + Classical.choice ⋯ +rather than to the 'isTrue' constructor. +-/ +``` + +## Properties and relations + +For equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`. +```lean +example : 1 + 1 = 2 := by decide +example : 1 + 1 = 2 := by rfl +``` +-/ +syntax (name := decide) "decide" optConfig : tactic + +/-- +`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal. +It has the following properties: +- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything. +- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds, + and once during kernel type checking), the `decide!` tactic reduces it exactly once. + +The `decide!` syntax is short for `decide +kernel`. +-/ +syntax (name := decideBang) "decide!" optConfig : tactic + +/-- +`native_decide` is a synonym for `decide +native`. +It will attempt to prove a goal of type `p` by synthesizing an instance +of `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this +uses `#eval` to evaluate the decidability instance. + +This should be used with care because it adds the entire lean compiler to the trusted +part, and the axiom `Lean.ofReduceBool` will show up in `#print axioms` for theorems using +this method or anything that transitively depends on them. Nevertheless, because it is +compiled, this can be significantly more efficient than using `decide`, and for very +large computations this is one way to run external programs and trust the result. +```lean +example : (List.range 1000).length = 1000 := by native_decide +``` +-/ +syntax (name := nativeDecide) "native_decide" optConfig : tactic + +macro_rules | `(tactic| trivial) => `(tactic| assumption) +macro_rules | `(tactic| trivial) => `(tactic| rfl) +macro_rules | `(tactic| trivial) => `(tactic| contradiction) +macro_rules | `(tactic| trivial) => `(tactic| decide) +macro_rules | `(tactic| trivial) => `(tactic| apply True.intro) +macro_rules | `(tactic| trivial) => `(tactic| apply And.intro <;> trivial) + /-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index 1d05fc3e9577..98af2c5b4dde 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/src/Lean/Elab/Tactic/ElabTerm.lean @@ -7,9 +7,11 @@ prelude import Lean.Meta.Tactic.Constructor import Lean.Meta.Tactic.Assert import Lean.Meta.Tactic.AuxLemma +import Lean.Meta.Tactic.Cleanup import Lean.Meta.Tactic.Clear import Lean.Meta.Tactic.Rename import Lean.Elab.Tactic.Basic +import Lean.Elab.Tactic.Config import Lean.Elab.SyntheticMVars namespace Lean.Elab.Tactic @@ -347,6 +349,7 @@ def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId replaceMainGoal [← (← getMainGoal).rename fvarId h.getId] | _ => throwUnsupportedSyntax + /-- Make sure `expectedType` does not contain free and metavariables. It applies zeta and zetaDelta-reduction to eliminate let-free-vars. @@ -355,8 +358,11 @@ private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do let mut expectedType ← instantiateMVars expectedType if expectedType.hasFVar then expectedType ← zetaReduce expectedType - if expectedType.hasFVar || expectedType.hasMVar then - throwError "expected type must not contain free or meta variables{indentExpr expectedType}" + if expectedType.hasMVar then + throwError "expected type must not contain meta variables{indentExpr expectedType}" + if expectedType.hasFVar then + throwError "expected type must not contain free variables{indentExpr expectedType}\n\ + Use the '+revert' option to automatically cleanup and revert free variables." return expectedType /-- @@ -381,36 +387,96 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := wi return ← blameDecideReductionFailure inst'' return inst -def evalDecideCore (tacticName : Name) (kernelOnly : Bool) : TacticM Unit := +private unsafe def elabNativeDecideCoreUnsafe (tacticName : Name) (expectedType : Expr) : TacticM Expr := do + let d ← mkDecide expectedType + let levels := (collectLevelParams {} expectedType).params.toList + let auxDeclName ← Term.mkAuxName `_nativeDecide + let decl := Declaration.defnDecl { + name := auxDeclName + levelParams := levels + type := mkConst ``Bool + value := d + hints := .abbrev + safety := .safe + } + addAndCompile decl + -- get instance from `d` + let s := d.appArg! + let rflPrf ← mkEqRefl (toExpr true) + let levelParams := levels.map .param + let pf := mkApp3 (mkConst ``of_decide_eq_true) expectedType s <| + mkApp3 (mkConst ``Lean.ofReduceBool) (mkConst auxDeclName levelParams) (toExpr true) rflPrf + try + let lemmaName ← mkAuxLemma levels expectedType pf + return .const lemmaName levelParams + catch ex => + -- Diagnose error + throwError MessageData.ofLazyM (es := #[expectedType]) do + let r ← + try + evalConst Bool auxDeclName + catch ex => + return m!"\ + tactic '{tacticName}' failed, could not evaluate decidable instance. \ + Error: {ex.toMessageData}" + if !r then + return m!"\ + tactic '{tacticName}' evaluated that the proposition\ + {indentExpr expectedType}\n\ + is false" + else + return m!"tactic '{tacticName}' failed. Error: {ex.toMessageData}" + +@[implemented_by elabNativeDecideCoreUnsafe] +private opaque elabNativeDecideCore (tacticName : Name) (expectedType : Expr) : TacticM Expr + +def evalDecideCore (tacticName : Name) (cfg : Parser.Tactic.DecideConfig) : TacticM Unit := do + if cfg.revert then + -- In revert mode: clean up the local context and then revert everything that is left. + liftMetaTactic1 fun g => do + let g ← g.cleanup + let (_, g) ← g.revert (clearAuxDeclsInsteadOfRevert := true) (← g.getDecl).lctx.getFVarIds + return g closeMainGoalUsing tacticName fun expectedType _ => do + if cfg.kernel && cfg.native then + throwError "tactic '{tacticName}' failed, cannot simultaneously set both '+kernel' and '+native'" let expectedType ← preprocessPropToDecide expectedType + if cfg.native then + elabNativeDecideCore tacticName expectedType + else if cfg.kernel then + doKernel expectedType + else + doElab expectedType +where + doElab (expectedType : Expr) : TacticM Expr := do let pf ← mkDecideProof expectedType -- Get instance from `pf` let s := pf.appFn!.appArg! - if kernelOnly then - -- Reduce the decidable instance to (hopefully!) `isTrue` by passing `pf` to the kernel. - -- The `mkAuxLemma` function caches the result in two ways: - -- 1. First, the function makes use of a `type`-indexed cache per module. - -- 2. Second, once the proof is added to the environment, the kernel doesn't need to check the proof again. - let levelsInType := (collectLevelParams {} expectedType).params - -- Level variables occurring in `expectedType`, in ambient order - let lemmaLevels := (← Term.getLevelNames).reverse.filter levelsInType.contains - try - let lemmaName ← mkAuxLemma lemmaLevels expectedType pf - return mkConst lemmaName (lemmaLevels.map .param) - catch _ => - diagnose expectedType s none + let r ← withAtLeastTransparency .default <| whnf s + if r.isAppOf ``isTrue then + -- Success! + -- While we have a proof from reduction, we do not embed it in the proof term, + -- and instead we let the kernel recompute it during type checking from the following more + -- efficient term. The kernel handles the unification `e =?= true` specially. + return pf else - let r ← withAtLeastTransparency .default <| whnf s - if r.isAppOf ``isTrue then - -- Success! - -- While we have a proof from reduction, we do not embed it in the proof term, - -- and instead we let the kernel recompute it during type checking from the following more - -- efficient term. The kernel handles the unification `e =?= true` specially. - return pf - else - diagnose expectedType s r -where + diagnose expectedType s r + doKernel (expectedType : Expr) : TacticM Expr := do + let pf ← mkDecideProof expectedType + -- Get instance from `pf` + let s := pf.appFn!.appArg! + -- Reduce the decidable instance to (hopefully!) `isTrue` by passing `pf` to the kernel. + -- The `mkAuxLemma` function caches the result in two ways: + -- 1. First, the function makes use of a `type`-indexed cache per module. + -- 2. Second, once the proof is added to the environment, the kernel doesn't need to check the proof again. + let levelsInType := (collectLevelParams {} expectedType).params + -- Level variables occurring in `expectedType`, in ambient order + let lemmaLevels := (← Term.getLevelNames).reverse.filter levelsInType.contains + try + let lemmaName ← mkAuxLemma lemmaLevels expectedType pf + return mkConst lemmaName (lemmaLevels.map .param) + catch _ => + diagnose expectedType s none diagnose {α : Type} (expectedType s : Expr) (r? : Option Expr) : TacticM α := -- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively. throwError MessageData.ofLazyM (es := #[expectedType]) do @@ -470,30 +536,20 @@ where did not reduce to '{.ofConstName ``isTrue}' or '{.ofConstName ``isFalse}'.\n\n\ {stuckMsg}{hint}" -@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun _ => - evalDecideCore `decide false +declare_config_elab elabDecideConfig Parser.Tactic.DecideConfig -@[builtin_tactic Lean.Parser.Tactic.decideBang] def evalDecideBang : Tactic := fun _ => - evalDecideCore `decide! true +@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun stx => do + let cfg ← elabDecideConfig stx[1] + evalDecideCore `decide cfg -private def mkNativeAuxDecl (baseName : Name) (type value : Expr) : TermElabM Name := do - let auxName ← Term.mkAuxName baseName - let decl := Declaration.defnDecl { - name := auxName, levelParams := [], type, value - hints := .abbrev - safety := .safe - } - addDecl decl - compileDecl decl - pure auxName +@[builtin_tactic Lean.Parser.Tactic.decideBang] def evalDecideBang : Tactic := fun stx => do + let cfg ← elabDecideConfig stx[1] + let cfg := { cfg with kernel := true } + evalDecideCore `decide! cfg -@[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun _ => - closeMainGoalUsing `nativeDecide fun expectedType _ => do - let expectedType ← preprocessPropToDecide expectedType - let d ← mkDecide expectedType - let auxDeclName ← mkNativeAuxDecl `_nativeDecide (Lean.mkConst `Bool) d - let rflPrf ← mkEqRefl (toExpr true) - let s := d.appArg! -- get instance from `d` - return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s <| mkApp3 (Lean.mkConst ``Lean.ofReduceBool) (Lean.mkConst auxDeclName) (toExpr true) rflPrf +@[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun stx => do + let cfg ← elabDecideConfig stx[1] + let cfg := { cfg with native := true } + evalDecideCore `native_decide cfg end Lean.Elab.Tactic diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean index 2bde2cc08634..d08ce518d95b 100644 --- a/src/Lean/Parser/Tactic.lean +++ b/src/Lean/Parser/Tactic.lean @@ -67,90 +67,6 @@ doing a pattern match. This is equivalent to `fun` with match arms in term mode. @[builtin_tactic_parser] def introMatch := leading_parser nonReservedSymbol "intro" >> matchAlts -/-- -`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p` -and then reducing that instance to evaluate the truth value of `p`. -If it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal. - -Limitations: -- The target is not allowed to contain local variables or metavariables. - If there are local variables, you can try first using the `revert` tactic with these local variables - to move them into the target, which may allow `decide` to succeed. -- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined - by well-founded recursion might not work, because evaluating them requires reducing proofs. - The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions. - These can appear for instances defined using tactics (such as `rw` and `simp`). - To avoid this, use definitions such as `decidable_of_iff` instead. - -## Examples - -Proving inequalities: -```lean -example : 2 + 2 ≠ 5 := by decide -``` - -Trying to prove a false proposition: -```lean -example : 1 ≠ 1 := by decide -/- -tactic 'decide' proved that the proposition - 1 ≠ 1 -is false --/ -``` - -Trying to prove a proposition whose `Decidable` instance fails to reduce -```lean -opaque unknownProp : Prop - -open scoped Classical in -example : unknownProp := by decide -/- -tactic 'decide' failed for proposition - unknownProp -since its 'Decidable' instance reduced to - Classical.choice ⋯ -rather than to the 'isTrue' constructor. --/ -``` - -## Properties and relations - -For equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`. -```lean -example : 1 + 1 = 2 := by decide -example : 1 + 1 = 2 := by rfl -``` --/ -@[builtin_tactic_parser] def decide := leading_parser - nonReservedSymbol "decide" - -/-- -`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal. -It has the following properties: -- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything. -- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds, - and once during kernel type checking), the `decide!` tactic reduces it exactly once. --/ -@[builtin_tactic_parser] def decideBang := leading_parser - nonReservedSymbol "decide!" - -/-- `native_decide` will attempt to prove a goal of type `p` by synthesizing an instance -of `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this -uses `#eval` to evaluate the decidability instance. - -This should be used with care because it adds the entire lean compiler to the trusted -part, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using -this method or anything that transitively depends on them. Nevertheless, because it is -compiled, this can be significantly more efficient than using `decide`, and for very -large computations this is one way to run external programs and trust the result. -``` -example : (List.range 1000).length = 1000 := by native_decide -``` --/ -@[builtin_tactic_parser] def nativeDecide := leading_parser - nonReservedSymbol "native_decide" - builtin_initialize register_parser_alias "matchRhsTacticSeq" matchRhs diff --git a/tests/lean/1825.lean.expected.out b/tests/lean/1825.lean.expected.out index ad5c7a9d63d3..6a0a23d32169 100644 --- a/tests/lean/1825.lean.expected.out +++ b/tests/lean/1825.lean.expected.out @@ -1,6 +1,3 @@ -1825.lean:2:8-2:13: error: application type mismatch - Lean.ofReduceBool boom'._nativeDecide_1 true (Eq.refl true) -argument has type - true = true -but function has type - Lean.reduceBool boom'._nativeDecide_1 = true → boom'._nativeDecide_1 = true +1825.lean:2:71-2:84: error: tactic 'native_decide' evaluated that the proposition + -2147483648 + 2147483648 = -18446744069414584320 +is false diff --git a/tests/lean/interactive/completionTactics.lean.expected.out b/tests/lean/interactive/completionTactics.lean.expected.out index 596dbd0658b6..f68e2e2f77c5 100644 --- a/tests/lean/interactive/completionTactics.lean.expected.out +++ b/tests/lean/interactive/completionTactics.lean.expected.out @@ -4,7 +4,7 @@ {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 23, "character": 21}} {"items": - [{"sortText": "00", + [{"sortText": "0", "label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, @@ -12,29 +12,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 23, "character": 21}}}}, - {"sortText": "01", - "label": "Lean.Parser.Tactic.decide", - "kind": 14, - "documentation": - {"value": - "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n If there are local variables, you can try first using the `revert` tactic with these local variables\n to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n by well-founded recursion might not work, because evaluating them requires reducing proofs.\n The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n These can appear for instances defined using tactics (such as `rw` and `simp`).\n To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n 1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n unknownProp\nsince its 'Decidable' instance reduced to\n Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 23, "character": 21}}}}, - {"sortText": "02", - "label": "Lean.Parser.Tactic.decideBang", - "kind": 14, - "documentation": - {"value": - "`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.\nIt has the following properties:\n- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.\n- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,\n and once during kernel type checking), the `decide!` tactic reduces it exactly once.\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 23, "character": 21}}}}, - {"sortText": "03", + {"sortText": "1", "label": "Lean.Parser.Tactic.introMatch", "kind": 14, "documentation": @@ -45,7 +23,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 23, "character": 21}}}}, - {"sortText": "04", + {"sortText": "2", "label": "Lean.Parser.Tactic.match", "kind": 14, "documentation": @@ -56,25 +34,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 23, "character": 21}}}}, - {"sortText": "05", - "label": "Lean.Parser.Tactic.nativeDecide", - "kind": 14, - "documentation": - {"value": - "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 23, "character": 21}}}}, - {"sortText": "06", + {"sortText": "3", "label": "Lean.Parser.Tactic.nestedTactic", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 23, "character": 21}}}}, - {"sortText": "07", + {"sortText": "4", "label": "Lean.Parser.Tactic.open", "kind": 14, "documentation": @@ -85,7 +52,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 23, "character": 21}}}}, - {"sortText": "08", + {"sortText": "5", "label": "Lean.Parser.Tactic.set_option", "kind": 14, "documentation": @@ -96,14 +63,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 23, "character": 21}}}}, - {"sortText": "09", + {"sortText": "6", "label": "Lean.Parser.Tactic.unknown", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 23, "character": 21}}}}, - {"sortText": "10", + {"sortText": "7", "label": "skip", "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, @@ -115,7 +82,7 @@ {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 26, "character": 24}} {"items": - [{"sortText": "00", + [{"sortText": "0", "label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, @@ -123,29 +90,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 26, "character": 24}}}}, - {"sortText": "01", - "label": "Lean.Parser.Tactic.decide", - "kind": 14, - "documentation": - {"value": - "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n If there are local variables, you can try first using the `revert` tactic with these local variables\n to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n by well-founded recursion might not work, because evaluating them requires reducing proofs.\n The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n These can appear for instances defined using tactics (such as `rw` and `simp`).\n To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n 1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n unknownProp\nsince its 'Decidable' instance reduced to\n Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 26, "character": 24}}}}, - {"sortText": "02", - "label": "Lean.Parser.Tactic.decideBang", - "kind": 14, - "documentation": - {"value": - "`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.\nIt has the following properties:\n- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.\n- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,\n and once during kernel type checking), the `decide!` tactic reduces it exactly once.\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 26, "character": 24}}}}, - {"sortText": "03", + {"sortText": "1", "label": "Lean.Parser.Tactic.introMatch", "kind": 14, "documentation": @@ -156,7 +101,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 26, "character": 24}}}}, - {"sortText": "04", + {"sortText": "2", "label": "Lean.Parser.Tactic.match", "kind": 14, "documentation": @@ -167,25 +112,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 26, "character": 24}}}}, - {"sortText": "05", - "label": "Lean.Parser.Tactic.nativeDecide", - "kind": 14, - "documentation": - {"value": - "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 26, "character": 24}}}}, - {"sortText": "06", + {"sortText": "3", "label": "Lean.Parser.Tactic.nestedTactic", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 26, "character": 24}}}}, - {"sortText": "07", + {"sortText": "4", "label": "Lean.Parser.Tactic.open", "kind": 14, "documentation": @@ -196,7 +130,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 26, "character": 24}}}}, - {"sortText": "08", + {"sortText": "5", "label": "Lean.Parser.Tactic.set_option", "kind": 14, "documentation": @@ -207,14 +141,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 26, "character": 24}}}}, - {"sortText": "09", + {"sortText": "6", "label": "Lean.Parser.Tactic.unknown", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 26, "character": 24}}}}, - {"sortText": "10", + {"sortText": "7", "label": "skip", "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, @@ -229,7 +163,7 @@ {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 32, "character": 26}} {"items": - [{"sortText": "00", + [{"sortText": "0", "label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, @@ -237,29 +171,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 32, "character": 26}}}}, - {"sortText": "01", - "label": "Lean.Parser.Tactic.decide", - "kind": 14, - "documentation": - {"value": - "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n If there are local variables, you can try first using the `revert` tactic with these local variables\n to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n by well-founded recursion might not work, because evaluating them requires reducing proofs.\n The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n These can appear for instances defined using tactics (such as `rw` and `simp`).\n To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n 1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n unknownProp\nsince its 'Decidable' instance reduced to\n Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 32, "character": 26}}}}, - {"sortText": "02", - "label": "Lean.Parser.Tactic.decideBang", - "kind": 14, - "documentation": - {"value": - "`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.\nIt has the following properties:\n- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.\n- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,\n and once during kernel type checking), the `decide!` tactic reduces it exactly once.\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 32, "character": 26}}}}, - {"sortText": "03", + {"sortText": "1", "label": "Lean.Parser.Tactic.introMatch", "kind": 14, "documentation": @@ -270,7 +182,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 32, "character": 26}}}}, - {"sortText": "04", + {"sortText": "2", "label": "Lean.Parser.Tactic.match", "kind": 14, "documentation": @@ -281,25 +193,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 32, "character": 26}}}}, - {"sortText": "05", - "label": "Lean.Parser.Tactic.nativeDecide", - "kind": 14, - "documentation": - {"value": - "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 32, "character": 26}}}}, - {"sortText": "06", + {"sortText": "3", "label": "Lean.Parser.Tactic.nestedTactic", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 32, "character": 26}}}}, - {"sortText": "07", + {"sortText": "4", "label": "Lean.Parser.Tactic.open", "kind": 14, "documentation": @@ -310,7 +211,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 32, "character": 26}}}}, - {"sortText": "08", + {"sortText": "5", "label": "Lean.Parser.Tactic.set_option", "kind": 14, "documentation": @@ -321,14 +222,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 32, "character": 26}}}}, - {"sortText": "09", + {"sortText": "6", "label": "Lean.Parser.Tactic.unknown", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 32, "character": 26}}}}, - {"sortText": "10", + {"sortText": "7", "label": "skip", "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, @@ -340,7 +241,7 @@ {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 35, "character": 27}} {"items": - [{"sortText": "00", + [{"sortText": "0", "label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, @@ -348,29 +249,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 35, "character": 27}}}}, - {"sortText": "01", - "label": "Lean.Parser.Tactic.decide", - "kind": 14, - "documentation": - {"value": - "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n If there are local variables, you can try first using the `revert` tactic with these local variables\n to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n by well-founded recursion might not work, because evaluating them requires reducing proofs.\n The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n These can appear for instances defined using tactics (such as `rw` and `simp`).\n To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n 1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n unknownProp\nsince its 'Decidable' instance reduced to\n Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 35, "character": 27}}}}, - {"sortText": "02", - "label": "Lean.Parser.Tactic.decideBang", - "kind": 14, - "documentation": - {"value": - "`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.\nIt has the following properties:\n- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.\n- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,\n and once during kernel type checking), the `decide!` tactic reduces it exactly once.\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 35, "character": 27}}}}, - {"sortText": "03", + {"sortText": "1", "label": "Lean.Parser.Tactic.introMatch", "kind": 14, "documentation": @@ -381,7 +260,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 35, "character": 27}}}}, - {"sortText": "04", + {"sortText": "2", "label": "Lean.Parser.Tactic.match", "kind": 14, "documentation": @@ -392,25 +271,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 35, "character": 27}}}}, - {"sortText": "05", - "label": "Lean.Parser.Tactic.nativeDecide", - "kind": 14, - "documentation": - {"value": - "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 35, "character": 27}}}}, - {"sortText": "06", + {"sortText": "3", "label": "Lean.Parser.Tactic.nestedTactic", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 35, "character": 27}}}}, - {"sortText": "07", + {"sortText": "4", "label": "Lean.Parser.Tactic.open", "kind": 14, "documentation": @@ -421,7 +289,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 35, "character": 27}}}}, - {"sortText": "08", + {"sortText": "5", "label": "Lean.Parser.Tactic.set_option", "kind": 14, "documentation": @@ -432,14 +300,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 35, "character": 27}}}}, - {"sortText": "09", + {"sortText": "6", "label": "Lean.Parser.Tactic.unknown", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 35, "character": 27}}}}, - {"sortText": "10", + {"sortText": "7", "label": "skip", "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, @@ -451,7 +319,7 @@ {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 40, "character": 7}} {"items": - [{"sortText": "00", + [{"sortText": "0", "label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, @@ -459,29 +327,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 40, "character": 7}}}}, - {"sortText": "01", - "label": "Lean.Parser.Tactic.decide", - "kind": 14, - "documentation": - {"value": - "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n If there are local variables, you can try first using the `revert` tactic with these local variables\n to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n by well-founded recursion might not work, because evaluating them requires reducing proofs.\n The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n These can appear for instances defined using tactics (such as `rw` and `simp`).\n To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n 1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n unknownProp\nsince its 'Decidable' instance reduced to\n Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 40, "character": 7}}}}, - {"sortText": "02", - "label": "Lean.Parser.Tactic.decideBang", - "kind": 14, - "documentation": - {"value": - "`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.\nIt has the following properties:\n- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.\n- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,\n and once during kernel type checking), the `decide!` tactic reduces it exactly once.\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 40, "character": 7}}}}, - {"sortText": "03", + {"sortText": "1", "label": "Lean.Parser.Tactic.introMatch", "kind": 14, "documentation": @@ -492,7 +338,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 40, "character": 7}}}}, - {"sortText": "04", + {"sortText": "2", "label": "Lean.Parser.Tactic.match", "kind": 14, "documentation": @@ -503,25 +349,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 40, "character": 7}}}}, - {"sortText": "05", - "label": "Lean.Parser.Tactic.nativeDecide", - "kind": 14, - "documentation": - {"value": - "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 40, "character": 7}}}}, - {"sortText": "06", + {"sortText": "3", "label": "Lean.Parser.Tactic.nestedTactic", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 40, "character": 7}}}}, - {"sortText": "07", + {"sortText": "4", "label": "Lean.Parser.Tactic.open", "kind": 14, "documentation": @@ -532,7 +367,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 40, "character": 7}}}}, - {"sortText": "08", + {"sortText": "5", "label": "Lean.Parser.Tactic.set_option", "kind": 14, "documentation": @@ -543,14 +378,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 40, "character": 7}}}}, - {"sortText": "09", + {"sortText": "6", "label": "Lean.Parser.Tactic.unknown", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 40, "character": 7}}}}, - {"sortText": "10", + {"sortText": "7", "label": "skip", "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, @@ -562,7 +397,7 @@ {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 44, "character": 2}} {"items": - [{"sortText": "00", + [{"sortText": "0", "label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, @@ -570,29 +405,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 44, "character": 2}}}}, - {"sortText": "01", - "label": "Lean.Parser.Tactic.decide", - "kind": 14, - "documentation": - {"value": - "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n If there are local variables, you can try first using the `revert` tactic with these local variables\n to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n by well-founded recursion might not work, because evaluating them requires reducing proofs.\n The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n These can appear for instances defined using tactics (such as `rw` and `simp`).\n To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n 1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n unknownProp\nsince its 'Decidable' instance reduced to\n Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 44, "character": 2}}}}, - {"sortText": "02", - "label": "Lean.Parser.Tactic.decideBang", - "kind": 14, - "documentation": - {"value": - "`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.\nIt has the following properties:\n- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.\n- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,\n and once during kernel type checking), the `decide!` tactic reduces it exactly once.\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 44, "character": 2}}}}, - {"sortText": "03", + {"sortText": "1", "label": "Lean.Parser.Tactic.introMatch", "kind": 14, "documentation": @@ -603,7 +416,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 44, "character": 2}}}}, - {"sortText": "04", + {"sortText": "2", "label": "Lean.Parser.Tactic.match", "kind": 14, "documentation": @@ -614,25 +427,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 44, "character": 2}}}}, - {"sortText": "05", - "label": "Lean.Parser.Tactic.nativeDecide", - "kind": 14, - "documentation": - {"value": - "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 44, "character": 2}}}}, - {"sortText": "06", + {"sortText": "3", "label": "Lean.Parser.Tactic.nestedTactic", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 44, "character": 2}}}}, - {"sortText": "07", + {"sortText": "4", "label": "Lean.Parser.Tactic.open", "kind": 14, "documentation": @@ -643,7 +445,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 44, "character": 2}}}}, - {"sortText": "08", + {"sortText": "5", "label": "Lean.Parser.Tactic.set_option", "kind": 14, "documentation": @@ -654,14 +456,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 44, "character": 2}}}}, - {"sortText": "09", + {"sortText": "6", "label": "Lean.Parser.Tactic.unknown", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 44, "character": 2}}}}, - {"sortText": "10", + {"sortText": "7", "label": "skip", "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, @@ -673,7 +475,7 @@ {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 49, "character": 2}} {"items": - [{"sortText": "00", + [{"sortText": "0", "label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, @@ -681,29 +483,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 49, "character": 2}}}}, - {"sortText": "01", - "label": "Lean.Parser.Tactic.decide", - "kind": 14, - "documentation": - {"value": - "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n If there are local variables, you can try first using the `revert` tactic with these local variables\n to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n by well-founded recursion might not work, because evaluating them requires reducing proofs.\n The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n These can appear for instances defined using tactics (such as `rw` and `simp`).\n To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n 1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n unknownProp\nsince its 'Decidable' instance reduced to\n Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 49, "character": 2}}}}, - {"sortText": "02", - "label": "Lean.Parser.Tactic.decideBang", - "kind": 14, - "documentation": - {"value": - "`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.\nIt has the following properties:\n- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.\n- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,\n and once during kernel type checking), the `decide!` tactic reduces it exactly once.\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 49, "character": 2}}}}, - {"sortText": "03", + {"sortText": "1", "label": "Lean.Parser.Tactic.introMatch", "kind": 14, "documentation": @@ -714,7 +494,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 49, "character": 2}}}}, - {"sortText": "04", + {"sortText": "2", "label": "Lean.Parser.Tactic.match", "kind": 14, "documentation": @@ -725,25 +505,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 49, "character": 2}}}}, - {"sortText": "05", - "label": "Lean.Parser.Tactic.nativeDecide", - "kind": 14, - "documentation": - {"value": - "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 49, "character": 2}}}}, - {"sortText": "06", + {"sortText": "3", "label": "Lean.Parser.Tactic.nestedTactic", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 49, "character": 2}}}}, - {"sortText": "07", + {"sortText": "4", "label": "Lean.Parser.Tactic.open", "kind": 14, "documentation": @@ -754,7 +523,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 49, "character": 2}}}}, - {"sortText": "08", + {"sortText": "5", "label": "Lean.Parser.Tactic.set_option", "kind": 14, "documentation": @@ -765,14 +534,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 49, "character": 2}}}}, - {"sortText": "09", + {"sortText": "6", "label": "Lean.Parser.Tactic.unknown", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 49, "character": 2}}}}, - {"sortText": "10", + {"sortText": "7", "label": "skip", "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, @@ -784,7 +553,7 @@ {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 53, "character": 2}} {"items": - [{"sortText": "00", + [{"sortText": "0", "label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, @@ -792,29 +561,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 53, "character": 2}}}}, - {"sortText": "01", - "label": "Lean.Parser.Tactic.decide", - "kind": 14, - "documentation": - {"value": - "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n If there are local variables, you can try first using the `revert` tactic with these local variables\n to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n by well-founded recursion might not work, because evaluating them requires reducing proofs.\n The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n These can appear for instances defined using tactics (such as `rw` and `simp`).\n To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n 1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n unknownProp\nsince its 'Decidable' instance reduced to\n Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 53, "character": 2}}}}, - {"sortText": "02", - "label": "Lean.Parser.Tactic.decideBang", - "kind": 14, - "documentation": - {"value": - "`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.\nIt has the following properties:\n- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.\n- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,\n and once during kernel type checking), the `decide!` tactic reduces it exactly once.\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 53, "character": 2}}}}, - {"sortText": "03", + {"sortText": "1", "label": "Lean.Parser.Tactic.introMatch", "kind": 14, "documentation": @@ -825,7 +572,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 53, "character": 2}}}}, - {"sortText": "04", + {"sortText": "2", "label": "Lean.Parser.Tactic.match", "kind": 14, "documentation": @@ -836,25 +583,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 53, "character": 2}}}}, - {"sortText": "05", - "label": "Lean.Parser.Tactic.nativeDecide", - "kind": 14, - "documentation": - {"value": - "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 53, "character": 2}}}}, - {"sortText": "06", + {"sortText": "3", "label": "Lean.Parser.Tactic.nestedTactic", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 53, "character": 2}}}}, - {"sortText": "07", + {"sortText": "4", "label": "Lean.Parser.Tactic.open", "kind": 14, "documentation": @@ -865,7 +601,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 53, "character": 2}}}}, - {"sortText": "08", + {"sortText": "5", "label": "Lean.Parser.Tactic.set_option", "kind": 14, "documentation": @@ -876,14 +612,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 53, "character": 2}}}}, - {"sortText": "09", + {"sortText": "6", "label": "Lean.Parser.Tactic.unknown", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 53, "character": 2}}}}, - {"sortText": "10", + {"sortText": "7", "label": "skip", "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, @@ -895,7 +631,7 @@ {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 59, "character": 4}} {"items": - [{"sortText": "00", + [{"sortText": "0", "label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, @@ -903,29 +639,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 59, "character": 4}}}}, - {"sortText": "01", - "label": "Lean.Parser.Tactic.decide", - "kind": 14, - "documentation": - {"value": - "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n If there are local variables, you can try first using the `revert` tactic with these local variables\n to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n by well-founded recursion might not work, because evaluating them requires reducing proofs.\n The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n These can appear for instances defined using tactics (such as `rw` and `simp`).\n To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n 1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n unknownProp\nsince its 'Decidable' instance reduced to\n Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 59, "character": 4}}}}, - {"sortText": "02", - "label": "Lean.Parser.Tactic.decideBang", - "kind": 14, - "documentation": - {"value": - "`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.\nIt has the following properties:\n- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.\n- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,\n and once during kernel type checking), the `decide!` tactic reduces it exactly once.\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 59, "character": 4}}}}, - {"sortText": "03", + {"sortText": "1", "label": "Lean.Parser.Tactic.introMatch", "kind": 14, "documentation": @@ -936,7 +650,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 59, "character": 4}}}}, - {"sortText": "04", + {"sortText": "2", "label": "Lean.Parser.Tactic.match", "kind": 14, "documentation": @@ -947,25 +661,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 59, "character": 4}}}}, - {"sortText": "05", - "label": "Lean.Parser.Tactic.nativeDecide", - "kind": 14, - "documentation": - {"value": - "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 59, "character": 4}}}}, - {"sortText": "06", + {"sortText": "3", "label": "Lean.Parser.Tactic.nestedTactic", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 59, "character": 4}}}}, - {"sortText": "07", + {"sortText": "4", "label": "Lean.Parser.Tactic.open", "kind": 14, "documentation": @@ -976,7 +679,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 59, "character": 4}}}}, - {"sortText": "08", + {"sortText": "5", "label": "Lean.Parser.Tactic.set_option", "kind": 14, "documentation": @@ -987,14 +690,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 59, "character": 4}}}}, - {"sortText": "09", + {"sortText": "6", "label": "Lean.Parser.Tactic.unknown", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 59, "character": 4}}}}, - {"sortText": "10", + {"sortText": "7", "label": "skip", "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, @@ -1006,7 +709,7 @@ {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 64, "character": 2}} {"items": - [{"sortText": "00", + [{"sortText": "0", "label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, @@ -1014,29 +717,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 64, "character": 2}}}}, - {"sortText": "01", - "label": "Lean.Parser.Tactic.decide", - "kind": 14, - "documentation": - {"value": - "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n If there are local variables, you can try first using the `revert` tactic with these local variables\n to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n by well-founded recursion might not work, because evaluating them requires reducing proofs.\n The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n These can appear for instances defined using tactics (such as `rw` and `simp`).\n To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n 1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n unknownProp\nsince its 'Decidable' instance reduced to\n Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 64, "character": 2}}}}, - {"sortText": "02", - "label": "Lean.Parser.Tactic.decideBang", - "kind": 14, - "documentation": - {"value": - "`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.\nIt has the following properties:\n- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.\n- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,\n and once during kernel type checking), the `decide!` tactic reduces it exactly once.\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 64, "character": 2}}}}, - {"sortText": "03", + {"sortText": "1", "label": "Lean.Parser.Tactic.introMatch", "kind": 14, "documentation": @@ -1047,7 +728,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 64, "character": 2}}}}, - {"sortText": "04", + {"sortText": "2", "label": "Lean.Parser.Tactic.match", "kind": 14, "documentation": @@ -1058,25 +739,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 64, "character": 2}}}}, - {"sortText": "05", - "label": "Lean.Parser.Tactic.nativeDecide", - "kind": 14, - "documentation": - {"value": - "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 64, "character": 2}}}}, - {"sortText": "06", + {"sortText": "3", "label": "Lean.Parser.Tactic.nestedTactic", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 64, "character": 2}}}}, - {"sortText": "07", + {"sortText": "4", "label": "Lean.Parser.Tactic.open", "kind": 14, "documentation": @@ -1087,7 +757,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 64, "character": 2}}}}, - {"sortText": "08", + {"sortText": "5", "label": "Lean.Parser.Tactic.set_option", "kind": 14, "documentation": @@ -1098,14 +768,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 64, "character": 2}}}}, - {"sortText": "09", + {"sortText": "6", "label": "Lean.Parser.Tactic.unknown", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 64, "character": 2}}}}, - {"sortText": "10", + {"sortText": "7", "label": "skip", "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, @@ -1117,7 +787,7 @@ {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 70, "character": 4}} {"items": - [{"sortText": "00", + [{"sortText": "0", "label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, @@ -1125,29 +795,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 70, "character": 4}}}}, - {"sortText": "01", - "label": "Lean.Parser.Tactic.decide", - "kind": 14, - "documentation": - {"value": - "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n If there are local variables, you can try first using the `revert` tactic with these local variables\n to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n by well-founded recursion might not work, because evaluating them requires reducing proofs.\n The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n These can appear for instances defined using tactics (such as `rw` and `simp`).\n To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n 1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n unknownProp\nsince its 'Decidable' instance reduced to\n Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 70, "character": 4}}}}, - {"sortText": "02", - "label": "Lean.Parser.Tactic.decideBang", - "kind": 14, - "documentation": - {"value": - "`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.\nIt has the following properties:\n- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.\n- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,\n and once during kernel type checking), the `decide!` tactic reduces it exactly once.\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 70, "character": 4}}}}, - {"sortText": "03", + {"sortText": "1", "label": "Lean.Parser.Tactic.introMatch", "kind": 14, "documentation": @@ -1158,7 +806,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 70, "character": 4}}}}, - {"sortText": "04", + {"sortText": "2", "label": "Lean.Parser.Tactic.match", "kind": 14, "documentation": @@ -1169,25 +817,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 70, "character": 4}}}}, - {"sortText": "05", - "label": "Lean.Parser.Tactic.nativeDecide", - "kind": 14, - "documentation": - {"value": - "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 70, "character": 4}}}}, - {"sortText": "06", + {"sortText": "3", "label": "Lean.Parser.Tactic.nestedTactic", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 70, "character": 4}}}}, - {"sortText": "07", + {"sortText": "4", "label": "Lean.Parser.Tactic.open", "kind": 14, "documentation": @@ -1198,7 +835,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 70, "character": 4}}}}, - {"sortText": "08", + {"sortText": "5", "label": "Lean.Parser.Tactic.set_option", "kind": 14, "documentation": @@ -1209,14 +846,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 70, "character": 4}}}}, - {"sortText": "09", + {"sortText": "6", "label": "Lean.Parser.Tactic.unknown", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 70, "character": 4}}}}, - {"sortText": "10", + {"sortText": "7", "label": "skip", "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, @@ -1228,7 +865,7 @@ {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 76, "character": 2}} {"items": - [{"sortText": "00", + [{"sortText": "0", "label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, @@ -1236,29 +873,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 76, "character": 2}}}}, - {"sortText": "01", - "label": "Lean.Parser.Tactic.decide", - "kind": 14, - "documentation": - {"value": - "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n If there are local variables, you can try first using the `revert` tactic with these local variables\n to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n by well-founded recursion might not work, because evaluating them requires reducing proofs.\n The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n These can appear for instances defined using tactics (such as `rw` and `simp`).\n To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n 1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n unknownProp\nsince its 'Decidable' instance reduced to\n Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 76, "character": 2}}}}, - {"sortText": "02", - "label": "Lean.Parser.Tactic.decideBang", - "kind": 14, - "documentation": - {"value": - "`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.\nIt has the following properties:\n- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.\n- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,\n and once during kernel type checking), the `decide!` tactic reduces it exactly once.\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 76, "character": 2}}}}, - {"sortText": "03", + {"sortText": "1", "label": "Lean.Parser.Tactic.introMatch", "kind": 14, "documentation": @@ -1269,7 +884,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 76, "character": 2}}}}, - {"sortText": "04", + {"sortText": "2", "label": "Lean.Parser.Tactic.match", "kind": 14, "documentation": @@ -1280,25 +895,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 76, "character": 2}}}}, - {"sortText": "05", - "label": "Lean.Parser.Tactic.nativeDecide", - "kind": 14, - "documentation": - {"value": - "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 76, "character": 2}}}}, - {"sortText": "06", + {"sortText": "3", "label": "Lean.Parser.Tactic.nestedTactic", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 76, "character": 2}}}}, - {"sortText": "07", + {"sortText": "4", "label": "Lean.Parser.Tactic.open", "kind": 14, "documentation": @@ -1309,7 +913,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 76, "character": 2}}}}, - {"sortText": "08", + {"sortText": "5", "label": "Lean.Parser.Tactic.set_option", "kind": 14, "documentation": @@ -1320,14 +924,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 76, "character": 2}}}}, - {"sortText": "09", + {"sortText": "6", "label": "Lean.Parser.Tactic.unknown", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 76, "character": 2}}}}, - {"sortText": "10", + {"sortText": "7", "label": "skip", "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, @@ -1342,7 +946,7 @@ {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 86, "character": 2}} {"items": - [{"sortText": "00", + [{"sortText": "0", "label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, @@ -1350,29 +954,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 86, "character": 2}}}}, - {"sortText": "01", - "label": "Lean.Parser.Tactic.decide", - "kind": 14, - "documentation": - {"value": - "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n If there are local variables, you can try first using the `revert` tactic with these local variables\n to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n by well-founded recursion might not work, because evaluating them requires reducing proofs.\n The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n These can appear for instances defined using tactics (such as `rw` and `simp`).\n To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n 1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n unknownProp\nsince its 'Decidable' instance reduced to\n Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 86, "character": 2}}}}, - {"sortText": "02", - "label": "Lean.Parser.Tactic.decideBang", - "kind": 14, - "documentation": - {"value": - "`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.\nIt has the following properties:\n- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.\n- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,\n and once during kernel type checking), the `decide!` tactic reduces it exactly once.\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 86, "character": 2}}}}, - {"sortText": "03", + {"sortText": "1", "label": "Lean.Parser.Tactic.introMatch", "kind": 14, "documentation": @@ -1383,7 +965,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 86, "character": 2}}}}, - {"sortText": "04", + {"sortText": "2", "label": "Lean.Parser.Tactic.match", "kind": 14, "documentation": @@ -1394,25 +976,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 86, "character": 2}}}}, - {"sortText": "05", - "label": "Lean.Parser.Tactic.nativeDecide", - "kind": 14, - "documentation": - {"value": - "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 86, "character": 2}}}}, - {"sortText": "06", + {"sortText": "3", "label": "Lean.Parser.Tactic.nestedTactic", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 86, "character": 2}}}}, - {"sortText": "07", + {"sortText": "4", "label": "Lean.Parser.Tactic.open", "kind": 14, "documentation": @@ -1423,7 +994,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 86, "character": 2}}}}, - {"sortText": "08", + {"sortText": "5", "label": "Lean.Parser.Tactic.set_option", "kind": 14, "documentation": @@ -1434,14 +1005,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 86, "character": 2}}}}, - {"sortText": "09", + {"sortText": "6", "label": "Lean.Parser.Tactic.unknown", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 86, "character": 2}}}}, - {"sortText": "10", + {"sortText": "7", "label": "skip", "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, @@ -1453,7 +1024,7 @@ {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 91, "character": 4}} {"items": - [{"sortText": "00", + [{"sortText": "0", "label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, @@ -1461,29 +1032,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 91, "character": 4}}}}, - {"sortText": "01", - "label": "Lean.Parser.Tactic.decide", - "kind": 14, - "documentation": - {"value": - "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n If there are local variables, you can try first using the `revert` tactic with these local variables\n to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n by well-founded recursion might not work, because evaluating them requires reducing proofs.\n The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n These can appear for instances defined using tactics (such as `rw` and `simp`).\n To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n 1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n unknownProp\nsince its 'Decidable' instance reduced to\n Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 91, "character": 4}}}}, - {"sortText": "02", - "label": "Lean.Parser.Tactic.decideBang", - "kind": 14, - "documentation": - {"value": - "`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.\nIt has the following properties:\n- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.\n- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,\n and once during kernel type checking), the `decide!` tactic reduces it exactly once.\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 91, "character": 4}}}}, - {"sortText": "03", + {"sortText": "1", "label": "Lean.Parser.Tactic.introMatch", "kind": 14, "documentation": @@ -1494,7 +1043,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 91, "character": 4}}}}, - {"sortText": "04", + {"sortText": "2", "label": "Lean.Parser.Tactic.match", "kind": 14, "documentation": @@ -1505,25 +1054,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 91, "character": 4}}}}, - {"sortText": "05", - "label": "Lean.Parser.Tactic.nativeDecide", - "kind": 14, - "documentation": - {"value": - "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 91, "character": 4}}}}, - {"sortText": "06", + {"sortText": "3", "label": "Lean.Parser.Tactic.nestedTactic", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 91, "character": 4}}}}, - {"sortText": "07", + {"sortText": "4", "label": "Lean.Parser.Tactic.open", "kind": 14, "documentation": @@ -1534,7 +1072,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 91, "character": 4}}}}, - {"sortText": "08", + {"sortText": "5", "label": "Lean.Parser.Tactic.set_option", "kind": 14, "documentation": @@ -1545,14 +1083,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 91, "character": 4}}}}, - {"sortText": "09", + {"sortText": "6", "label": "Lean.Parser.Tactic.unknown", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 91, "character": 4}}}}, - {"sortText": "10", + {"sortText": "7", "label": "skip", "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, @@ -1564,7 +1102,7 @@ {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 96, "character": 2}} {"items": - [{"sortText": "00", + [{"sortText": "0", "label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, @@ -1572,29 +1110,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 96, "character": 2}}}}, - {"sortText": "01", - "label": "Lean.Parser.Tactic.decide", - "kind": 14, - "documentation": - {"value": - "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n If there are local variables, you can try first using the `revert` tactic with these local variables\n to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n by well-founded recursion might not work, because evaluating them requires reducing proofs.\n The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n These can appear for instances defined using tactics (such as `rw` and `simp`).\n To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n 1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n unknownProp\nsince its 'Decidable' instance reduced to\n Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 96, "character": 2}}}}, - {"sortText": "02", - "label": "Lean.Parser.Tactic.decideBang", - "kind": 14, - "documentation": - {"value": - "`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.\nIt has the following properties:\n- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.\n- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,\n and once during kernel type checking), the `decide!` tactic reduces it exactly once.\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 96, "character": 2}}}}, - {"sortText": "03", + {"sortText": "1", "label": "Lean.Parser.Tactic.introMatch", "kind": 14, "documentation": @@ -1605,7 +1121,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 96, "character": 2}}}}, - {"sortText": "04", + {"sortText": "2", "label": "Lean.Parser.Tactic.match", "kind": 14, "documentation": @@ -1616,25 +1132,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 96, "character": 2}}}}, - {"sortText": "05", - "label": "Lean.Parser.Tactic.nativeDecide", - "kind": 14, - "documentation": - {"value": - "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 96, "character": 2}}}}, - {"sortText": "06", + {"sortText": "3", "label": "Lean.Parser.Tactic.nestedTactic", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 96, "character": 2}}}}, - {"sortText": "07", + {"sortText": "4", "label": "Lean.Parser.Tactic.open", "kind": 14, "documentation": @@ -1645,7 +1150,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 96, "character": 2}}}}, - {"sortText": "08", + {"sortText": "5", "label": "Lean.Parser.Tactic.set_option", "kind": 14, "documentation": @@ -1656,14 +1161,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 96, "character": 2}}}}, - {"sortText": "09", + {"sortText": "6", "label": "Lean.Parser.Tactic.unknown", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 96, "character": 2}}}}, - {"sortText": "10", + {"sortText": "7", "label": "skip", "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, @@ -1675,7 +1180,7 @@ {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 102, "character": 4}} {"items": - [{"sortText": "00", + [{"sortText": "0", "label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, @@ -1683,29 +1188,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 102, "character": 4}}}}, - {"sortText": "01", - "label": "Lean.Parser.Tactic.decide", - "kind": 14, - "documentation": - {"value": - "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n If there are local variables, you can try first using the `revert` tactic with these local variables\n to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n by well-founded recursion might not work, because evaluating them requires reducing proofs.\n The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n These can appear for instances defined using tactics (such as `rw` and `simp`).\n To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n 1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n unknownProp\nsince its 'Decidable' instance reduced to\n Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 102, "character": 4}}}}, - {"sortText": "02", - "label": "Lean.Parser.Tactic.decideBang", - "kind": 14, - "documentation": - {"value": - "`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.\nIt has the following properties:\n- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.\n- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,\n and once during kernel type checking), the `decide!` tactic reduces it exactly once.\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 102, "character": 4}}}}, - {"sortText": "03", + {"sortText": "1", "label": "Lean.Parser.Tactic.introMatch", "kind": 14, "documentation": @@ -1716,7 +1199,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 102, "character": 4}}}}, - {"sortText": "04", + {"sortText": "2", "label": "Lean.Parser.Tactic.match", "kind": 14, "documentation": @@ -1727,25 +1210,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 102, "character": 4}}}}, - {"sortText": "05", - "label": "Lean.Parser.Tactic.nativeDecide", - "kind": 14, - "documentation": - {"value": - "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 102, "character": 4}}}}, - {"sortText": "06", + {"sortText": "3", "label": "Lean.Parser.Tactic.nestedTactic", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 102, "character": 4}}}}, - {"sortText": "07", + {"sortText": "4", "label": "Lean.Parser.Tactic.open", "kind": 14, "documentation": @@ -1756,7 +1228,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 102, "character": 4}}}}, - {"sortText": "08", + {"sortText": "5", "label": "Lean.Parser.Tactic.set_option", "kind": 14, "documentation": @@ -1767,14 +1239,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 102, "character": 4}}}}, - {"sortText": "09", + {"sortText": "6", "label": "Lean.Parser.Tactic.unknown", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 102, "character": 4}}}}, - {"sortText": "10", + {"sortText": "7", "label": "skip", "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, @@ -1789,7 +1261,7 @@ {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 112, "character": 2}} {"items": - [{"sortText": "00", + [{"sortText": "0", "label": "exact", "kind": 14, "documentation": {"value": "Another docstring ", "kind": "markdown"}, @@ -1797,29 +1269,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 112, "character": 2}}}}, - {"sortText": "01", - "label": "Lean.Parser.Tactic.decide", - "kind": 14, - "documentation": - {"value": - "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n If there are local variables, you can try first using the `revert` tactic with these local variables\n to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n by well-founded recursion might not work, because evaluating them requires reducing proofs.\n The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n These can appear for instances defined using tactics (such as `rw` and `simp`).\n To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n 1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n unknownProp\nsince its 'Decidable' instance reduced to\n Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 112, "character": 2}}}}, - {"sortText": "02", - "label": "Lean.Parser.Tactic.decideBang", - "kind": 14, - "documentation": - {"value": - "`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.\nIt has the following properties:\n- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.\n- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,\n and once during kernel type checking), the `decide!` tactic reduces it exactly once.\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 112, "character": 2}}}}, - {"sortText": "03", + {"sortText": "1", "label": "Lean.Parser.Tactic.introMatch", "kind": 14, "documentation": @@ -1830,7 +1280,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 112, "character": 2}}}}, - {"sortText": "04", + {"sortText": "2", "label": "Lean.Parser.Tactic.match", "kind": 14, "documentation": @@ -1841,25 +1291,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 112, "character": 2}}}}, - {"sortText": "05", - "label": "Lean.Parser.Tactic.nativeDecide", - "kind": 14, - "documentation": - {"value": - "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionTactics.lean"}, - "position": {"line": 112, "character": 2}}}}, - {"sortText": "06", + {"sortText": "3", "label": "Lean.Parser.Tactic.nestedTactic", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 112, "character": 2}}}}, - {"sortText": "07", + {"sortText": "4", "label": "Lean.Parser.Tactic.open", "kind": 14, "documentation": @@ -1870,7 +1309,7 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 112, "character": 2}}}}, - {"sortText": "08", + {"sortText": "5", "label": "Lean.Parser.Tactic.set_option", "kind": 14, "documentation": @@ -1881,14 +1320,14 @@ {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 112, "character": 2}}}}, - {"sortText": "09", + {"sortText": "6", "label": "Lean.Parser.Tactic.unknown", "kind": 14, "data": {"params": {"textDocument": {"uri": "file:///completionTactics.lean"}, "position": {"line": 112, "character": 2}}}}, - {"sortText": "10", + {"sortText": "7", "label": "skip", "kind": 14, "documentation": {"value": "A docstring ", "kind": "markdown"}, diff --git a/tests/lean/run/4306.lean b/tests/lean/run/4306.lean index 5f3920a2f519..9a4d2017035b 100644 --- a/tests/lean/run/4306.lean +++ b/tests/lean/run/4306.lean @@ -11,12 +11,9 @@ info: 12776324570088369205 #eval (123456789012345678901).toUInt64.toNat /-- -error: application type mismatch - Lean.ofReduceBool false._nativeDecide_1 true (Eq.refl true) -argument has type - true = true -but function has type - Lean.reduceBool false._nativeDecide_1 = true → false._nativeDecide_1 = true +error: tactic 'native_decide' evaluated that the proposition + (Nat.toUInt64 123456789012345678901).toNat = 123456789012345678901 +is false -/ #guard_msgs in theorem false : False := by diff --git a/tests/lean/run/decideBang.lean b/tests/lean/run/decideBang.lean index 3bd7f2e9209f..08da5805e5f6 100644 --- a/tests/lean/run/decideBang.lean +++ b/tests/lean/run/decideBang.lean @@ -69,3 +69,28 @@ info: theorem thm1' : ∀ (x : Nat), x < 100 → x * x ≤ 10000 := decideBang._auxLemma.3 -/ #guard_msgs in #print thm1' + + +/-! +Reverting free variables. +-/ + +/-- +error: expected type must not contain free variables + x + 1 ≤ 5 +Use the '+revert' option to automatically cleanup and revert free variables. +-/ +#guard_msgs in +example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by decide! + +example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by decide! +revert + + +/-- +Can handle universe levels. +-/ + +instance (p : PUnit.{u} → Prop) [Decidable (p PUnit.unit)] : Decidable (∀ x : PUnit.{u}, p x) := + decidable_of_iff (p PUnit.unit) (by constructor; rintro _ ⟨⟩; assumption; intro h; apply h) + +example : ∀ (x : PUnit.{u}), x = PUnit.unit := by decide! diff --git a/tests/lean/run/decideNative.lean b/tests/lean/run/decideNative.lean new file mode 100644 index 000000000000..86023ab3324a --- /dev/null +++ b/tests/lean/run/decideNative.lean @@ -0,0 +1,130 @@ +import Lean +/-! +# `native_decide` +-/ + +/-! +Simplest example. +-/ +theorem ex1 : True := by native_decide +/-- info: 'ex1' depends on axioms: [Lean.ofReduceBool] -/ +#guard_msgs in #print axioms ex1 + + +/-! +The decidable instance is only evaluated once. +It is evaluated at elaboration time, hence stdout can be collected by `collect_stdout`. +-/ + +elab "collect_stdout " t:tactic : tactic => do + let (out, _) ← IO.FS.withIsolatedStreams <| Lean.Elab.Tactic.evalTactic t + Lean.logInfo m!"output: {out}" + +def P (n : Nat) := ∃ k, n = 2 * k + +instance instP : DecidablePred P := + fun + | 0 => isTrue ⟨0, rfl⟩ + | 1 => isFalse (by intro ⟨k, h⟩; omega) + | n + 2 => + dbg_trace "step"; + match instP n with + | isTrue h => isTrue (by have ⟨k, h⟩ := h; exact ⟨k + 1, by omega⟩) + | isFalse h => isFalse (by intro ⟨k, h'⟩; apply h; exists k - 1; omega) + +/-- info: output: step -/ +#guard_msgs in example : P 2 := by collect_stdout native_decide + + +/-! +The `native_decide` tactic can fail at elaboration time, rather than waiting until kernel checking. +-/ + +-- Check the error message +/-- +error: tactic 'native_decide' evaluated that the proposition + False +is false +-/ +#guard_msgs in +example : False := by native_decide + +/-- +error: second case +⊢ False +-/ +#guard_msgs in +example : False := by first | native_decide | fail "second case" + + +/-! +Reverting free variables. +-/ + +/-- +error: expected type must not contain free variables + x + 1 ≤ 5 +Use the '+revert' option to automatically cleanup and revert free variables. +-/ +#guard_msgs in +example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by native_decide + +example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by native_decide +revert + + +/-! +Make sure `native_decide` fails at elaboration time. +https://github.com/leanprover/lean4/issues/2072 +-/ + +/-- +error: tactic 'native_decide' evaluated that the proposition + False +is false +--- +info: let_fun this := sorry; +this : False +-/ +#guard_msgs in #check show False by native_decide + + +/-- +Can handle universe levels. +-/ + +instance (p : PUnit.{u} → Prop) [Decidable (p PUnit.unit)] : Decidable (∀ x : PUnit.{u}, p x) := + decidable_of_iff (p PUnit.unit) (by constructor; rintro _ ⟨⟩; assumption; intro h; apply h) + +example : ∀ (x : PUnit.{u}), x = PUnit.unit := by native_decide + + +/-! +Can't evaluate +-/ + +inductive ItsTrue : Prop + | mk + +instance : Decidable ItsTrue := sorry + +/-- +error: tactic 'native_decide' failed, could not evaluate decidable instance. +Error: cannot evaluate code because 'instDecidableItsTrue' uses 'sorry' and/or contains errors +-/ +#guard_msgs in example : ItsTrue := by native_decide + + +/-! +Panic during evaluation +-/ + +inductive ItsTrue2 : Prop + | mk + +instance : Decidable ItsTrue2 := + have : Inhabited (Decidable ItsTrue2) := ⟨isTrue .mk⟩ + panic! "oh no" + +-- Note: this test fails within VS Code +/-- info: output: PANIC at instDecidableItsTrue2 decideNative:126:2: oh no -/ +#guard_msgs in example : ItsTrue2 := by collect_stdout native_decide diff --git a/tests/lean/run/decideTactic.lean b/tests/lean/run/decideTactic.lean index 2b58bdfde78c..e171fa142dc7 100644 --- a/tests/lean/run/decideTactic.lean +++ b/tests/lean/run/decideTactic.lean @@ -52,7 +52,7 @@ example : unknownProp := by decide Reporting unfolded instances and give hint about Eq.rec. From discussion with Heather Macbeth on Zulip -/ -structure Nice (n : Nat) : Prop := +structure Nice (n : Nat) : Prop where (large : 100 ≤ n) theorem nice_iff (n : Nat) : Nice n ↔ 100 ≤ n := ⟨Nice.rec id, Nice.mk⟩ @@ -102,3 +102,28 @@ defined using tactics such as 'rw' or 'simp'. To avoid tactics, make use of func -/ #guard_msgs in example : ¬ Nice 102 := by decide + + +/-! +Reverting free variables. +-/ + +/-- +error: expected type must not contain free variables + x + 1 ≤ 5 +Use the '+revert' option to automatically cleanup and revert free variables. +-/ +#guard_msgs in +example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by decide + +example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by decide +revert + + +/-- +Can handle universe levels. +-/ + +instance (p : PUnit.{u} → Prop) [Decidable (p PUnit.unit)] : Decidable (∀ x : PUnit.{u}, p x) := + decidable_of_iff (p PUnit.unit) (by constructor; rintro _ ⟨⟩; assumption; intro h; apply h) + +example : ∀ (x : PUnit.{u}), x = PUnit.unit := by decide