feat: Let tactic #70

Merged
aniva merged 4 commits from goal/let into dev 2024-04-12 21:42:32 -07:00
3 changed files with 128 additions and 2 deletions

View File

@ -177,6 +177,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
}, },
newMVars, newMVars,
parentMVar? := .some goal, parentMVar? := .some goal,
calcPrevRhs? := .none
} }
catch exception => catch exception =>
return .failure #[← exception.toMessageData.toString] return .failure #[← exception.toMessageData.toString]
@ -249,6 +250,49 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St
}, },
newMVars := nextGoals.toSSet, newMVars := nextGoals.toSSet,
parentMVar? := .some goal, 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 => catch exception =>
return .failure #[← exception.toMessageData.toString] return .failure #[← exception.toMessageData.toString]
@ -280,6 +324,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
newMVars := newMVarSet prevMCtx nextMCtx, newMVars := newMVarSet prevMCtx nextMCtx,
parentMVar? := .some goal, parentMVar? := .some goal,
convMVar? := .some (convRhs, goal), convMVar? := .some (convRhs, goal),
calcPrevRhs? := .none
} }
catch exception => catch exception =>
return .failure #[← exception.toMessageData.toString] return .failure #[← exception.toMessageData.toString]
@ -318,6 +363,7 @@ protected def GoalState.convExit (state: GoalState):
newMVars := newMVarSet prevMCtx nextMCtx, newMVars := newMVarSet prevMCtx nextMCtx,
parentMVar? := .some convGoal, parentMVar? := .some convGoal,
convMVar? := .none convMVar? := .none
calcPrevRhs? := .none
} }
catch exception => catch exception =>
return .failure #[← exception.toMessageData.toString] 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] @[export pantograph_goal_have_m]
def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult :=
runTermElabM <| state.tryHave goalId binderName type 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] @[export pantograph_goal_conv_m]
def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult := def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult :=

View File

@ -542,14 +542,89 @@ def test_calc: TestM Unit := do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome
where where
interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) := interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) :=
let free := [("a", "Nat"), ("b", "Nat"), ("c", "Nat"), ("d", "Nat"), let free := [("a", "Nat"), ("b", "Nat"), ("c", "Nat"), ("d", "Nat"),
("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
buildGoal free target userName? 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) := def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
let tests := [ let tests := [
("Nat.add_comm", test_nat_add_comm false), ("Nat.add_comm", test_nat_add_comm false),
@ -560,6 +635,8 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
("have", test_have), ("have", test_have),
("conv", test_conv), ("conv", test_conv),
("calc", test_calc), ("calc", test_calc),
("let via assign", test_let false),
("let via tryLet", test_let true),
] ]
tests.map (fun (name, test) => (name, proofRunner env test)) tests.map (fun (name, test) => (name, proofRunner env test))