From abf14f107d45b725fab1bf80de5d1c33a144eedb Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 6 Sep 2023 15:39:55 +1000 Subject: [PATCH 1/6] chore: upstream on_goal / pick_goal / swap --- Std.lean | 1 + Std/Tactic/PermuteGoals.lean | 60 ++++++++++++++++++++++++++++++++++++ test/on_goal.lean | 44 ++++++++++++++++++++++++++ 3 files changed, 105 insertions(+) create mode 100644 Std/Tactic/PermuteGoals.lean create mode 100644 test/on_goal.lean diff --git a/Std.lean b/Std.lean index fc3d44ed55..fe6aed3ada 100644 --- a/Std.lean +++ b/Std.lean @@ -116,6 +116,7 @@ import Std.Tactic.NoMatch import Std.Tactic.NormCast.Ext import Std.Tactic.NormCast.Lemmas import Std.Tactic.OpenPrivate +import Std.Tactic.PermuteGoals import Std.Tactic.PrintDependents import Std.Tactic.RCases import Std.Tactic.Replace diff --git a/Std/Tactic/PermuteGoals.lean b/Std/Tactic/PermuteGoals.lean new file mode 100644 index 0000000000..855bfebed5 --- /dev/null +++ b/Std/Tactic/PermuteGoals.lean @@ -0,0 +1,60 @@ +/- +Copyright (c) 2022 Arthur Paulino. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Arthur Paulino, Mario Carneiro +-/ + +import Lean +import Std.Data.List.Basic + +namespace Mathlib.Tactic + +open Lean Elab.Tactic + +/-- +If the current goals are `g₁ ⋯ gᵢ ⋯ gₙ`, `splitGoalsAndGetNth i` returns +`(gᵢ, [g₁, ⋯, gᵢ₋₁], [gᵢ₊₁, ⋯, gₙ])`. + +If `reverse` is passed as `true`, the `i`-th goal is picked by counting backwards. +For instance, `splitGoalsAndGetNth 1 true` puts the last goal in the first component +of the returned term. +-/ +def splitGoalsAndGetNth (nth : Nat) (reverse : Bool := false) : + TacticM (MVarId × List MVarId × List MVarId) := do + if nth = 0 then throwError "goals are 1-indexed" + let goals ← getGoals + let nGoals := goals.length + if nth > nGoals then throwError "goal index out of bounds" + let n := if ¬reverse then nth - 1 else nGoals - nth + let (gl, g :: gr) := goals.splitAt n | throwNoGoalsToBeSolved + pure (g, gl, gr) + +/-- +`pick_goal n` will move the `n`-th goal to the front. + +`pick_goal -n` will move the `n`-th goal (counting from the bottom) to the front. + +See also `Tactic.rotate_goals`, which moves goals from the front to the back and vice-versa. +-/ +elab "pick_goal " reverse:"-"? n:num : tactic => do + let (g, gl, gr) ← splitGoalsAndGetNth n.1.toNat !reverse.isNone + setGoals $ g :: (gl ++ gr) + +/-- `swap` is a shortcut for `pick_goal 2`, which interchanges the 1st and 2nd goals. -/ +macro "swap" : tactic => `(tactic| pick_goal 2) + +/-- +`on_goal n => tacSeq` creates a block scope for the `n`-th goal and tries the sequence +of tactics `tacSeq` on it. + +`on_goal -n => tacSeq` does the same, but the `n`-th goal is chosen by counting from the +bottom. + +The goal is not required to be solved and any resulting subgoals are inserted back into the +list of goals, replacing the chosen goal. +-/ +elab "on_goal " reverse:"-"? n:num " => " seq:tacticSeq : tactic => do + let (g, gl, gr) ← splitGoalsAndGetNth n.1.toNat !reverse.isNone + setGoals [g] + evalTactic seq + setGoals $ gl ++ (← getUnsolvedGoals) ++ gr diff --git a/test/on_goal.lean b/test/on_goal.lean new file mode 100644 index 0000000000..e669a624f7 --- /dev/null +++ b/test/on_goal.lean @@ -0,0 +1,44 @@ +import Std.Tactic.GuardExpr +import Std.Tactic.PermuteGoals + +example (p q r : Prop) : p → q → r → p ∧ q ∧ r := by + intros + constructor + on_goal 2 => + guard_target = q ∧ r + constructor + assumption + -- Note that we have not closed all the subgoals here. + guard_target = p + assumption + guard_target = r + assumption + +example (p q r : Prop) : p → q → r → p ∧ q ∧ r := by + intros a b c + constructor + fail_if_success on_goal -3 => unreachable! + fail_if_success on_goal -1 => exact a + fail_if_success on_goal 0 => unreachable! + fail_if_success on_goal 2 => exact a + fail_if_success on_goal 3 => unreachable! + on_goal 1 => exact a + constructor + swap + exact c + exact b + +example (p q : Prop) : p → q → p ∧ q := by + intros a b + constructor + fail_if_success pick_goal -3 + fail_if_success pick_goal 0 + fail_if_success pick_goal 3 + pick_goal -1 + exact b + exact a + +example (p : Prop) : p → p := by + intros + fail_if_success swap -- can't swap with a single goal + assumption From 1e8abf103d136727ad10d4f6fd0fa384f72e5ef4 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 6 Sep 2023 15:44:29 +1000 Subject: [PATCH 2/6] module doc --- Std/Tactic/PermuteGoals.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/Std/Tactic/PermuteGoals.lean b/Std/Tactic/PermuteGoals.lean index 855bfebed5..232014198e 100644 --- a/Std/Tactic/PermuteGoals.lean +++ b/Std/Tactic/PermuteGoals.lean @@ -7,6 +7,18 @@ Authors: Arthur Paulino, Mario Carneiro import Lean import Std.Data.List.Basic +/-! +# The `on_goal`, `pick_goal`, and `swap` tactics. + +`pick_goal n` moves the `n`-th goal to the front. If `n` is negative this is counted from the back. + +`on_goal n => tacSeq` focuses on the `n`-th goal and runs a tactic block `tacSeq`. +If `tacSeq` does not close the goal any resulting subgoals are inserted back into the list of goals. +If `n` is negative this is counted from the back. + +`swap` is a shortcut for `pick_goal 2`, which interchanges the 1st and 2nd goals. +-/ + namespace Mathlib.Tactic open Lean Elab.Tactic From ce98ff6f235b6670b0a2e31c8a8144dc52351547 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 6 Sep 2023 16:00:09 +1000 Subject: [PATCH 3/6] chore: upstream classical tactic --- Std.lean | 1 + Std/Tactic/Classical.lean | 51 +++++++++++++++++++++++++++++++++++++++ test/classical.lean | 32 ++++++++++++++++++++++++ 3 files changed, 84 insertions(+) create mode 100644 Std/Tactic/Classical.lean create mode 100644 test/classical.lean diff --git a/Std.lean b/Std.lean index fe6aed3ada..90a4b0cc89 100644 --- a/Std.lean +++ b/Std.lean @@ -97,6 +97,7 @@ import Std.Logic import Std.Tactic.Alias import Std.Tactic.Basic import Std.Tactic.ByCases +import Std.Tactic.Classical import Std.Tactic.CoeExt import Std.Tactic.Congr import Std.Tactic.Exact diff --git a/Std/Tactic/Classical.lean b/Std/Tactic/Classical.lean new file mode 100644 index 0000000000..afedd2b5a2 --- /dev/null +++ b/Std/Tactic/Classical.lean @@ -0,0 +1,51 @@ +/- +Copyright (c) 2021 Mario Carneiro. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mario Carneiro +-/ +import Lean.Elab.ElabRules + +/-! # `classical` and `classical!` tactics -/ + +namespace Mathlib.Tactic +open Lean Meta + +/-- +`classical!` adds a proof of `Classical.propDecidable` as a local variable, which makes it +available for instance search and effectively makes all propositions decidable. +``` +noncomputable def foo : Bool := by + classical! + have := ∀ p, decide p -- uses the classical instance + exact decide (0 < 1) -- uses the classical instance even though `0 < 1` is decidable +``` +Consider using `classical` instead if you want to use the decidable instance when available. +-/ +macro (name := classical!) "classical!" : tactic => + `(tactic| have em := Classical.propDecidable) + +/-- +`classical tacs` runs `tacs` in a scope where `Classical.propDecidable` is a low priority +local instance. It differs from `classical!` in that `classical!` uses a local variable, +which has high priority: +``` +noncomputable def foo : Bool := by + classical! + have := ∀ p, decide p -- uses the classical instance + exact decide (0 < 1) -- uses the classical instance even though `0 < 1` is decidable + +def bar : Bool := by + classical + have := ∀ p, decide p -- uses the classical instance + exact decide (0 < 1) -- uses the decidable instance +``` +Note that (unlike lean 3) `classical` is a scoping tactic - it adds the instance only within the +scope of the tactic. +-/ +-- FIXME: using ppDedent looks good in the common case, but produces the incorrect result when +-- the `classical` does not scope over the rest of the block. +elab "classical" tacs:ppDedent(tacticSeq) : tactic => do + modifyEnv Meta.instanceExtension.pushScope + Meta.addInstance ``Classical.propDecidable .local 10 + try Elab.Tactic.evalTactic tacs + finally modifyEnv Meta.instanceExtension.popScope diff --git a/test/classical.lean b/test/classical.lean new file mode 100644 index 0000000000..a9c527eb75 --- /dev/null +++ b/test/classical.lean @@ -0,0 +1,32 @@ +import Std.Tactic.Classical +import Std.Tactic.PermuteGoals +import Std.Tactic.GuardExpr + +noncomputable example : Bool := by + fail_if_success have := ∀ p, decide p -- no classical in scope + classical! + have := ∀ p, decide p -- uses the classical instance + -- uses the classical instance even though `0 < 1` is decidable + guard_expr decide (0 < 1) = @decide (0 < 1) (‹(a : Prop) → Decidable a› _) + exact decide (0 < 1) + +example : Bool := by + fail_if_success have := ∀ p, decide p -- no classical in scope + classical + have := ∀ p, decide p -- uses the classical instance + guard_expr decide (0 < 1) = @decide (0 < 1) (Nat.decLt 0 1) + exact decide (0 < 1) -- uses the decidable instance + +-- double check no leakage +example : Bool := by + fail_if_success have := ∀ p, decide p -- no classical in scope + exact decide (0 < 1) -- uses the decidable instance + +-- check that classical respects tactic blocks +example : Bool := by + fail_if_success have := ∀ p, decide p -- no classical in scope + on_goal 1 => + classical + have := ∀ p, decide p -- uses the classical instance + fail_if_success have := ∀ p, decide p -- no classical in scope again + exact decide (0 < 1) -- uses the decidable instance From 89e6e2705e22159280ee14d8715ea0b7a0280a90 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 27 Nov 2023 10:10:22 +1100 Subject: [PATCH 4/6] lint --- Std/Tactic/PermuteGoals.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Std/Tactic/PermuteGoals.lean b/Std/Tactic/PermuteGoals.lean index 232014198e..726aa13010 100644 --- a/Std/Tactic/PermuteGoals.lean +++ b/Std/Tactic/PermuteGoals.lean @@ -19,7 +19,7 @@ If `n` is negative this is counted from the back. `swap` is a shortcut for `pick_goal 2`, which interchanges the 1st and 2nd goals. -/ -namespace Mathlib.Tactic +namespace Std.Tactic open Lean Elab.Tactic From a36bc3a98f71706293d450d5b187ef22481f9fb1 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 27 Nov 2023 10:28:59 +1100 Subject: [PATCH 5/6] lint --- Std/Tactic/PermuteGoals.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Std/Tactic/PermuteGoals.lean b/Std/Tactic/PermuteGoals.lean index 726aa13010..e085e8b944 100644 --- a/Std/Tactic/PermuteGoals.lean +++ b/Std/Tactic/PermuteGoals.lean @@ -3,8 +3,6 @@ Copyright (c) 2022 Arthur Paulino. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Arthur Paulino, Mario Carneiro -/ - -import Lean import Std.Data.List.Basic /-! From 8dccbceed56cfba2cf5cc515f242cc45e648bfbf Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 27 Nov 2023 14:48:17 +1100 Subject: [PATCH 6/6] fix namespace --- Std/Tactic/Classical.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Std/Tactic/Classical.lean b/Std/Tactic/Classical.lean index afedd2b5a2..3bd386c858 100644 --- a/Std/Tactic/Classical.lean +++ b/Std/Tactic/Classical.lean @@ -7,7 +7,7 @@ import Lean.Elab.ElabRules /-! # `classical` and `classical!` tactics -/ -namespace Mathlib.Tactic +namespace Std.Tactic open Lean Meta /--