feat: Select and insert widgets (#7260)

Builds a framework to define widgets allowing users to select some sub-expressions of the main goal to generate a tactic call. Four examples using this framework are included, generating calls to tactics `conv`, `congrm` and `gcongr` and generating new calc steps. Also includes a `calc` tactic code action to start a calc proof.



Co-authored-by: Wojciech Nawrocki <wjnawrocki@protonmail.com>

Author: PatrickMassot

Mathlib.lean

@@ -3229,7 +3229,13 @@ import Mathlib.Tactic.UnsetOption
 import Mathlib.Tactic.Use
 import Mathlib.Tactic.Variable
 import Mathlib.Tactic.WLOG
+import Mathlib.Tactic.Widget.Calc
 import Mathlib.Tactic.Widget.CommDiag
+import Mathlib.Tactic.Widget.Congrm
+import Mathlib.Tactic.Widget.Conv
+import Mathlib.Tactic.Widget.Gcongr
+import Mathlib.Tactic.Widget.SelectInsertParamsClass
+import Mathlib.Tactic.Widget.SelectPanelUtils
 import Mathlib.Tactic.Zify
 import Mathlib.Testing.SlimCheck.Functions
 import Mathlib.Testing.SlimCheck.Gen

Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

@@ -372,7 +372,7 @@ theorem exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux (X : Scheme
   exact e
 #align algebraic_geometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux
 
-set_option maxHeartbeats 700000 in
+set_option maxHeartbeats 1000000 in
 theorem exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated (X : Scheme.{u}) (U : Opens X.carrier)
     (hU : IsCompact U.1) (hU' : IsQuasiSeparated U.1) (f : X.presheaf.obj (op U))
     (x : X.presheaf.obj (op <| X.basicOpen f)) :

Mathlib/Tactic.lean

@@ -168,5 +168,11 @@ import Mathlib.Tactic.UnsetOption
 import Mathlib.Tactic.Use
 import Mathlib.Tactic.Variable
 import Mathlib.Tactic.WLOG
+import Mathlib.Tactic.Widget.Calc
 import Mathlib.Tactic.Widget.CommDiag
+import Mathlib.Tactic.Widget.Congrm
+import Mathlib.Tactic.Widget.Conv
+import Mathlib.Tactic.Widget.Gcongr
+import Mathlib.Tactic.Widget.SelectInsertParamsClass
+import Mathlib.Tactic.Widget.SelectPanelUtils
 import Mathlib.Tactic.Zify

Mathlib/Tactic/Widget/Calc.lean

@@ -0,0 +1,142 @@
+/-
+Copyright (c) 2023 Patrick Massot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Patrick Massot
+-/
+
+import Std.CodeAction
+
+import Mathlib.Data.String.Defs
+import Mathlib.Tactic.Widget.SelectPanelUtils
+
+/-! # Calc widget
+
+This file redefines the `calc` tactic so that it displays a widget panel allowing to create
+new calc steps with holes specified by selected sub-expressions in the goal.
+-/
+
+section code_action
+open Std CodeAction
+open Lean Server RequestM
+
+/-- Code action to create a `calc` tactic from the current goal. -/
+@[tactic_code_action calcTactic]
+def createCalc : TacticCodeAction := fun params _snap ctx _stack node => do
+  let .node (.ofTacticInfo info) _ := node | return #[]
+  if info.goalsBefore.isEmpty then return #[]
+  let eager := {
+    title := s!"Generate a calc block."
+    kind? := "quickfix"
+  }
+  let doc ← readDoc
+  return #[{
+    eager
+    lazy? := some do
+      let tacPos := doc.meta.text.utf8PosToLspPos info.stx.getPos?.get!
+      let endPos := doc.meta.text.utf8PosToLspPos info.stx.getTailPos?.get!
+      let goal := info.goalsBefore[0]!
+      let goalFmt ← ctx.runMetaM {} <| goal.withContext do Meta.ppExpr (← goal.getType)
+      return { eager with
+        edit? := some <|.ofTextEdit params.textDocument.uri
+          { range := ⟨tacPos, endPos⟩, newText := s!"calc {goalFmt} := by sorry" }
+      }
+  }]
+end code_action
+
+open ProofWidgets
+open Lean Meta
+
+open Lean Server in
+
+/-- Parameters for the calc widget. -/
+structure CalcParams extends SelectInsertParams where
+  /-- Is this the first calc step? -/
+  isFirst : Bool
+  /-- indentation level of the calc block. -/
+  indent : Nat
+  deriving SelectInsertParamsClass, RpcEncodable
+
+open Lean Meta
+
+/-- Return the link text and inserted text above and below of the calc widget. -/
+def suggestSteps (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr) (params : CalcParams) :
+    MetaM (String × String × Option (String.Pos × String.Pos)) := do
+  let subexprPos := getGoalLocations pos
+  let some (rel, lhs, rhs) ← Lean.Elab.Term.getCalcRelation? goalType |
+      throwError "invalid 'calc' step, relation expected{indentExpr goalType}"
+  let relApp := mkApp2 rel
+    (← mkFreshExprMVar none)
+    (← mkFreshExprMVar none)
+  let some relStr := (← Meta.ppExpr relApp) |> toString |>.splitOn |>.get? 1
+    | throwError "could not find relation symbol in {relApp}"
+  let isSelectedLeft := subexprPos.any (fun L ↦ #[0, 1].isPrefixOf L.toArray)
+  let isSelectedRight := subexprPos.any (fun L ↦ #[1].isPrefixOf L.toArray)
+
+  let mut goalType := goalType
+  for pos in subexprPos do
+    goalType ← insertMetaVar goalType pos
+  let some (_, newLhs, newRhs) ← Lean.Elab.Term.getCalcRelation? goalType | unreachable!
+
+  let lhsStr := (toString <| ← Meta.ppExpr lhs).renameMetaVar
+  let newLhsStr := (toString <| ← Meta.ppExpr newLhs).renameMetaVar
+  let rhsStr := (toString <| ← Meta.ppExpr rhs).renameMetaVar
+  let newRhsStr := (toString <| ← Meta.ppExpr newRhs).renameMetaVar
+
+  let spc := String.replicate params.indent ' '
+  let insertedCode := match isSelectedLeft, isSelectedRight with
+  | true, true =>
+    if params.isFirst then
+      s!"{lhsStr} {relStr} {newLhsStr} := by sorry\n{spc}_ {relStr} {newRhsStr} := by sorry\n" ++
+      s!"{spc}_ {relStr} {rhsStr} := by sorry"
+    else
+      s!"_ {relStr} {newLhsStr} := by sorry\n{spc}_ {relStr} {newRhsStr} := by sorry\n" ++
+      s!"{spc}_ {relStr} {rhsStr} := by sorry"
+  | false, true  =>
+    if params.isFirst then
+      s!"{lhsStr} {relStr} {newRhsStr} := by sorry\n{spc}_ {relStr} {rhsStr} := by sorry"
+    else
+      s!"_ {relStr} {newRhsStr} := by sorry\n{spc}_ {relStr} {rhsStr} := by sorry"
+  | true, false =>
+    if params.isFirst then
+      s!"{lhsStr} {relStr} {newLhsStr} := by sorry\n{spc}_ {relStr} {rhsStr} := by sorry"
+    else
+      s!"_ {relStr} {newLhsStr} := by sorry\n{spc}_ {relStr} {rhsStr} := by sorry"
+  | false, false => "This should not happen"
+
+  let stepInfo := match isSelectedLeft, isSelectedRight with
+  | true, true => "Create two new steps"
+  | true, false | false, true => "Create a new step"
+  | false, false => "This should not happen"
+  let pos : String.Pos := insertedCode.find (fun c => c == '?')
+  return (stepInfo, insertedCode, some (pos, ⟨pos.byteIdx + 2⟩) )
+
+/-- Rpc function for the calc widget. -/
+@[server_rpc_method]
+def CalcPanel.rpc := mkSelectionPanelRPC suggestSteps
+  "Please select subterms."
+  "Calc 🔍"
+
+/-- The calc widget. -/
+@[widget_module]
+def CalcPanel : Component CalcParams :=
+  mk_rpc_widget% CalcPanel.rpc
+
+namespace Lean.Elab.Tactic
+open Meta
+
+/-- Elaborator for the `calc` tactic mode variant with widgets. -/
+elab_rules : tactic
+| `(tactic|calc%$calcstx $stx) => do
+  let steps : TSyntax ``calcSteps := ⟨stx⟩
+  let some calcRange := (← getFileMap).rangeOfStx? calcstx | unreachable!
+  let indent := calcRange.start.character
+  let mut isFirst := true
+  for step in ← Lean.Elab.Term.getCalcSteps steps do
+    let some replaceRange := (← getFileMap).rangeOfStx? step | unreachable!
+    let `(calcStep| $(_) := $proofTerm) := step | unreachable!
+    let json := open scoped ProofWidgets.Json in json% {"replaceRange": $(replaceRange),
+                                                        "isFirst": $(isFirst),
+                                                        "indent": $(indent)}
+    ProofWidgets.savePanelWidgetInfo proofTerm `CalcPanel (pure json)
+    isFirst := false
+  evalCalc (← `(tactic|calc%$calcstx $stx))

Mathlib/Tactic/Widget/Congrm.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2023 Patrick Massot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Patrick Massot
+-/
+
+import Mathlib.Tactic.Widget.SelectPanelUtils
+import Mathlib.Tactic.Congrm
+
+
+/-! # Congrm widget
+
+This file defines a `congrm?` tactic that displays a widget panel allowing to generate
+a `congrm` call with holes specified by selecting subexpressions in the goal.
+-/
+
+open Lean Meta Server ProofWidgets
+
+
+/-! # Gcongr widget -/
+
+/-- Return the link text and inserted text above and below of the congrm widget. -/
+@[nolint unusedArguments]
+def makeCongrmString (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr)
+    (_ : SelectInsertParams) : MetaM (String × String × Option (String.Pos × String.Pos)) := do
+  let subexprPos := getGoalLocations pos
+  unless goalType.isAppOf `Eq || goalType.isAppOf `Iff do
+    throwError "The goal must be an equality or iff."
+  let mut goalTypeWithMetaVars := goalType
+  for pos in subexprPos do
+    goalTypeWithMetaVars ← insertMetaVar goalTypeWithMetaVars pos
+
+  let side := if subexprPos[0]!.toArray[0]! = 0 then 1 else 2
+  let sideExpr := goalTypeWithMetaVars.getAppArgs[side]!
+  let res := "congrm " ++ (toString (← Meta.ppExpr sideExpr)).renameMetaVar
+  return (res, res, none)
+
+/-- Rpc function for the congrm widget. -/
+@[server_rpc_method]
+def CongrmSelectionPanel.rpc := mkSelectionPanelRPC makeCongrmString
+  "Use shift-click to select sub-expressions in the goal that should become holes in congrm."
+  "Congrm 🔍"
+
+/-- The congrm widget. -/
+@[widget_module]
+def CongrmSelectionPanel : Component SelectInsertParams :=
+  mk_rpc_widget% CongrmSelectionPanel.rpc
+
+open scoped Json in
+/-- Display a widget panel allowing to generate a `congrm` call with holes specified by selecting
+subexpressions in the goal.-/
+elab stx:"congrm?" : tactic => do
+  let some replaceRange := (← getFileMap).rangeOfStx? stx | return
+  savePanelWidgetInfo stx ``CongrmSelectionPanel $ pure $ json% { replaceRange: $(replaceRange) }

Mathlib/Tactic/Widget/Conv.lean

@@ -0,0 +1,129 @@
+/-
+Copyright (c) 2023 Robin Böhne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robin Böhne, Wojciech Nawrocki, Patrick Massot
+-/
+import Mathlib.Tactic.Widget.SelectPanelUtils
+import Mathlib.Data.String.Defs
+
+/-! # Conv widget
+
+This is a slightly improved version of one of the examples in the ProofWidget library.
+It defines a `conv?` tactic that displays a widget panel allowing to generate
+a `conv` call zooming to the subexpression selected in the goal.
+-/
+
+
+open Lean Meta Server ProofWidgets
+
+private structure SolveReturn where
+  expr : Expr
+  val? : Option String
+  listRest : List Nat
+
+private def solveLevel (expr : Expr) (path : List Nat) : MetaM SolveReturn := match expr with
+  | Expr.app _ _ => do
+    let mut descExp := expr
+    let mut count := 0
+    let mut explicitList := []
+
+    -- we go through the application until we reach the end, counting how many explicit arguments
+    -- it has and noting whether they are explicit or implicit
+    while descExp.isApp do
+      if (←Lean.Meta.inferType descExp.appFn!).bindingInfo!.isExplicit then
+        explicitList := true::explicitList
+        count := count + 1
+      else
+        explicitList := false::explicitList
+      descExp := descExp.appFn!
+
+    -- we get the correct `enter` command by subtracting the number of `true`s in our list
+    let mut mutablePath := path
+    let mut length := count
+    explicitList := List.reverse explicitList
+    while !mutablePath.isEmpty && mutablePath.head! == 0 do
+      if explicitList.head! == true then
+        count := count - 1
+      explicitList := explicitList.tail!
+      mutablePath := mutablePath.tail!
+
+    let mut nextExp := expr
+    while length > count do
+      nextExp := nextExp.appFn!
+      length := length - 1
+    nextExp := nextExp.appArg!
+
+    let pathRest := if mutablePath.isEmpty then [] else mutablePath.tail!
+
+    return { expr := nextExp, val? := toString count , listRest := pathRest }
+
+  | Expr.lam n _ b _ => do
+    let name := match n with
+      | Name.str _ s => s
+      | _ => panic! "no name found"
+    return { expr := b, val? := name, listRest := path.tail! }
+
+  | Expr.forallE n _ b _ => do
+    let name := match n with
+      | Name.str _ s => s
+      | _ => panic! "no name found"
+    return { expr := b, val? := name, listRest := path.tail! }
+
+  | Expr.mdata _ b => do
+    match b with
+      | Expr.mdata _ _ => return { expr := b, val? := none, listRest := path }
+      | _ => return { expr := b.appFn!.appArg!, val? := none, listRest := path.tail!.tail! }
+
+  | _ => do
+    return {
+      expr := ←(Lean.Core.viewSubexpr path.head! expr)
+      val? := toString (path.head! + 1)
+      listRest := path.tail!
+    }
+
+open Lean Syntax in
+/-- Return the link text and inserted text above and below of the conv widget. -/
+@[nolint unusedArguments]
+def insertEnter (locations : Array Lean.SubExpr.GoalsLocation) (goalType : Expr)
+    (params : SelectInsertParams): MetaM (String × String × Option (String.Pos × String.Pos)) := do
+  let some pos := locations[0]? | throwError "You must select something."
+  let ⟨_, .target subexprPos⟩ := pos | throwError "You must select something in the goal."
+  let mut list := (SubExpr.Pos.toArray subexprPos).toList
+    let mut expr := goalType
+  let mut retList := []
+  -- generate list of commands for `enter`
+  while !list.isEmpty do
+    let res ← solveLevel expr list
+    expr := res.expr
+    retList := match res.val? with
+      | none => retList
+      | some val => val::retList
+    list := res.listRest
+
+  -- build `enter [...]` string
+  retList := List.reverse retList
+  -- prepare `enter` indentation
+  let spc := String.replicate (SelectInsertParamsClass.replaceRange params).start.character ' '
+  let mut enterval := s!"conv =>\n{spc} enter {retList}"
+  if enterval.contains '0' then enterval := "Error: Not a valid conv target"
+  if retList.isEmpty then enterval := ""
+  return ("Generate conv", enterval, none)
+
+/-- Rpc function for the conv widget. -/
+@[server_rpc_method]
+def ConvSelectionPanel.rpc :=
+mkSelectionPanelRPC insertEnter
+  "Use shift-click to select one sub-expression in the goal that you want to zoom on."
+  "Conv 🔍" (onlyOne := true)
+
+/-- The conv widget. -/
+@[widget_module]
+def ConvSelectionPanel : Component SelectInsertParams :=
+  mk_rpc_widget% ConvSelectionPanel.rpc
+
+open scoped Json in
+/-- Display a widget panel allowing to generate a `conv` call zooming to the subexpression selected
+in the goal.-/
+elab stx:"conv?" : tactic => do
+  let some replaceRange := (← getFileMap).rangeOfStx? stx | return
+  savePanelWidgetInfo stx ``ConvSelectionPanel $ pure $ json% { replaceRange: $(replaceRange) }