From 8d2cd6dfc737a2ddcd6e89523e9a96f6d547ff7a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 3 Sep 2024 14:15:52 -0700 Subject: [PATCH 1/2] fix: Bindings in prograde tactics --- Pantograph/Tactic/Prograde.lean | 25 +++++++++-------- Test/Common.lean | 11 ++++++-- Test/Tactic/Prograde.lean | 50 +++++++++++++++++++++++++++------ 3 files changed, 64 insertions(+), 22 deletions(-) diff --git a/Pantograph/Tactic/Prograde.lean b/Pantograph/Tactic/Prograde.lean index 58c6050..0b4719f 100644 --- a/Pantograph/Tactic/Prograde.lean +++ b/Pantograph/Tactic/Prograde.lean @@ -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 diff --git a/Test/Common.lean b/Test/Common.lean index e572b72..83f2e7b 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -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] } diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean index dd194e7..22b342e 100644 --- a/Test/Tactic/Prograde.lean +++ b/Test/Tactic/Prograde.lean @@ -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)) -- 2.44.1 From f8df2599f99b1b77816299ebdeecbff9c5758339 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 3 Sep 2024 14:18:47 -0700 Subject: [PATCH 2/2] fix: Use `replaceMainGoal` instead of `setGoals` --- Pantograph/Goal.lean | 2 +- Pantograph/Tactic/Assign.lean | 2 +- Pantograph/Tactic/Congruence.lean | 6 +++--- Pantograph/Tactic/MotivatedApply.lean | 2 +- Pantograph/Tactic/NoConfuse.lean | 2 +- 5 files changed, 7 insertions(+), 7 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 9be5164..d92a807 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -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 diff --git a/Pantograph/Tactic/Assign.lean b/Pantograph/Tactic/Assign.lean index acf5d16..8a5b998 100644 --- a/Pantograph/Tactic/Assign.lean +++ b/Pantograph/Tactic/Assign.lean @@ -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 diff --git a/Pantograph/Tactic/Congruence.lean b/Pantograph/Tactic/Congruence.lean index 2ff23d2..dfb329d 100644 --- a/Pantograph/Tactic/Congruence.lean +++ b/Pantograph/Tactic/Congruence.lean @@ -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 diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean index 99e499d..2c52f12 100644 --- a/Pantograph/Tactic/MotivatedApply.lean +++ b/Pantograph/Tactic/MotivatedApply.lean @@ -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 diff --git a/Pantograph/Tactic/NoConfuse.lean b/Pantograph/Tactic/NoConfuse.lean index f4ce78f..e9ff459 100644 --- a/Pantograph/Tactic/NoConfuse.lean +++ b/Pantograph/Tactic/NoConfuse.lean @@ -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 -- 2.44.1