max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add withReducible <tacticSeq>

Browse source 
Use `try (withReducible rfl)` after `rw` and `erw`
This commit is contained in:
Leonardo de Moura 2020-11-29 16:46:57 -08:00
parent 62639da58c
commit 40e51270f5
2 changed files with 18 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/Init/Notation.lean
View file

@ -134,6 +134,14 @@ syntax[traceState] "traceState" : tactic
syntax[failIfSuccess] "failIfSuccess " tacticSeq : tactic
syntax[generalize] "generalize " atomic(ident " : ")? term:51 " = " ident : tactic
syntax[paren] "(" tacticSeq ")" : tactic
syntax[withReducible] "withReducible " tacticSeq : tactic
syntax:2[orelse] tactic "<|>" tactic:1 : tactic
macro "try " t:tacticSeq : tactic => `(($t) <|> skip)
macro "rfl" : tactic => `(exact rfl)
macro "decide!" : tactic => `(exact decide!)
macro "admit" : tactic => `(exact sorry)
syntax locationWildcard := "*"
syntax locationTarget := "⊢" <|> "|-"
@ -156,23 +164,24 @@ syntax[rwSeq, 1] "rw " rwRuleSeq (location)? : tactic
syntax[erw] "erw " rwRule (location)? : tactic
syntax[erwSeq, 1] "erw " rwRuleSeq (location)? : tactic
private def withCheapRefl (tac : Syntax) : MacroM Syntax :=
`(tactic| $tac; try (withReducible rfl))
@[macro rw]
def expandRw : Macro :=
fun stx => return stx.setKind `Lean.Parser.Tactic.rewrite |>.setArg 0 (mkAtomFrom stx "rewrite")
fun stx => withCheapRefl (stx.setKind `Lean.Parser.Tactic.rewrite |>.setArg 0 (mkAtomFrom stx "rewrite"))
@[macro rwSeq]
def expandRwSeq : Macro :=
fun stx => return stx.setKind `Lean.Parser.Tactic.rewriteSeq |>.setArg 0 (mkAtomFrom stx "rewrite")
fun stx => withCheapRefl (stx.setKind `Lean.Parser.Tactic.rewriteSeq |>.setArg 0 (mkAtomFrom stx "rewrite"))
@[macro erw]
def expandERw : Macro :=
fun stx => return stx.setKind `Lean.Parser.Tactic.erewrite |>.setArg 0 (mkAtomFrom stx "erewrite")
fun stx => withCheapRefl (stx.setKind `Lean.Parser.Tactic.erewrite |>.setArg 0 (mkAtomFrom stx "erewrite"))
@[macro erwSeq]
def expandERwSeq : Macro :=
fun stx => return stx.setKind `Lean.Parser.Tactic.erewriteSeq |>.setArg 0 (mkAtomFrom stx "erewrite")
syntax:2[orelse] tactic "<|>" tactic:1 : tactic
fun stx => withCheapRefl (stx.setKind `Lean.Parser.Tactic.erewriteSeq |>.setArg 0 (mkAtomFrom stx "erewrite"))
syntax[injection] "injection " term (" with " (colGt (ident <|> "_"))+)? : tactic
@ -197,9 +206,6 @@ syntax[introMatch] "intro " matchAlts : tactic
syntax[existsIntro] "exists " term : tactic
macro "rfl" : tactic => `(exact rfl)
macro "decide!" : tactic => `(exact decide!)
macro "admit" : tactic => `(exact sorry)
/- We use a priority > 0, to avoid ambiguity with the builtin `have` notation -/
macro[1] "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
@ -207,6 +213,4 @@ syntax "repeat " tacticSeq : tactic
macro_rules
| `(tactic| repeat $seq) => `(tactic| (($seq); repeat $seq) <|> skip)
macro "try " t:tacticSeq : tactic => `(($t) <|> skip)
end Lean.Parser.Tactic

3
src/Lean/Elab/Tactic/ElabTerm.lean
View file

@ -95,6 +95,9 @@ def evalApplyLikeTactic (tac : MVarId → Expr → MetaM (List MVarId)) (e : Syn
| `(tactic| exists $e) => evalApplyLikeTactic (fun mvarId e => return [(← Meta.existsIntro mvarId e)]) e
| _ => throwUnsupportedSyntax
@[builtinTactic Lean.Parser.Tactic.withReducible] def evalWithReducible : Tactic := fun stx =>
withReducible <| evalTactic stx[1]
/--
Elaborate `stx`. If it a free variable, return it. Otherwise, assert it, and return the free variable.
Note that, the main goal is updated when `Meta.assert` is used in the second case. -/