Main.lean

@@ -7,7 +7,7 @@ import Pantograph
 -- Main IO functions
 open Pantograph
 
-unsafe def loop : Subroutine Unit := do
+unsafe def loop : MainM Unit := do
   let command ← (← IO.getStdin).getLine
   if command.trim.length = 0 then return ()
   match parse_command command with

Pantograph.lean

@@ -15,7 +15,10 @@ structure State where
   proofTrees:   Array ProofTree := #[]
 
 -- State monad
-abbrev Subroutine := ReaderT Context (StateT State Lean.Elab.TermElabM)
+abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM)
+-- For some reason writing `CommandM α := MainM (Except ... α)` disables certain
+-- monadic features in `MainM`
+abbrev CR α := Except Commands.InteractionError α
 
 /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
 def parse_command (s: String): Except String Commands.Command := do
@@ -32,77 +35,62 @@ def parse_command (s: String): Except String Commands.Command := do
       return { cmd := s.take offset, payload := payload }
   | .none => throw "Command is empty"
 
-def execute (command: Commands.Command): Subroutine Lean.Json := do
+def execute (command: Commands.Command): MainM Lean.Json := do
+  let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
+    match Lean.fromJson? command.payload with
+    | .ok args => do
+      match (← comm args) with
+      | .ok result =>  return Lean.toJson result
+      | .error ierror => return Lean.toJson ierror
+    | .error error => pure $ error
   match command.cmd with
-  | "options.set" =>
+  | "options.set"     => run options_set
-    match Lean.fromJson? command.payload with
+  | "options.print"   => run options_print
-    | .ok args => options_set args
+  | "catalog"         => run catalog
-    | .error x => return errorJson x
+  | "inspect"         => run inspect
-  | "options.print" =>
+  | "clear"           => run clear
-    match Lean.fromJson? command.payload with
+  | "expr.echo"       => run expr_echo
-    | .ok args => options_print args
+  | "proof.start"     => run proof_start
-    | .error x => return errorJson x
+  | "proof.tactic"    => run proof_tactic
-  | "catalog" =>
+  | "proof.printTree" => run proof_print_tree
-    match Lean.fromJson? command.payload with
-    | .ok args => catalog args
-    | .error x => return errorJson x
-  | "inspect" =>
-    match Lean.fromJson? command.payload with
-    | .ok args => inspect args
-    | .error x => return errorJson x
-  | "clear" => clear
-  | "expr.echo" =>
-    match Lean.fromJson? command.payload with
-    | .ok args => expr_echo args
-    | .error x => return errorJson x
-  | "proof.start" =>
-    match Lean.fromJson? command.payload with
-    | .ok args => proof_start args
-    | .error x => return errorJson x
-  | "proof.tactic" =>
-    match Lean.fromJson? command.payload with
-    | .ok args => proof_tactic args
-    | .error x => return errorJson x
-  | "proof.printTree" =>
-    match Lean.fromJson? command.payload with
-    | .ok args => proof_print_tree args
-    | .error x => return errorJson x
   | cmd =>
     let error: Commands.InteractionError :=
       { error := "unknown", desc := s!"Unknown command {cmd}" }
     return Lean.toJson error
   where
-  errorI (type desc: String) := Lean.toJson (
+  errorI (type desc: String): Commands.InteractionError := { error := type, desc := desc }
-    { error := type, desc := desc }: Commands.InteractionError)
-  errorJson := errorI "json"
   errorIndex := errorI "index"
   -- Command Functions
-  options_set (args: Commands.OptionsSet): Subroutine Lean.Json := do
+  options_set (args: Commands.OptionsSet): MainM (CR Commands.OptionsSetResult) := do
     let state ← get
+    let options := state.options
     set { state with
       options := {
-        printExprPretty := args.printExprPretty?.getD true,
+        -- FIXME: This should be replaced with something more elegant
-        printExprAST := args.printExprAST?.getD true,
+        printExprPretty := args.printExprPretty?.getD options.printExprPretty,
-        proofVariableDelta := args.proofVariableDelta?.getD false
+        printExprAST := args.printExprAST?.getD options.printExprAST,
+        proofVariableDelta := args.proofVariableDelta?.getD options.proofVariableDelta,
+        printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
+        printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
       }
     }
