fix: Bindings in prograde tactics #90

Merged
aniva merged 2 commits from bug/hidden-fvar-in-define into dev 2024-09-03 18:15:58 -07:00
8 changed files with 71 additions and 29 deletions

View File

@ -247,7 +247,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
-- See Lean.Elab.Tactic.Conv.convTarget
let convMVar ← Elab.Tactic.withMainContext do
let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
Elab.Tactic.setGoals [newGoal.mvarId!]
Elab.Tactic.replaceMainGoal [newGoal.mvarId!]
pure rhs.mvarId!
return (← MonadBacktrack.saveState, convMVar)
try

View File

@ -25,7 +25,7 @@ def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
(tagSuffix := .anonymous )
(allowNaturalHoles := true)
goal.assign expr
Elab.Tactic.setGoals nextGoals
Elab.Tactic.replaceMainGoal nextGoals
end Pantograph.Tactic

View File

@ -31,7 +31,7 @@ def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
def evalCongruenceArg: Elab.Tactic.TacticM Unit := do
let goal ← Elab.Tactic.getMainGoal
let nextGoals ← congruenceArg goal
Elab.Tactic.setGoals nextGoals
Elab.Tactic.replaceMainGoal nextGoals
def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
mvarId.checkNotAssigned `Pantograph.Tactic.congruenceFun
@ -60,7 +60,7 @@ def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
def evalCongruenceFun: Elab.Tactic.TacticM Unit := do
let goal ← Elab.Tactic.getMainGoal
let nextGoals ← congruenceFun goal
Elab.Tactic.setGoals nextGoals
Elab.Tactic.replaceMainGoal nextGoals
def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
mvarId.checkNotAssigned `Pantograph.Tactic.congruence
@ -93,6 +93,6 @@ def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
def evalCongruence: Elab.Tactic.TacticM Unit := do
let goal ← Elab.Tactic.getMainGoal
let nextGoals ← congruence goal
Elab.Tactic.setGoals nextGoals
Elab.Tactic.replaceMainGoal nextGoals
end Pantograph.Tactic

View File

@ -100,6 +100,6 @@ def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.Inducti
def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
let recursor ← Elab.Term.elabTerm (stx := stx) .none
let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor
Elab.Tactic.setGoals $ nextGoals.toList.map (·.mvarId)
Elab.Tactic.replaceMainGoal $ nextGoals.toList.map (·.mvarId)
end Pantograph.Tactic

View File

@ -17,6 +17,6 @@ def evalNoConfuse: Elab.Tactic.Tactic := λ stx => do
let goal ← Elab.Tactic.getMainGoal
let h ← goal.withContext $ Elab.Term.elabTerm (stx := stx) .none
noConfuse goal h
Elab.Tactic.setGoals []
Elab.Tactic.replaceMainGoal []
end Pantograph.Tactic

View File

@ -5,22 +5,25 @@ open Lean
namespace Pantograph.Tactic
private def mkUpstreamMVar (goal: MVarId) : MetaM Expr := do
Meta.mkFreshExprSyntheticOpaqueMVar (← goal.getType) (tag := ← goal.getTag)
/-- Introduces a fvar to the current mvar -/
def define (mvarId: MVarId) (binderName: Name) (expr: Expr): MetaM (FVarId × MVarId) := mvarId.withContext do
mvarId.checkNotAssigned `Pantograph.Tactic.define
let type ← Meta.inferType expr
Meta.withLetDecl binderName type expr λ fvar => do
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
(← mvarId.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
mvarId.assign mvarUpstream
let mvarUpstream ← mkUpstreamMVar mvarId
mvarId.assign $ ← Meta.mkLetFVars #[fvar] mvarUpstream
pure (fvar.fvarId!, mvarUpstream.mvarId!)
def evalDefine (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
let goal ← Elab.Tactic.getMainGoal
let expr ← goal.withContext $ Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
let (_, mvarId) ← define goal binderName expr
Elab.Tactic.setGoals [mvarId]
Elab.Tactic.replaceMainGoal [mvarId]
structure BranchResult where
fvarId?: Option FVarId := .none
@ -39,10 +42,9 @@ def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResul
let mvarUpstream ←
withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
Meta.withNewLocalInstances #[.fvar fvarId] 0 do
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
(← mvarId.getType) (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag)
let mvarUpstream ← mkUpstreamMVar mvarId
--let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
mvarId.assign mvarUpstream
mvarId.assign $ ← Meta.mkLambdaFVars #[.fvar fvarId] mvarUpstream
pure mvarUpstream
return {
@ -57,7 +59,7 @@ def evalHave (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
let type ← Elab.Term.elabType (stx := type)
let result ← «have» goal binderName type
pure [result.branch, result.main]
Elab.Tactic.setGoals nextGoals
Elab.Tactic.replaceMainGoal nextGoals
def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do
mvarId.checkNotAssigned `Pantograph.Tactic.let
@ -68,9 +70,8 @@ def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult
assert! ¬ type.hasLooseBVars
let mvarUpstream ← Meta.withLetDecl binderName type mvarBranch $ λ fvar => do
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
(type := ← mvarId.getType) (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag)
mvarId.assign $ .letE binderName type fvar mvarUpstream (nonDep := false)
let mvarUpstream ← mkUpstreamMVar mvarId
mvarId.assign $ ← Meta.mkLetFVars #[fvar] mvarUpstream
pure mvarUpstream
return {
@ -82,6 +83,6 @@ def evalLet (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
let goal ← Elab.Tactic.getMainGoal
let type ← goal.withContext $ Elab.Term.elabType (stx := type)
let result ← «let» goal binderName type
Elab.Tactic.setGoals [result.branch, result.main]
Elab.Tactic.replaceMainGoal [result.branch, result.main]
end Pantograph.Tactic

View File

@ -94,15 +94,22 @@ def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq)
def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
def strToTermSyntax [Monad m] [MonadEnv m] (s: String): m Syntax := do
let .ok stx := Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `term)
(input := s)
(fileName := filename) | panic! s!"Failed to parse {s}"
return stx
def parseSentence (s: String): Elab.TermElabM Expr := do
let recursor ← match Parser.runParserCategory
let stx ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `term)
(input := s)
(fileName := filename) with
| .ok syn => pure syn
| .error error => throwError "Failed to parse: {error}"
Elab.Term.elabTerm (stx := recursor) .none
Elab.Term.elabTerm (stx := stx) .none
def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do
let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }

