From c781797898f0122879247dbc2da71c1d19d21913 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 22 May 2023 22:48:48 -0700 Subject: [PATCH] Save core state in proofs --- Main.lean | 5 +---- Pantograph/Meta.lean | 35 ++++++++++++++++++++++++++++------- Test/Proofs.lean | 18 ++++++++++++++++-- 3 files changed, 45 insertions(+), 13 deletions(-) diff --git a/Main.lean b/Main.lean index ad84760..60a59b9 100644 --- a/Main.lean +++ b/Main.lean @@ -200,10 +200,7 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do match state.proofTrees.get? args.treeId with | .none => return Lean.toJson <| errorIndex "Invalid tree index {args.treeId}" | .some tree => - let parents := tree.states.map λ state => match state.parent with - | .none => "" - | .some parent => s!"{parent}.{state.parentGoalId}" - return Lean.toJson ({parents := parents}: ProofPrintTreeResult) + return Lean.toJson ({parents := tree.structure_array}: ProofPrintTreeResult) end Pantograph diff --git a/Pantograph/Meta.lean b/Pantograph/Meta.lean index e0216a6..f6209f8 100644 --- a/Pantograph/Meta.lean +++ b/Pantograph/Meta.lean @@ -27,11 +27,22 @@ structure ProofState where parentGoalId : Nat := 0 structure ProofTree where -- All parameters needed to run a `TermElabM` monad - env: Lean.Environment name: Lean.Name coreContext : Lean.Core.Context elabContext : Lean.Elab.Term.Context + /- + This state must be saved so it preserves existing variable assignments. See + + https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Resume.20proof.20in.20IO.20monad/near/360429763 + + It is unknown what will happen to this in the case of backtracking. Since we + never delete any proof states, it should be fine to store this here for now. A + test case `Or.comm` illustrates branching which will fail if the core state is + replaced every time. + -/ + coreState : Lean.Core.State + -- Set of proof states states : Array ProofState := #[] @@ -39,24 +50,34 @@ abbrev ProofM := StateRefT ProofTree IO def createProofTree (name: Lean.Name) (env: Lean.Environment) (coreContext: Lean.Core.Context): ProofTree := { - env := env, name := name, coreContext := coreContext, elabContext := { declName? := some (name ++ "_pantograph"), errToSorry := false } + coreState := { + env := env + } } +-- Tree structures + +def ProofTree.structure_array (tree: ProofTree): Array String := + tree.states.map λ state => match state.parent with + | .none => "" + | .some parent => s!"{parent}.{state.parentGoalId}" + -- Executing a `TermElabM` def ProofM.runTermElabM (termElabM: Lean.Elab.TermElabM α): ProofM (α × Lean.Core.State) := do let context ← get let metaM : Lean.MetaM α := termElabM.run' (ctx := context.elabContext) let coreM : Lean.CoreM α := metaM.run' - let coreState : Lean.Core.State := { env := context.env } - coreM.toIO context.coreContext coreState + coreM.toIO context.coreContext context.coreState def ProofM.runTermElabM' (termElabM: Lean.Elab.TermElabM α): ProofM α := do - return Prod.fst <| ← ProofM.runTermElabM termElabM + let (ret, coreState) ← ProofM.runTermElabM termElabM + set { ← get with coreState := coreState } + return ret -- Parsing syntax under the environment def ProofM.syntax_to_expr (syn: Lean.Syntax): ProofM (Except String Lean.Expr) := do @@ -103,11 +124,11 @@ def execute_tactic (env: Lean.Environment) (state: Lean.Elab.Tactic.SavedState) (fileName := "") with | Except.error err => return .error #[err] | Except.ok stx => do - state.term.restore let tac : Lean.Elab.Tactic.TacticM Unit := set state.tactic *> Lean.Elab.Tactic.evalTactic stx match state.tactic.goals.get? goalId with | .none => return .error #[s!"Invalid goalId {goalId}"] | .some mvarId => + state.term.restore try Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing let unsolvedGoals ← Lean.Elab.Tactic.run mvarId tac @@ -146,7 +167,7 @@ def ProofM.execute (stateId: Nat) (goalId: Nat) (tactic: String): ProofM TacticR match context.states.get? stateId with | .none => return .invalid s!"Invalid state id {stateId}" | .some state => - match (← ProofM.runTermElabM' <| execute_tactic (env := context.env) (state := state.savedState) (goalId := goalId) (tactic := tactic)) with + match (← ProofM.runTermElabM' <| execute_tactic (env := context.coreState.env) (state := state.savedState) (goalId := goalId) (tactic := tactic)) with | .error errors => return .failure errors | .ok nextState => diff --git a/Test/Proofs.lean b/Test/Proofs.lean index f422dc4..9dd6bb8 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -65,6 +65,9 @@ def proof_step (stateId: Nat) (goalId: Nat) (tactic: String) return LSpec.test s!"{stateId}.{goalId} {tactic}" (result = expected) | _, _ => return LSpec.test s!"{stateId}.{goalId} {tactic}" (result = expected) +def proof_inspect (expected: Array String) : Meta.ProofM LSpec.TestSeq := do + let result := (← get).structure_array + return LSpec.test s!"Tree structure" (result = expected) def proof_runner (start: Start) (steps: List (Meta.ProofM LSpec.TestSeq)): IO LSpec.TestSeq := do let (testSeq, state?) ← start_proof start @@ -96,6 +99,7 @@ def proof_nat_add_comm_manual: IO LSpec.TestSeq := do (.success .none #[]) ] +-- Two ways to write the same theorem example: ∀ (p q: Prop), p ∨ q → q ∨ p := by intro p q h cases h @@ -103,20 +107,30 @@ example: ∀ (p q: Prop), p ∨ q → q ∨ p := by assumption apply Or.inl assumption +example: ∀ (p q: Prop), p ∨ q → q ∨ p := by + intro p q h + cases h + . apply Or.inr + assumption + . apply Or.inl + assumption def proof_or_comm: IO LSpec.TestSeq := do proof_runner (.expr "∀ (p q: Prop), p ∨ q → q ∨ p") [ proof_step 0 0 "intro p q h" (.success (.some 1) #["p q : Prop\nh : p ∨ q\n⊢ q ∨ p"]), proof_step 1 0 "cases h" (.success (.some 2) #[]), + proof_inspect #["", "0.0", "1.0"], proof_step 2 0 "apply Or.inr" - (.success (.some 3) #[]), + (.success (.some 3) #[""]), + proof_inspect #["", "0.0", "1.0", "2.0"], proof_step 3 0 "assumption" (.success .none #[]), proof_step 2 1 "apply Or.inl" (.success (.some 4) #[]), proof_step 4 0 "assumption" - (.success .none #[]) + (.success .none #[]), + proof_inspect #["", "0.0", "1.0", "2.0", "1.1"] ] def test_proofs : IO LSpec.TestSeq := do