feat(goal): Detect unsafe and sorry #201
|
@ -140,8 +140,7 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S
|
|||
-- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
|
||||
let unassigned := goals.filter λ goal =>
|
||||
let isSolved := state.mctx.eAssignment.contains goal || state.mctx.dAssignment.contains goal
|
||||
let isDuplicate := state.goals.contains goal
|
||||
(¬ isDuplicate) && (¬ isSolved)
|
||||
¬ isSolved
|
||||
return {
|
||||
state with
|
||||
savedState := {
|
||||
|
@ -162,18 +161,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?
|
||||
|
|
|
@ -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]
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -338,11 +338,14 @@ def execute (command: Protocol.Command): MainM Json := do
|
|||
pure result
|
||||
| false, _ => pure nextGoalState
|
||||
let nextStateId ← newGoalState nextGoalState
|
||||
let parentExpr := nextGoalState.parentExpr?.get!
|
||||
let goals ← runCoreM $ nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
|
||||
return {
|
||||
nextStateId? := .some nextStateId,
|
||||
goals? := .some goals,
|
||||
messages? := .some messages,
|
||||
hasSorry := parentExpr.hasSorry,
|
||||
hasUnsafe := (← getEnv).hasUnsafe parentExpr,
|
||||
}
|
||||
| .ok (.parseError message) =>
|
||||
return { messages? := .none, parseError? := .some message }
|
||||
|
|
|
@ -84,12 +84,17 @@ 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)
|
||||
({ messages? := .some #["tactic 'apply' failed, failed to unify\n ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith\n ∀ (q : Prop), x ∨ q → q ∨ x\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }:
|
||||
Protocol.GoalTacticResult)
|
||||
Protocol.GoalTacticResult),
|
||||
step "goal.tactic" ({ stateId := 0, tactic? := .some "sorry" }: Protocol.GoalTactic)
|
||||
({ nextStateId? := .some 3, goals? := .some #[], hasSorry := true }: Protocol.GoalTacticResult),
|
||||
]
|
||||
example : (1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3 := by
|
||||
simp
|
||||
|
|
|
@ -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
|
||||
|
@ -238,23 +238,23 @@ def test_partial_continuation: TestM Unit := do
|
|||
addTest $ assertUnreachable $ msg
|
||||
return ()
|
||||
| .ok state => pure state
|
||||
addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
|
||||
addTest $ LSpec.check "(continue 1)" ((← 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 =>
|
||||
-- { name := str_to_name $ serializeName g.name (sanitize := false)})
|
||||
let coupled_goals := coupled_goals.map (λ g => serializeName g.name (sanitize := false))
|
||||
let coupled_goals := coupled_goals.map (λ g => { name := g.toName })
|
||||
let coupled_goals := coupled_goals.map (·.name.toString)
|
||||
let coupled_goals := coupled_goals.map ({ name := ·.toName })
|
||||
let state1b ← match state2.resume (goals := coupled_goals) with
|
||||
| .error msg => do
|
||||
addTest $ assertUnreachable $ msg
|
||||
return ()
|
||||
| .ok state => pure state
|
||||
addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
|
||||
addTest $ LSpec.check "(continue 2)" ((← 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
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in New Issue