feat: Elementarized tactics with motives, congruence, and absurdity #72

Merged
aniva merged 41 commits from goal/mapply into dev 2024-06-12 13:52:46 -07:00
7 changed files with 69 additions and 61 deletions
Showing only changes of commit c0e6e3ec39 - Show all commits

View File

@ -71,7 +71,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
Environment.addDecl args Environment.addDecl args
expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
let state ← get let state ← get
exprEcho args.expr args.type? state.options exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
let state ← get let state ← get
let options := state.options let options := state.options
@ -94,7 +94,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let state ← get let state ← get
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
| .some expr, .none => goalStartExpr expr | .some expr, .none => goalStartExpr expr (args.levels.getD #[])
| .none, .some copyFrom => | .none, .some copyFrom =>
(match env.find? <| copyFrom.toName with (match env.find? <| copyFrom.toName with
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"

View File

@ -34,16 +34,16 @@ def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO O
end Lean end Lean
open Lean
namespace Pantograph namespace Pantograph
def defaultTermElabMContext: Lean.Elab.Term.Context := { def defaultTermElabMContext: Elab.Term.Context := {
autoBoundImplicit := true,
declName? := .some `_pantograph,
errToSorry := false errToSorry := false
} }
def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α := def runMetaM { α } (metaM: MetaM α): CoreM α :=
metaM.run' metaM.run'
def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α := def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α :=
termElabM.run' (ctx := defaultTermElabMContext) |>.run' termElabM.run' (ctx := defaultTermElabMContext) |>.run'
def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc } def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
@ -56,13 +56,13 @@ unsafe def initSearch (sp: String): IO Unit := do
/-- Creates a Core.Context object needed to run all monads -/ /-- Creates a Core.Context object needed to run all monads -/
@[export pantograph_create_core_context] @[export pantograph_create_core_context]
def createCoreContext (options: Array String): IO Lean.Core.Context := do def createCoreContext (options: Array String): IO Core.Context := do
let options? ← options.foldlM Lean.setOptionFromString' Lean.Options.empty |>.run let options? ← options.foldlM setOptionFromString' Options.empty |>.run
let options ← match options? with let options ← match options? with
| .ok options => pure options | .ok options => pure options
| .error e => throw $ IO.userError s!"Options cannot be parsed: {e}" | .error e => throw $ IO.userError s!"Options cannot be parsed: {e}"
return { return {
currNamespace := Lean.Name.str .anonymous "Aniva" currNamespace := Name.str .anonymous "Aniva"
openDecls := [], -- No 'open' directives needed openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph>", fileName := "<Pantograph>",
fileMap := { source := "", positions := #[0] }, fileMap := { source := "", positions := #[0] },
@ -71,7 +71,7 @@ def createCoreContext (options: Array String): IO Lean.Core.Context := do
/-- Creates a Core.State object needed to run all monads -/ /-- Creates a Core.State object needed to run all monads -/
@[export pantograph_create_core_state] @[export pantograph_create_core_state]
def createCoreState (imports: Array String): IO Lean.Core.State := do def createCoreState (imports: Array String): IO Core.State := do
let env ← Lean.importModules let env ← Lean.importModules
(imports := imports.map (λ str => { module := str.toName, runtimeOnly := false })) (imports := imports.map (λ str => { module := str.toName, runtimeOnly := false }))
(opts := {}) (opts := {})
@ -83,33 +83,33 @@ def createMetaContext: IO Lean.Meta.Context := do
return {} return {}
@[export pantograph_env_catalog_m] @[export pantograph_env_catalog_m]
def envCatalog: Lean.CoreM Protocol.EnvCatalogResult := def envCatalog: CoreM Protocol.EnvCatalogResult :=
Environment.catalog ({}: Protocol.EnvCatalog) Environment.catalog ({}: Protocol.EnvCatalog)
@[export pantograph_env_inspect_m] @[export pantograph_env_inspect_m]
def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options): def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options):
Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) := CoreM (Protocol.CR Protocol.EnvInspectResult) :=
Environment.inspect ({ Environment.inspect ({
name, value? := .some value, dependency?:= .some dependency name, value? := .some value, dependency?:= .some dependency
}: Protocol.EnvInspect) options }: Protocol.EnvInspect) options
@[export pantograph_env_add_m] @[export pantograph_env_add_m]
def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool): def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
Lean.CoreM (Protocol.CR Protocol.EnvAddResult) := CoreM (Protocol.CR Protocol.EnvAddResult) :=
Environment.addDecl { name, type, value, isTheorem } Environment.addDecl { name, type, value, isTheorem }
def parseElabType (type: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do
let env ← Lean.MonadEnv.getEnv let env ← MonadEnv.getEnv
let syn ← match parseTerm env type with let syn ← match parseTerm env type with
| .error str => return .error $ errorI "parsing" str | .error str => return .error $ errorI "parsing" str
| .ok syn => pure syn | .ok syn => pure syn
match ← elabType syn with match ← elabType syn with
| .error str => return .error $ errorI "elab" str | .error str => return .error $ errorI "elab" str
| .ok expr => return .ok (← Lean.instantiateMVars expr) | .ok expr => return .ok (← instantiateMVars expr)
/-- This must be a TermElabM since the parsed expr contains extra information -/ /-- This must be a TermElabM since the parsed expr contains extra information -/
def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do def parseElabExpr (expr: String) (expectedType?: Option String := .none): Elab.TermElabM (Protocol.CR Expr) := do
let env ← Lean.MonadEnv.getEnv let env ← MonadEnv.getEnv
let expectedType? ← match ← expectedType?.mapM parseElabType with let expectedType? ← match ← expectedType?.mapM parseElabType with
| .none => pure $ .none | .none => pure $ .none
| .some (.ok t) => pure $ .some t | .some (.ok t) => pure $ .some t
@ -119,17 +119,17 @@ def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.E
| .ok syn => pure syn | .ok syn => pure syn
match ← elabTerm syn expectedType? with match ← elabTerm syn expectedType? with
| .error str => return .error $ errorI "elab" str | .error str => return .error $ errorI "elab" str
| .ok expr => return .ok (← Lean.instantiateMVars expr) | .ok expr => return .ok (← instantiateMVars expr)
@[export pantograph_expr_echo_m] @[export pantograph_expr_echo_m]
def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options): def exprEcho (expr: String) (expectedType?: Option String := .none) (levels: Array String := #[]) (options: @&Protocol.Options := {}):
Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := CoreM (Protocol.CR Protocol.ExprEchoResult) :=
runTermElabM do runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
let expr ← match ← parseElabExpr expr expectedType? with let expr ← match ← parseElabExpr expr expectedType? with
| .error e => return .error e | .error e => return .error e
| .ok expr => pure expr | .ok expr => pure expr
try try
let type ← unfoldAuxLemmas (← Lean.Meta.inferType expr) let type ← unfoldAuxLemmas (← Meta.inferType expr)
return .ok { return .ok {
type := (← serializeExpression options type), type := (← serializeExpression options type),
expr := (← serializeExpression options expr) expr := (← serializeExpression options expr)
@ -138,8 +138,8 @@ def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&
return .error $ errorI "typing" (← exception.toMessageData.toString) return .error $ errorI "typing" (← exception.toMessageData.toString)
@[export pantograph_goal_start_expr_m] @[export pantograph_goal_start_expr_m]
def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) := def goalStartExpr (expr: String) (levels: Array String): CoreM (Protocol.CR GoalState) :=
runTermElabM do runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
let expr ← match ← parseElabType expr with let expr ← match ← parseElabType expr with
| .error e => return .error e | .error e => return .error e
| .ok expr => pure $ expr | .ok expr => pure $ expr
@ -154,11 +154,11 @@ def goalContinue (target: GoalState) (branch: GoalState): Except String GoalStat
target.continue branch target.continue branch
@[export pantograph_goal_serialize_m] @[export pantograph_goal_serialize_m]
def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) := def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) :=
runMetaM <| state.serializeGoals (parent := .none) options runMetaM <| state.serializeGoals (parent := .none) options
@[export pantograph_goal_print_m] @[export pantograph_goal_print_m]
def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult :=
runMetaM do runMetaM do
state.restoreMetaM state.restoreMetaM
return { return {
@ -170,38 +170,38 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto
serializeExpression options (← instantiateAll expr)), serializeExpression options (← instantiateAll expr)),
} }
@[export pantograph_goal_diag_m] @[export pantograph_goal_diag_m]
def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : Lean.CoreM String := def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : CoreM String :=
runMetaM $ state.diag diagOptions runMetaM $ state.diag diagOptions
@[export pantograph_goal_tactic_m] @[export pantograph_goal_tactic_m]
def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult := def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticResult :=
runTermElabM <| state.tryTactic goalId tactic runTermElabM <| state.tryTactic goalId tactic
@[export pantograph_goal_assign_m] @[export pantograph_goal_assign_m]
def goalAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult := def goalAssign (state: GoalState) (goalId: Nat) (expr: String): CoreM TacticResult :=
runTermElabM <| state.tryAssign goalId expr runTermElabM <| state.tryAssign goalId expr
@[export pantograph_goal_have_m] @[export pantograph_goal_have_m]
def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
runTermElabM <| state.tryHave goalId binderName type runTermElabM <| state.tryHave goalId binderName type
@[export pantograph_goal_let_m] @[export pantograph_goal_let_m]
def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
runTermElabM <| state.tryLet goalId binderName type runTermElabM <| state.tryLet goalId binderName type
@[export pantograph_goal_conv_m] @[export pantograph_goal_conv_m]
def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult := def goalConv (state: GoalState) (goalId: Nat): CoreM TacticResult :=
runTermElabM <| state.conv goalId runTermElabM <| state.conv goalId
@[export pantograph_goal_conv_exit_m] @[export pantograph_goal_conv_exit_m]
def goalConvExit (state: GoalState): Lean.CoreM TacticResult := def goalConvExit (state: GoalState): CoreM TacticResult :=
runTermElabM <| state.convExit runTermElabM <| state.convExit
@[export pantograph_goal_calc_m] @[export pantograph_goal_calc_m]
def goalCalc (state: GoalState) (goalId: Nat) (pred: String): Lean.CoreM TacticResult := def goalCalc (state: GoalState) (goalId: Nat) (pred: String): CoreM TacticResult :=
runTermElabM <| state.tryCalc goalId pred runTermElabM <| state.tryCalc goalId pred
@[export pantograph_goal_focus] @[export pantograph_goal_focus]
def goalFocus (state: GoalState) (goalId: Nat): Option GoalState := def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
state.focus goalId state.focus goalId
@[export pantograph_goal_motivated_apply_m] @[export pantograph_goal_motivated_apply_m]
def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean.CoreM TacticResult := def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): CoreM TacticResult :=
runTermElabM <| state.tryMotivatedApply goalId recursor runTermElabM <| state.tryMotivatedApply goalId recursor
@[export pantograph_goal_no_confuse_m] @[export pantograph_goal_no_confuse_m]
def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Lean.CoreM TacticResult := def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): CoreM TacticResult :=
runTermElabM <| state.tryNoConfuse goalId eq runTermElabM <| state.tryNoConfuse goalId eq
inductive TacticExecute where inductive TacticExecute where
@ -209,7 +209,7 @@ inductive TacticExecute where
| congruenceFun | congruenceFun
| congruence | congruence
@[export pantograph_goal_tactic_execute_m] @[export pantograph_goal_tactic_execute_m]
def goalTacticExecute (state: GoalState) (goalId: Nat) (tacticExecute: TacticExecute): Lean.CoreM TacticResult := def goalTacticExecute (state: GoalState) (goalId: Nat) (tacticExecute: TacticExecute): CoreM TacticResult :=
runTermElabM do runTermElabM do
state.restoreElabM state.restoreElabM
state.execute goalId $ match tacticExecute with state.execute goalId $ match tacticExecute with

View File

@ -101,6 +101,8 @@ structure StatResult where
structure ExprEcho where structure ExprEcho where
expr: String expr: String
type?: Option String type?: Option String
-- universe levels
levels: Option (Array String) := .none
deriving Lean.FromJson deriving Lean.FromJson
structure ExprEchoResult where structure ExprEchoResult where
expr: Expression expr: Expression
@ -197,6 +199,8 @@ structure OptionsPrint where
structure GoalStart where structure GoalStart where
-- Only one of the fields below may be populated. -- Only one of the fields below may be populated.
expr: Option String -- Directly parse in an expression expr: Option String -- Directly parse in an expression
-- universe levels
levels: Option (Array String) := .none
copyFrom: Option String -- Copy the type from a theorem in the environment copyFrom: Option String -- Copy the type from a theorem in the environment
deriving Lean.FromJson deriving Lean.FromJson
structure GoalStartResult where structure GoalStartResult where

View File

@ -1,5 +1,7 @@
/- /-
All serialisation functions All serialisation functions;
This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without
using `Scope`s.
-/ -/
import Lean import Lean
import Pantograph.Expr import Pantograph.Expr

View File

@ -82,8 +82,8 @@ where the application of `assumption` should lead to a failure.
See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON.
* `reset`: Delete all cached expressions and proof trees * `reset`: Delete all cached expressions and proof trees
* `stat`: Display resource usage * `stat`: Display resource usage
* `expr.echo {"expr": <expr>, "type": <optional expected type>}`: Determine the * `expr.echo {"expr": <expr>, "type": <optional expected type>, ["levels": [<levels>]]}`: Determine the
type of an expression and format it type of an expression and format it.
* `env.catalog`: Display a list of all safe Lean symbols in the current environment * `env.catalog`: Display a list of all safe Lean symbols in the current environment
* `env.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a * `env.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
given symbol; If value flag is set, the value is printed or hidden. By default given symbol; If value flag is set, the value is printed or hidden. By default
@ -91,7 +91,7 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
* `options.set { key: value, ... }`: Set one or more options (not Lean options; those * `options.set { key: value, ... }`: Set one or more options (not Lean options; those
have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
* `options.print`: Display the current set of options * `options.print`: Display the current set of options
* `goal.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: * `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
Start a new proof from a given expression or symbol Start a new proof from a given expression or symbol
* `goal.tactic {"stateId": <id>, "goalId": <id>, ...}`: Execute a tactic string on a * `goal.tactic {"stateId": <id>, "goalId": <id>, ...}`: Execute a tactic string on a
given goal. The tactic is supplied as additional key-value pairs in one of the following formats: given goal. The tactic is supplied as additional key-value pairs in one of the following formats:

View File

@ -35,7 +35,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d
def test_elab : IO LSpec.TestSeq := def test_elab : IO LSpec.TestSeq :=
subroutine_runner [ subroutine_runner [
subroutine_step "expr.echo" subroutine_step "expr.echo"
[("expr", .str "λ {α : Sort (u + 1)} => List α")] [("expr", .str "λ {α : Sort (u + 1)} => List α"), ("levels", .arr #["u"])]
(Lean.toJson ({ (Lean.toJson ({
type := { pp? := .some "{α : Type u} → Type u" }, type := { pp? := .some "{α : Type u} → Type u" },
expr := { pp? := .some "fun {α} => List α" } expr := { pp? := .some "fun {α} => List α" }

View File

@ -47,14 +47,15 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
let entries: List (String × String) := [ let entries: List (String × (List Name) × String) := [
("λ x: Nat × Bool => x.1", "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"), ("λ x: Nat × Bool => x.1", [], "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
("λ x: Array Nat => x.data", "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"), ("λ x: Array Nat => x.data", [], "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
-- This tests `autoBoundImplicit` ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"),
("λ {α : Sort (u + 1)} => List α", "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"), ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :implicit)"),
("(2: Nat) <= (5: Nat)", "((:c LE.le) (:mv _uniq.37) (:mv _uniq.38) ((:c OfNat.ofNat) (:mv _uniq.23) (:lit 2) (:mv _uniq.24)) ((:c OfNat.ofNat) (:mv _uniq.33) (:lit 5) (:mv _uniq.34)))"), ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.18) (:mv _uniq.19) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))"),
] ]
let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do entries.foldlM (λ suites (source, levels, target) =>
let termElabM := do
let env ← MonadEnv.getEnv let env ← MonadEnv.getEnv
let s ← match parseTerm env source with let s ← match parseTerm env source with
| .ok s => pure s | .ok s => pure s
@ -62,9 +63,10 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
let expr ← match (← elabTerm s) with let expr ← match (← elabTerm s) with
| .ok expr => pure expr | .ok expr => pure expr
| .error e => return elabFailure e | .error e => return elabFailure e
let test := LSpec.check source ((← serializeExpressionSexp expr) = target) return LSpec.check source ((← serializeExpressionSexp expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := defaultTermElabMContext)
runMetaMSeq env $ termElabM.run' (ctx := defaultTermElabMContext) return LSpec.TestSeq.append suites (← runMetaMSeq env metaM))
LSpec.TestSeq.done
def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
let entries: List (Expr × String) := [ let entries: List (Expr × String) := [