Add proof variable delta; Bump version to 0.2.1

2023-08-15 15:40:54 -07:00 · 2023-08-15 15:40:54 -07:00 · 0e61093f47
parent d476354a4a
commit 0e61093f47
8 changed files with 154 additions and 118 deletions
--- a/Main.lean
+++ b/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
--- a/Pantograph.lean
+++ b/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" =>
-    match Lean.fromJson? command.payload with
-    | .ok args => options_set args
-    | .error x => return errorJson x
-  | "options.print" =>
-    match Lean.fromJson? command.payload with
-    | .ok args => options_print args
-    | .error x => return errorJson x
-  | "catalog" =>
-    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
+  | "options.set"     => run options_set
+  | "options.print"   => run options_print
+  | "catalog"         => run catalog
+  | "inspect"         => run inspect
+  | "clear"           => run clear
+  | "expr.echo"       => run expr_echo
+  | "proof.start"     => run proof_start
+  | "proof.tactic"    => run proof_tactic
+  | "proof.printTree" => run proof_print_tree
  | cmd =>
    let error: Commands.InteractionError :=
      { error := "unknown", desc := s!"Unknown command {cmd}" }
    return Lean.toJson error
  where
-  errorI (type desc: String) := Lean.toJson (
-    { error := type, desc := desc }: Commands.InteractionError)
-  errorJson := errorI "json"
+  errorI (type desc: String): Commands.InteractionError := { error := type, desc := desc }
  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,
-        printExprAST := args.printExprAST?.getD true,
-        proofVariableDelta := args.proofVariableDelta?.getD false
+        -- FIXME: This should be replaced with something more elegant
+        printExprPretty := args.printExprPretty?.getD options.printExprPretty,
+        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)
-  options_print (_: Commands.OptionsPrint): Subroutine Lean.Json := do
-    return Lean.toJson (← get).options
-  catalog (_: Commands.Catalog): Subroutine Lean.Json := do
+    return .ok {  }
+  options_print (_: Commands.OptionsPrint): MainM (CR Commands.OptionsPrintResult) := do
+    return .ok (← get).options
+  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)
-  inspect (args: Commands.Inspect): Subroutine Lean.Json := do
+    return .ok { symbols := names }
+  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)
-  expr_echo (args: Commands.ExprEcho): Subroutine Lean.Json := do
+    return .ok { nTrees := nTrees }
+  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)
-  proof_start (args: Commands.ProofStart): Subroutine Lean.Json := do
+          return .error $ errorI "typing" (← exception.toMessageData.toString)
+  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)
-  proof_tactic (args: Commands.ProofTactic): Subroutine Lean.Json := do
+      return .ok { treeId := nextTreeId }
+  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 (
-          { nextId? := nextId?, goals := goals }: Commands.ProofTacticResultSuccess)
+        return .ok { nextId? := nextId?, goals? := .some goals }
      | .failure messages =>
-        return Lean.toJson (
-          { tacticErrors := messages }: Commands.ProofTacticResultFailure)
-  proof_print_tree (args: Commands.ProofPrintTree): Subroutine Lean.Json := do
+        return .ok { tacticErrors? := .some messages }
+  proof_print_tree (args: Commands.ProofPrintTree): MainM (CR Commands.ProofPrintTreeResult) := 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
--- a/Pantograph/Commands.lean
+++ b/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
-  type: Expression
+  isInaccessible?: Option Bool := .none
+  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
-  goals: Array Goal
-  nextId?: Option Nat -- Next proof state id
-  deriving Lean.ToJson
-structure ProofTacticResultFailure where
-  tacticErrors: Array String -- Error messages generated by tactic
+structure ProofTacticResult where
+  -- Existence of this field shows success
+  goals?: Option (Array Goal)          := .none
+  -- Next proof state id, if successful
+  nextId?: Option Nat                  := .none
+  -- Existence of this field shows failure
+  tacticErrors?: Option (Array String) := .none
  deriving Lean.ToJson

 structure ProofPrintTree where
--- a/Pantograph/Serial.lean
+++ b/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 ppAuxDecls     := false
-  let ppImplDetailHyps := false
+  let showLetValues  := true
+  let ppAuxDecls     := options.printAuxDecls
+  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,
-          type := (← serialize_expression options type)
+          isInaccessible? := .some varName.isInaccessibleUserName
+          type? := .some (← serialize_expression options type)
        }
      | .ldecl _ _ varName type val _ _ => do
        let varName := varName.simpMacroScopes
@ -165,17 +177,22 @@ def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) : MetaM C
          pure $ .none
        return {
          name := toString varName,
-          isInaccessible := varName.isInaccessibleUserName,
-          type := (← serialize_expression options type)
+          isInaccessible? := .some varName.isInaccessibleUserName
+          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
-       if skip then
-         return acc
-       else
-         let var ← ppVars localDecl
-         return var::acc
+      let skip := !ppAuxDecls && localDecl.isAuxDecl ||
+        !ppImplDetailHyps && localDecl.isImplementationDetail
+      if skip then
+        return acc
+      else
+        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
        | Name.anonymous => .none
--- a/Pantograph/Tactic.lean
+++ b/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

--- a/Pantograph/Version.lean
+++ b/Pantograph/Version.lean
@ -1,5 +1,5 @@
 namespace Pantograph

-def version := "0.2"
+def version := "0.2.1"

 end Pantograph
--- a/Test/Integration.lean
+++ b/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))
  ]

--- a/Test/Proofs.lean
+++ b/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 := "q", type := typeProp },
-      { name := "h✝", type := { pp? := .some name }, isInaccessible := true }
+      { name := "p", type? := .some typeProp, isInaccessible? := .some false },
+      { name := "q", type? := .some typeProp, isInaccessible? := .some false },
+      { 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