From 09a43990aae8d929ea9ccafd2937d759f626436a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 Feb 2024 10:53:02 -0800 Subject: [PATCH] refactor: move `if-then-else` tactic to `Init` --- src/Init.lean | 1 + src/Init/Tactics.lean | 35 +++++++++++ src/Init/TacticsExtra.lean | 44 ++++++++++++++ src/Lean/Elab/Tactic.lean | 1 - src/Lean/Elab/Tactic/ByCases.lean | 77 ------------------------ tests/lean/bintreeGoal.lean.expected.out | 19 +----- 6 files changed, 81 insertions(+), 96 deletions(-) create mode 100644 src/Init/TacticsExtra.lean delete mode 100644 src/Lean/Elab/Tactic/ByCases.lean diff --git a/src/Init.lean b/src/Init.lean index d23607ad4b..b2800e45b7 100644 --- a/src/Init.lean +++ b/src/Init.lean @@ -7,6 +7,7 @@ prelude import Init.Prelude import Init.Notation import Init.Tactics +import Init.TacticsExtra import Init.Core import Init.Control import Init.Data.Basic diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 4e5e0c417c..8b090cf4c1 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -816,6 +816,41 @@ while `congr 2` produces the intended `⊢ x + y = y + x`. -/ syntax (name := congr) "congr" (ppSpace num)? : tactic + +/-- +In tactic mode, `if h : t then tac1 else tac2` can be used as alternative syntax for: +``` +by_cases h : t +· tac1 +· tac2 +``` +It performs case distinction on `h : t` or `h : ¬t` and `tac1` and `tac2` are the subproofs. + +You can use `?_` or `_` for either subproof to delay the goal to after the tactic, but +if a tactic sequence is provided for `tac1` or `tac2` then it will require the goal to be closed +by the end of the block. +-/ +syntax (name := tacDepIfThenElse) + ppRealGroup(ppRealFill(ppIndent("if " binderIdent " : " term " then") ppSpace matchRhsTacticSeq) + ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic + +/-- +In tactic mode, `if t then tac1 else tac2` is alternative syntax for: +``` +by_cases t +· tac1 +· tac2 +``` +It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous +hypothesis, and `tac1` and `tac2` are the subproofs. (It doesn't actually use +nondependent `if`, since this wouldn't add anything to the context and hence would be +useless for proving theorems. To actually insert an `ite` application use +`refine if t then ?_ else ?_`.) +-/ +syntax (name := tacIfThenElse) + ppRealGroup(ppRealFill(ppIndent("if " term " then") ppSpace matchRhsTacticSeq) + ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic + end Tactic namespace Attr diff --git a/src/Init/TacticsExtra.lean b/src/Init/TacticsExtra.lean new file mode 100644 index 0000000000..1fb5666bb9 --- /dev/null +++ b/src/Init/TacticsExtra.lean @@ -0,0 +1,44 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura, Mario Carneiro +-/ +prelude +import Init.Tactics +import Init.NotationExtra + +/-! +Extra tactics and implementation for some tactics defined at `Init/Tactic.lean` +-/ +namespace Lean.Parser.Tactic + +private def expandIfThenElse + (ifTk thenTk elseTk pos neg : Syntax) + (mkIf : Term → Term → MacroM Term) : MacroM (TSyntax `tactic) := do + let mkCase tk holeOrTacticSeq mkName : MacroM (Term × Array (TSyntax `tactic)) := do + if holeOrTacticSeq.isOfKind `Lean.Parser.Term.syntheticHole then + pure (⟨holeOrTacticSeq⟩, #[]) + else if holeOrTacticSeq.isOfKind `Lean.Parser.Term.hole then + pure (← mkName, #[]) + else + let hole ← withFreshMacroScope mkName + let holeId := hole.raw[1] + let case ← (open TSyntax.Compat in `(tactic| + case $holeId:ident =>%$tk + -- annotate `then/else` with state after `case` + with_annotate_state $tk skip + $holeOrTacticSeq)) + pure (hole, #[case]) + let (posHole, posCase) ← mkCase thenTk pos `(?pos) + let (negHole, negCase) ← mkCase elseTk neg `(?neg) + `(tactic| (open Classical in refine%$ifTk $(← mkIf posHole negHole); $[$(posCase ++ negCase)]*)) + +macro_rules + | `(tactic| if%$tk $h : $c then%$ttk $pos else%$etk $neg) => + expandIfThenElse tk ttk etk pos neg fun pos neg => `(if $h : $c then $pos else $neg) + +macro_rules + | `(tactic| if%$tk $c then%$ttk $pos else%$etk $neg) => + expandIfThenElse tk ttk etk pos neg fun pos neg => `(if h : $c then $pos else $neg) + +end Lean.Parser.Tactic diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean index a6d126fe07..b58a9fd159 100644 --- a/src/Lean/Elab/Tactic.lean +++ b/src/Lean/Elab/Tactic.lean @@ -5,7 +5,6 @@ Authors: Leonardo de Moura, Sebastian Ullrich -/ import Lean.Elab.Term import Lean.Elab.Tactic.Basic -import Lean.Elab.Tactic.ByCases import Lean.Elab.Tactic.ElabTerm import Lean.Elab.Tactic.Induction import Lean.Elab.Tactic.Generalize diff --git a/src/Lean/Elab/Tactic/ByCases.lean b/src/Lean/Elab/Tactic/ByCases.lean deleted file mode 100644 index 410201e4c2..0000000000 --- a/src/Lean/Elab/Tactic/ByCases.lean +++ /dev/null @@ -1,77 +0,0 @@ -/- -Copyright (c) 2022 Mario Carneiro. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Mario Carneiro --/ -import Lean.Parser.Tactic - -/-! -# `by_cases` and `if then else` tactics - -This implements the `if` tactic, which is a structured proof version of `by_cases`. -It allows writing `if h : t then tac1 else tac2` for case analysis on `h : t`, --/ -open Lean Parser.Tactic - -private def expandIfThenElse - (ifTk thenTk elseTk pos neg : Syntax) - (mkIf : Term → Term → MacroM Term) : MacroM (TSyntax `tactic) := do - let mkCase tk holeOrTacticSeq mkName : MacroM (Term × Array (TSyntax `tactic)) := do - if holeOrTacticSeq.isOfKind ``Parser.Term.syntheticHole then - pure (⟨holeOrTacticSeq⟩, #[]) - else if holeOrTacticSeq.isOfKind ``Parser.Term.hole then - pure (← mkName, #[]) - else - let hole ← withFreshMacroScope mkName - let holeId := hole.raw[1] - let case ← (open TSyntax.Compat in `(tactic| - case $holeId:ident =>%$tk - -- annotate `then/else` with state after `case` - with_annotate_state $tk skip - $holeOrTacticSeq)) - pure (hole, #[case]) - let (posHole, posCase) ← mkCase thenTk pos `(?pos) - let (negHole, negCase) ← mkCase elseTk neg `(?neg) - `(tactic| (open Classical in refine%$ifTk $(← mkIf posHole negHole); $[$(posCase ++ negCase)]*)) - -/-- -In tactic mode, `if h : t then tac1 else tac2` can be used as alternative syntax for: -``` -by_cases h : t -· tac1 -· tac2 -``` -It performs case distinction on `h : t` or `h : ¬t` and `tac1` and `tac2` are the subproofs. - -You can use `?_` or `_` for either subproof to delay the goal to after the tactic, but -if a tactic sequence is provided for `tac1` or `tac2` then it will require the goal to be closed -by the end of the block. --/ -syntax (name := tacDepIfThenElse) - ppRealGroup(ppRealFill(ppIndent("if " binderIdent " : " term " then") ppSpace matchRhs) - ppDedent(ppSpace) ppRealFill("else " matchRhs)) : tactic - -/-- -In tactic mode, `if t then tac1 else tac2` is alternative syntax for: -``` -by_cases t -· tac1 -· tac2 -``` -It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous -hypothesis, and `tac1` and `tac2` are the subproofs. (It doesn't actually use -nondependent `if`, since this wouldn't add anything to the context and hence would be -useless for proving theorems. To actually insert an `ite` application use -`refine if t then ?_ else ?_`.) --/ -syntax (name := tacIfThenElse) - ppRealGroup(ppRealFill(ppIndent("if " term " then") ppSpace matchRhs) - ppDedent(ppSpace) ppRealFill("else " matchRhs)) : tactic - -macro_rules - | `(tactic| if%$tk $h : $c then%$ttk $pos else%$etk $neg) => - expandIfThenElse tk ttk etk pos neg fun pos neg => `(if $h : $c then $pos else $neg) - -macro_rules - | `(tactic| if%$tk $c then%$ttk $pos else%$etk $neg) => - expandIfThenElse tk ttk etk pos neg fun pos neg => `(if h : $c then $pos else $neg) diff --git a/tests/lean/bintreeGoal.lean.expected.out b/tests/lean/bintreeGoal.lean.expected.out index 2829f2d73f..e00cc2b9eb 100644 --- a/tests/lean/bintreeGoal.lean.expected.out +++ b/tests/lean/bintreeGoal.lean.expected.out @@ -1,19 +1,2 @@ bintreeGoal.lean:53:4-53:18: warning: declaration uses 'sorry' -bintreeGoal.lean:66:26-66:30: error: unsolved goals -case node.inl.node -β : Type u_1 -b : BinTree β -k : Nat -v : β -left : Tree β -key : Nat -value : β -right : Tree β -ihl : BST left → Tree.find? (Tree.insert left k v) k = some v -ihr : BST right → Tree.find? (Tree.insert right k v) k = some v -h✝ : k < key -a✝³ : BST left -a✝² : ForallTree (fun k v => k < key) left -a✝¹ : BST right -a✝ : ForallTree (fun k v => key < k) right -⊢ BST left +bintreeGoal.lean:60:8-60:27: warning: declaration uses 'sorry'