From aa8da3014ed0695a2d3176000ca4aa7c89fb5802 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 6 Apr 2024 21:52:25 -0700 Subject: [PATCH] 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