From ace2ddf478e16b53de86bd42a444108b8bab28a4 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 6 Apr 2024 16:33:20 -0700 Subject: [PATCH 01/19] feat: `GoalState.tryHave` tactic (tests failing) --- Pantograph/Goal.lean | 128 +++++++++++++++++++++++++--------------- Pantograph/Library.lean | 2 +- Pantograph/Serial.lean | 4 +- Test/Metavar.lean | 18 +++--- Test/Proofs.lean | 86 +++++++++++++++++++-------- 5 files changed, 150 insertions(+), 88 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index b56c893..5b6e467 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -10,6 +10,8 @@ def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog := namespace Pantograph open Lean +def filename: String := "" + structure GoalState where savedState : Elab.Tactic.SavedState @@ -18,9 +20,6 @@ structure GoalState where -- New metavariables acquired in this state newMVars: SSet MVarId - -- The id of the goal in the parent - parentGoalId: Nat := 0 - -- Parent state metavariable source parentMVar: Option MVarId @@ -56,7 +55,7 @@ private def GoalState.mvars (state: GoalState): SSet MVarId := state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k private def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit := state.savedState.term.restore -def GoalState.restoreMetaM (state: GoalState): MetaM Unit := +protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit := state.savedState.term.meta.restore /-- Inner function for executing tactic on goal state -/ @@ -89,7 +88,7 @@ inductive TacticResult where | indexError (goalId: Nat) /-- Execute tactic on given state -/ -protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String): +protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String): M TacticResult := do state.restoreElabM let goal ← match state.savedState.tactic.goals.get? goalId with @@ -99,7 +98,7 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String (env := ← MonadEnv.getEnv) (catName := `tactic) (input := tactic) - (fileName := "") with + (fileName := filename) with | .ok stx => pure $ stx | .error error => return .parseError error match (← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic)) with @@ -122,10 +121,48 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String root := state.root, savedState := nextSavedState newMVars, - parentGoalId := goalId, parentMVar := .some goal, } +/-- Assumes elabM has already been restored -/ +protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr): M TacticResult := do + let goalType ← goal.getType + try + let exprType ← Meta.inferType expr + -- This elaboration is necessary + if !(← Meta.isDefEq goalType exprType) then + return .failure #["Type unification failed", toString (← Meta.ppExpr goalType), toString (← Meta.ppExpr exprType)] + goal.checkNotAssigned `GoalState.tryAssign + goal.assign expr + if (← getThe Core.State).messages.hasErrors then + let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray + let errors ← (messages.map Message.data).mapM fun md => md.toString + return .failure errors + else + let prevMCtx := state.savedState.term.meta.meta.mctx + let nextMCtx ← getMCtx + -- Generate a list of mvarIds that exist in the parent state; Also test the + -- assertion that the types have not changed on any mvars. + let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do + if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then + assert! prevMVarDecl.type == mvarDecl.type + return acc + else + return mvarId :: acc + ) [] + let nextGoals ← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned)) + return .success { + root := state.root, + savedState := { + term := ← MonadBacktrack.saveState, + tactic := { goals := nextGoals } + }, + newMVars := newMVars.toSSet, + parentMVar := .some goal, + } + catch exception => + return .failure #[← exception.toMessageData.toString] + protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do state.restoreElabM let goal ← match state.savedState.tactic.goals.get? goalId with @@ -135,50 +172,43 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String (env := state.env) (catName := `term) (input := expr) - (fileName := "") with + (fileName := filename) with | .ok syn => pure syn | .error error => return .parseError error - let tacticM: Elab.Tactic.TacticM TacticResult := do - state.savedState.restore - Elab.Tactic.setGoals [goal] - try - let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none) - -- Attempt to unify the expression - let goalType ← goal.getType - let exprType ← Meta.inferType expr - if !(← Meta.isDefEq goalType exprType) then - return .failure #["Type unification failed", toString (← Meta.ppExpr goalType), toString (← Meta.ppExpr exprType)] - goal.checkNotAssigned `GoalState.tryAssign - goal.assign expr - if (← getThe Core.State).messages.hasErrors then - let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray - let errors ← (messages.map Message.data).mapM fun md => md.toString - return .failure errors - else - let prevMCtx := state.savedState.term.meta.meta.mctx - let nextMCtx ← getMCtx - -- Generate a list of mvarIds that exist in the parent state; Also test the - -- assertion that the types have not changed on any mvars. - let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do - if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then - assert! prevMVarDecl.type == mvarDecl.type - return acc - else - return mvarId :: acc - ) [] - -- The new goals are the newMVars that lack an assignment - Elab.Tactic.setGoals (← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned))) - let nextSavedState ← MonadBacktrack.saveState - return .success { - root := state.root, - savedState := nextSavedState, - newMVars := newMVars.toSSet, - parentGoalId := goalId, - parentMVar := .some goal, - } - catch exception => - return .failure #[← exception.toMessageData.toString] - tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic + let goalType ← goal.getType + try + let expr ← Elab.Term.elabTermAndSynthesize (stx := expr) (expectedType? := .some goalType) + state.assign goal expr + catch exception => + return .failure #[← exception.toMessageData.toString] + +-- Specialized Tactics + +protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): M 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 + try + let type ← Elab.Term.elabType (stx := type) + + -- The branch created by "have" + let mvarBranch ← Meta.mkFreshExprSyntheticOpaqueMVar type + + -- The main branch + let mvarUpstream ← Meta.mkFreshExprSyntheticOpaqueMVar (← goal.getType) + let expr := Expr.app (.lam binderName.toName type mvarBranch .default) mvarUpstream + state.assign goal expr + catch exception => + return .failure #[← exception.toMessageData.toString] + /-- Brings into scope a list of goals diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index d36866a..1d31e97 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -160,7 +160,7 @@ def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) := @[export pantograph_goal_tactic_m] def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult := - runTermElabM <| GoalState.execute state goalId tactic + runTermElabM <| GoalState.tryTactic state goalId tactic @[export pantograph_goal_try_assign_m] def goalTryAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult := diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 8bb61df..6ff8150 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -251,9 +251,7 @@ protected def GoalState.serializeGoals MetaM (Array Protocol.Goal):= do state.restoreMetaM let goals := state.goals.toArray - let parentDecl? := parent.bind (λ parentState => - let parentGoal := parentState.goals.get! state.parentGoalId - parentState.mctx.findDecl? parentGoal) + let parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar.get!) goals.mapM fun goal => do match state.mctx.findDecl? goal with | .some mvarDecl => diff --git a/Test/Metavar.lean b/Test/Metavar.lean index 433326d..1b49e95 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -84,7 +84,7 @@ def test_m_couple: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -93,7 +93,7 @@ def test_m_couple: TestM Unit := do #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"]) addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone -- Set m to 3 - let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 3") with + let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "exact 3") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -116,14 +116,14 @@ def test_m_couple_simp: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) = #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"]) - let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 2") with + let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "exact 2") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -137,7 +137,7 @@ def test_m_couple_simp: TestM Unit := do addTest $ LSpec.check "exact 2" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = #[.some "2 ≤ 2", .some "2 ≤ 5"]) addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone - let state3 ← match ← state1b.execute (goalId := 0) (tactic := "simp") with + let state3 ← match ← state1b.tryTactic (goalId := 0) (tactic := "simp") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -147,7 +147,7 @@ def test_m_couple_simp: TestM Unit := do addTest $ assertUnreachable $ msg return () | .ok state => pure state - let state5 ← match ← state4.execute (goalId := 0) (tactic := "simp") with + let state5 ← match ← state4.tryTactic (goalId := 0) (tactic := "simp") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -174,7 +174,7 @@ def test_proposition_generation: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply PSigma.mk") with + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply PSigma.mk") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -216,7 +216,7 @@ def test_partial_continuation: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -224,7 +224,7 @@ def test_partial_continuation: TestM Unit := do addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) = #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"]) - let state2 ← match ← state1.execute (goalId := 2) (tactic := "apply Nat.succ") with + let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "apply Nat.succ") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString diff --git a/Test/Proofs.lean b/Test/Proofs.lean index a4a1927..91c8f0c 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -75,7 +75,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := example: ∀ (a b: Nat), a + b = b + a := by intro n m rw [Nat.add_comm] -def proof_nat_add_comm (manual: Bool): TestM Unit := do +def test_nat_add_comm (manual: Bool): TestM Unit := do let state? ← startProof <| match manual with | false => .copy "Nat.add_comm" | true => .expr "∀ (a b: Nat), a + b = b + a" @@ -86,7 +86,7 @@ def proof_nat_add_comm (manual: Bool): TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro n m") with + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro n m") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -94,13 +94,13 @@ def proof_nat_add_comm (manual: Bool): TestM Unit := do addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = #[buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"]) - match ← state1.execute (goalId := 0) (tactic := "assumption") with + match ← state1.tryTactic (goalId := 0) (tactic := "assumption") with | .failure #[message] => addTest $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n") | other => do addTest $ assertUnreachable $ other.toString - let state2 ← match ← state1.execute (goalId := 0) (tactic := "rw [Nat.add_comm]") with + let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "rw [Nat.add_comm]") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -108,7 +108,7 @@ def proof_nat_add_comm (manual: Bool): TestM Unit := do addTest $ LSpec.test "rw [Nat.add_comm]" state2.goals.isEmpty return () -def proof_delta_variable: TestM Unit := do +def test_delta_variable: TestM Unit := do let options: Protocol.Options := { noRepeat := true } let state? ← startProof <| .expr "∀ (a b: Nat), a + b = b + a" addTest $ LSpec.check "Start goal" state?.isSome @@ -118,14 +118,14 @@ def proof_delta_variable: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro n") with + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro n") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check "intro n" ((← state1.serializeGoals (parent := state0) options).map (·.devolatilize) = #[buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"]) - let state2 ← match ← state1.execute (goalId := 0) (tactic := "intro m") with + let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "intro m") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -149,7 +149,7 @@ example (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at * assumption -def proof_arith: TestM Unit := do +def test_arith: TestM Unit := do let state? ← startProof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)") let state0 ← match state? with | .some state => pure state @@ -157,21 +157,21 @@ def proof_arith: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let state1 ← match ← state0.execute (goalId := 0) (tactic := "intros") with + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intros") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check "intros" (state1.goals.length = 1) addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone - let state2 ← match ← state1.execute (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with + let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check "simp ..." (state2.goals.length = 1) addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone - let state3 ← match ← state2.execute (goalId := 0) (tactic := "assumption") with + let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := "assumption") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -195,7 +195,7 @@ example: ∀ (p q: Prop), p ∨ q → q ∨ p := by assumption . apply Or.inl assumption -def proof_or_comm: TestM Unit := do +def test_or_comm: TestM Unit := do let state? ← startProof (.expr "∀ (p q: Prop), p ∨ q → q ∨ p") let state0 ← match state? with | .some state => pure state @@ -205,16 +205,16 @@ def proof_or_comm: TestM Unit := do addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone - let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") with + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro p q h") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = + addTest $ LSpec.check "intro p q h" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"]) addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone - let state2 ← match ← state1.execute (goalId := 0) (tactic := "cases h") with + let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "cases h") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -229,7 +229,7 @@ def proof_or_comm: TestM Unit := do addTest $ LSpec.test "(2 parent)" (state2parent == "((:mv _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))") - let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with + let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -237,7 +237,7 @@ def proof_or_comm: TestM Unit := do let state3_1parent ← serialize_expression_ast state3_1.parentExpr?.get! (sanitize := false) addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.78))") addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1) - let state4_1 ← match ← state3_1.execute (goalId := 0) (tactic := "assumption") with + let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -246,13 +246,13 @@ def proof_or_comm: TestM Unit := do let state4_1parent ← serialize_expression_ast state4_1.parentExpr?.get! (sanitize := false) addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.47)") addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone - let state3_2 ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with + let state3_2 ← match ← state2.tryTactic (goalId := 1) (tactic := "apply Or.inl") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check "· apply Or.inl" (state3_2.goals.length = 1) - let state4_2 ← match ← state3_2.execute (goalId := 0) (tactic := "assumption") with + let state4_2 ← match ← state3_2.tryTactic (goalId := 0) (tactic := "assumption") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -266,13 +266,13 @@ def proof_or_comm: TestM Unit := do return () | .ok state => pure state addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals.get! 0]) - let state3_1 ← match ← state2b.execute (goalId := 0) (tactic := "apply Or.inr") with + let state3_1 ← match ← state2b.tryTactic (goalId := 0) (tactic := "apply Or.inr") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1) - let state4_1 ← match ← state3_1.execute (goalId := 0) (tactic := "assumption") with + let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -292,14 +292,48 @@ def proof_or_comm: TestM Unit := do { userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible? := .some true } ] } +def test_have_tactic: TestM Unit := do + let state? ← startProof (.expr "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))") + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone + addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone + + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro p q h") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "intro p q h" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = + #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"]) + + let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "Or.inl (Or.inl h)") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "have" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = + #[buildGoal [] ""]) + + let state2 ← match ← state1.tryHave (goalId := 0) (binderName := "y") (type := "p ∨ q") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "have" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = + #[buildGoal [] ""]) def suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ - ("Nat.add_comm", proof_nat_add_comm false), - ("Nat.add_comm manual", proof_nat_add_comm true), - ("Nat.add_comm delta", proof_delta_variable), - ("arithmetic", proof_arith), - ("Or.comm", proof_or_comm) + ("Nat.add_comm", test_nat_add_comm false), + ("Nat.add_comm manual", test_nat_add_comm true), + ("Nat.add_comm delta", test_delta_variable), + ("arithmetic", test_arith), + ("Or.comm", test_or_comm), + ("Have", test_have_tactic), ] tests.map (fun (name, test) => (name, proofRunner env test)) -- 2.44.1 From 951c2cec19f64b8fc3ebd87f8c1219441cbafe03 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 6 Apr 2024 16:40:22 -0700 Subject: [PATCH 02/19] feat: Bindings for the `have` tactic --- Pantograph.lean | 13 ++++++++----- Pantograph/Goal.lean | 5 +++++ Pantograph/Library.lean | 8 ++++++-- Pantograph/Protocol.lean | 5 +++++ 4 files changed, 24 insertions(+), 7 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index 97f03f4..70d64b9 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -114,12 +114,15 @@ def execute (command: Protocol.Command): MainM Lean.Json := do match state.goalStates.find? args.stateId with | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" | .some goalState => do - let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with - | .some tactic, .none => do + let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr?, args.have? with + | .some tactic, .none, .none => do pure ( Except.ok (← goalTactic goalState args.goalId tactic)) - | .none, .some expr => do - pure ( Except.ok (← goalTryAssign goalState args.goalId expr)) - | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied") + | .none, .some expr, .none => do + pure ( Except.ok (← goalAssign goalState args.goalId expr)) + | .none, .none, .some type => do + let binderName := args.binderName?.getD "" + pure ( Except.ok (← goalHave goalState args.goalId binderName type)) + | _, _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr, have} must be supplied") match nextGoalState? with | .error error => return .error error | .ok (.success nextGoalState) => diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 5b6e467..04fa0d5 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -1,3 +1,8 @@ +/- +Functions for handling metavariables + +All the functions starting with `try` resume their inner monadic state. +-/ import Pantograph.Protocol import Lean diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 1d31e97..04a8d71 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -162,10 +162,14 @@ def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) := def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult := runTermElabM <| GoalState.tryTactic state goalId tactic -@[export pantograph_goal_try_assign_m] -def goalTryAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult := +@[export pantograph_goal_assign_m] +def goalAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult := runTermElabM <| GoalState.tryAssign state goalId expr +@[export pantograph_goal_have_m] +def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := + runTermElabM <| GoalState.tryHave state goalId binderName type + @[export pantograph_goal_continue] def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState := target.continue branch diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 6ee3354..3055136 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -201,6 +201,11 @@ structure GoalTactic where -- One of the fields here must be filled tactic?: Option String := .none expr?: Option String := .none + have?: Option String := .none + + -- In case of the `have` tactic, the new free variable name + binderName?: Option String := .none + deriving Lean.FromJson structure GoalTacticResult where -- The next goal state id. Existence of this field shows success -- 2.44.1 From 3db1207aa6666249442c0e56497011b8d6011788 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 6 Apr 2024 17:22:09 -0700 Subject: [PATCH 03/19] test: Tests for conv and calc --- Test/Proofs.lean | 77 ++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 72 insertions(+), 5 deletions(-) diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 91c8f0c..ca46d95 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -292,16 +292,14 @@ def test_or_comm: TestM Unit := do { userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible? := .some true } ] } -def test_have_tactic: TestM Unit := do + +def test_have: TestM Unit := do let state? ← startProof (.expr "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))") let state0 ← match state? with | .some state => pure state | .none => do addTest $ assertUnreachable "Goal could not parse" return () - addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone - addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro p q h") with | .success state => pure state | other => do @@ -326,6 +324,71 @@ def test_have_tactic: TestM Unit := do addTest $ LSpec.check "have" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = #[buildGoal [] ""]) +example : ∀ (a b c: Nat), (a + b) + c = (b + a) + c := by + intro a b c + conv => + lhs + congr + rw [Nat.add_comm] + rfl + +def test_conv: TestM Unit := do + let state? ← startProof (.expr "∀ (a b c: Nat), (a + b) + c = (b + a) + c") + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + let tactic := "intro a b c" + 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) = + #[buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "a + b + c = b + a + c"]) + + -- This solves the state in one-shot + let tactic := "conv => { lhs; congr; rw [Nat.add_comm]; rfl }" + let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = + #[]) + +example : ∀ (a: Nat), 1 + a + 1 = a + 2 := by + intro a + calc 1 + a + 1 = a + 1 + 1 := by conv => + rhs + rw [Nat.add_comm] + _ = a + 2 := by rw [Nat.add_assoc] + +def test_calc: TestM Unit := do + let state? ← startProof (.expr "∀ (a: Nat), 1 + a + 1 = a + 2") + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + let tactic := "intro a" + 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) = + #[buildGoal [("a", "Nat")] "1 + a + 1 = a + 2"]) + let tactic := "calc" + let state2 ← match ← state1.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) = + #[buildGoal [("a", "Nat")] "1 + a + 1 = a + 2"]) + def suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ ("Nat.add_comm", test_nat_add_comm false), @@ -333,8 +396,12 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("Nat.add_comm delta", test_delta_variable), ("arithmetic", test_arith), ("Or.comm", test_or_comm), - ("Have", test_have_tactic), + ("have", test_have), + ("conv", test_conv), + ("calc", test_calc), ] tests.map (fun (name, test) => (name, proofRunner env test)) + + end Pantograph.Test.Proofs -- 2.44.1 From aa8da3014ed0695a2d3176000ca4aa7c89fb5802 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 6 Apr 2024 21:52:25 -0700 Subject: [PATCH 04/19] feat: The `have` tactic --- Pantograph/Goal.lean | 90 ++++++++++++++++++++++++++++++-------------- Test/Metavar.lean | 2 +- Test/Proofs.lean | 61 +++++++++++++++++++++++------- 3 files changed, 110 insertions(+), 43 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 04fa0d5..57f524b 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -17,6 +17,9 @@ open Lean def filename: String := "" +/-- +Represents an interconnected set of metavariables, or a state in proof search + -/ structure GoalState where savedState : Elab.Tactic.SavedState @@ -28,15 +31,13 @@ structure GoalState where -- Parent state metavariable source parentMVar: Option MVarId -abbrev M := Elab.TermElabM - -protected def GoalState.create (expr: Expr): M GoalState := do +protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do -- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context. -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070 --Elab.Term.synthesizeSyntheticMVarsNoPostponing --let expr ← instantiateMVars expr - let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous)) + let goal ← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous) let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState let root := goal.mvarId! let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root]} @@ -46,12 +47,8 @@ protected def GoalState.create (expr: Expr): M GoalState := do newMVars := SSet.insert .empty root, parentMVar := .none, } -protected def GoalState.goals (state: GoalState): List MVarId := state.savedState.tactic.goals - -protected def GoalState.runM {α: Type} (state: GoalState) (m: Elab.TermElabM α) : M α := do - state.savedState.term.restore - m - +protected def GoalState.goals (state: GoalState): List MVarId := + state.savedState.tactic.goals protected def GoalState.mctx (state: GoalState): MetavarContext := state.savedState.term.meta.meta.mctx protected def GoalState.env (state: GoalState): Environment := @@ -65,7 +62,7 @@ protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit := /-- Inner function for executing tactic on goal state -/ def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) : - M (Except (Array String) Elab.Tactic.SavedState):= do + Elab.TermElabM (Except (Array String) Elab.Tactic.SavedState):= do let tacticM (stx: Syntax): Elab.Tactic.TacticM (Except (Array String) Elab.Tactic.SavedState) := do state.restore Elab.Tactic.setGoals [goal] @@ -94,11 +91,12 @@ inductive TacticResult where /-- Execute tactic on given state -/ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String): - M TacticResult := do + Elab.TermElabM TacticResult := do state.restoreElabM let goal ← match state.savedState.tactic.goals.get? goalId with | .some goal => pure $ goal | .none => return .indexError goalId + goal.checkNotAssigned `GoalState.tryTactic let tactic ← match Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `tactic) @@ -129,15 +127,22 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri parentMVar := .some goal, } -/-- Assumes elabM has already been restored -/ -protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr): M TacticResult := do +/-- Assumes elabM has already been restored. Assumes expr has already typechecked -/ +protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr): + Elab.TermElabM TacticResult := do let goalType ← goal.getType try - let exprType ← Meta.inferType expr - -- This elaboration is necessary - if !(← Meta.isDefEq goalType exprType) then - return .failure #["Type unification failed", toString (← Meta.ppExpr goalType), toString (← Meta.ppExpr exprType)] - goal.checkNotAssigned `GoalState.tryAssign + -- For some reason this is needed. One of the unit tests will fail if this isn't here + let error?: Option String ← goal.withContext (do + let exprType ← Meta.inferType expr + if ← Meta.isDefEq goalType exprType then + pure .none + else do + return .some s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} != {← Meta.ppExpr goalType}" + ) + if let .some error := error? then + return .failure #["Type unification failed", error] + goal.checkNotAssigned `GoalState.assign goal.assign expr if (← getThe Core.State).messages.hasErrors then let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray @@ -168,7 +173,8 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr): M catch exception => return .failure #[← exception.toMessageData.toString] -protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do +protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): + Elab.TermElabM TacticResult := do state.restoreElabM let goal ← match state.savedState.tactic.goals.get? goalId with | .some goal => pure goal @@ -182,14 +188,16 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String | .error error => return .parseError error let goalType ← goal.getType try - let expr ← Elab.Term.elabTermAndSynthesize (stx := expr) (expectedType? := .some goalType) + let expr ← goal.withContext $ + Elab.Term.elabTermAndSynthesize (stx := expr) (expectedType? := .some goalType) state.assign goal expr catch exception => return .failure #[← exception.toMessageData.toString] -- Specialized Tactics -protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): M TacticResult := do +protected def GoalState.tryHave (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 @@ -201,16 +209,40 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St (fileName := filename) with | .ok syn => pure syn | .error error => return .parseError error + let binderName := binderName.toName try - let type ← Elab.Term.elabType (stx := type) + -- 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 created by "have" - let mvarBranch ← Meta.mkFreshExprSyntheticOpaqueMVar type + -- The branch goal inherits the same context, but with a different type + let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type - -- The main branch - let mvarUpstream ← Meta.mkFreshExprSyntheticOpaqueMVar (← goal.getType) - let expr := Expr.app (.lam binderName.toName type mvarBranch .default) mvarUpstream - state.assign goal expr + -- Create the context for the `upstream` goal + let fvarId ← mkFreshFVarId + let lctxUpstream := lctx.mkLocalDecl fvarId binderName type + let fvar := mkFVar fvarId + let mvarUpstream ← + withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do + Meta.withNewLocalInstances #[fvar] 0 (do + let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) + (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous) + let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream + goal.assign expr + pure mvarUpstream) + + pure [mvarBranch.mvarId!, mvarUpstream.mvarId!] + ) + return .success { + root := state.root, + savedState := { + term := ← MonadBacktrack.saveState, + tactic := { goals := nextGoals } + }, + newMVars := nextGoals.toSSet, + parentMVar := .some goal, + } catch exception => return .failure #[← exception.toMessageData.toString] diff --git a/Test/Metavar.lean b/Test/Metavar.lean index 1b49e95..eff2103 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -8,7 +8,7 @@ namespace Pantograph.Test.Metavar open Pantograph open Lean -abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M) +abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM) def addTest (test: LSpec.TestSeq): TestM Unit := do set $ (← get) ++ test diff --git a/Test/Proofs.lean b/Test/Proofs.lean index ca46d95..5a25b87 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -14,7 +14,7 @@ inductive Start where | copy (name: String) -- Start from some name in the environment | expr (expr: String) -- Start from some expression -abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M) +abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM) def addTest (test: LSpec.TestSeq): TestM Unit := do set $ (← get) ++ test @@ -205,21 +205,24 @@ def test_or_comm: TestM Unit := do addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro p q h") with + let tactic := "intro p q 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 "intro p q h" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = + addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"]) addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone - let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "cases h") with + + let tactic := "cases h" + let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "cases h" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = + addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = #[branchGoal "inl" "p", branchGoal "inr" "q"]) addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone @@ -300,29 +303,61 @@ def test_have: TestM Unit := do | .none => do addTest $ assertUnreachable "Goal could not parse" return () - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro p q h") with + let tactic := "intro p q 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 "intro p q h" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = + addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"]) - let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "Or.inl (Or.inl h)") with + let expr := "Or.inl (Or.inl h)" + let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "have" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = - #[buildGoal [] ""]) + addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = + #[]) - let state2 ← match ← state1.tryHave (goalId := 0) (binderName := "y") (type := "p ∨ q") with + let haveBind := "y" + let haveType := "p ∨ q" + let state2 ← match ← state1.tryHave (goalId := 0) (binderName := haveBind) (type := haveType) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "have" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = - #[buildGoal [] ""]) + addTest $ LSpec.check s!"have {haveBind}: {haveType}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = + #[ + buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "p ∨ q", + buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p"), ("y", "p ∨ q")] "(p ∨ q) ∨ p ∨ q" + ]) + + let expr := "Or.inl h" + let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) = + #[]) + + let state2b ← match state3.continue state2 with + | .ok state => pure state + | .error e => do + addTest $ assertUnreachable e + return () + let expr := "Or.inl y" + let state4 ← match ← state2b.tryAssign (goalId := 0) (expr := expr) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) = + #[]) + + addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome example : ∀ (a b c: Nat), (a + b) + c = (b + a) + c := by intro a b c -- 2.44.1 From 9d7c9598f51f49b88a770b25373b855ac554bcad Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 7 Apr 2024 14:22:20 -0700 Subject: [PATCH 05/19] feat: Partial implementation of `conv` --- Pantograph/Goal.lean | 85 ++++++++++++++++++++++++++++++++++++++++++-- Test/Proofs.lean | 40 +++++++++++++++++---- 2 files changed, 117 insertions(+), 8 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 57f524b..b0be1d1 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -55,10 +55,13 @@ protected def GoalState.env (state: GoalState): Environment := state.savedState.term.meta.core.env private def GoalState.mvars (state: GoalState): SSet MVarId := state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k -private def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit := - state.savedState.term.restore protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit := state.savedState.term.meta.restore +private def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit := + state.savedState.term.restore +private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do + state.savedState.restore + Elab.Tactic.setGoals [goal] /-- Inner function for executing tactic on goal state -/ def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) : @@ -246,6 +249,84 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St catch exception => return .failure #[← exception.toMessageData.toString] +/-- Enter conv tactic mode -/ +protected def GoalState.tryConv (state: GoalState) (goalId: Nat): + Elab.TermElabM TacticResult := do + let goal ← match state.savedState.tactic.goals.get? goalId with + | .some goal => pure goal + | .none => return .indexError goalId + let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do + state.restoreTacticM goal + --let mm ← Meta.matchEq? (← goal.getType) + --if let .some (_, _, rhs) := mm then + -- if rhs.getAppFn.isMVar then + -- IO.println "isMVar ok" + -- else + -- IO.println "isMVar failed" + --else + -- IO.println "matchEq? failed" + IO.println s!"Old goals: {(← Elab.Tactic.getGoals).map (λ x => x.name.toString)}" + --Elab.Tactic.Conv.remarkAsConvGoal + let goalNew ← Elab.Tactic.Conv.markAsConvGoal goal + -- TODO: Error if `goal == goalNew` + Elab.Tactic.setGoals [goalNew] + --Elab.Tactic.Conv.remarkAsConvGoal + IO.println s!"New goals: {(← Elab.Tactic.getGoals).map (λ x => x.name.toString)}" + MonadBacktrack.saveState + let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic + let prevMCtx := state.savedState.term.meta.meta.mctx + let nextMCtx := nextSavedState.term.meta.meta.mctx + -- Generate a list of mvarIds that exist in the parent state; Also test the + -- assertion that the types have not changed on any mvars. + let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do + if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then + assert! prevMVarDecl.type == mvarDecl.type + return acc + else + return acc.insert mvarId + ) SSet.empty + return .success { + root := state.root, + savedState := nextSavedState + newMVars, + parentMVar := .some goal, + } + +protected def GoalState.tryConvTactic (state: GoalState) (goalId: Nat) (convTactic: String): + Elab.TermElabM TacticResult := do + let goal ← match state.savedState.tactic.goals.get? goalId with + | .some goal => pure goal + | .none => return .indexError goalId + let convTactic ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `conv) + (input := convTactic) + (fileName := filename) with + | .ok stx => pure $ stx + | .error error => return .parseError error + let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do + state.restoreTacticM goal + Elab.Tactic.Conv.evalConvTactic convTactic + MonadBacktrack.saveState + let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic + let nextMCtx := nextSavedState.term.meta.meta.mctx + let prevMCtx := state.savedState.term.meta.meta.mctx + -- Generate a list of mvarIds that exist in the parent state; Also test the + -- assertion that the types have not changed on any mvars. + let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do + if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then + assert! prevMVarDecl.type == mvarDecl.type + return acc + else + return acc.insert mvarId + ) SSet.empty + return .success { + root := state.root, + savedState := nextSavedState + newMVars, + parentMVar := .some goal, + } + /-- Brings into scope a list of goals diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 5a25b87..bfc0d4e 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -157,12 +157,13 @@ def test_arith: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intros") with + let tactic := "intros" + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "intros" (state1.goals.length = 1) + addTest $ LSpec.check tactic (state1.goals.length = 1) addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with | .success state => pure state @@ -171,12 +172,13 @@ def test_arith: TestM Unit := do return () addTest $ LSpec.check "simp ..." (state2.goals.length = 1) addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone - let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := "assumption") with + let tactic := "assumption" + let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.test "assumption" state3.goals.isEmpty + addTest $ LSpec.test tactic state3.goals.isEmpty addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome return () @@ -385,14 +387,40 @@ def test_conv: TestM Unit := do -- This solves the state in one-shot let tactic := "conv => { lhs; congr; rw [Nat.add_comm]; rfl }" - let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with + let stateT ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = + addTest $ LSpec.check tactic ((← stateT.serializeGoals (options := ← read)).map (·.devolatilize) = #[]) + let state2 ← match ← state1.tryConv (goalId := 0) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = + #[{ buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "a + b + c" with isConversion := true }]) + + let convTactic := "lhs" + let state3L ← match ← state2.tryConvTactic (goalId := 0) (convTactic := convTactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!" {convTactic}" ((← state3L.serializeGoals (options := ← read)).map (·.devolatilize) = + #[{ buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "a + b + c" with isConversion := true }]) + + let convTactic := "rhs" + let state3R ← match ← state2.tryConvTactic (goalId := 0) (convTactic := convTactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!" {convTactic}" ((← state3R.serializeGoals (options := ← read)).map (·.devolatilize) = + #[{ buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "b + a + c" with isConversion := true }]) + example : ∀ (a: Nat), 1 + a + 1 = a + 2 := by intro a calc 1 + a + 1 = a + 1 + 1 := by conv => -- 2.44.1 From aba1d9be10e98dd7097fb95f0c46de300c93dfee Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 7 Apr 2024 14:32:25 -0700 Subject: [PATCH 06/19] refactor: Metavariable set diff function --- Pantograph/Goal.lean | 52 +++++++++++++------------------------------- 1 file changed, 15 insertions(+), 37 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index b0be1d1..6257627 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -63,6 +63,15 @@ private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tac state.savedState.restore Elab.Tactic.setGoals [goal] +private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext): SSet MVarId := + mctxNew.decls.foldl (fun acc mvarId mvarDecl => + if let .some prevMVarDecl := mctxOld.decls.find? mvarId then + assert! prevMVarDecl.type == mvarDecl.type + acc + else + acc.insert mvarId + ) SSet.empty + /-- Inner function for executing tactic on goal state -/ def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) : Elab.TermElabM (Except (Array String) Elab.Tactic.SavedState):= do @@ -116,17 +125,10 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri let prevMCtx := state.savedState.term.meta.meta.mctx -- Generate a list of mvarIds that exist in the parent state; Also test the -- assertion that the types have not changed on any mvars. - let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do - if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then - assert! prevMVarDecl.type == mvarDecl.type - return acc - else - return acc.insert mvarId - ) SSet.empty return .success { root := state.root, savedState := nextSavedState - newMVars, + newMVars := newMVarSet prevMCtx nextMCtx, parentMVar := .some goal, } @@ -156,21 +158,15 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr): let nextMCtx ← getMCtx -- Generate a list of mvarIds that exist in the parent state; Also test the -- assertion that the types have not changed on any mvars. - let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do - if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then - assert! prevMVarDecl.type == mvarDecl.type - return acc - else - return mvarId :: acc - ) [] - let nextGoals ← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned)) + let newMVars := newMVarSet prevMCtx nextMCtx + let nextGoals ← newMVars.toList.filterM (λ mvar => do pure !(← mvar.isAssigned)) return .success { root := state.root, savedState := { term := ← MonadBacktrack.saveState, tactic := { goals := nextGoals } }, - newMVars := newMVars.toSSet, + newMVars, parentMVar := .some goal, } catch exception => @@ -276,19 +272,10 @@ protected def GoalState.tryConv (state: GoalState) (goalId: Nat): let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic let prevMCtx := state.savedState.term.meta.meta.mctx let nextMCtx := nextSavedState.term.meta.meta.mctx - -- Generate a list of mvarIds that exist in the parent state; Also test the - -- assertion that the types have not changed on any mvars. - let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do - if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then - assert! prevMVarDecl.type == mvarDecl.type - return acc - else - return acc.insert mvarId - ) SSet.empty return .success { root := state.root, savedState := nextSavedState - newMVars, + newMVars := newMVarSet prevMCtx nextMCtx, parentMVar := .some goal, } @@ -311,19 +298,10 @@ protected def GoalState.tryConvTactic (state: GoalState) (goalId: Nat) (convTact let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic let nextMCtx := nextSavedState.term.meta.meta.mctx let prevMCtx := state.savedState.term.meta.meta.mctx - -- Generate a list of mvarIds that exist in the parent state; Also test the - -- assertion that the types have not changed on any mvars. - let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do - if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then - assert! prevMVarDecl.type == mvarDecl.type - return acc - else - return acc.insert mvarId - ) SSet.empty return .success { root := state.root, savedState := nextSavedState - newMVars, + newMVars := newMVarSet prevMCtx nextMCtx, parentMVar := .some goal, } -- 2.44.1 From ab0d87450a4a785758c1e2b970c16053bf52152c Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 7 Apr 2024 17:03:49 -0700 Subject: [PATCH 07/19] feat: Conv tactic mode --- Pantograph/Goal.lean | 26 ++++++++++---------------- Test/Proofs.lean | 2 +- 2 files changed, 11 insertions(+), 17 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 6257627..b238332 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -253,21 +253,15 @@ protected def GoalState.tryConv (state: GoalState) (goalId: Nat): | .none => return .indexError goalId let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do state.restoreTacticM goal - --let mm ← Meta.matchEq? (← goal.getType) - --if let .some (_, _, rhs) := mm then - -- if rhs.getAppFn.isMVar then - -- IO.println "isMVar ok" - -- else - -- IO.println "isMVar failed" - --else - -- IO.println "matchEq? failed" - IO.println s!"Old goals: {(← Elab.Tactic.getGoals).map (λ x => x.name.toString)}" - --Elab.Tactic.Conv.remarkAsConvGoal - let goalNew ← Elab.Tactic.Conv.markAsConvGoal goal - -- TODO: Error if `goal == goalNew` - Elab.Tactic.setGoals [goalNew] - --Elab.Tactic.Conv.remarkAsConvGoal - IO.println s!"New goals: {(← Elab.Tactic.getGoals).map (λ x => x.name.toString)}" + + -- TODO: Fail if this is already in conv + + -- See Lean.Elab.Tactic.Conv.convTarget + Elab.Tactic.withMainContext do + -- TODO: Memorize this `rhs` as a conv resultant goal + let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget) + Elab.Tactic.setGoals [newGoal.mvarId!] + --Elab.Tactic.liftMetaTactic1 fun mvarId => mvarId.replaceTargetEq rhs proof MonadBacktrack.saveState let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic let prevMCtx := state.savedState.term.meta.meta.mctx @@ -293,7 +287,7 @@ protected def GoalState.tryConvTactic (state: GoalState) (goalId: Nat) (convTact | .error error => return .parseError error let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do state.restoreTacticM goal - Elab.Tactic.Conv.evalConvTactic convTactic + Elab.Tactic.evalTactic convTactic MonadBacktrack.saveState let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic let nextMCtx := nextSavedState.term.meta.meta.mctx diff --git a/Test/Proofs.lean b/Test/Proofs.lean index bfc0d4e..4b2b57e 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -401,7 +401,7 @@ def test_conv: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = - #[{ buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "a + b + c" with isConversion := true }]) + #[{ buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "a + b + c = b + a + c" with isConversion := true }]) let convTactic := "lhs" let state3L ← match ← state2.tryConvTactic (goalId := 0) (convTactic := convTactic) with -- 2.44.1 From 3094d11e48a38a21d85a6a43e92bbf4c0e81c513 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 8 Apr 2024 12:26:22 -0700 Subject: [PATCH 08/19] feat: Conv tactic functions --- Pantograph.lean | 2 + Pantograph/Goal.lean | 112 +++++++++++++++++++++++++++++++++---------- Test/Common.lean | 1 + Test/Proofs.lean | 106 ++++++++++++++++++++++++++++++---------- 4 files changed, 171 insertions(+), 50 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index 70d64b9..626afae 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -140,6 +140,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do return .ok { parseError? := .some message } | .ok (.indexError goalId) => return .error $ errorIndex s!"Invalid goal id index {goalId}" + | .ok (.invalidAction message) => + return .error $ errorI "invalid" message | .ok (.failure messages) => return .ok { tacticErrors? := .some messages } goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index b238332..78affd7 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -31,6 +31,9 @@ structure GoalState where -- Parent state metavariable source parentMVar: Option MVarId + -- Existence of this field shows that we are currently in `conv` mode. + convMVar: Option (MVarId × MVarId × List MVarId) := .none + protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do -- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context. -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070 @@ -100,6 +103,8 @@ inductive TacticResult where | parseError (message: String) -- The goal index is out of bounds | indexError (goalId: Nat) + -- The given action cannot be executed in the state + | invalidAction (message: String) /-- Execute tactic on given state -/ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String): @@ -122,11 +127,11 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri | .ok nextSavedState => -- Assert that the definition of metavariables are the same let nextMCtx := nextSavedState.term.meta.meta.mctx - let prevMCtx := state.savedState.term.meta.meta.mctx + let prevMCtx := state.mctx -- Generate a list of mvarIds that exist in the parent state; Also test the -- assertion that the types have not changed on any mvars. return .success { - root := state.root, + state with savedState := nextSavedState newMVars := newMVarSet prevMCtx nextMCtx, parentMVar := .some goal, @@ -146,7 +151,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr): return .some s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} != {← Meta.ppExpr goalType}" ) if let .some error := error? then - return .failure #["Type unification failed", error] + return .parseError error goal.checkNotAssigned `GoalState.assign goal.assign expr if (← getThe Core.State).messages.hasErrors then @@ -246,35 +251,45 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St return .failure #[← exception.toMessageData.toString] /-- Enter conv tactic mode -/ -protected def GoalState.tryConv (state: GoalState) (goalId: Nat): +protected def GoalState.conv (state: GoalState) (goalId: Nat): Elab.TermElabM TacticResult := do + if state.convMVar.isSome then + return .invalidAction "Already in conv state" let goal ← match state.savedState.tactic.goals.get? goalId with | .some goal => pure goal | .none => return .indexError goalId - let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do + let tacticM : Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do state.restoreTacticM goal -- TODO: Fail if this is already in conv -- See Lean.Elab.Tactic.Conv.convTarget - Elab.Tactic.withMainContext do + let convMVar ← Elab.Tactic.withMainContext do -- TODO: Memorize this `rhs` as a conv resultant goal let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget) Elab.Tactic.setGoals [newGoal.mvarId!] - --Elab.Tactic.liftMetaTactic1 fun mvarId => mvarId.replaceTargetEq rhs proof - MonadBacktrack.saveState - let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic - let prevMCtx := state.savedState.term.meta.meta.mctx - let nextMCtx := nextSavedState.term.meta.meta.mctx - return .success { - root := state.root, - savedState := nextSavedState - newMVars := newMVarSet prevMCtx nextMCtx, - parentMVar := .some goal, - } + pure rhs.mvarId! + return (← MonadBacktrack.saveState, convMVar) + try + let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic + let prevMCtx := state.mctx + let nextMCtx := nextSavedState.term.meta.meta.mctx + return .success { + root := state.root, + savedState := nextSavedState + newMVars := newMVarSet prevMCtx nextMCtx, + parentMVar := .some goal, + convMVar := .some (convRhs, goal, state.goals), + } + catch exception => + return .failure #[← exception.toMessageData.toString] +/-- Execute a tactic in conv mode -/ protected def GoalState.tryConvTactic (state: GoalState) (goalId: Nat) (convTactic: String): Elab.TermElabM TacticResult := do + let _ ← match state.convMVar with + | .some mvar => pure mvar + | .none => return .invalidAction "Not in conv state" let goal ← match state.savedState.tactic.goals.get? goalId with | .some goal => pure goal | .none => return .indexError goalId @@ -289,15 +304,60 @@ protected def GoalState.tryConvTactic (state: GoalState) (goalId: Nat) (convTact state.restoreTacticM goal Elab.Tactic.evalTactic convTactic MonadBacktrack.saveState - let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic - let nextMCtx := nextSavedState.term.meta.meta.mctx - let prevMCtx := state.savedState.term.meta.meta.mctx - return .success { - root := state.root, - savedState := nextSavedState - newMVars := newMVarSet prevMCtx nextMCtx, - parentMVar := .some goal, - } + try + let prevMCtx := state.mctx + let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic + let nextMCtx := nextSavedState.term.meta.meta.mctx + return .success { + state with + savedState := nextSavedState + newMVars := newMVarSet prevMCtx nextMCtx, + parentMVar := .some goal, + } + catch exception => + return .failure #[← exception.toMessageData.toString] + +protected def GoalState.convExit (state: GoalState): + Elab.TermElabM TacticResult := do + let (convRhs, convGoal, savedGoals) ← match state.convMVar with + | .some mvar => pure mvar + | .none => return .invalidAction "Not in conv state" + let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do + -- Vide `Lean.Elab.Tactic.Conv.convert` + state.savedState.restore + + IO.println "Restored state" + + -- Close all existing goals with `refl` + for mvarId in (← Elab.Tactic.getGoals) do + liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure () + Elab.Tactic.pruneSolvedGoals + unless (← Elab.Tactic.getGoals).isEmpty do + throwError "convert tactic failed, there are unsolved goals\n{Elab.goalsToMessageData (← Elab.Tactic.getGoals)}" + + IO.println "Caching" + Elab.Tactic.setGoals savedGoals + + let targetNew ← instantiateMVars (.mvar convRhs) + let proof ← instantiateMVars (.mvar convGoal) + + Elab.Tactic.liftMetaTactic1 fun mvarId => mvarId.replaceTargetEq targetNew proof + MonadBacktrack.saveState + try + let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic + IO.println "Finished caching" + let nextMCtx := nextSavedState.term.meta.meta.mctx + let prevMCtx := state.savedState.term.meta.meta.mctx + return .success { + root := state.root, + savedState := nextSavedState + newMVars := newMVarSet prevMCtx nextMCtx, + parentMVar := .some convGoal, + convMVar := .none + } + catch exception => + return .failure #[← exception.toMessageData.toString] + /-- diff --git a/Test/Common.lean b/Test/Common.lean index 6fa858b..8719ebd 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -37,6 +37,7 @@ def TacticResult.toString : TacticResult → String s!".failure {messages}" | .parseError error => s!".parseError {error}" | .indexError index => s!".indexError {index}" + | .invalidAction error => s!".invalidAction {error}" namespace Test diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 4b2b57e..c8ceeee 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -361,47 +361,48 @@ def test_have: TestM Unit := do addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome -example : ∀ (a b c: Nat), (a + b) + c = (b + a) + c := by - intro a b c +example : ∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2 := by + intro a b c1 c2 h conv => lhs congr - rw [Nat.add_comm] - rfl + . rw [Nat.add_comm] + . rfl + exact h def test_conv: TestM Unit := do - let state? ← startProof (.expr "∀ (a b c: Nat), (a + b) + c = (b + a) + c") + let state? ← startProof (.expr "∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2") let state0 ← match state? with | .some state => pure state | .none => do addTest $ assertUnreachable "Goal could not parse" return () - let tactic := "intro a b c" + + let tactic := "intro a b c1 c2 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) = - #[buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "a + b + c = b + a + c"]) + #[interiorGoal [] "a + b + c1 = b + a + c2"]) - -- This solves the state in one-shot - let tactic := "conv => { lhs; congr; rw [Nat.add_comm]; rfl }" - let stateT ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check tactic ((← stateT.serializeGoals (options := ← read)).map (·.devolatilize) = - #[]) - - let state2 ← match ← state1.tryConv (goalId := 0) with + let state2 ← match ← state1.conv (goalId := 0) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = - #[{ buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "a + b + c = b + a + c" with isConversion := true }]) + #[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }]) + + let convTactic := "rhs" + let state3R ← match ← state2.tryConvTactic (goalId := 0) (convTactic := convTactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!" {convTactic} (discard)" ((← state3R.serializeGoals (options := ← read)).map (·.devolatilize) = + #[{ interiorGoal [] "b + a + c2" with isConversion := true }]) let convTactic := "lhs" let state3L ← match ← state2.tryConvTactic (goalId := 0) (convTactic := convTactic) with @@ -410,16 +411,73 @@ def test_conv: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check s!" {convTactic}" ((← state3L.serializeGoals (options := ← read)).map (·.devolatilize) = - #[{ buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "a + b + c" with isConversion := true }]) + #[{ interiorGoal [] "a + b + c1" with isConversion := true }]) - let convTactic := "rhs" - let state3R ← match ← state2.tryConvTactic (goalId := 0) (convTactic := convTactic) with + let convTactic := "congr" + let state4 ← match ← state3L.tryConvTactic (goalId := 0) (convTactic := convTactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check s!" {convTactic}" ((← state3R.serializeGoals (options := ← read)).map (·.devolatilize) = - #[{ buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "b + a + c" with isConversion := true }]) + addTest $ LSpec.check s!" {convTactic}" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) = + #[ + { interiorGoal [] "a + b" with isConversion := true, userName? := .some "a" }, + { interiorGoal [] "c1" with isConversion := true, userName? := .some "a" } + ]) + + let convTactic := "rw [Nat.add_comm]" + let state5_1 ← match ← state4.tryConvTactic (goalId := 0) (convTactic := convTactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!" · {convTactic}" ((← state5_1.serializeGoals (options := ← read)).map (·.devolatilize) = + #[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }]) + + let convTactic := "rfl" + let state6_1 ← match ← state5_1.tryConvTactic (goalId := 0) (convTactic := convTactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!" {convTactic}" ((← state6_1.serializeGoals (options := ← read)).map (·.devolatilize) = + #[]) + + let state4_1 ← match state6_1.continue state4 with + | .ok state => pure state + | .error e => do + addTest $ expectationFailure "continue" e + return () + + let convTactic := "rfl" + let state6 ← match ← state4_1.tryConvTactic (goalId := 0) (convTactic := convTactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!" · {convTactic}" ((← state6.serializeGoals (options := ← read)).map (·.devolatilize) = + #[]) + + let state1_1 ← match ← state6.convExit with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + + let tactic := "exact h" + let stateF ← match ← state1_1.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← stateF.serializeGoals (options := ← read)).map (·.devolatilize) = + #[]) + + where + h := "b + a + c1 = b + a + c2" + interiorGoal (free: List (String × String)) (target: String) := + let free := [("a", "Nat"), ("b", "Nat"), ("c1", "Nat"), ("c2", "Nat"), ("h", h)] ++ free + buildGoal free target example : ∀ (a: Nat), 1 + a + 1 = a + 2 := by intro a -- 2.44.1 From 73bdcb6be65a9302697c79301121e7718484cf14 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 8 Apr 2024 12:32:27 -0700 Subject: [PATCH 09/19] refactor: Use the `tactic interface for `conv --- Pantograph/Goal.lean | 38 ++++---------------------------------- Test/Proofs.lean | 12 ++++++------ 2 files changed, 10 insertions(+), 40 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 78affd7..ed181a3 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -50,6 +50,8 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do newMVars := SSet.insert .empty root, parentMVar := .none, } +protected def GoalState.isConv (state: GoalState): Bool := + state.convMVar.isSome protected def GoalState.goals (state: GoalState): List MVarId := state.savedState.tactic.goals protected def GoalState.mctx (state: GoalState): MetavarContext := @@ -116,7 +118,7 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri goal.checkNotAssigned `GoalState.tryTactic let tactic ← match Parser.runParserCategory (env := ← MonadEnv.getEnv) - (catName := `tactic) + (catName := if state.isConv then `conv else `tactic) (input := tactic) (fileName := filename) with | .ok stx => pure $ stx @@ -284,39 +286,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat): catch exception => return .failure #[← exception.toMessageData.toString] -/-- Execute a tactic in conv mode -/ -protected def GoalState.tryConvTactic (state: GoalState) (goalId: Nat) (convTactic: String): - Elab.TermElabM TacticResult := do - let _ ← match state.convMVar with - | .some mvar => pure mvar - | .none => return .invalidAction "Not in conv state" - let goal ← match state.savedState.tactic.goals.get? goalId with - | .some goal => pure goal - | .none => return .indexError goalId - let convTactic ← match Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `conv) - (input := convTactic) - (fileName := filename) with - | .ok stx => pure $ stx - | .error error => return .parseError error - let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do - state.restoreTacticM goal - Elab.Tactic.evalTactic convTactic - MonadBacktrack.saveState - try - let prevMCtx := state.mctx - let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic - let nextMCtx := nextSavedState.term.meta.meta.mctx - return .success { - state with - savedState := nextSavedState - newMVars := newMVarSet prevMCtx nextMCtx, - parentMVar := .some goal, - } - catch exception => - return .failure #[← exception.toMessageData.toString] - +/-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/ protected def GoalState.convExit (state: GoalState): Elab.TermElabM TacticResult := do let (convRhs, convGoal, savedGoals) ← match state.convMVar with diff --git a/Test/Proofs.lean b/Test/Proofs.lean index c8ceeee..7a23290 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -396,7 +396,7 @@ def test_conv: TestM Unit := do #[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }]) let convTactic := "rhs" - let state3R ← match ← state2.tryConvTactic (goalId := 0) (convTactic := convTactic) with + let state3R ← match ← state2.tryTactic (goalId := 0) convTactic with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -405,7 +405,7 @@ def test_conv: TestM Unit := do #[{ interiorGoal [] "b + a + c2" with isConversion := true }]) let convTactic := "lhs" - let state3L ← match ← state2.tryConvTactic (goalId := 0) (convTactic := convTactic) with + let state3L ← match ← state2.tryTactic (goalId := 0) convTactic with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -414,7 +414,7 @@ def test_conv: TestM Unit := do #[{ interiorGoal [] "a + b + c1" with isConversion := true }]) let convTactic := "congr" - let state4 ← match ← state3L.tryConvTactic (goalId := 0) (convTactic := convTactic) with + let state4 ← match ← state3L.tryTactic (goalId := 0) convTactic with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -426,7 +426,7 @@ def test_conv: TestM Unit := do ]) let convTactic := "rw [Nat.add_comm]" - let state5_1 ← match ← state4.tryConvTactic (goalId := 0) (convTactic := convTactic) with + let state5_1 ← match ← state4.tryTactic (goalId := 0) convTactic with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -435,7 +435,7 @@ def test_conv: TestM Unit := do #[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }]) let convTactic := "rfl" - let state6_1 ← match ← state5_1.tryConvTactic (goalId := 0) (convTactic := convTactic) with + let state6_1 ← match ← state5_1.tryTactic (goalId := 0) convTactic with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -450,7 +450,7 @@ def test_conv: TestM Unit := do return () let convTactic := "rfl" - let state6 ← match ← state4_1.tryConvTactic (goalId := 0) (convTactic := convTactic) with + let state6 ← match ← state4_1.tryTactic (goalId := 0) convTactic with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString -- 2.44.1 From f3a3ca31a05884e2fa9de0483ef5708672a9163d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 8 Apr 2024 12:45:03 -0700 Subject: [PATCH 10/19] doc: Remove outdated comments --- Pantograph/Goal.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index ed181a3..07a432b 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -263,11 +263,8 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat): let tacticM : Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do state.restoreTacticM goal - -- TODO: Fail if this is already in conv - -- See Lean.Elab.Tactic.Conv.convTarget let convMVar ← Elab.Tactic.withMainContext do - -- TODO: Memorize this `rhs` as a conv resultant goal let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget) Elab.Tactic.setGoals [newGoal.mvarId!] pure rhs.mvarId! -- 2.44.1 From 9fbc65829d24eaded6ed2111555c28daddb94096 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 8 Apr 2024 12:50:41 -0700 Subject: [PATCH 11/19] feat: FFI interface to conv functions --- Pantograph/Library.lean | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 5ac38c8..04d1a57 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -162,15 +162,23 @@ def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) := @[export pantograph_goal_tactic_m] def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult := - runTermElabM <| GoalState.tryTactic state goalId tactic + runTermElabM <| state.tryTactic goalId tactic @[export pantograph_goal_assign_m] def goalAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult := - runTermElabM <| GoalState.tryAssign state goalId expr + runTermElabM <| state.tryAssign goalId expr @[export pantograph_goal_have_m] def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := - runTermElabM <| GoalState.tryHave state goalId binderName type + runTermElabM <| state.tryHave goalId binderName type + +@[export pantograph_goal_conv_m] +def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult := + runTermElabM <| state.conv goalId + +@[export pantograph_goal_conv_exit_m] +def goalConvExit (state: GoalState): Lean.CoreM TacticResult := + runTermElabM <| state.convExit @[export pantograph_goal_continue] def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState := -- 2.44.1 From dd94e29293483e03a0866d6808389271f7a2faac Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 8 Apr 2024 12:54:02 -0700 Subject: [PATCH 12/19] refactor: Monads in library --- Pantograph/Library.lean | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 04d1a57..6da555d 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -136,8 +136,8 @@ def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.E @[export pantograph_expr_echo_m] def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options): - Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do - let termElabM: Lean.Elab.TermElabM _ := do + Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := + runTermElabM do let expr ← match ← parseElabExpr expr expectedType? with | .error e => return .error e | .ok expr => pure expr @@ -149,16 +149,14 @@ def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @& } catch exception => return .error $ errorI "typing" (← exception.toMessageData.toString) - runTermElabM termElabM @[export pantograph_goal_start_expr_m] def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) := - let termElabM: Lean.Elab.TermElabM _ := do + runTermElabM do let expr ← match ← parseElabType expr with | .error e => return .error e | .ok expr => pure $ expr return .ok $ ← GoalState.create expr - runTermElabM termElabM @[export pantograph_goal_tactic_m] def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult := @@ -193,8 +191,8 @@ def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM ( runMetaM <| state.serializeGoals (parent := .none) options @[export pantograph_goal_print_m] -def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := do - let metaM := do +def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := + runMetaM do state.restoreMetaM return { root? := ← state.rootExpr?.mapM (λ expr => do @@ -202,7 +200,6 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto parent? := ← state.parentExpr?.mapM (λ expr => do serialize_expression options (← unfoldAuxLemmas expr)), } - runMetaM metaM end Pantograph -- 2.44.1 From 9a04fd48196951000874a545f287e90febd7a2a3 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 8 Apr 2024 13:12:51 -0700 Subject: [PATCH 13/19] feat: Focus command --- Pantograph/Goal.lean | 11 ++++++++++- Pantograph/Library.lean | 10 +++++++--- 2 files changed, 17 insertions(+), 4 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 07a432b..7609dae 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -327,6 +327,16 @@ protected def GoalState.convExit (state: GoalState): +protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do + let goal ← state.savedState.tactic.goals.get? goalId + return { + state with + savedState := { + state.savedState with + tactic := { goals := [goal] }, + }, + } + /-- Brings into scope a list of goals -/ @@ -345,7 +355,6 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S tactic := { goals := unassigned }, }, } - /-- Brings into scope all goals from `branch` -/ diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 6da555d..0febba4 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -178,14 +178,18 @@ def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult := def goalConvExit (state: GoalState): Lean.CoreM TacticResult := runTermElabM <| state.convExit -@[export pantograph_goal_continue] -def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState := - target.continue branch +@[export pantograph_goal_focus] +def goalFocus (state: GoalState) (goalId: Nat): Option GoalState := + state.focus goalId @[export pantograph_goal_resume] def goalResume (target: GoalState) (goals: Array String): Except String GoalState := target.resume (goals.map (λ n => { name := n.toName }) |>.toList) +@[export pantograph_goal_continue] +def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState := + target.continue branch + @[export pantograph_goal_serialize_m] def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) := runMetaM <| state.serializeGoals (parent := .none) options -- 2.44.1 From 100cdd885f6b6fb853d34c2306c238fe10b2c7d5 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 9 Apr 2024 09:11:15 -0700 Subject: [PATCH 14/19] fix: Coupling from unrelated goals --- Pantograph/Goal.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 7609dae..7e5c0c2 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -32,7 +32,7 @@ structure GoalState where parentMVar: Option MVarId -- Existence of this field shows that we are currently in `conv` mode. - convMVar: Option (MVarId × MVarId × List MVarId) := .none + convMVar: Option (MVarId × MVarId) := .none protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do -- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context. @@ -278,7 +278,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat): savedState := nextSavedState newMVars := newMVarSet prevMCtx nextMCtx, parentMVar := .some goal, - convMVar := .some (convRhs, goal, state.goals), + convMVar := .some (convRhs, goal), } catch exception => return .failure #[← exception.toMessageData.toString] @@ -286,7 +286,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat): /-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/ protected def GoalState.convExit (state: GoalState): Elab.TermElabM TacticResult := do - let (convRhs, convGoal, savedGoals) ← match state.convMVar with + let (convRhs, convGoal) ← match state.convMVar with | .some mvar => pure mvar | .none => return .invalidAction "Not in conv state" let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do @@ -303,7 +303,7 @@ protected def GoalState.convExit (state: GoalState): throwError "convert tactic failed, there are unsolved goals\n{Elab.goalsToMessageData (← Elab.Tactic.getGoals)}" IO.println "Caching" - Elab.Tactic.setGoals savedGoals + Elab.Tactic.setGoals [convGoal] let targetNew ← instantiateMVars (.mvar convRhs) let proof ← instantiateMVars (.mvar convGoal) -- 2.44.1 From 403d92692e056b730c98cfca615a910463ec7399 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 11 Apr 2024 14:59:55 -0700 Subject: [PATCH 15/19] feat: Calc tactic --- Pantograph/Goal.lean | 105 ++++++++++++++++++++++++++++++++++------- Pantograph/Serial.lean | 2 +- Test/Proofs.lean | 63 ++++++++++++++++++++----- 3 files changed, 138 insertions(+), 32 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 7e5c0c2..a6d99bc 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -29,10 +29,12 @@ structure GoalState where newMVars: SSet MVarId -- Parent state metavariable source - parentMVar: Option MVarId + parentMVar?: Option MVarId -- Existence of this field shows that we are currently in `conv` mode. - convMVar: Option (MVarId × MVarId) := .none + convMVar?: Option (MVarId × MVarId) := .none + -- Previous RHS for calc, so we don't have to repeat it every time + calcPrevRhs?: Option Expr := .none protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do -- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context. @@ -48,10 +50,10 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do savedState, root, newMVars := SSet.insert .empty root, - parentMVar := .none, + parentMVar? := .none, } protected def GoalState.isConv (state: GoalState): Bool := - state.convMVar.isSome + state.convMVar?.isSome protected def GoalState.goals (state: GoalState): List MVarId := state.savedState.tactic.goals protected def GoalState.mctx (state: GoalState): MetavarContext := @@ -136,7 +138,7 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri state with savedState := nextSavedState newMVars := newMVarSet prevMCtx nextMCtx, - parentMVar := .some goal, + parentMVar? := .some goal, } /-- Assumes elabM has already been restored. Assumes expr has already typechecked -/ @@ -174,7 +176,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr): tactic := { goals := nextGoals } }, newMVars, - parentMVar := .some goal, + parentMVar? := .some goal, } catch exception => return .failure #[← exception.toMessageData.toString] @@ -247,7 +249,7 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St tactic := { goals := nextGoals } }, newMVars := nextGoals.toSSet, - parentMVar := .some goal, + parentMVar? := .some goal, } catch exception => return .failure #[← exception.toMessageData.toString] @@ -255,7 +257,7 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St /-- Enter conv tactic mode -/ protected def GoalState.conv (state: GoalState) (goalId: Nat): Elab.TermElabM TacticResult := do - if state.convMVar.isSome then + if state.convMVar?.isSome then return .invalidAction "Already in conv state" let goal ← match state.savedState.tactic.goals.get? goalId with | .some goal => pure goal @@ -277,8 +279,8 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat): root := state.root, savedState := nextSavedState newMVars := newMVarSet prevMCtx nextMCtx, - parentMVar := .some goal, - convMVar := .some (convRhs, goal), + parentMVar? := .some goal, + convMVar? := .some (convRhs, goal), } catch exception => return .failure #[← exception.toMessageData.toString] @@ -286,15 +288,13 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat): /-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/ protected def GoalState.convExit (state: GoalState): Elab.TermElabM TacticResult := do - let (convRhs, convGoal) ← match state.convMVar with + let (convRhs, convGoal) ← match state.convMVar? with | .some mvar => pure mvar | .none => return .invalidAction "Not in conv state" let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do -- Vide `Lean.Elab.Tactic.Conv.convert` state.savedState.restore - IO.println "Restored state" - -- Close all existing goals with `refl` for mvarId in (← Elab.Tactic.getGoals) do liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure () @@ -302,7 +302,6 @@ protected def GoalState.convExit (state: GoalState): unless (← Elab.Tactic.getGoals).isEmpty do throwError "convert tactic failed, there are unsolved goals\n{Elab.goalsToMessageData (← Elab.Tactic.getGoals)}" - IO.println "Caching" Elab.Tactic.setGoals [convGoal] let targetNew ← instantiateMVars (.mvar convRhs) @@ -312,19 +311,89 @@ protected def GoalState.convExit (state: GoalState): MonadBacktrack.saveState try let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic - IO.println "Finished caching" let nextMCtx := nextSavedState.term.meta.meta.mctx let prevMCtx := state.savedState.term.meta.meta.mctx return .success { root := state.root, savedState := nextSavedState newMVars := newMVarSet prevMCtx nextMCtx, - parentMVar := .some convGoal, - convMVar := .none + parentMVar? := .some convGoal, + convMVar? := .none } catch exception => return .failure #[← exception.toMessageData.toString] +protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): + Elab.TermElabM TacticResult := do + state.restoreElabM + if state.convMVar?.isSome then + return .invalidAction "Cannot initiate `calc` while in `conv` state" + let goal ← match state.savedState.tactic.goals.get? goalId with + | .some goal => pure goal + | .none => return .indexError goalId + let `(term|$pred) ← match Parser.runParserCategory + (env := state.env) + (catName := `term) + (input := pred) + (fileName := filename) with + | .ok syn => pure syn + | .error error => return .parseError error + try + goal.withContext do + let target ← instantiateMVars (← goal.getDecl).type + let tag := (← goal.getDecl).userName + + let mut step ← Elab.Term.elabType <| ← do + if let some prevRhs := state.calcPrevRhs? then + Elab.Term.annotateFirstHoleWithType pred (← Meta.inferType prevRhs) + else + pure pred + + let some (_, lhs, rhs) ← Elab.Term.getCalcRelation? step | + throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}" + if let some prevRhs := state.calcPrevRhs? then + unless (← Meta.isDefEqGuarded lhs prevRhs) do + throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- " + + -- Creates a mvar to represent the proof that the calc tactic solves the + -- current branch + -- In the Lean `calc` tactic this is gobbled up by + -- `withCollectingNewGoalsFrom` + let mut proof ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) step + (userName := tag ++ `calc) + let mvarBranch := proof.mvarId! + + let calcPrevRhs? := Option.some rhs + let mut proofType ← Meta.inferType proof + let mut remainder := Option.none + + -- The calc tactic either solves the main goal or leaves another relation. + -- Replace the main goal, and save the new goal if necessary + if ¬(← Meta.isDefEq proofType target) then + let rec throwFailed := + throwError "'calc' tactic failed, has type{indentExpr proofType}\nbut it is expected to have type{indentExpr target}" + let some (_, _, rhs) ← Elab.Term.getCalcRelation? proofType | throwFailed + let some (r, _, rhs') ← Elab.Term.getCalcRelation? target | throwFailed + let lastStep := mkApp2 r rhs rhs' + let lastStepGoal ← Meta.mkFreshExprSyntheticOpaqueMVar lastStep tag + (proof, proofType) ← Elab.Term.mkCalcTrans proof proofType lastStepGoal lastStep + unless (← Meta.isDefEq proofType target) do throwFailed + remainder := .some lastStepGoal.mvarId! + goal.assign proof + + let goals := [ mvarBranch ] ++ remainder.toList + return .success { + root := state.root, + savedState := { + term := ← MonadBacktrack.saveState, + tactic := { goals }, + }, + newMVars := goals.toSSet, + parentMVar? := .some goal, + calcPrevRhs? + } + catch exception => + return .failure #[← exception.toMessageData.toString] protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do @@ -377,7 +446,7 @@ protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do assert! goalState.goals.isEmpty return expr protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do - let parent ← goalState.parentMVar + let parent ← goalState.parentMVar? let expr := goalState.mctx.eAssignment.find! parent let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) return expr diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 57df5de..f975f76 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -249,7 +249,7 @@ protected def GoalState.serializeGoals MetaM (Array Protocol.Goal):= do state.restoreMetaM let goals := state.goals.toArray - let parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar.get!) + let parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar?.get!) goals.mapM fun goal => do match state.mctx.findDecl? goal with | .some mvarDecl => diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 7a23290..9ede63e 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -479,36 +479,73 @@ def test_conv: TestM Unit := do let free := [("a", "Nat"), ("b", "Nat"), ("c1", "Nat"), ("c2", "Nat"), ("h", h)] ++ free buildGoal free target -example : ∀ (a: Nat), 1 + a + 1 = a + 2 := by - intro a - calc 1 + a + 1 = a + 1 + 1 := by conv => - rhs - rw [Nat.add_comm] - _ = a + 2 := by rw [Nat.add_assoc] +example : ∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d := by + intro a b c d h1 h2 + calc a + b = b + c := by apply h1 + _ = c + d := by apply h2 def test_calc: TestM Unit := do - let state? ← startProof (.expr "∀ (a: Nat), 1 + a + 1 = a + 2") + let state? ← startProof (.expr "∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d") let state0 ← match state? with | .some state => pure state | .none => do addTest $ assertUnreachable "Goal could not parse" return () - let tactic := "intro a" + let tactic := "intro a b c d h1 h2" 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) = - #[buildGoal [("a", "Nat")] "1 + a + 1 = a + 2"]) - let tactic := "calc" - let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with + #[interiorGoal [] "a + b = c + d"]) + let pred := "a + b = b + c" + let state2 ← match ← state1.tryCalc (goalId := 0) (pred := pred) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = - #[buildGoal [("a", "Nat")] "1 + a + 1 = a + 2"]) + addTest $ LSpec.check s!"calc {pred} := _" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = + #[ + interiorGoal [] "a + b = b + c" (.some "calc"), + interiorGoal [] "b + c = c + d" + ]) + + let tactic := "apply h1" + let state2m ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + let state3 ← match state2m.continue state2 with + | .ok state => pure state + | .error e => do + addTest $ expectationFailure "continue" e + return () + let pred := "_ = c + d" + let state4 ← match ← state3.tryCalc (goalId := 0) (pred := pred) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!"calc {pred} := _" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) = + #[ + interiorGoal [] "b + c = c + d" (.some "calc") + ]) + let tactic := "apply h2" + let state4m ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => 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 suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ -- 2.44.1 From 663651b10eff8627aa3c39dce3f8d8a7a8e75472 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 11 Apr 2024 15:03:14 -0700 Subject: [PATCH 16/19] fix: Remove `calcPrevRhs?` in non-calc tactics --- Pantograph/Goal.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index a6d99bc..fbb850a 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -34,6 +34,7 @@ structure GoalState where -- Existence of this field shows that we are currently in `conv` mode. convMVar?: Option (MVarId × MVarId) := .none -- Previous RHS for calc, so we don't have to repeat it every time + -- WARNING: If using `state with` outside of `calc`, this must be set to `.none` calcPrevRhs?: Option Expr := .none protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do @@ -139,6 +140,7 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri savedState := nextSavedState newMVars := newMVarSet prevMCtx nextMCtx, parentMVar? := .some goal, + calcPrevRhs? := .none, } /-- Assumes elabM has already been restored. Assumes expr has already typechecked -/ @@ -404,6 +406,7 @@ protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState state.savedState with tactic := { goals := [goal] }, }, + calcPrevRhs? := .none, } /-- @@ -423,6 +426,7 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S term := state.savedState.term, tactic := { goals := unassigned }, }, + calcPrevRhs? := .none, } /-- Brings into scope all goals from `branch` -- 2.44.1 From 222cb035d1d0a9f8bda842b8a1f3bab967a8366f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 11 Apr 2024 15:04:36 -0700 Subject: [PATCH 17/19] feat: Add library bindings for calc --- Pantograph/Library.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 0febba4..ff365b2 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -178,6 +178,10 @@ def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult := def goalConvExit (state: GoalState): Lean.CoreM TacticResult := runTermElabM <| state.convExit +@[export pantograph_goal_calc_m] +def goalCalc (state: GoalState) (goalId: Nat) (pred: String): Lean.CoreM TacticResult := + runTermElabM <| state.tryCalc goalId pred + @[export pantograph_goal_focus] def goalFocus (state: GoalState) (goalId: Nat): Option GoalState := state.focus goalId -- 2.44.1 From 327b402cdf398cb0899edf3369980bc8a6e48bdd Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 11 Apr 2024 15:11:10 -0700 Subject: [PATCH 18/19] feat: REPL interface for `calc` --- Pantograph.lean | 17 ++++++++++++----- Pantograph/Protocol.lean | 5 ++++- 2 files changed, 16 insertions(+), 6 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index 626afae..a0580d2 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -114,15 +114,22 @@ def execute (command: Protocol.Command): MainM Lean.Json := do match state.goalStates.find? args.stateId with | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" | .some goalState => do - let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr?, args.have? with - | .some tactic, .none, .none => do + let nextGoalState?: Except _ GoalState ← + match args.tactic?, args.expr?, args.have?, args.calc?, args.conv? with + | .some tactic, .none, .none, .none, .none => do pure ( Except.ok (← goalTactic goalState args.goalId tactic)) - | .none, .some expr, .none => do + | .none, .some expr, .none, .none, .none => do pure ( Except.ok (← goalAssign goalState args.goalId expr)) - | .none, .none, .some type => do + | .none, .none, .some type, .none, .none => do let binderName := args.binderName?.getD "" pure ( Except.ok (← goalHave goalState args.goalId binderName type)) - | _, _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr, have} must be supplied") + | .none, .none, .none, .some pred, .none => do + pure ( Except.ok (← goalCalc goalState args.goalId pred)) + | .none, .none, .none, .none, .some true => do + pure ( Except.ok (← goalConv goalState args.goalId)) + | .none, .none, .none, .none, .some false => do + pure ( Except.ok (← goalConvExit goalState)) + | _, _, _, _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr, have} must be supplied") match nextGoalState? with | .error error => return .error error | .ok (.success nextGoalState) => diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 3055136..86ab14b 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -202,8 +202,11 @@ structure GoalTactic where tactic?: Option String := .none expr?: Option String := .none have?: Option String := .none + calc?: Option String := .none + -- true to enter `conv`, `false` to exit. In case of exit the `goalId` is ignored. + conv?: Option Bool := .none - -- In case of the `have` tactic, the new free variable name + -- In case of the `have` tactic, the new free variable name is provided here binderName?: Option String := .none deriving Lean.FromJson -- 2.44.1 From db35ec7187cfad262640458dc926ca7349f74eab Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 11 Apr 2024 15:13:12 -0700 Subject: [PATCH 19/19] doc: New tactics in README.md --- README.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index f60ee22..4a8f448 100644 --- a/README.md +++ b/README.md @@ -81,7 +81,12 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` - `options.print`: Display the current set of options - `goal.start {["name": ], ["expr": ], ["copyFrom": ]}`: Start a new goal from a given expression or symbol -- `goal.tactic {"stateId": , "goalId": , ["tactic": ], ["expr": ]}`: Execute a tactic string on a given goal +- `goal.tactic {"stateId": , "goalId": , ["tactic": ], ["expr": + ]}`: Execute a tactic string on a given goal. `tactic` executes an + ordinary tactic, `expr` assigns an expression to the current goal, `have` + executes the have tactic, ``calc` (of the form `lhs op rhs`) executes one step + of `calc`, and `"conv": true`/`"conv": false` enters/exits conversion tactic + mode. - `goal.continue {"stateId": , ["branch": ], ["goals": ]}`: Continue from a proof state - `goal.remove {"stateIds": []}"`: Remove a bunch of stored goals. - `goal.print {"stateId": }"`: Print a goal state -- 2.44.1