Merge pull request 'feat: Let tactic' (#70) from goal/let into dev

Reviewed-on: #70

Pantograph/Goal.lean

@@ -177,6 +177,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
       },
       newMVars,
       parentMVar? := .some goal,
+      calcPrevRhs? := .none
     }
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
@@ -249,6 +250,49 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St
       },
       newMVars := nextGoals.toSSet,
       parentMVar? := .some goal,
+      calcPrevRhs? := .none
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure goal
+    | .none => return .indexError goalId
+  let type ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := type)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  let binderName := binderName.toName
+  try
+    -- Implemented similarly to the intro tactic
+    let nextGoals: List MVarId ← goal.withContext do
+      let type ← Elab.Term.elabType (stx := type)
+      let lctx ← MonadLCtx.getLCtx
+
+      -- The branch goal inherits the same context, but with a different type
+      let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
+
+      let upstreamType := .letE binderName type mvarBranch (← goal.getType) false
+      let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
+        upstreamType (kind := MetavarKind.synthetic) (userName := (← goal.getTag))
+
+      goal.assign mvarUpstream
+
+      pure [mvarBranch.mvarId!, mvarUpstream.mvarId!]
+    return .success {
+      root := state.root,
+      savedState := {
+        term := ← MonadBacktrack.saveState,
+        tactic := { goals := nextGoals }
+      },
+      newMVars := nextGoals.toSSet,
+      parentMVar? := .some goal,
+      calcPrevRhs? := .none
     }
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
@@ -280,6 +324,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
       newMVars := newMVarSet prevMCtx nextMCtx,
       parentMVar? := .some goal,
       convMVar? := .some (convRhs, goal),
+      calcPrevRhs? := .none
     }
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
@@ -318,6 +363,7 @@ protected def GoalState.convExit (state: GoalState):
       newMVars := newMVarSet prevMCtx nextMCtx,
       parentMVar? := .some convGoal,
       convMVar? := .none
+      calcPrevRhs? := .none
     }
   catch exception =>
     return .failure #[← exception.toMessageData.toString]

Pantograph/Library.lean

@@ -169,6 +169,9 @@ def goalAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM Tacti
 @[export pantograph_goal_have_m]
 def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult :=
   runTermElabM <| state.tryHave goalId binderName type
+@[export pantograph_goal_let_m]
+def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult :=
+  runTermElabM <| state.tryLet goalId binderName type
 
 @[export pantograph_goal_conv_m]
 def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult :=

Test/Proofs.lean

@@ -542,14 +542,89 @@ def test_calc: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome
-
-
   where
     interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) :=
       let free := [("a", "Nat"), ("b", "Nat"), ("c", "Nat"), ("d", "Nat"),
         ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
       buildGoal free target userName?
 
+def test_let (specialized: Bool): TestM Unit := do
+  let state? ← startProof (.expr "∀ (a: Nat) (p: Prop), p → p ∨ ¬p")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+  let tactic := "intro a p h"
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[interiorGoal [] "p ∨ ¬p"])
+
+
+  let letType := "Nat"
+  let expr := s!"let b: {letType} := _; _"
+  let result2 ← match specialized with
+    | true => state1.tryLet (goalId := 0) (binderName := "b") (type := letType)
+    | false => state1.tryAssign (goalId := 0) (expr := expr)
+  let state2 ← match result2 with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let serializedState2 ← state2.serializeGoals (options := ← read)
+  addTest $ LSpec.check expr (serializedState2.map (·.devolatilize) =
+    #[
+      interiorGoal [] letType,
+      interiorGoal [] "let b := ?m.20;\np ∨ ¬p"
+    ])
+  -- Check that the goal mvar ids match up
+  addTest $ LSpec.check expr ((serializedState2.map (·.name) |>.get! 0) = "_uniq.20")
+
+  let tactic := "exact a"
+  let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) = #[])
+
+  let state3r ← match state3.continue state2 with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  addTest $ LSpec.check "(continue)" ((← state3r.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[interiorGoal [] "let b := a;\np ∨ ¬p"])
+
+  let tactic := "exact h"
+  match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with
+  | .failure #[message] =>
+    addTest $ LSpec.check tactic  (message = "type mismatch\n  h\nhas type\n  p : Prop\nbut is expected to have type\n  let b := a;\n  p ∨ ¬p : Prop")
+  | other => do
+    addTest $ assertUnreachable $ other.toString
+
+  let tactic := "intro b"
+  let state4 ← match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let tactic := "exact Or.inl h"
+  let state5 ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.test "(5 root)" state5.rootExpr?.isSome
+  where
+    interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) :=
+      let free := [("a", "Nat"), ("p", "Prop"), ("h", "p")] ++ free
+      buildGoal free target userName?
+
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
     ("Nat.add_comm", test_nat_add_comm false),
@@ -560,6 +635,8 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("have", test_have),
     ("conv", test_conv),
     ("calc", test_calc),
+    ("let via assign", test_let false),
+    ("let via tryLet", test_let true),
   ]
   tests.map (fun (name, test) => (name, proofRunner env test))