View File

@ -7,7 +7,7 @@ open Pantograph
namespace Pantograph.Test.Tactic.Prograde
def test_eval : TestT Elab.TermElabM Unit := do
def test_define : TestT Elab.TermElabM Unit := do
let expr := "forall (p q : Prop) (h: p), And (Or p q) (Or p q)"
let expr ← parseSentence expr
Meta.forallTelescope expr $ λ _ body => do
@ -48,9 +48,10 @@ def test_eval : TestT Elab.TermElabM Unit := do
],
target,
})
addTest $ LSpec.test "assign" ((← getExprMVarAssignment? goal.mvarId!) == .some (.mvar newGoal))
let .some e ← getExprMVarAssignment? goal.mvarId! | panic! "Tactic must assign"
addTest $ LSpec.test "assign" e.isLet
def test_proof_eval : TestT Elab.TermElabM Unit := do
def test_define_proof : TestT Elab.TermElabM Unit := do
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p q) (p q))"
let state0 ← GoalState.create rootExpr
let tactic := "intro p q h"
@ -103,7 +104,38 @@ def test_proof_eval : TestT Elab.TermElabM Unit := do
addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
def test_proof_have : TestT Elab.TermElabM Unit := do
def fun_define_root_expr: ∀ (p: Prop), PProd (Nat → p) Unit → p := by
intro p x
apply x.fst
exact 5
def test_define_root_expr : TestT Elab.TermElabM Unit := do
--let rootExpr ← parseSentence "Nat"
--let state0 ← GoalState.create rootExpr
--let .success state1 ← state0.tryTactic (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5"
--let .some rootExpr := state1.rootExpr? | addTest $ assertUnreachable "Root expr"
--addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "5")
let rootExpr ← parseSentence "∀ (p: Prop), PProd (Nat → p) Unit → p"
let state0 ← GoalState.create rootExpr
let tactic := "intro p x"
let .success state1 ← state0.tryTactic (goalId := 0) tactic | addTest $ assertUnreachable tactic
let binderName := `binder
let value := "x.fst"
let expr ← state1.goals[0]!.withContext $ strToTermSyntax value
let tacticM := Tactic.evalDefine binderName expr
let .success state2 ← state1.tryTacticM (goalId := 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}"
let tactic := s!"apply {binderName}"
let .success state3 ← state2.tryTactic (goalId := 0) tactic | addTest $ assertUnreachable tactic
let tactic := s!"exact 5"
let .success state4 ← state3.tryTactic (goalId := 0) tactic | addTest $ assertUnreachable tactic
let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n let binder := x.fst;\n binder 5")
--set_option pp.all true
--#check @PSigma (α := Prop) (β := λ (p: Prop) => p)
--def test_define_root_expr : TestT Elab.TermElabM Unit := do
def test_have_proof : TestT Elab.TermElabM Unit := do
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p q) (p q))"
let state0 ← GoalState.create rootExpr
let tactic := "intro p q h"
@ -160,7 +192,8 @@ def test_proof_have : TestT Elab.TermElabM Unit := do
addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals).map (·.devolatilize) =
#[])
addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome
let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p q h y => Or.inl y")
def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p q) (p q))"
@ -256,9 +289,10 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[
("eval", test_eval),
("Proof eval", test_proof_eval),
("Proof have", test_proof_have),
("define", test_define),
("define proof", test_define_proof),
("define root expr", test_define_root_expr),
("have proof", test_have_proof),
("let via assign", test_let false),
("let via tryLet", test_let true),
] |>.map (λ (name, t) => (name, runTestTermElabM env t))