From 0c5f4390678b8a27d0a0cc73ac4b57a30942c930 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 27 Aug 2023 19:53:09 -0700 Subject: [PATCH 1/4] Add SemihashMap structure for goal bookkeeping --- Pantograph.lean | 54 +++--- Pantograph/Commands.lean | 16 +- Pantograph/SemihashMap.lean | 89 ++++++++++ Pantograph/Tactic.lean | 83 ++++------ README.md | 14 +- Test/Proofs.lean | 320 ++++++++++++++++++++---------------- 6 files changed, 339 insertions(+), 237 deletions(-) create mode 100644 Pantograph/SemihashMap.lean diff --git a/Pantograph.lean b/Pantograph.lean index 525b834..543c49e 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -2,6 +2,7 @@ import Pantograph.Commands import Pantograph.Serial import Pantograph.Symbols import Pantograph.Tactic +import Pantograph.SemihashMap namespace Pantograph @@ -11,8 +12,7 @@ structure Context where /-- Stores state of the REPL -/ structure State where options: Commands.Options := {} - --environments: Array Lean.Environment := #[] - proofTrees: Array ProofTree := #[] + goalStates: SemihashMap GoalState := SemihashMap.empty -- State monad abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM) @@ -49,9 +49,9 @@ def execute (command: Commands.Command): MainM Lean.Json := do -- Command Functions reset (_: Commands.Reset): MainM (CR Commands.ResetResult) := do let state ← get - let nTrees := state.proofTrees.size - set { state with proofTrees := #[] } - return .ok { nTrees := nTrees } + let nStates := state.goalStates.size + set { state with goalStates := SemihashMap.empty } + return .ok { nStates := nStates } lib_catalog (_: Commands.LibCatalog): MainM (CR Commands.LibCatalogResult) := do let env ← Lean.MonadEnv.getEnv let names := env.constants.fold (init := #[]) (λ acc name info => @@ -134,32 +134,34 @@ def execute (command: Commands.Command): MainM Lean.Json := do match expr? with | .error error => return .error error | .ok expr => - let tree ← ProofTree.create expr - -- Put the new tree in the environment - let nextTreeId := state.proofTrees.size - set { state with proofTrees := state.proofTrees.push tree } - return .ok { treeId := nextTreeId } + let goalState ← GoalState.create expr + let (goalStates, goalId) := state.goalStates.insert goalState + set { state with goalStates } + return .ok { goalId } proof_tactic (args: Commands.ProofTactic): MainM (CR Commands.ProofTacticResult) := do let state ← get - match state.proofTrees.get? args.treeId with - | .none => return .error $ errorIndex "Invalid tree index {args.treeId}" - | .some tree => - let (result, nextTree) ← ProofTree.execute - (stateId := args.stateId) - (goalId := args.goalId.getD 0) - (tactic := args.tactic) |>.run state.options |>.run tree + match state.goalStates.get? args.goalId with + | .none => return .error $ errorIndex "Invalid goal index {args.goalId}" + | .some goalState => + let result ← GoalState.execute goalState args.tactic |>.run state.options match result with - | .invalid message => return .error $ errorIndex message - | .success nextId? goals => - set { state with proofTrees := state.proofTrees.set! args.treeId nextTree } - return .ok { nextId? := nextId?, goals? := .some goals } + | .success goals => + if goals.isEmpty then + return .ok {} + 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 => return .ok { tacticErrors? := .some messages } - proof_print_tree (args: Commands.ProofPrintTree): MainM (CR Commands.ProofPrintTreeResult) := do + proof_print_tree (_: Commands.ProofPrintTree): MainM (CR Commands.ProofPrintTreeResult) := do let state ← get - match state.proofTrees.get? args.treeId with - | .none => return .error $ errorIndex "Invalid tree index {args.treeId}" - | .some tree => - return .ok { parents := tree.structure_array } + return .ok { nGoals := state.goalStates.size } end Pantograph diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index 6e28af8..8c8b509 100644 --- a/Pantograph/Commands.lean +++ b/Pantograph/Commands.lean @@ -81,7 +81,7 @@ structure InteractionError where structure Reset where deriving Lean.FromJson structure ResetResult where - nTrees: Nat + nStates: Nat deriving Lean.ToJson -- Return the type of an expression @@ -133,29 +133,27 @@ structure ProofStart where copyFrom: Option String -- Theorem name deriving Lean.FromJson structure ProofStartResult where - treeId: Nat := 0 -- Proof tree id + goalId: Nat := 0 -- Proof tree id deriving Lean.ToJson structure ProofTactic where -- Identifiers for tree, state, and goal - treeId: Nat - stateId: Nat - goalId: Option Nat -- Defaults to 0 + goalId: Nat tactic: String deriving Lean.FromJson structure ProofTacticResult where -- Existence of this field shows success goals?: Option (Array Goal) := .none -- Next proof state id, if successful - nextId?: Option Nat := .none + goalIds?: Option (Array Nat) := .none -- Existence of this field shows failure tacticErrors?: Option (Array String) := .none deriving Lean.ToJson + structure ProofPrintTree where - treeId: Nat deriving Lean.FromJson structure ProofPrintTreeResult where - -- "" if no parents, otherwise "parentId.goalId" - parents: Array String + -- Total number of goals + nGoals: Nat deriving Lean.ToJson end Pantograph.Commands diff --git a/Pantograph/SemihashMap.lean b/Pantograph/SemihashMap.lean new file mode 100644 index 0000000..362be94 --- /dev/null +++ b/Pantograph/SemihashMap.lean @@ -0,0 +1,89 @@ + +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 + + +@[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: Nat): Imp β := + match map.data.getD index .none 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: Nat): Option β := + map.data.getD index .none +@[inline] def capacity (map: Imp β): Nat := map.data.size + +end Imp + +def empty (capacity := 16): Imp β := + { + data := mkArray capacity .none, + size := 0, + allocFront := 0, + deallocs := mkArray capacity 0, + lastDealloc := 0, + } + +/-- +This is like a hashmap but you cannot control the keys. +-/ +def _root_.Pantograph.SemihashMap β := Imp β + +end Pantograph.SemihashMap diff --git a/Pantograph/Tactic.lean b/Pantograph/Tactic.lean index 50ddf3a..a736064 100644 --- a/Pantograph/Tactic.lean +++ b/Pantograph/Tactic.lean @@ -24,35 +24,22 @@ def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog := namespace Pantograph open Lean -structure ProofState where - goals : List MVarId +structure GoalState where + mvarId: MVarId 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 -def ProofTree.create (expr: Expr): M ProofTree := do +def GoalState.create (expr: Expr): M GoalState := do let expr ← instantiateMVars expr let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic)) let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]} return { - states := #[{ - savedState := savedState, - goals := [goal.mvarId!] - }] + savedState := savedState, + 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) : 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 @@ -78,44 +65,38 @@ def execute_tactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Strin /-- Response for executing a tactic -/ inductive TacticResult where - -- Invalid id - | invalid (message: String): TacticResult -- Goes to next state - | success (nextId?: Option Nat) (goals: Array Commands.Goal) + | success (goals: Array (GoalState × Commands.Goal)) -- Fails with messages | failure (messages: Array String) +namespace TacticResult + +def is_success: TacticResult → Bool + | .success _ => true + | .failure _ => false + +end TacticResult + /-- Execute tactic on given state -/ -def ProofTree.execute (stateId: Nat) (goalId: Nat) (tactic: String): - Commands.OptionsT StateRefT ProofTree M TacticResult := do +def GoalState.execute (goal: GoalState) (tactic: String): + Commands.OptionsT M TacticResult := do let options ← read - let tree ← get - 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 => - return .failure errors - | .ok (nextState, nextGoals) => - let nextId := tree.states.size - if nextGoals.isEmpty then - return .success .none #[] - else - let proofState: ProofState := { - savedState := nextState, - goals := nextGoals, - parent := stateId, - parentGoalId := goalId - } - modify fun s => { s with states := s.states.push proofState } - let parentDecl? := (← MonadMCtx.getMCtx).findDecl? goal - let goals ← nextGoals.mapM fun mvarId => do - match (← MonadMCtx.getMCtx).findDecl? mvarId with - | .some mvarDecl => serialize_goal options mvarDecl (parentDecl? := parentDecl?) - | .none => throwError mvarId - return .success (.some nextId) goals.toArray + match (← execute_tactic (state := goal.savedState) (goal := goal.mvarId) (tactic := tactic)) with + | .error errors => + return .failure errors + | .ok (nextState, nextGoals) => + if nextGoals.isEmpty then + return .success #[] + else + let nextGoals: List GoalState := nextGoals.map fun mvarId => { mvarId, savedState := nextState } + let parentDecl? := (← MonadMCtx.getMCtx).findDecl? goal.mvarId + let goals ← nextGoals.mapM fun nextGoal => do + match (← MonadMCtx.getMCtx).findDecl? nextGoal.mvarId with + | .some mvarDecl => + let serializedGoal ← serialize_goal options mvarDecl (parentDecl? := parentDecl?) + return (nextGoal, serializedGoal) + | .none => throwError nextGoal.mvarId + return .success goals.toArray end Pantograph diff --git a/README.md b/README.md index 82d3db3..8407d49 100644 --- a/README.md +++ b/README.md @@ -54,11 +54,11 @@ Example proving a theorem: (alternatively use `proof.start {"copyFrom": "Nat.add ``` $ env build/bin/Pantograph Init proof.start {"expr": "∀ (n m : Nat), n + m = m + n"} -proof.tactic {"treeId": 0, "stateId": 0, "goalId": 0, "tactic": "intro n m"} -proof.tactic {"treeId": 0, "stateId": 1, "goalId": 0, "tactic": "assumption"} -proof.printTree {"treeId": 0} -proof.tactic {"treeId": 0, "stateId": 1, "goalId": 0, "tactic": "rw [Nat.add_comm]"} -proof.printTree {"treeId": 0} +proof.tactic {"goalId": 0, "tactic": "intro n m"} +proof.tactic {"goalId": 1, "tactic": "assumption"} +proof.printTree {} +proof.tactic {"goalId": 1, "tactic": "rw [Nat.add_comm]"} +proof.printTree ``` where the application of `assumption` should lead to a failure. @@ -75,8 +75,8 @@ See `Pantograph/Commands.lean` for a description of the parameters and return va have to be set via command line arguments.), for options, see `Pantograph/Commands.lean` - `options.print`: Display the current set of options - `proof.start {["name": ], ["expr": ], ["copyFrom": ]}`: Start a new proof state from a given expression or symbol -- `proof.tactic {"treeId": , "stateId": , "goalId": , "tactic": string}`: Execute a tactic on a given proof state -- `proof.printTree {"treeId": }`: Print the topological structure of a proof tree +- `proof.tactic {"goalId": , "tactic": }`: Execute a tactic string on a given proof state +- `proof.printTree`: Print the number of goals ## Errors diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 505eec9..ccf7b01 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -10,87 +10,46 @@ inductive Start where | copy (name: String) -- Start from some name in the environment | expr (expr: String) -- Start from some expression -abbrev TestM := ReaderT Commands.Options StateRefT ProofTree 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) +abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Commands.Options M) deriving instance DecidableEq, Repr for Commands.Expression deriving instance DecidableEq, Repr for Commands.Variable deriving instance DecidableEq, Repr for Commands.Goal -deriving instance DecidableEq, Repr for TacticResult -/-- Check the output of each proof step -/ -def proof_step (stateId: Nat) (goalId: Nat) (tactic: String) - (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) +def add_test (test: LSpec.TestSeq): TestM Unit := do + set $ (← get) ++ test -/-- Check that the tree structure is correct -/ -def proof_inspect (expected: Array String) : TestM LSpec.TestSeq := do - let result := (← get).structure_array - return LSpec.test s!"tree structure" (result = expected) +def start_proof (start: Start): TestM (Option GoalState) := do + let env ← Lean.MonadEnv.getEnv + match start with + | .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 - 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 := "", - 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 assert_unreachable (message: String): LSpec.TestSeq := LSpec.check message false 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 })).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 intro n m rw [Nat.add_comm] -def proof_nat_add_comm (env: Lean.Environment): IO LSpec.TestSeq := do - let goal1: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n" - proof_runner env {} (.copy "Nat.add_comm") [ - proof_step 0 0 "intro n m" - (.success (.some 1) #[goal1]), - proof_step 1 0 "assumption" - (.failure #[s!"tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n"]), - proof_step 1 0 "rw [Nat.add_comm]" - (.success .none #[]) - ] -def proof_nat_add_comm_manual (env: Lean.Environment): IO LSpec.TestSeq := do - let goal1: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n" - proof_runner env {} (.expr "∀ (a b: Nat), a + b = b + a") [ - proof_step 0 0 "intro n m" - (.success (.some 1) #[goal1]), - proof_step 1 0 "assumption" - (.failure #[s!"tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n"]), - proof_step 1 0 "rw [Nat.add_comm]" - (.success .none #[]) - ] +def proof_nat_add_comm: TestM Unit := do + let goal? ← start_proof (.copy "Nat.add_comm") + 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" +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 example: ∀ (p q: Prop), p ∨ q → q ∨ p := by @@ -141,7 +131,7 @@ example: ∀ (p q: Prop), p ∨ q → q ∨ p := by assumption . apply Or.inl 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 branchGoal (caseName name: String): Commands.Goal := { 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 } ] } - proof_runner env {} (.expr "∀ (p q: Prop), p ∨ q → q ∨ p") [ - proof_step 0 0 "intro p q h" - (.success (.some 1) #[build_goal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"]), - proof_step 1 0 "cases h" - (.success (.some 2) #[branchGoal "inl" "p", branchGoal "inr" "q"]), - proof_inspect #["", "0.0", "1.0"], - proof_step 2 0 "apply Or.inr" - (.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 #[]), - proof_inspect #["", "0.0", "1.0", "2.0", "2.1"] - ] + let goal? ← start_proof (.expr "∀ (p q: Prop), p ∨ q → q ∨ p") + add_test $ LSpec.check "Start goal" goal?.isSome + if let .some goal := goal? then + if let .success #[(goal, sGoal)] ← goal.execute "intro p q h" then + let sGoal1e := build_goal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p" + add_test $ LSpec.check "intro p q h" (sGoal = sGoal1e) + + if let .success #[(goal1, sGoal1), (goal2, sGoal2)] ← goal.execute "cases h" then + add_test $ LSpec.check "cases h/1" (sGoal1 = branchGoal "inl" "p") + if let .success #[(goal, _)] ← goal1.execute "apply Or.inr" then + if let .success #[] ← goal.execute "assumption" then + return () + else + add_test $ assert_unreachable "assumption" + else + 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) (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_1 (env: Lean.Environment): IO LSpec.TestSeq := 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)") [ - proof_step 0 0 "intros" - (.success (.some 1) #[]), - 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 *" - (.success (.some 2) #[]), - proof_step 2 0 "assumption" - (.success .none #[]) - ] +def proof_arith_1: TestM Unit := do + 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)") + add_test $ LSpec.check "Start goal" goal?.isSome + if let .some goal := goal? then + if let .success #[(goal, _)] ← goal.execute "intros" then + 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 + if let .success #[] ← goal.execute "assumption" then + 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 := - { - 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 +def proof_delta_variable: TestM Unit := withReader (fun _ => {proofVariableDelta := true}) 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" then + let sGoal1e: Commands.Goal := build_goal_selective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n" + add_test $ LSpec.check "intro n" (sGoal = sGoal1e) + + 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 := "", + fileMap := { source := "", positions := #[0], lines := #[1] } } -def proof_delta_variable (env: Lean.Environment): IO LSpec.TestSeq := do - let goal1: Commands.Goal := build_goal_selective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n" - let goal2: Commands.Goal := build_goal_selective [("n", .none), ("m", .some "Nat")] "n + m = m + n" - proof_runner env { proofVariableDelta := true } (.expr "∀ (a b: Nat), a + b = b + a") [ - proof_step 0 0 "intro n" - (.success (.some 1) #[goal1]), - proof_step 1 0 "intro m" - (.success (.some 2) #[goal2]) - ] + 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 test_proofs : IO LSpec.TestSeq := do let env: Lean.Environment ← Lean.importModules (imports := ["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false })) (opts := {}) (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" $ - (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)) + return LSpec.group "Proofs" tests end Pantograph.Test From 80ad7a2bd0647916d6f725f993ae1c2a1ea62e63 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 27 Aug 2023 19:58:52 -0700 Subject: [PATCH 2/4] Rename proof commands to goal commands --- Pantograph.lean | 35 ++++++++++++++++++----------------- Pantograph/Commands.lean | 13 +++++-------- README.md | 20 ++++++++++---------- 3 files changed, 33 insertions(+), 35 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index 543c49e..bb2635e 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -29,15 +29,15 @@ def execute (command: Commands.Command): MainM Lean.Json := do | .error ierror => return Lean.toJson ierror | .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}" match command.cmd with - | "reset" => run reset - | "expr.echo" => run expr_echo - | "lib.catalog" => run lib_catalog - | "lib.inspect" => run lib_inspect - | "options.set" => run options_set - | "options.print" => run options_print - | "proof.start" => run proof_start - | "proof.tactic" => run proof_tactic - | "proof.printTree" => run proof_print_tree + | "reset" => run reset + | "stat" => run stat + | "expr.echo" => run expr_echo + | "lib.catalog" => run lib_catalog + | "lib.inspect" => run lib_inspect + | "options.set" => run options_set + | "options.print" => run options_print + | "goal.start" => run goal_start + | "goal.tactic" => run goal_tactic | cmd => let error: Commands.InteractionError := errorCommand s!"Unknown command {cmd}" @@ -47,11 +47,15 @@ def execute (command: Commands.Command): MainM Lean.Json := do errorCommand := errorI "command" errorIndex := errorI "index" -- Command Functions - reset (_: Commands.Reset): MainM (CR Commands.ResetResult) := do + reset (_: Commands.Reset): MainM (CR Commands.StatResult) := do let state ← get - let nStates := state.goalStates.size + let nGoals := state.goalStates.size set { state with goalStates := SemihashMap.empty } - return .ok { nStates := nStates } + 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 let env ← Lean.MonadEnv.getEnv let names := env.constants.fold (init := #[]) (λ acc name info => @@ -113,7 +117,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do return .ok { } options_print (_: Commands.OptionsPrint): MainM (CR Commands.OptionsPrintResult) := do return .ok (← get).options - proof_start (args: Commands.ProofStart): MainM (CR Commands.ProofStartResult) := do + goal_start (args: Commands.ProofStart): MainM (CR Commands.ProofStartResult) := do let state ← get let env ← Lean.MonadEnv.getEnv let expr?: Except _ Lean.Expr ← (match args.expr, args.copyFrom with @@ -138,7 +142,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do let (goalStates, goalId) := state.goalStates.insert goalState set { state with goalStates } return .ok { goalId } - proof_tactic (args: Commands.ProofTactic): MainM (CR Commands.ProofTacticResult) := do + goal_tactic (args: Commands.ProofTactic): MainM (CR Commands.ProofTacticResult) := do let state ← get match state.goalStates.get? args.goalId with | .none => return .error $ errorIndex "Invalid goal index {args.goalId}" @@ -160,8 +164,5 @@ def execute (command: Commands.Command): MainM Lean.Json := do return .ok { goals? := .some sGoals.reverse.toArray, goalIds? := .some goalIds.reverse.toArray } | .failure messages => return .ok { tacticErrors? := .some messages } - proof_print_tree (_: Commands.ProofPrintTree): MainM (CR Commands.ProofPrintTreeResult) := do - let state ← get - return .ok { nGoals := state.goalStates.size } end Pantograph diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index 8c8b509..f9abf9d 100644 --- a/Pantograph/Commands.lean +++ b/Pantograph/Commands.lean @@ -80,8 +80,11 @@ structure InteractionError where structure Reset where deriving Lean.FromJson -structure ResetResult where - nStates: Nat +structure Stat where + deriving Lean.FromJson +structure StatResult where + -- Number of goals states + nGoals: Nat deriving Lean.ToJson -- Return the type of an expression @@ -149,11 +152,5 @@ structure ProofTacticResult where tacticErrors?: Option (Array String) := .none deriving Lean.ToJson -structure ProofPrintTree where - deriving Lean.FromJson -structure ProofPrintTreeResult where - -- Total number of goals - nGoals: Nat - deriving Lean.ToJson end Pantograph.Commands diff --git a/README.md b/README.md index 8407d49..9a2ec5b 100644 --- a/README.md +++ b/README.md @@ -50,15 +50,15 @@ Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting) $ lake env build/bin/Pantograph Mathlib.Analysis.Seminorm 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 -proof.start {"expr": "∀ (n m : Nat), n + m = m + n"} -proof.tactic {"goalId": 0, "tactic": "intro n m"} -proof.tactic {"goalId": 1, "tactic": "assumption"} -proof.printTree {} -proof.tactic {"goalId": 1, "tactic": "rw [Nat.add_comm]"} -proof.printTree +goal.start {"expr": "∀ (n m : Nat), n + m = m + n"} +goal.tactic {"goalId": 0, "tactic": "intro n m"} +goal.tactic {"goalId": 1, "tactic": "assumption"} +stat {} +goal.tactic {"goalId": 1, "tactic": "rw [Nat.add_comm]"} +stat ``` where the application of `assumption` should lead to a failure. @@ -74,9 +74,9 @@ 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 have to be set via command line arguments.), for options, see `Pantograph/Commands.lean` - `options.print`: Display the current set of options -- `proof.start {["name": ], ["expr": ], ["copyFrom": ]}`: Start a new proof state from a given expression or symbol -- `proof.tactic {"goalId": , "tactic": }`: Execute a tactic string on a given proof state -- `proof.printTree`: Print the number of goals +- `goal.start {["name": ], ["expr": ], ["copyFrom": ]}`: Start a new goal from a given expression or symbol +- `goal.tactic {"goalId": , "tactic": }`: Execute a tactic string on a given goal +- `stat`: Display resource usage ## Errors From 8d5d7b6e3e1499e8220a2eb47c1738495d5b2168 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 27 Aug 2023 19:59:31 -0700 Subject: [PATCH 3/4] Version bump to 0.2.4 due to breaking change --- Pantograph/Version.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean index e4ebd2c..f179705 100644 --- a/Pantograph/Version.lean +++ b/Pantograph/Version.lean @@ -1,5 +1,5 @@ namespace Pantograph -def version := "0.2.3" +def version := "0.2.4" end Pantograph From 46347d8244f7e9c7b84b5276bd8f303a8a236ce6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 30 Aug 2023 19:16:33 -0700 Subject: [PATCH 4/4] Add SemihashMap interface, rename proof commands to goal commands, allow deletion --- Pantograph.lean | 12 ++++-- Pantograph/Commands.lean | 15 +++++-- Pantograph/SemihashMap.lean | 86 +++++++++++++++++++++++++++++++------ README.md | 2 + 4 files changed, 95 insertions(+), 20 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index bb2635e..3e53859 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -38,6 +38,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do | "options.print" => run options_print | "goal.start" => run goal_start | "goal.tactic" => run goal_tactic + | "goal.delete" => run goal_delete | cmd => let error: Commands.InteractionError := errorCommand s!"Unknown command {cmd}" @@ -117,7 +118,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do return .ok { } options_print (_: Commands.OptionsPrint): MainM (CR Commands.OptionsPrintResult) := do return .ok (← get).options - goal_start (args: Commands.ProofStart): MainM (CR Commands.ProofStartResult) := do + goal_start (args: Commands.GoalStart): MainM (CR Commands.GoalStartResult) := do let state ← get let env ← Lean.MonadEnv.getEnv let expr?: Except _ Lean.Expr ← (match args.expr, args.copyFrom with @@ -142,10 +143,10 @@ def execute (command: Commands.Command): MainM Lean.Json := do let (goalStates, goalId) := state.goalStates.insert goalState set { state with goalStates } return .ok { goalId } - goal_tactic (args: Commands.ProofTactic): MainM (CR Commands.ProofTacticResult) := do + goal_tactic (args: Commands.GoalTactic): MainM (CR Commands.GoalTacticResult) := do let state ← get match state.goalStates.get? args.goalId with - | .none => return .error $ errorIndex "Invalid goal index {args.goalId}" + | .none => return .error $ errorIndex s!"Invalid goal index {args.goalId}" | .some goalState => let result ← GoalState.execute goalState args.tactic |>.run state.options match result with @@ -164,5 +165,10 @@ def execute (command: Commands.Command): MainM Lean.Json := do return .ok { goals? := .some sGoals.reverse.toArray, goalIds? := .some goalIds.reverse.toArray } | .failure messages => return .ok { tacticErrors? := .some messages } + goal_delete (args: Commands.GoalDelete): MainM (CR Commands.GoalDeleteResult) := do + let state ← get + let goalStates := args.goalIds.foldl (λ map id => map.remove id) state.goalStates + set { state with goalStates } + return .ok {} end Pantograph diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index f9abf9d..72194b0 100644 --- a/Pantograph/Commands.lean +++ b/Pantograph/Commands.lean @@ -130,20 +130,20 @@ structure OptionsPrint where deriving Lean.FromJson abbrev OptionsPrintResult := Options -structure ProofStart where +structure GoalStart where -- Only one of the fields below may be populated. expr: Option String -- Proof expression copyFrom: Option String -- Theorem name deriving Lean.FromJson -structure ProofStartResult where +structure GoalStartResult where goalId: Nat := 0 -- Proof tree id deriving Lean.ToJson -structure ProofTactic where +structure GoalTactic where -- Identifiers for tree, state, and goal goalId: Nat tactic: String deriving Lean.FromJson -structure ProofTacticResult where +structure GoalTacticResult where -- Existence of this field shows success goals?: Option (Array Goal) := .none -- Next proof state id, if successful @@ -152,5 +152,12 @@ structure ProofTacticResult where tacticErrors?: Option (Array String) := .none deriving Lean.ToJson +-- Remove a bunch of goals. +structure GoalDelete where + goalIds: List Nat + deriving Lean.FromJson +structure GoalDeleteResult where + deriving Lean.ToJson + end Pantograph.Commands diff --git a/Pantograph/SemihashMap.lean b/Pantograph/SemihashMap.lean index 362be94..1d9ebae 100644 --- a/Pantograph/SemihashMap.lean +++ b/Pantograph/SemihashMap.lean @@ -18,7 +18,56 @@ structure Imp (β: Type u) where 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 @@ -53,8 +102,9 @@ namespace Imp } (result, nextIndex) -@[inline] def remove (map: Imp β) (index: Nat): Imp β := - match map.data.getD index .none with +@[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 _ => { @@ -66,24 +116,34 @@ namespace Imp } /-- Retrieval is efficient -/ -@[inline] def get? (map: Imp β) (index: Nat): Option β := - map.data.getD index .none +@[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 -def empty (capacity := 16): Imp β := - { - data := mkArray capacity .none, - size := 0, - allocFront := 0, - deallocs := mkArray capacity 0, - lastDealloc := 0, - } /-- This is like a hashmap but you cannot control the keys. -/ -def _root_.Pantograph.SemihashMap β := Imp β +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 diff --git a/README.md b/README.md index 9a2ec5b..273e865 100644 --- a/README.md +++ b/README.md @@ -56,6 +56,7 @@ $ env build/bin/Pantograph Init goal.start {"expr": "∀ (n m : Nat), n + m = m + n"} goal.tactic {"goalId": 0, "tactic": "intro n m"} goal.tactic {"goalId": 1, "tactic": "assumption"} +goal.delete {"goalIds": [0]} stat {} goal.tactic {"goalId": 1, "tactic": "rw [Nat.add_comm]"} stat @@ -76,6 +77,7 @@ See `Pantograph/Commands.lean` for a description of the parameters and return va - `options.print`: Display the current set of options - `goal.start {["name": ], ["expr": ], ["copyFrom": ]}`: Start a new goal from a given expression or symbol - `goal.tactic {"goalId": , "tactic": }`: Execute a tactic string on a given goal +- `goal.remove {"goalIds": []}"`: Remove a bunch of stored goals. - `stat`: Display resource usage ## Errors