-    return Lean.toJson ({ }: Commands.OptionsSetResult)
+    return .ok {  }
-  options_print (_: Commands.OptionsPrint): Subroutine Lean.Json := do
+  options_print (_: Commands.OptionsPrint): MainM (CR Commands.OptionsPrintResult) := do
-    return Lean.toJson (← get).options
+    return .ok (← get).options
-  catalog (_: Commands.Catalog): Subroutine Lean.Json := do
+  catalog (_: Commands.Catalog): MainM (CR Commands.CatalogResult) := do
     let env ← Lean.MonadEnv.getEnv
     let names := env.constants.fold (init := #[]) (λ acc name info =>
       match to_filtered_symbol name info with
       | .some x => acc.push x
       | .none => acc)
-    return Lean.toJson <| ({ symbols := names }: Commands.CatalogResult)
+    return .ok { symbols := names }
-  inspect (args: Commands.Inspect): Subroutine Lean.Json := do
+  inspect (args: Commands.Inspect): MainM (CR Commands.InspectResult) := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
     let name := str_to_name args.name
     let info? := env.find? name
     match info? with
-    | none => return  errorIndex s!"Symbol not found {args.name}"
+    | none => return .error $ errorIndex s!"Symbol not found {args.name}"
     | some info =>
       let module? := env.getModuleIdxFor? name >>=
         (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
@@ -111,37 +99,37 @@ def execute (command: Commands.Command): Subroutine Lean.Json := do
         | .some false, _ => .none
         | .none, .defnInfo _ => info.value?
         | .none, _ => .none
-      return Lean.toJson ({
+      return .ok {
         type := ← serialize_expression state.options info.type,
         value? := ← value?.mapM (λ v => serialize_expression state.options v),
         module? := module?
-      }: Commands.InspectResult)
+      }
-  clear : Subroutine Lean.Json := do
+  clear (_: Commands.Clear): MainM (CR Commands.ClearResult) := do
     let state ← get
     let nTrees := state.proofTrees.size
     set { state with proofTrees := #[] }
-    return Lean.toJson ({ nTrees := nTrees }: Commands.ClearResult)
+    return .ok { nTrees := nTrees }
-  expr_echo (args: Commands.ExprEcho): Subroutine Lean.Json := do
+  expr_echo (args: Commands.ExprEcho): MainM (CR Commands.ExprEchoResult) := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
     match syntax_from_str env args.expr with
-    | .error str => return errorI "parsing" str
+    | .error str => return .error $ errorI "parsing" str
     | .ok syn => do
       match (← syntax_to_expr syn) with
-      | .error str => return errorI "elab" str
+      | .error str => return .error $ errorI "elab" str
       | .ok expr => do
         try
           let type ← Lean.Meta.inferType expr
-          return Lean.toJson <| ({
+          return .ok {
               type := (← serialize_expression (options := state.options) type),
               expr := (← serialize_expression (options := state.options) expr)
-          }: Commands.ExprEchoResult)
+          }
         catch exception =>
-          return errorI "typing" (← exception.toMessageData.toString)
+          return .error $ errorI "typing" (← exception.toMessageData.toString)
-  proof_start (args: Commands.ProofStart): Subroutine Lean.Json := do
+  proof_start (args: Commands.ProofStart): MainM (CR Commands.ProofStartResult) := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
-    let expr?: Except Lean.Json Lean.Expr ← (match args.expr, args.copyFrom with
+    let expr?: Except _ Lean.Expr ← (match args.expr, args.copyFrom with
       | .some expr, .none =>
         (match syntax_from_str env expr with
         | .error str => return .error <| errorI "parsing" str
@@ -157,37 +145,34 @@ def execute (command: Commands.Command): Subroutine Lean.Json := do
         return .error <| errorI "arguments" "At least one of {expr, copyFrom} must be supplied"
       | _, _ => return .error <| errorI "arguments" "Cannot populate both of {expr, copyFrom}")
     match expr? with
-    | .error error => return error
+    | .error error => return .error error
     | .ok expr =>
       let tree ← ProofTree.create (str_to_name <| args.name.getD "Untitled") expr
       -- Put the new tree in the environment
       let nextTreeId := state.proofTrees.size
       set { state with proofTrees := state.proofTrees.push tree }
-      return Lean.toJson ({ treeId := nextTreeId }: Commands.ProofStartResult)
+      return .ok { treeId := nextTreeId }
-  proof_tactic (args: Commands.ProofTactic): Subroutine Lean.Json := do
+  proof_tactic (args: Commands.ProofTactic): MainM (CR Commands.ProofTacticResult) := do
     let state ← get
     match state.proofTrees.get? args.treeId with
-    | .none => return errorIndex "Invalid tree index {args.treeId}"
+    | .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 result with
-      | .invalid message => return Lean.toJson <| errorIndex message
+      | .invalid message => return .error $  errorIndex message
       | .success nextId? goals =>
         set { state with proofTrees := state.proofTrees.set! args.treeId nextTree }
-        return Lean.toJson (
+        return .ok { nextId? := nextId?, goals? := .some goals }
-          { nextId? := nextId?, goals := goals }: Commands.ProofTacticResultSuccess)
       | .failure messages =>
-        return Lean.toJson (
+        return .ok { tacticErrors? := .some messages }
-          { tacticErrors := messages }: Commands.ProofTacticResultFailure)
+  proof_print_tree (args: Commands.ProofPrintTree): MainM (CR Commands.ProofPrintTreeResult) := do
-  proof_print_tree (args: Commands.ProofPrintTree): Subroutine Lean.Json := do
     let state ← get
     match state.proofTrees.get? args.treeId with
-    | .none => return errorIndex "Invalid tree index {args.treeId}"
+    | .none => return .error $ errorIndex "Invalid tree index {args.treeId}"
     | .some tree =>
-      return Lean.toJson ({parents := tree.structure_array}: Commands.ProofPrintTreeResult)
+      return .ok { parents := tree.structure_array }
-
 
 end Pantograph

Pantograph/Commands.lean

@@ -17,8 +17,11 @@ structure Options where
   printExprAST: Bool       := false
   -- When enabled, the types and values of persistent variables in a proof goal
   -- are not shown unless they are new to the proof step. Reduces overhead
-  -- TODO: Not implemented yet.
   proofVariableDelta: Bool := false
+  -- See `pp.auxDecls`
+  printAuxDecls: Bool      := false
+  -- See `pp.implementationDetailHyps`
+  printImplementationDetailHyps: Bool := false
   deriving Lean.ToJson
 
 abbrev OptionsT := ReaderT Options
@@ -39,8 +42,8 @@ structure Expression where
 structure Variable where
   name: String
   /-- Does the name contain a dagger -/
-  isInaccessible: Bool      := false
+  isInaccessible?: Option Bool := .none
-  type: Expression
+  type?: Option Expression  := .none
   value?: Option Expression := .none
   deriving Lean.ToJson
 structure Goal where
@@ -76,6 +79,8 @@ structure OptionsSet where
   printExprPretty?: Option Bool
   printExprAST?: Option Bool
   proofVariableDelta?: Option Bool
+  printAuxDecls?: Option Bool
+  printImplementationDetailHyps?: Option Bool
   deriving Lean.FromJson
 structure OptionsSetResult where
   deriving Lean.ToJson
@@ -105,6 +110,8 @@ structure InspectResult where
   module?: Option String
   deriving Lean.ToJson
 
+structure Clear where
+  deriving Lean.FromJson
 structure ClearResult where
   nTrees: Nat
   deriving Lean.ToJson
@@ -135,12 +142,13 @@ structure ProofTactic where
   goalId: Option Nat
   tactic: String
   deriving Lean.FromJson
-structure ProofTacticResultSuccess where
+structure ProofTacticResult where
-  goals: Array Goal
+  -- Existence of this field shows success
-  nextId?: Option Nat -- Next proof state id
+  goals?: Option (Array Goal)          := .none
-  deriving Lean.ToJson
+  -- Next proof state id, if successful
-structure ProofTacticResultFailure where
+  nextId?: Option Nat                  := .none
-  tacticErrors: Array String -- Error messages generated by tactic
+  -- Existence of this field shows failure
+  tacticErrors?: Option (Array String) := .none
   deriving Lean.ToJson
 
 structure ProofPrintTree where

Pantograph/Serial.lean

@@ -137,23 +137,35 @@ def serialize_expression (options: Commands.Options) (e: Expr): MetaM Commands.E
   }
 
 /-- Adapted from ppGoal -/
-def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) : MetaM Commands.Goal := do
+def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
+      : MetaM Commands.Goal := do
   -- Options for printing; See Meta.ppGoal for details
-  let showLetValues  := True
+  let showLetValues  := true
-  let ppAuxDecls     := false
+  let ppAuxDecls     := options.printAuxDecls
-  let ppImplDetailHyps := false
+  let ppImplDetailHyps := options.printImplementationDetailHyps
   let lctx           := mvarDecl.lctx
   let lctx           := lctx.sanitizeNames.run' { options := (← getOptions) }
   Meta.withLCtx lctx mvarDecl.localInstances do
-    let rec ppVars (localDecl : LocalDecl) : MetaM Commands.Variable := do
+    let ppVarNameOnly (localDecl: LocalDecl): MetaM Commands.Variable := do
+      match localDecl with
+      | .cdecl _ _ varName _ _ _ =>
+        let varName := varName.simpMacroScopes
+        return {
+          name := toString varName,
+        }
+      | .ldecl _ _ varName _ _ _ _ => do
+        return {
+          name := toString varName,
+        }
+    let ppVar (localDecl : LocalDecl) : MetaM Commands.Variable := do
       match localDecl with
       | .cdecl _ _ varName type _ _ =>
         let varName := varName.simpMacroScopes
         let type ← instantiateMVars type
         return {
           name := toString varName,
-          isInaccessible := varName.isInaccessibleUserName,
+          isInaccessible? := .some varName.isInaccessibleUserName
-          type := (← serialize_expression options type)
+          type? := .some (← serialize_expression options type)
         }
       | .ldecl _ _ varName type val _ _ => do
         let varName := varName.simpMacroScopes
@@ -165,16 +177,21 @@ def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) : MetaM C
           pure $ .none
         return {
           name := toString varName,
-          isInaccessible := varName.isInaccessibleUserName,
+          isInaccessible? := .some varName.isInaccessibleUserName
-          type := (← serialize_expression options type)
+          type? := .some (← serialize_expression options type)
           value? := value?
         }
     let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
-       let skip := !ppAuxDecls && localDecl.isAuxDecl || !ppImplDetailHyps && localDecl.isImplementationDetail
+      let skip := !ppAuxDecls && localDecl.isAuxDecl ||
+        !ppImplDetailHyps && localDecl.isImplementationDetail
       if skip then
         return acc
       else
-         let var ← ppVars localDecl
+        let nameOnly := options.proofVariableDelta && (parentDecl?.map
+          (λ decl => decl.lctx.find? localDecl.fvarId |>.isSome) |>.getD false)
+        let var ← match nameOnly with
+          | true => ppVarNameOnly localDecl
+          | false => ppVar localDecl
         return var::acc
     return {
       caseName? := match mvarDecl.userName with

Pantograph/Tactic.lean

@@ -115,9 +115,10 @@ def ProofTree.execute (stateId: Nat) (goalId: Nat) (tactic: String):
             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
+          | .some mvarDecl => serialize_goal options mvarDecl (parentDecl? := parentDecl?)
           | .none => throwError mvarId
         return .success (.some nextId) goals.toArray
 

Pantograph/Version.lean

@@ -1,5 +1,5 @@
 namespace Pantograph
 
-def version := "0.2"
+def version := "0.2.1"
 
 end Pantograph

Test/Integration.lean

@@ -6,11 +6,11 @@ namespace Pantograph.Test
 open Pantograph
 
 def subroutine_step (cmd: String) (payload: List (String × Lean.Json))
-    (expected: Lean.Json): Subroutine LSpec.TestSeq := do
+    (expected: Lean.Json): MainM LSpec.TestSeq := do
   let result ← execute { cmd := cmd, payload := Lean.Json.mkObj payload }
   return LSpec.test s!"{cmd}" (toString result = toString expected)
 
-def subroutine_runner (steps: List (Subroutine LSpec.TestSeq)): IO LSpec.TestSeq := do
+def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := do
   -- Setup the environment for execution
   let env ← Lean.importModules
     (imports := [{module := Lean.Name.str .anonymous "Init", runtimeOnly := false }])
@@ -26,7 +26,7 @@ def subroutine_runner (steps: List (Subroutine LSpec.TestSeq)): IO LSpec.TestSeq
     fileMap := { source := "", positions := #[0], lines := #[1] },
     options := Lean.Options.empty
   }
-  let commands: Subroutine LSpec.TestSeq :=
+  let commands: MainM LSpec.TestSeq :=
     steps.foldlM (λ suite step => do
       let result ← step
       return suite ++ result) LSpec.TestSeq.done
@@ -45,6 +45,7 @@ def test_option_print : IO LSpec.TestSeq :=
   let pp? := Option.some "∀ (n : Nat), n + 1 = Nat.succ n"
   let sexp? := Option.some "(:forall n (:c Nat) ((((:c Eq) (:c Nat)) (((((((:c HAdd.hAdd) (:c Nat)) (:c Nat)) (:c Nat)) (((:c instHAdd) (:c Nat)) (:c instAddNat))) 0) ((((:c OfNat.ofNat) (:c Nat)) (:lit 1)) ((:c instOfNatNat) (:lit 1))))) ((:c Nat.succ) 0)))"
   let module? := Option.some "Init.Data.Nat.Basic"
+  let options: Commands.Options := {}
   subroutine_runner [
     subroutine_step "inspect"
       [("name", .str "Nat.add_one")]
@@ -62,7 +63,7 @@ def test_option_print : IO LSpec.TestSeq :=
       Commands.InspectResult)),
     subroutine_step "options.print"
       []
-     (Lean.toJson ({ printExprAST := true }:
+     (Lean.toJson ({ options with printExprAST := true }:
       Commands.OptionsPrintResult))
   ]
 

Test/Proofs.lean

@@ -10,7 +10,7 @@ inductive Start where
   | copy (name: String) -- Start from some name in the environment
   | expr (expr: String) -- Start from some expression
 
-abbrev TestM := StateRefT ProofTree M
+abbrev TestM := ReaderT Commands.Options StateRefT ProofTree M
 
 def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do
   let env ← Lean.MonadEnv.getEnv
@@ -55,7 +55,8 @@ 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 result: TacticResult ← ProofTree.execute stateId goalId tactic |>.run {}
+  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
@@ -70,12 +71,12 @@ def proof_inspect (expected: Array String) : TestM LSpec.TestSeq := do
   let result := (← get).structure_array
   return LSpec.test s!"tree structure" (result = expected)
 
-def proof_runner (env: Lean.Environment) (start: Start) (steps: List (TestM LSpec.TestSeq)): IO LSpec.TestSeq := do
+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' state
+    | .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",
@@ -97,7 +98,10 @@ def build_goal (nameType: List (String × String)) (target: String): Commands.Go
   {
     target := { pp? := .some target},
     vars := (nameType.map fun x => ({
-      name := x.fst, type := { pp? := .some x.snd } })).toArray
+      name := x.fst,
+      type? := .some { pp? := .some x.snd },
+      isInaccessible? := .some false
+    })).toArray
   }
 
 example: ∀ (a b: Nat), a + b = b + a := by
