From 2bd187044f7ebcba1200cc582aa2fe4fc7db8554 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 14 Feb 2024 18:22:57 -0800 Subject: [PATCH] chore: builtin `haveI` and `letI` --- src/Init/NotationExtra.lean | 17 +++++++++ src/Init/Tactics.lean | 6 +++ src/Lean/Elab/BuiltinNotation.lean | 25 +++++++++++++ src/Lean/Elab/ElabRules.lean | 8 +--- src/Lean/Elab/Tactic.lean | 1 - src/Lean/Elab/Tactic/HaveI.lean | 59 ------------------------------ src/Lean/Elab/Term.lean | 6 +++ tests/lean/1021.lean.expected.out | 8 ++-- tests/lean/run/haveI.lean | 4 ++ 9 files changed, 63 insertions(+), 71 deletions(-) delete mode 100644 src/Lean/Elab/Tactic/HaveI.lean create mode 100644 tests/lean/run/haveI.lean diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index 239a7fc80c..b420a79858 100644 --- a/src/Init/NotationExtra.lean +++ b/src/Init/NotationExtra.lean @@ -391,6 +391,23 @@ macro_rules `($mods:declModifiers class $id $params* extends $parents,* $[: $ty]? attribute [instance] $ctor) +macro_rules + | `(haveI $hy:hygieneInfo $bs* $[: $ty]? := $val; $body) => + `(haveI $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $ty]? := $val; $body) + | `(haveI _ $bs* := $val; $body) => `(haveI x $bs* : _ := $val; $body) + | `(haveI _ $bs* : $ty := $val; $body) => `(haveI x $bs* : $ty := $val; $body) + | `(haveI $x:ident $bs* := $val; $body) => `(haveI $x $bs* : _ := $val; $body) + | `(haveI $_:ident $_* : $_ := $_; $_) => Lean.Macro.throwUnsupported -- handled by elab + +macro_rules + | `(letI $hy:hygieneInfo $bs* $[: $ty]? := $val; $body) => + `(letI $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $ty]? := $val; $body) + | `(letI _ $bs* := $val; $body) => `(letI x $bs* : _ := $val; $body) + | `(letI _ $bs* : $ty := $val; $body) => `(letI x $bs* : $ty := $val; $body) + | `(letI $x:ident $bs* := $val; $body) => `(letI $x $bs* : _ := $val; $body) + | `(letI $_:ident $_* : $_ := $_; $_) => Lean.Macro.throwUnsupported -- handled by elab + + syntax cdotTk := patternIgnore("· " <|> ". ") /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/ syntax (name := cdot) cdotTk tacticSeqIndentGt : tactic diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 78008cf2a5..3c7e570103 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -944,6 +944,12 @@ macro_rules | `(tactic| and_intros) => `(tactic| repeat' refine And.intro ?_ ?_) /-- The `run_tac doSeq` tactic executes code in `TacticM Unit`. -/ syntax (name := runTac) "run_tac " doSeq : tactic +/-- `haveI` behaves like `have`, but inlines the value instead of producing a `let_fun` term. -/ +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; ?_) + end Tactic namespace Attr diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index ed7a776b02..b94046e20b 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -10,6 +10,7 @@ import Lean.Meta.MatchUtil import Lean.Compiler.ImplementedByAttr import Lean.Elab.SyntheticMVars import Lean.Elab.Eval +import Lean.Elab.Binders namespace Lean.Elab.Term open Meta @@ -467,4 +468,28 @@ def elabUnsafe : TermElab := fun stx expectedType? => (← `(do $cmds))) | _ => throwUnsupportedSyntax +@[builtin_term_elab Lean.Parser.Term.haveI] def elabHaveI : TermElab := fun stx expectedType? => do + match stx with + | `(haveI $x:ident $bs* : $ty := $val; $body) => + withExpectedType expectedType? fun expectedType => do + let (ty, val) ← elabBinders bs fun bs => do + let ty ← elabType ty + let val ← elabTermEnsuringType val ty + pure (← mkForallFVars bs ty, ← mkLambdaFVars bs val) + withLocalDeclD x.getId ty fun x => do + return (← (← elabTerm body expectedType).abstractM #[x]).instantiate #[val] + | _ => throwUnsupportedSyntax + +@[builtin_term_elab Lean.Parser.Term.letI] def elabLetI : TermElab := fun stx expectedType? => do + match stx with + | `(letI $x:ident $bs* : $ty := $val; $body) => + withExpectedType expectedType? fun expectedType => do + let (ty, val) ← elabBinders bs fun bs => do + let ty ← elabType ty + let val ← elabTermEnsuringType val ty + pure (← mkForallFVars bs ty, ← mkLambdaFVars bs val) + withLetDecl x.getId ty val fun x => do + return (← (← elabTerm body expectedType).abstractM #[x]).instantiate #[val] + | _ => throwUnsupportedSyntax + end Lean.Elab.Term diff --git a/src/Lean/Elab/ElabRules.lean b/src/Lean/Elab/ElabRules.lean index 35071ddf51..135393ef67 100644 --- a/src/Lean/Elab/ElabRules.lean +++ b/src/Lean/Elab/ElabRules.lean @@ -11,12 +11,6 @@ open Lean.Syntax open Lean.Parser.Term hiding macroArg open Lean.Parser.Command -def withExpectedType (expectedType? : Option Expr) (x : Expr → TermElabM Expr) : TermElabM Expr := do - Term.tryPostponeIfNoneOrMVar expectedType? - let some expectedType ← pure expectedType? - | throwError "expected type must be known" - x expectedType - def elabElabRulesAux (doc? : Option (TSyntax ``docComment)) (attrs? : Option (TSepArray ``attrInstance ",")) (attrKind : TSyntax ``attrKind) (k : SyntaxNodeKind) (cat? expty? : Option (Ident)) (alts : Array (TSyntax ``matchAlt)) : @@ -54,7 +48,7 @@ def elabElabRulesAux (doc? : Option (TSyntax ``docComment)) if catName == `term then `($[$doc?:docComment]? @[$(← mkAttrs `term_elab),*] aux_def elabRules $(mkIdent k) : Lean.Elab.Term.TermElab := - fun stx expectedType? => Lean.Elab.Command.withExpectedType expectedType? fun $expId => match stx with + fun stx expectedType? => Lean.Elab.Term.withExpectedType expectedType? fun $expId => match stx with $alts:matchAlt* | _ => no_error_if_unused% throwUnsupportedSyntax) else throwErrorAt expId "syntax category '{catName}' does not support expected type specification" diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean index 86a7d6b0a4..b0dc3647c3 100644 --- a/src/Lean/Elab/Tactic.lean +++ b/src/Lean/Elab/Tactic.lean @@ -27,4 +27,3 @@ import Lean.Elab.Tactic.Guard import Lean.Elab.Tactic.RCases import Lean.Elab.Tactic.Repeat import Lean.Elab.Tactic.Change -import Lean.Elab.Tactic.HaveI diff --git a/src/Lean/Elab/Tactic/HaveI.lean b/src/Lean/Elab/Tactic/HaveI.lean deleted file mode 100644 index 01fb27c869..0000000000 --- a/src/Lean/Elab/Tactic/HaveI.lean +++ /dev/null @@ -1,59 +0,0 @@ -/- -Copyright (c) 2022 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Gabriel Ebner --/ -import Lean.Elab.ElabRules -open Lean Elab Parser Term Meta Macro - -/-! -Defines variants of `have` and `let` syntax which do not produce `let_fun` or `let` bindings, -but instead inline the value instead. - -This is useful to declare local instances and proofs in theorem statements -and subgoals, where the extra binding is inconvenient. --/ - -#exit - -namespace Std.Tactic - - -macro_rules - | `(haveI $hy:hygieneInfo $bs* $[: $ty]? := $val; $body) => - `(haveI $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $ty]? := $val; $body) - | `(haveI _ $bs* := $val; $body) => `(haveI x $bs* : _ := $val; $body) - | `(haveI _ $bs* : $ty := $val; $body) => `(haveI x $bs* : $ty := $val; $body) - | `(haveI $x:ident $bs* := $val; $body) => `(haveI $x $bs* : _ := $val; $body) - | `(haveI $_:ident $_* : $_ := $_; $_) => throwUnsupported -- handled by elab - -macro_rules - | `(letI $hy:hygieneInfo $bs* $[: $ty]? := $val; $body) => - `(letI $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $ty]? := $val; $body) - | `(letI _ $bs* := $val; $body) => `(letI x $bs* : _ := $val; $body) - | `(letI _ $bs* : $ty := $val; $body) => `(letI x $bs* : $ty := $val; $body) - | `(letI $x:ident $bs* := $val; $body) => `(letI $x $bs* : _ := $val; $body) - | `(letI $_:ident $_* : $_ := $_; $_) => throwUnsupported -- handled by elab - -elab_rules <= expectedType - | `(haveI $x:ident $bs* : $ty := $val; $body) => do - let (ty, val) ← elabBinders bs fun bs => do - let ty ← elabType ty - let val ← elabTermEnsuringType val ty - pure (← mkForallFVars bs ty, ← mkLambdaFVars bs val) - withLocalDeclD x.getId ty fun x => do - return (← (← elabTerm body expectedType).abstractM #[x]).instantiate #[val] - -elab_rules <= expectedType - | `(letI $x:ident $bs* : $ty := $val; $body) => do - let (ty, val) ← elabBinders bs fun bs => do - let ty ← elabType ty - let val ← elabTermEnsuringType val ty - pure (← mkForallFVars bs ty, ← mkLambdaFVars bs val) - withLetDecl x.getId ty val fun x => do - return (← (← elabTerm body expectedType).abstractM #[x]).instantiate #[val] - -/-- `haveI` behaves like `have`, but inlines the value instead of producing a `let_fun` term. -/ -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; ?_) diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 7ce6f963ea..1de38397f0 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -865,6 +865,12 @@ def tryPostponeIfHasMVars (expectedType? : Option Expr) (msg : String) : TermEla throwError "{msg}, expected type contains metavariables{indentD expectedType?}" return expectedType +def withExpectedType (expectedType? : Option Expr) (x : Expr → TermElabM Expr) : TermElabM Expr := do + tryPostponeIfNoneOrMVar expectedType? + let some expectedType ← pure expectedType? + | throwError "expected type must be known" + x expectedType + /-- Save relevant context for term elaboration postponement. -/ diff --git a/tests/lean/1021.lean.expected.out b/tests/lean/1021.lean.expected.out index 8a4ece1ae3..a673eb54c4 100644 --- a/tests/lean/1021.lean.expected.out +++ b/tests/lean/1021.lean.expected.out @@ -1,8 +1,8 @@ -some { range := { pos := { line := 192, column := 42 }, +some { range := { pos := { line := 193, column := 42 }, charUtf16 := 42, - endPos := { line := 198, column := 31 }, + endPos := { line := 199, column := 31 }, endCharUtf16 := 31 }, - selectionRange := { pos := { line := 192, column := 46 }, + selectionRange := { pos := { line := 193, column := 46 }, charUtf16 := 46, - endPos := { line := 192, column := 58 }, + endPos := { line := 193, column := 58 }, endCharUtf16 := 58 } } diff --git a/tests/lean/run/haveI.lean b/tests/lean/run/haveI.lean new file mode 100644 index 0000000000..6bac90a1dd --- /dev/null +++ b/tests/lean/run/haveI.lean @@ -0,0 +1,4 @@ +example (a : Array α) (x : α) (i : Nat) (h : i < a.size) : + haveI : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt] + (a.push x)[i] = a[i] := by + sorry