Simplify goal bookkeeping mechanism #10

Merged
aniva merged 5 commits from tactic/book into dev 2023-08-30 19:18:37 -07:00
7 changed files with 435 additions and 260 deletions

View File

@ -2,6 +2,7 @@ import Pantograph.Commands
import Pantograph.Serial import Pantograph.Serial
import Pantograph.Symbols import Pantograph.Symbols
import Pantograph.Tactic import Pantograph.Tactic
import Pantograph.SemihashMap
namespace Pantograph namespace Pantograph
@ -11,8 +12,7 @@ structure Context where
/-- Stores state of the REPL -/ /-- Stores state of the REPL -/
structure State where structure State where
options: Commands.Options := {} options: Commands.Options := {}
--environments: Array Lean.Environment := #[] goalStates: SemihashMap GoalState := SemihashMap.empty
proofTrees: Array ProofTree := #[]
-- State monad -- State monad
abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM) abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM)
@ -30,14 +30,15 @@ def execute (command: Commands.Command): MainM Lean.Json := do
| .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}" | .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
match command.cmd with match command.cmd with
| "reset" => run reset | "reset" => run reset
| "stat" => run stat
| "expr.echo" => run expr_echo | "expr.echo" => run expr_echo
| "lib.catalog" => run lib_catalog | "lib.catalog" => run lib_catalog
| "lib.inspect" => run lib_inspect | "lib.inspect" => run lib_inspect
| "options.set" => run options_set | "options.set" => run options_set
| "options.print" => run options_print | "options.print" => run options_print
| "proof.start" => run proof_start | "goal.start" => run goal_start
| "proof.tactic" => run proof_tactic | "goal.tactic" => run goal_tactic
| "proof.printTree" => run proof_print_tree | "goal.delete" => run goal_delete
| cmd => | cmd =>
let error: Commands.InteractionError := let error: Commands.InteractionError :=
errorCommand s!"Unknown command {cmd}" errorCommand s!"Unknown command {cmd}"
@ -47,11 +48,15 @@ def execute (command: Commands.Command): MainM Lean.Json := do
errorCommand := errorI "command" errorCommand := errorI "command"
errorIndex := errorI "index" errorIndex := errorI "index"
-- Command Functions -- Command Functions
reset (_: Commands.Reset): MainM (CR Commands.ResetResult) := do reset (_: Commands.Reset): MainM (CR Commands.StatResult) := do
let state ← get let state ← get
let nTrees := state.proofTrees.size let nGoals := state.goalStates.size
set { state with proofTrees := #[] } set { state with goalStates := SemihashMap.empty }
return .ok { nTrees := nTrees } return .ok { nGoals }
stat (_: Commands.Stat): MainM (CR Commands.StatResult) := do
let state ← get
let nGoals := state.goalStates.size
return .ok { nGoals }
lib_catalog (_: Commands.LibCatalog): MainM (CR Commands.LibCatalogResult) := do lib_catalog (_: Commands.LibCatalog): MainM (CR Commands.LibCatalogResult) := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let names := env.constants.fold (init := #[]) (λ acc name info => let names := env.constants.fold (init := #[]) (λ acc name info =>
@ -113,7 +118,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do
return .ok { } return .ok { }
options_print (_: Commands.OptionsPrint): MainM (CR Commands.OptionsPrintResult) := do options_print (_: Commands.OptionsPrint): MainM (CR Commands.OptionsPrintResult) := do
return .ok (← get).options return .ok (← get).options
proof_start (args: Commands.ProofStart): MainM (CR Commands.ProofStartResult) := do goal_start (args: Commands.GoalStart): MainM (CR Commands.GoalStartResult) := do
let state ← get let state ← get
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let expr?: Except _ Lean.Expr ← (match args.expr, args.copyFrom with let expr?: Except _ Lean.Expr ← (match args.expr, args.copyFrom with
@ -134,32 +139,36 @@ def execute (command: Commands.Command): MainM Lean.Json := do
match expr? with match expr? with
| .error error => return .error error | .error error => return .error error
| .ok expr => | .ok expr =>
let tree ← ProofTree.create expr let goalState ← GoalState.create expr
-- Put the new tree in the environment let (goalStates, goalId) := state.goalStates.insert goalState
let nextTreeId := state.proofTrees.size set { state with goalStates }
set { state with proofTrees := state.proofTrees.push tree } return .ok { goalId }
return .ok { treeId := nextTreeId } goal_tactic (args: Commands.GoalTactic): MainM (CR Commands.GoalTacticResult) := do
proof_tactic (args: Commands.ProofTactic): MainM (CR Commands.ProofTacticResult) := do
let state ← get let state ← get
match state.proofTrees.get? args.treeId with match state.goalStates.get? args.goalId with
| .none => return .error $ errorIndex "Invalid tree index {args.treeId}" | .none => return .error $ errorIndex s!"Invalid goal index {args.goalId}"
| .some tree => | .some goalState =>
let (result, nextTree) ← ProofTree.execute let result ← GoalState.execute goalState args.tactic |>.run state.options
(stateId := args.stateId)
(goalId := args.goalId.getD 0)
(tactic := args.tactic) |>.run state.options |>.run tree
match result with match result with
| .invalid message => return .error $ errorIndex message | .success goals =>
| .success nextId? goals => if goals.isEmpty then
set { state with proofTrees := state.proofTrees.set! args.treeId nextTree } return .ok {}
return .ok { nextId? := nextId?, goals? := .some goals } else
-- Append all goals
let (goalStates, goalIds, sGoals) := Array.foldl (λ acc itr =>
let (map, indices, serializedGoals) := acc
let (goalState, sGoal) := itr
let (map, index) := map.insert goalState
(map, index :: indices, sGoal :: serializedGoals)
) (state.goalStates, [], []) goals
set { state with goalStates }
return .ok { goals? := .some sGoals.reverse.toArray, goalIds? := .some goalIds.reverse.toArray }
| .failure messages => | .failure messages =>
return .ok { tacticErrors? := .some messages } return .ok { tacticErrors? := .some messages }
proof_print_tree (args: Commands.ProofPrintTree): MainM (CR Commands.ProofPrintTreeResult) := do goal_delete (args: Commands.GoalDelete): MainM (CR Commands.GoalDeleteResult) := do
let state ← get let state ← get
match state.proofTrees.get? args.treeId with let goalStates := args.goalIds.foldl (λ map id => map.remove id) state.goalStates
| .none => return .error $ errorIndex "Invalid tree index {args.treeId}" set { state with goalStates }
| .some tree => return .ok {}
return .ok { parents := tree.structure_array }
end Pantograph end Pantograph

View File

@ -80,8 +80,11 @@ structure InteractionError where
structure Reset where structure Reset where
deriving Lean.FromJson deriving Lean.FromJson
structure ResetResult where structure Stat where
nTrees: Nat deriving Lean.FromJson
structure StatResult where
-- Number of goals states
nGoals: Nat
deriving Lean.ToJson deriving Lean.ToJson
-- Return the type of an expression -- Return the type of an expression
@ -127,35 +130,34 @@ structure OptionsPrint where
deriving Lean.FromJson deriving Lean.FromJson
abbrev OptionsPrintResult := Options abbrev OptionsPrintResult := Options
structure ProofStart where structure GoalStart where
-- Only one of the fields below may be populated. -- Only one of the fields below may be populated.
expr: Option String -- Proof expression expr: Option String -- Proof expression
copyFrom: Option String -- Theorem name copyFrom: Option String -- Theorem name
deriving Lean.FromJson deriving Lean.FromJson
structure ProofStartResult where structure GoalStartResult where
treeId: Nat := 0 -- Proof tree id goalId: Nat := 0 -- Proof tree id
deriving Lean.ToJson deriving Lean.ToJson
structure ProofTactic where structure GoalTactic where
-- Identifiers for tree, state, and goal -- Identifiers for tree, state, and goal
treeId: Nat goalId: Nat
stateId: Nat
goalId: Option Nat -- Defaults to 0
tactic: String tactic: String
deriving Lean.FromJson deriving Lean.FromJson
structure ProofTacticResult where structure GoalTacticResult where
-- Existence of this field shows success -- Existence of this field shows success
goals?: Option (Array Goal) := .none goals?: Option (Array Goal) := .none
-- Next proof state id, if successful -- Next proof state id, if successful
nextId?: Option Nat := .none goalIds?: Option (Array Nat) := .none
-- Existence of this field shows failure -- Existence of this field shows failure
tacticErrors?: Option (Array String) := .none tacticErrors?: Option (Array String) := .none
deriving Lean.ToJson deriving Lean.ToJson
structure ProofPrintTree where
treeId: Nat -- Remove a bunch of goals.
structure GoalDelete where
goalIds: List Nat
deriving Lean.FromJson deriving Lean.FromJson
structure ProofPrintTreeResult where structure GoalDeleteResult where
-- "" if no parents, otherwise "parentId.goalId"
parents: Array String
deriving Lean.ToJson deriving Lean.ToJson
end Pantograph.Commands end Pantograph.Commands

149
Pantograph/SemihashMap.lean Normal file
View File

@ -0,0 +1,149 @@
namespace Pantograph.SemihashMap
structure Imp (β: Type u) where
data: Array (Option β)
-- Number of elements currently in use
size: Nat
-- Next index that has never been touched
allocFront: Nat
-- Deallocated indices
deallocs: Array Nat
-- Number of valid entries in `deallocs` array
lastDealloc: Nat
namespace Imp
structure WF (m: Imp β): Prop where
capacity: m.data.size = m.deallocs.size
front_dealloc: ∀ i: Fin m.deallocs.size, (i < m.allocFront) → (m.deallocs.get i) < m.allocFront
front_data: ∀ i: Fin m.data.size, (i ≥ m.allocFront) → (m.data.get i).isNone
def empty (capacity := 16): Imp β :=
{
data := mkArray capacity .none,
size := 0,
allocFront := 0,
deallocs := mkArray capacity 0,
lastDealloc := 0,
}
private theorem list_get_replicate (x: α) (i: Fin (List.replicate n x).length):
List.get (List.replicate n x) i = x := by
sorry
theorem empty_wf : WF (empty n: Imp β) := by
unfold empty
apply WF.mk
case capacity =>
conv =>
lhs
congr
simp
conv =>
rhs
congr
simp
simp
case front_dealloc =>
simp_all
intro i
intro a
contradiction
case front_data =>
simp_all
intro i
unfold Imp.data at i
simp at i
conv =>
lhs
unfold Array.get
unfold mkArray
simp [List.replicate]
rewrite [list_get_replicate]
-- FIXME: Merge this with the well-formed versions below so proof and code can
-- mesh seamlessly.
@[inline] def insert (map: Imp β) (v: β): (Imp β × Nat) :=
match map.lastDealloc with
| 0 => -- Capacity is full, buffer expansion is required
if map.size == map.data.size then
let nextIndex := map.data.size
let extendCapacity := map.size
let result: Imp β := {
data := (map.data.append #[Option.some v]).append (mkArray extendCapacity .none),
size := map.size + 1,
allocFront := map.size + 1,
deallocs := mkArray (map.data.size + 1 + extendCapacity) 0,
lastDealloc := 0,
}
(result, nextIndex)
else
let nextIndex := map.size
let result: Imp β := {
map
with
data := map.data.set ⟨nextIndex, sorry⟩ (Option.some v),
size := map.size + 1,
allocFront := map.allocFront + 1,
}
(result, nextIndex)
| (.succ k) => -- Allocation list has space
let nextIndex := map.deallocs.get! k
let result: Imp β := {
map with
data := map.data.set ⟨nextIndex, sorry⟩ (Option.some v),
size := map.size + 1,
lastDealloc := map.lastDealloc - 1
}
(result, nextIndex)
@[inline] def remove (map: Imp β) (index: Fin (map.size)): Imp β :=
have h: index.val < map.data.size := by sorry
match map.data.get ⟨index.val, h⟩ with
| .none => map
| .some _ =>
{
map with
data := map.data.set ⟨index, sorry⟩ .none,
size := map.size - 1,
deallocs := map.deallocs.set ⟨map.lastDealloc, sorry⟩ index,
lastDealloc := map.lastDealloc + 1,
}
/-- Retrieval is efficient -/
@[inline] def get? (map: Imp β) (index: Fin (map.size)): Option β :=
have h: index.val < map.data.size := by sorry
map.data.get ⟨index.val, h⟩
@[inline] def capacity (map: Imp β): Nat := map.data.size
end Imp
/--
This is like a hashmap but you cannot control the keys.
-/
def _root_.Pantograph.SemihashMap β := {m: Imp β // m.WF}
@[inline] def empty (capacity := 16): SemihashMap β :=
⟨ Imp.empty capacity, Imp.empty_wf ⟩
@[inline] def insert (map: SemihashMap β) (v: β): (SemihashMap β × Nat) :=
let ⟨imp, pre⟩ := map
let ⟨result, id⟩ := imp.insert v
( ⟨ result, sorry ⟩, id)
@[inline] def remove (map: SemihashMap β) (index: Nat): SemihashMap β :=
let ⟨imp, pre⟩ := map
let result := imp.remove ⟨index, sorry⟩
⟨ result, sorry ⟩
@[inline] def get? (map: SemihashMap β) (index: Nat): Option β :=
let ⟨imp, _⟩ := map
imp.get? ⟨index, sorry⟩
@[inline] def size (map: SemihashMap β): Nat :=
let ⟨imp, _⟩ := map
imp.size
end Pantograph.SemihashMap

View File

@ -24,35 +24,22 @@ def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
namespace Pantograph namespace Pantograph
open Lean open Lean
structure ProofState where structure GoalState where
goals : List MVarId mvarId: MVarId
savedState : Elab.Tactic.SavedState savedState : Elab.Tactic.SavedState
parent : Option Nat := none
parentGoalId : Nat := 0
structure ProofTree where
-- Set of proof states
states : Array ProofState := #[]
abbrev M := Elab.TermElabM abbrev M := Elab.TermElabM
def ProofTree.create (expr: Expr): M ProofTree := do def GoalState.create (expr: Expr): M GoalState := do
let expr ← instantiateMVars expr let expr ← instantiateMVars expr
let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic)) let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic))
let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]} let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]}
return { return {
states := #[{
savedState := savedState, savedState := savedState,
goals := [goal.mvarId!] mvarId := goal.mvarId!
}]
} }
-- Print the tree structures in readable form
def ProofTree.structure_array (tree: ProofTree): Array String :=
tree.states.map λ state => match state.parent with
| .none => ""
| .some parent => s!"{parent}.{state.parentGoalId}"
def execute_tactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: String) : def execute_tactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: String) :
M (Except (Array String) (Elab.Tactic.SavedState × List MVarId)):= do M (Except (Array String) (Elab.Tactic.SavedState × List MVarId)):= do
let tacticM (stx: Syntax): Elab.Tactic.TacticM (Except (Array String) (Elab.Tactic.SavedState × List MVarId)) := do let tacticM (stx: Syntax): Elab.Tactic.TacticM (Except (Array String) (Elab.Tactic.SavedState × List MVarId)) := do
@ -78,44 +65,38 @@ def execute_tactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Strin
/-- Response for executing a tactic -/ /-- Response for executing a tactic -/
inductive TacticResult where inductive TacticResult where
-- Invalid id
| invalid (message: String): TacticResult
-- Goes to next state -- Goes to next state
| success (nextId?: Option Nat) (goals: Array Commands.Goal) | success (goals: Array (GoalState × Commands.Goal))
-- Fails with messages -- Fails with messages
| failure (messages: Array String) | failure (messages: Array String)
namespace TacticResult
def is_success: TacticResult → Bool
| .success _ => true
| .failure _ => false
end TacticResult
/-- Execute tactic on given state -/ /-- Execute tactic on given state -/
def ProofTree.execute (stateId: Nat) (goalId: Nat) (tactic: String): def GoalState.execute (goal: GoalState) (tactic: String):
Commands.OptionsT StateRefT ProofTree M TacticResult := do Commands.OptionsT M TacticResult := do
let options ← read let options ← read
let tree ← get match (← execute_tactic (state := goal.savedState) (goal := goal.mvarId) (tactic := tactic)) with
match tree.states.get? stateId with
| .none => return .invalid s!"Invalid state id {stateId}"
| .some state =>
match state.goals.get? goalId with
| .none => return .invalid s!"Invalid goal id {goalId}"
| .some goal =>
match (← execute_tactic (state := state.savedState) (goal := goal) (tactic := tactic)) with
| .error errors => | .error errors =>
return .failure errors return .failure errors
| .ok (nextState, nextGoals) => | .ok (nextState, nextGoals) =>
let nextId := tree.states.size
if nextGoals.isEmpty then if nextGoals.isEmpty then
return .success .none #[] return .success #[]
else else
let proofState: ProofState := { let nextGoals: List GoalState := nextGoals.map fun mvarId => { mvarId, savedState := nextState }
savedState := nextState, let parentDecl? := (← MonadMCtx.getMCtx).findDecl? goal.mvarId
goals := nextGoals, let goals ← nextGoals.mapM fun nextGoal => do
parent := stateId, match (← MonadMCtx.getMCtx).findDecl? nextGoal.mvarId with
parentGoalId := goalId | .some mvarDecl =>
} let serializedGoal ← serialize_goal options mvarDecl (parentDecl? := parentDecl?)
modify fun s => { s with states := s.states.push proofState } return (nextGoal, serializedGoal)
let parentDecl? := (← MonadMCtx.getMCtx).findDecl? goal | .none => throwError nextGoal.mvarId
let goals ← nextGoals.mapM fun mvarId => do return .success goals.toArray
match (← MonadMCtx.getMCtx).findDecl? mvarId with
| .some mvarDecl => serialize_goal options mvarDecl (parentDecl? := parentDecl?)
| .none => throwError mvarId
return .success (.some nextId) goals.toArray
end Pantograph end Pantograph

