From 4db09c3abc67149807ac21dd843cb031ee361461 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 1 May 2025 13:05:04 -0400 Subject: [PATCH] feat(goal): Check unsafe and sorry --- Pantograph/Goal.lean | 16 ++++++++-------- Pantograph/Library.lean | 7 ++++++- Pantograph/Protocol.lean | 7 +++++++ Test/Integration.lean | 5 ++++- Test/Metavar.lean | 20 ++++++++++---------- Test/Proofs.lean | 20 ++++++++++---------- 6 files changed, 45 insertions(+), 30 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 21d6dc1..38057be 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -162,18 +162,18 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except target.resume (goals := branch.goals) @[export pantograph_goal_state_root_expr] -protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do +protected def GoalState.rootExpr? (goalState : GoalState): Option Expr := do if goalState.root.name == .anonymous then .none let expr ← goalState.mctx.eAssignment.find? goalState.root let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) - if expr.hasExprMVar then - -- Must not assert that the goal state is empty here. We could be in a branch goal. - --assert! ¬goalState.goals.isEmpty - .none - else - assert! goalState.goals.isEmpty - return expr + return expr +@[export pantograph_goal_state_is_solved] +protected def GoalState.isSolved (goalState : GoalState) : Bool := + let solvedRoot := match goalState.rootExpr? with + | .some e => ¬ e.hasExprMVar + | .none => true + goalState.goals.isEmpty && solvedRoot @[export pantograph_goal_state_parent_expr] protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do let parent ← goalState.parentMVar? diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index e26b4ff..44630fa 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -123,8 +123,9 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo : CoreM Protocol.GoalPrintResult := runMetaM do state.restoreMetaM + let rootExpr? := state.rootExpr? let root? ← if rootExpr then - state.rootExpr?.mapM λ expr => state.withRootContext do + rootExpr?.mapM λ expr => state.withRootContext do serializeExpression options (← instantiateAll expr) else pure .none @@ -143,11 +144,15 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo state.withContext mvarId do let .some expr ← getExprMVarAssignment? mvarId | return {} serializeExpression options (← instantiateAll expr) + let env ← getEnv return { root?, parent?, goals, extraMVars, + rootHasSorry := rootExpr?.map (·.hasSorry) |>.getD false, + rootHasUnsafe := rootExpr?.map (env.hasUnsafe ·) |>.getD false, + rootHasMVar := rootExpr?.map (·.hasExprMVar) |>.getD false, } @[export pantograph_goal_have_m] diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 07f68e6..d77afd4 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -276,6 +276,9 @@ structure GoalTacticResult where -- Existence of this field shows the tactic parsing has failed parseError? : Option String := .none + + hasSorry : Bool := false + hasUnsafe : Bool := false deriving Lean.ToJson structure GoalContinue where -- State from which the continuation acquires the context @@ -319,6 +322,10 @@ structure GoalPrintResult where parent?: Option Expression := .none goals: Array Goal := #[] extraMVars: Array Expression := #[] + + rootHasSorry : Bool := false + rootHasUnsafe : Bool := false + rootHasMVar : Bool := true deriving Lean.ToJson -- Diagnostic Options, not available in REPL diff --git a/Test/Integration.lean b/Test/Integration.lean index 510753e..beec62a 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -84,7 +84,10 @@ def test_tactic : Test := step "goal.tactic" ({ stateId := 0, tactic? := .some "intro x" }: Protocol.GoalTactic) ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult), step "goal.print" ({ stateId := 1, parentExpr? := .some true, rootExpr? := .some true }: Protocol.GoalPrint) - ({ parent? := .some { pp? := .some "fun x => ?m.11" }, }: Protocol.GoalPrintResult), + ({ + root? := .some { pp? := "fun x => ?m.11"}, + parent? := .some { pp? := .some "fun x => ?m.11" }, + }: Protocol.GoalPrintResult), step "goal.tactic" ({ stateId := 1, tactic? := .some "intro y" }: Protocol.GoalTactic) ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult), step "goal.tactic" ({ stateId := 1, tactic? := .some "apply Nat.le_of_succ_le" }: Protocol.GoalTactic) diff --git a/Test/Metavar.lean b/Test/Metavar.lean index 8f355b8..8322abf 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -85,14 +85,14 @@ def test_m_couple: TestM Unit := do return () addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) = #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"]) - addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone + checkTrue "(1 root)" $ ¬ state1.isSolved -- Set m to 3 let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 3") with | .success state _ => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone + checkTrue "(1b root)" $ ¬ state2.isSolved let state1b ← match state2.continue state1 with | .error msg => do addTest $ assertUnreachable $ msg @@ -100,7 +100,7 @@ def test_m_couple: TestM Unit := do | .ok state => pure state addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = #[.some "2 ≤ 3", .some "3 ≤ 5"]) - addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone + checkTrue "(2 root)" $ ¬ state1b.isSolved def test_m_couple_simp: TestM Unit := do let state? ← startProof "(2: Nat) ≤ 5" @@ -126,7 +126,7 @@ def test_m_couple_simp: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone + checkTrue "(1b root)" $ ¬ state2.isSolved let state1b ← match state2.continue state1 with | .error msg => do addTest $ assertUnreachable $ msg @@ -134,7 +134,7 @@ def test_m_couple_simp: TestM Unit := do | .ok state => pure state 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 + checkTrue "(2 root)" $ ¬ state1b.isSolved let state3 ← match ← state1b.tacticOn (goalId := 0) (tactic := "simp") with | .success state _ => pure state | other => do @@ -184,7 +184,7 @@ def test_proposition_generation: TestM Unit := do ]) if let #[goal1, goal2] := ← state1.serializeGoals (options := { (← read) with printExprAST := true }) then addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})") - addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone + checkTrue "(1 root)" $ ¬ state1.isSolved let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := "λ (x: Nat) => _") with | .success state _ => pure state @@ -193,7 +193,7 @@ def test_proposition_generation: TestM Unit := do return () addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) = #[.some "?m.30 x"]) - addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone + checkTrue "(2 root)" $ ¬ state2.isSolved let assign := "Eq.refl x" let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := assign) with @@ -204,7 +204,7 @@ def test_proposition_generation: TestM Unit := do addTest $ LSpec.check s!":= {assign}" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) = #[]) - addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome + checkTrue "(3 root)" state3.isSolved return () def test_partial_continuation: TestM Unit := do @@ -240,7 +240,7 @@ def test_partial_continuation: TestM Unit := do | .ok state => pure state addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"]) - addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone + checkTrue "(2 root)" state1b.rootExpr?.get!.hasExprMVar -- Roundtrip --let coupled_goals := coupled_goals.map (λ g => @@ -254,7 +254,7 @@ def test_partial_continuation: TestM Unit := do | .ok state => pure state addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"]) - addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone + checkTrue "(2 root)" state1b.rootExpr?.get!.hasExprMVar -- Continuation should fail if the state does not exist: match state0.resume coupled_goals with diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 178d8d2..2436e13 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -192,14 +192,14 @@ def test_arith: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check tactic (state1.goals.length = 1) - addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone + checkTrue "(1 root)" state1.rootExpr?.get!.hasExprMVar let state2 ← match ← state1.tacticOn (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 + checkTrue "(2 root)" state2.rootExpr?.get!.hasExprMVar let tactic := "assumption" let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with | .success state _ => pure state @@ -207,7 +207,7 @@ def test_arith: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.test tactic state3.goals.isEmpty - addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome + checkTrue "(3 root)" $ ¬ state3.rootExpr?.get!.hasExprMVar return () -- Two ways to write the same theorem @@ -257,8 +257,8 @@ def test_or_comm: TestM Unit := do { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" } } ] }]) - addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome - addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone + checkTrue "(1 parent)" state1.parentExpr?.isSome + checkTrue "(1 root)" $ ¬ state1.isSolved let state1parent ← state1.withParentContext do serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) @@ -276,8 +276,8 @@ def test_or_comm: TestM Unit := do let (caseL, caseR) := (state2g0.name.toString, state2g1.name.toString) addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) = #[caseL, caseR]) - addTest $ LSpec.check "(2 parent exists)" state2.parentExpr?.isSome - addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone + checkTrue "(2 parent exists)" state2.parentExpr?.isSome + checkTrue "(2 root)" $ ¬ state2.isSolved let state2parent ← state2.withParentContext do serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) @@ -308,7 +308,7 @@ def test_or_comm: TestM Unit := do addTest $ LSpec.check " assumption" state4_1.goals.isEmpty let state4_1parent ← instantiateAll state4_1.parentExpr?.get! addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar - addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone + checkTrue "(4_1 root)" $ ¬ state4_1.isSolved let state3_2 ← match ← state2.tacticOn (goalId := 1) (tactic := "apply Or.inl") with | .success state _ => pure state | other => do @@ -321,7 +321,7 @@ def test_or_comm: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check " assumption" state4_2.goals.isEmpty - addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr?.isNone + checkTrue "(4_2 root)" $ ¬ state4_2.isSolved -- Ensure the proof can continue from `state4_2`. let state2b ← match state4_2.continue state2 with | .error msg => do @@ -341,7 +341,7 @@ def test_or_comm: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check " assumption" state4_1.goals.isEmpty - addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isSome + checkTrue "(4_1 root)" $ ¬ state4_1.rootExpr?.get!.hasExprMVar return () where