From 0e61093f47d778b9fcbaf7a5185e0561e85f8f1d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 15 Aug 2023 15:40:54 -0700 Subject: [PATCH] Add proof variable delta; Bump version to 0.2.1 --- Main.lean | 2 +- Pantograph.lean | 133 +++++++++++++++++---------------------- Pantograph/Commands.lean | 26 +++++--- Pantograph/Serial.lean | 47 +++++++++----- Pantograph/Tactic.lean | 3 +- Pantograph/Version.lean | 2 +- Test/Integration.lean | 9 +-- Test/Proofs.lean | 50 +++++++++++---- 8 files changed, 154 insertions(+), 118 deletions(-) diff --git a/Main.lean b/Main.lean index 9b8bedb..70f2494 100644 --- 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 diff --git a/Pantograph.lean b/Pantograph.lean index e7c2c59..e40a3e7 100644 --- 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 diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index 45eca35..57c5ddc 100644 --- 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 diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 67fb107..67a6963 100644 --- 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 diff --git a/Pantograph/Tactic.lean b/Pantograph/Tactic.lean index c051f3c..f661be5 100644 --- 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 diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean index d667eb3..a9c55b5 100644 --- 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 diff --git a/Test/Integration.lean b/Test/Integration.lean index d22eadf..cfcf557 100644 --- 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)) ] diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 9df7c84..52a2c69 100644 --- 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