View File

@ -1,5 +1,5 @@
namespace Pantograph namespace Pantograph
def version := "0.2.3" def version := "0.2.4"
end Pantograph end Pantograph

View File

@ -50,15 +50,16 @@ Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting)
$ lake env build/bin/Pantograph Mathlib.Analysis.Seminorm $ lake env build/bin/Pantograph Mathlib.Analysis.Seminorm
lib.catalog lib.catalog
``` ```
Example proving a theorem: (alternatively use `proof.start {"copyFrom": "Nat.add_comm"}`) to prime the proof Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) to prime the proof
``` ```
$ env build/bin/Pantograph Init $ env build/bin/Pantograph Init
proof.start {"expr": "∀ (n m : Nat), n + m = m + n"} goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
proof.tactic {"treeId": 0, "stateId": 0, "goalId": 0, "tactic": "intro n m"} goal.tactic {"goalId": 0, "tactic": "intro n m"}
proof.tactic {"treeId": 0, "stateId": 1, "goalId": 0, "tactic": "assumption"} goal.tactic {"goalId": 1, "tactic": "assumption"}
proof.printTree {"treeId": 0} goal.delete {"goalIds": [0]}
proof.tactic {"treeId": 0, "stateId": 1, "goalId": 0, "tactic": "rw [Nat.add_comm]"} stat {}
proof.printTree {"treeId": 0} goal.tactic {"goalId": 1, "tactic": "rw [Nat.add_comm]"}
stat
``` ```
where the application of `assumption` should lead to a failure. where the application of `assumption` should lead to a failure.
@ -74,9 +75,10 @@ See `Pantograph/Commands.lean` for a description of the parameters and return va
- `options.set { key: value, ... }`: Set one or more options (not Lean options; those - `options.set { key: value, ... }`: Set one or more options (not Lean options; those
have to be set via command line arguments.), for options, see `Pantograph/Commands.lean` have to be set via command line arguments.), for options, see `Pantograph/Commands.lean`
- `options.print`: Display the current set of options - `options.print`: Display the current set of options
- `proof.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new proof state from a given expression or symbol - `goal.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new goal from a given expression or symbol
- `proof.tactic {"treeId": <id>, "stateId": <id>, "goalId": <id>, "tactic": string}`: Execute a tactic on a given proof state - `goal.tactic {"goalId": <id>, "tactic": <tactic>}`: Execute a tactic string on a given goal
- `proof.printTree {"treeId": <id>}`: Print the topological structure of a proof tree - `goal.remove {"goalIds": [<id>]}"`: Remove a bunch of stored goals.
- `stat`: Display resource usage
## Errors ## Errors