@@ -105,7 +109,7 @@ example: ∀ (a b: Nat), a + b = b + a := by
   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_runner env {} (.copy "Nat.add_comm") [
     proof_step 0 0 "intro n m"
       (.success (.some 1) #[goal1]),
     proof_step 1 0 "assumption"
@@ -115,7 +119,7 @@ def proof_nat_add_comm (env: Lean.Environment): IO LSpec.TestSeq := do
   ]
 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_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"
@@ -145,12 +149,12 @@ def proof_or_comm (env: Lean.Environment): IO LSpec.TestSeq := do
     caseName? := .some caseName,
     target := { pp? := .some "q ∨ p" },
     vars := #[
-      { name := "p", type := typeProp },
+      { name := "p", type? := .some typeProp, isInaccessible? := .some false },
-      { name := "q", type := typeProp },
+      { name := "q", type? := .some typeProp, isInaccessible? := .some false },
-      { name := "h✝", type := { pp? := .some name }, isInaccessible := true }
+      { name := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true }
     ]
   }
-  proof_runner env (.expr "∀ (p q: Prop), p ∨ q → q ∨ p") [
+  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"
@@ -173,7 +177,7 @@ example (w x y z : Nat) (p : Nat → Prop)
   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_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 *"
@@ -182,6 +186,25 @@ def proof_arith_1 (env: Lean.Environment): IO LSpec.TestSeq := do
       (.success .none #[])
   ]
 
+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 (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])
+  ]
+
 def test_proofs : IO LSpec.TestSeq := do
   let env: Lean.Environment ← Lean.importModules
     (imports := ["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
@@ -192,7 +215,8 @@ def test_proofs : IO LSpec.TestSeq := do
     (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 "Arithmetic 1" $ (← proof_arith_1 env)) ++
+    (LSpec.group "Delta variable" $ (← proof_delta_variable env))
 
 end Pantograph.Test