feat: `goalLet` function

This commit is contained in:
Leni Aniva 2024-04-12 21:30:56 -07:00
parent 4ee955c21f
commit 77907fd060
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
3 changed files with 56 additions and 3 deletions

View File

@ -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]

View File

@ -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 :=

View File

@ -548,7 +548,7 @@ def test_calc: TestM Unit := do
("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
buildGoal free target userName?
def test_let: TestM Unit := do
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
@ -565,7 +565,10 @@ def test_let: TestM Unit := do
#[interiorGoal [] "p ¬p"])
let expr := "let b: Nat := _; _"
let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with
let result2 ← match specialized with
| true => state1.tryLet (goalId := 0) (binderName := "b") (type := "Nat")
| false => state1.tryAssign (goalId := 0) (expr := expr)
let state2 ← match result2 with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
@ -627,7 +630,8 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
("have", test_have),
("conv", test_conv),
("calc", test_calc),
("let", test_let),
("let via assign", test_let false),
("let via tryLet", test_let true),
]
tests.map (fun (name, test) => (name, proofRunner env test))