From ace2ddf478e16b53de86bd42a444108b8bab28a4 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 6 Apr 2024 16:33:20 -0700 Subject: [PATCH] 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))