View File

@ -10,87 +10,46 @@ inductive Start where
| copy (name: String) -- Start from some name in the environment | copy (name: String) -- Start from some name in the environment
| expr (expr: String) -- Start from some expression | expr (expr: String) -- Start from some expression
abbrev TestM := ReaderT Commands.Options StateRefT ProofTree M abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Commands.Options M)
def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do
let env ← Lean.MonadEnv.getEnv
let mut testSeq := LSpec.TestSeq.done
match start with
| .copy name =>
let cInfo? := str_to_name name |> env.find?
testSeq := testSeq ++ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
match cInfo? with
| .some cInfo =>
let state ← ProofTree.create
(expr := cInfo.type)
return (testSeq, Option.some state)
| .none =>
return (testSeq, Option.none)
| .expr expr =>
let syn? := syntax_from_str env expr
testSeq := testSeq ++ LSpec.check s!"Parsing {expr}" (syn?.isOk)
match syn? with
| .error error =>
IO.println error
return (testSeq, Option.none)
| .ok syn =>
let expr? ← syntax_to_expr syn
testSeq := testSeq ++ LSpec.check s!"Elaborating" expr?.isOk
match expr? with
| .error error =>
IO.println error
return (testSeq, Option.none)
| .ok expr =>
let state ← ProofTree.create
(expr := expr)
return (testSeq, Option.some state)
deriving instance DecidableEq, Repr for Commands.Expression deriving instance DecidableEq, Repr for Commands.Expression
deriving instance DecidableEq, Repr for Commands.Variable deriving instance DecidableEq, Repr for Commands.Variable
deriving instance DecidableEq, Repr for Commands.Goal deriving instance DecidableEq, Repr for Commands.Goal
deriving instance DecidableEq, Repr for TacticResult
/-- Check the output of each proof step -/ def add_test (test: LSpec.TestSeq): TestM Unit := do
def proof_step (stateId: Nat) (goalId: Nat) (tactic: String) set $ (← get) ++ test
(expected: TacticResult) : TestM LSpec.TestSeq := do
let options ← read
let result: TacticResult ← ProofTree.execute stateId goalId tactic |>.run options
match expected, result with
| .success (.some i) #[], .success (.some _) goals =>
-- If the goals are omitted but the next state is specified, we imply that
-- the tactic succeeded.
let expected := .success (.some i) goals
return LSpec.test s!"{stateId}.{goalId} {tactic}" (result = expected)
| _, _ =>
return LSpec.test s!"{stateId}.{goalId} {tactic}" (result = expected)
/-- Check that the tree structure is correct -/ def start_proof (start: Start): TestM (Option GoalState) := do
def proof_inspect (expected: Array String) : TestM LSpec.TestSeq := do let env ← Lean.MonadEnv.getEnv
let result := (← get).structure_array match start with
return LSpec.test s!"tree structure" (result = expected) | .copy name =>
let cInfo? := str_to_name name |> env.find?
add_test $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
match cInfo? with
| .some cInfo =>
let goal ← GoalState.create (expr := cInfo.type)
return Option.some goal
| .none =>
return Option.none
| .expr expr =>
let syn? := syntax_from_str env expr
add_test $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
match syn? with
| .error error =>
IO.println error
return Option.none
| .ok syn =>
let expr? ← syntax_to_expr syn
add_test $ LSpec.check s!"Elaborating" expr?.isOk
match expr? with
| .error error =>
IO.println error
return Option.none
| .ok expr =>
let goal ← GoalState.create (expr := expr)
return Option.some goal
def proof_runner (env: Lean.Environment) (options: Commands.Options) (start: Start) (steps: List (TestM LSpec.TestSeq)): IO LSpec.TestSeq := do def assert_unreachable (message: String): LSpec.TestSeq := LSpec.check message false
let termElabM := do
let (testSeq, state?) ← start_proof start
match state? with
| .none => return testSeq
| .some state => steps.foldlM (fun tests m => do pure $ tests ++ (← m)) testSeq |>.run options |>.run' state
let coreContext: Lean.Core.Context := {
currNamespace := str_to_name "Aniva",
openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph>",
fileMap := { source := "", positions := #[0], lines := #[1] }
}
let metaM := termElabM.run' (ctx := {
declName? := some "_pantograph",
errToSorry := false
})
let coreM := metaM.run'
match ← (coreM.run' coreContext { env := env }).toBaseIO with
| .error exception =>
return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
| .ok a => return a
def build_goal (nameType: List (String × String)) (target: String): Commands.Goal := def build_goal (nameType: List (String × String)) (target: String): Commands.Goal :=
{ {
@ -101,30 +60,61 @@ def build_goal (nameType: List (String × String)) (target: String): Commands.Go
isInaccessible? := .some false isInaccessible? := .some false
})).toArray })).toArray
} }
-- Like `build_goal` but allow certain variables to be elided.
def build_goal_selective (nameType: List (String × Option String)) (target: String): Commands.Goal :=
{
target := { pp? := .some target},
vars := (nameType.map fun x => ({
name := x.fst,
type? := x.snd.map (λ type => { pp? := type }),
isInaccessible? := x.snd.map (λ _ => false)
})).toArray
}
-- Individual test cases
example: ∀ (a b: Nat), a + b = b + a := by example: ∀ (a b: Nat), a + b = b + a := by
intro n m intro n m
rw [Nat.add_comm] rw [Nat.add_comm]
def proof_nat_add_comm (env: Lean.Environment): IO LSpec.TestSeq := do def proof_nat_add_comm: TestM Unit := do
let goal1: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n" let goal? ← start_proof (.copy "Nat.add_comm")
proof_runner env {} (.copy "Nat.add_comm") [ add_test $ LSpec.check "Start goal" goal?.isSome
proof_step 0 0 "intro n m" if let .some goal := goal? then
(.success (.some 1) #[goal1]), if let .success #[(goal, sGoal)] ← goal.execute "intro n m" then
proof_step 1 0 "assumption" let sGoal1e: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
(.failure #[s!"tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n"]), add_test $ LSpec.check "intro n m" (sGoal = sGoal1e)
proof_step 1 0 "rw [Nat.add_comm]"
(.success .none #[]) if let .failure #[message] ← goal.execute "assumption" then
] add_test $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
def proof_nat_add_comm_manual (env: Lean.Environment): IO LSpec.TestSeq := do else
let goal1: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n" add_test $ assert_unreachable "assumption"
proof_runner env {} (.expr "∀ (a b: Nat), a + b = b + a") [
proof_step 0 0 "intro n m" if let .success #[] ← goal.execute "rw [Nat.add_comm]" then
(.success (.some 1) #[goal1]), return ()
proof_step 1 0 "assumption" else
(.failure #[s!"tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n"]), add_test $ assert_unreachable "rw [Nat.add_comm]"
proof_step 1 0 "rw [Nat.add_comm]" else
(.success .none #[]) add_test $ assert_unreachable "intro n m"
] def proof_nat_add_comm_manual: TestM Unit := do
let goal? ← start_proof (.expr "∀ (a b: Nat), a + b = b + a")
add_test $ LSpec.check "Start goal" goal?.isSome
if let .some goal := goal? then
if let .success #[(goal, sGoal)] ← goal.execute "intro n m" then
let sGoal1e: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
add_test $ LSpec.check "intro n m" (sGoal = sGoal1e)
if let .failure #[message] ← goal.execute "assumption" then
add_test $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
else
add_test $ assert_unreachable "assumption"
if let .success #[] ← goal.execute "rw [Nat.add_comm]" then
return ()
else
add_test $ assert_unreachable "rw [Nat.add_comm]"
else
add_test $ assert_unreachable "intro n m"
-- Two ways to write the same theorem -- Two ways to write the same theorem
example: ∀ (p q: Prop), p q → q p := by example: ∀ (p q: Prop), p q → q p := by
@ -141,7 +131,7 @@ example: ∀ (p q: Prop), p q → q p := by
assumption assumption
. apply Or.inl . apply Or.inl
assumption assumption
def proof_or_comm (env: Lean.Environment): IO LSpec.TestSeq := do def proof_or_comm: TestM Unit := do
let typeProp: Commands.Expression := { pp? := .some "Prop" } let typeProp: Commands.Expression := { pp? := .some "Prop" }
let branchGoal (caseName name: String): Commands.Goal := { let branchGoal (caseName name: String): Commands.Goal := {
caseName? := .some caseName, caseName? := .some caseName,
@ -152,69 +142,111 @@ def proof_or_comm (env: Lean.Environment): IO LSpec.TestSeq := do
{ name := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true } { name := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true }
] ]
} }
proof_runner env {} (.expr "∀ (p q: Prop), p q → q p") [ let goal? ← start_proof (.expr "∀ (p q: Prop), p q → q p")
proof_step 0 0 "intro p q h" add_test $ LSpec.check "Start goal" goal?.isSome
(.success (.some 1) #[build_goal [("p", "Prop"), ("q", "Prop"), ("h", "p q")] "q p"]), if let .some goal := goal? then
proof_step 1 0 "cases h" if let .success #[(goal, sGoal)] ← goal.execute "intro p q h" then
(.success (.some 2) #[branchGoal "inl" "p", branchGoal "inr" "q"]), let sGoal1e := build_goal [("p", "Prop"), ("q", "Prop"), ("h", "p q")] "q p"
proof_inspect #["", "0.0", "1.0"], add_test $ LSpec.check "intro p q h" (sGoal = sGoal1e)
proof_step 2 0 "apply Or.inr"
(.success (.some 3) #[]), if let .success #[(goal1, sGoal1), (goal2, sGoal2)] ← goal.execute "cases h" then
proof_inspect #["", "0.0", "1.0", "2.0"], add_test $ LSpec.check "cases h/1" (sGoal1 = branchGoal "inl" "p")
proof_step 3 0 "assumption" if let .success #[(goal, _)] ← goal1.execute "apply Or.inr" then
(.success .none #[]), if let .success #[] ← goal.execute "assumption" then
proof_step 2 1 "apply Or.inl" return ()
(.success (.some 4) #[]), else
proof_step 4 0 "assumption" add_test $ assert_unreachable "assumption"
(.success .none #[]), else
proof_inspect #["", "0.0", "1.0", "2.0", "2.1"] add_test $ assert_unreachable "apply Or.inr"
]
add_test $ LSpec.check "cases h/2" (sGoal2 = branchGoal "inr" "q")
if let .success #[(goal, _)] ← goal2.execute "apply Or.inl" then
if let .success #[] ← goal.execute "assumption" then
return ()
else
add_test $ assert_unreachable "assumption"
else
add_test $ assert_unreachable "apply Or.inl"
else
add_test $ assert_unreachable "cases h"
else
add_test $ assert_unreachable "intro p q h"
example (w x y z : Nat) (p : Nat → Prop) example (w x y z : Nat) (p : Nat → Prop)
(h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by (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 * simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *
assumption assumption
def proof_arith_1 (env: Lean.Environment): IO LSpec.TestSeq := do def proof_arith_1: TestM Unit := do
proof_runner env {} (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)") [ let goal? ← start_proof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)")
proof_step 0 0 "intros" add_test $ LSpec.check "Start goal" goal?.isSome
(.success (.some 1) #[]), if let .some goal := goal? then
proof_step 1 0 "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *" if let .success #[(goal, _)] ← goal.execute "intros" then
(.success (.some 2) #[]), if let .success #[(goal, _)] ← goal.execute "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *" then
proof_step 2 0 "assumption" if let .success #[] ← goal.execute "assumption" then
(.success .none #[]) return ()
] else
add_test $ assert_unreachable "assumption"
else
add_test $ assert_unreachable "simp ..."
else
add_test $ assert_unreachable "intros"
def build_goal_selective (nameType: List (String × Option String)) (target: String): Commands.Goal := def proof_delta_variable: TestM Unit := withReader (fun _ => {proofVariableDelta := true}) do
{ let goal? ← start_proof (.expr "∀ (a b: Nat), a + b = b + a")
target := { pp? := .some target}, add_test $ LSpec.check "Start goal" goal?.isSome
vars := (nameType.map fun x => ({ if let .some goal := goal? then
name := x.fst, if let .success #[(goal, sGoal)] ← goal.execute "intro n" then
type? := x.snd.map (λ type => { pp? := type }), let sGoal1e: Commands.Goal := build_goal_selective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"
isInaccessible? := x.snd.map (λ _ => false) add_test $ LSpec.check "intro n" (sGoal = sGoal1e)
})).toArray
if let .success #[(_, sGoal)] ← goal.execute "intro m" then
let sGoal2e: Commands.Goal := build_goal_selective [("n", .none), ("m", .some "Nat")] "n + m = m + n"
add_test $ LSpec.check "intro m" (sGoal = sGoal2e)
else
add_test $ assert_unreachable "intro m"
else
add_test $ assert_unreachable "intro n"
def proof_runner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
let coreContext: Lean.Core.Context := {
currNamespace := str_to_name "Aniva",
openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph>",
fileMap := { source := "", positions := #[0], lines := #[1] }
} }
def proof_delta_variable (env: Lean.Environment): IO LSpec.TestSeq := do let metaM := termElabM.run' (ctx := {
let goal1: Commands.Goal := build_goal_selective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n" declName? := some "_pantograph",
let goal2: Commands.Goal := build_goal_selective [("n", .none), ("m", .some "Nat")] "n + m = m + n" errToSorry := false
proof_runner env { proofVariableDelta := true } (.expr "∀ (a b: Nat), a + b = b + a") [ })
proof_step 0 0 "intro n" let coreM := metaM.run'
(.success (.some 1) #[goal1]), match ← (coreM.run' coreContext { env := env }).toBaseIO with
proof_step 1 0 "intro m" | .error exception =>
(.success (.some 2) #[goal2]) return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
] | .ok (_, a) =>
return a
def test_proofs : IO LSpec.TestSeq := do def test_proofs : IO LSpec.TestSeq := do
let env: Lean.Environment ← Lean.importModules let env: Lean.Environment ← Lean.importModules
(imports := ["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false })) (imports := ["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
(opts := {}) (opts := {})
(trustLevel := 1) (trustLevel := 1)
let tests := [
("Nat.add_comm", proof_nat_add_comm),
("nat.add_comm manual", proof_nat_add_comm_manual),
("Or.comm", proof_or_comm),
("arithmetic 1", proof_arith_1),
("delta variable", proof_delta_variable)
]
let tests ← tests.foldlM (fun acc tests => do
let (name, tests) := tests
let tests ← proof_runner env tests
return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
return LSpec.group "Proofs" $ return LSpec.group "Proofs" tests
(LSpec.group "Nat.add_comm" $ (← proof_nat_add_comm env)) ++
(LSpec.group "Nat.add_comm manual" $ (← proof_nat_add_comm_manual env)) ++
(LSpec.group "Or.comm" $ (← proof_or_comm env)) ++
(LSpec.group "Arithmetic 1" $ (← proof_arith_1 env)) ++
(LSpec.group "Delta variable" $ (← proof_delta_variable env))
end Pantograph.Test end Pantograph.Test