From 76639d026665ca99edf78502837074652caf19b0 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 24 Feb 2025 15:45:31 -0800 Subject: [PATCH 1/6] fix: Panic edge case for module name --- Pantograph/Environment.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index 6bd3f76..aa4dd03 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -24,8 +24,11 @@ def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[ @[export pantograph_environment_module_of_name] def module_of_name (env: Environment) (name: Name): Option Name := do - let moduleId ← env.getModuleIdxFor? name - return env.allImportedModuleNames.get! moduleId.toNat + let moduleId ← env.getModuleIdxFor? name + if h : moduleId.toNat < env.allImportedModuleNames.size then + return env.allImportedModuleNames.get moduleId.toNat h + else + .none def toCompactSymbolName (n: Name) (info: ConstantInfo): String := let pref := match info with -- 2.44.1 From 999bb146fab96d2f026fc92e54857d529aef3f29 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 1 Mar 2025 20:12:30 -0800 Subject: [PATCH 2/6] chore: Remove all unused auxiliary tactics --- Pantograph/Library.lean | 16 --- Pantograph/Tactic.lean | 3 - Pantograph/Tactic/Congruence.lean | 98 --------------- Pantograph/Tactic/MotivatedApply.lean | 106 ---------------- Pantograph/Tactic/NoConfuse.lean | 22 ---- Test/Main.lean | 3 - Test/Proofs.lean | 175 -------------------------- Test/Tactic.lean | 3 - Test/Tactic/Congruence.lean | 88 ------------- Test/Tactic/MotivatedApply.lean | 113 ----------------- Test/Tactic/NoConfuse.lean | 72 ----------- 11 files changed, 699 deletions(-) delete mode 100644 Pantograph/Tactic/Congruence.lean delete mode 100644 Pantograph/Tactic/MotivatedApply.lean delete mode 100644 Pantograph/Tactic/NoConfuse.lean delete mode 100644 Test/Tactic/Congruence.lean delete mode 100644 Test/Tactic/MotivatedApply.lean delete mode 100644 Test/Tactic/NoConfuse.lean diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index b5c3655..b060275 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -191,22 +191,6 @@ protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: runTermElabM do state.restoreElabM state.tryTacticM goal (Tactic.evalDefine binderName.toName expr) -@[export pantograph_goal_try_motivated_apply_m] -protected def GoalState.tryMotivatedApply (state: GoalState) (goal: MVarId) (recursor: String): - Elab.TermElabM TacticResult := do - state.restoreElabM - let recursor ← match (← parseTermM recursor) with - | .ok syn => pure syn - | .error error => return .parseError error - state.tryTacticM goal (tacticM := Tactic.evalMotivatedApply recursor) -@[export pantograph_goal_try_no_confuse_m] -protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: String): - Elab.TermElabM TacticResult := do - state.restoreElabM - let eq ← match (← parseTermM eq) with - | .ok syn => pure syn - | .error error => return .parseError error - state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq) @[export pantograph_goal_try_draft_m] protected def GoalState.tryDraft (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticResult := do let expr ← match (← parseTermM expr) with diff --git a/Pantograph/Tactic.lean b/Pantograph/Tactic.lean index 72902f4..442e7ea 100644 --- a/Pantograph/Tactic.lean +++ b/Pantograph/Tactic.lean @@ -1,5 +1,2 @@ import Pantograph.Tactic.Assign -import Pantograph.Tactic.Congruence -import Pantograph.Tactic.MotivatedApply -import Pantograph.Tactic.NoConfuse import Pantograph.Tactic.Prograde diff --git a/Pantograph/Tactic/Congruence.lean b/Pantograph/Tactic/Congruence.lean deleted file mode 100644 index 0f6d80d..0000000 --- a/Pantograph/Tactic/Congruence.lean +++ /dev/null @@ -1,98 +0,0 @@ -import Lean - -open Lean - -namespace Pantograph.Tactic - -def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do - mvarId.checkNotAssigned `Pantograph.Tactic.congruenceArg - let target ← mvarId.getType - let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq" - let userName := (← mvarId.getDecl).userName - - let u ← Meta.mkFreshLevelMVar - let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u) - (tag := userName ++ `α) - let f ← Meta.mkFreshExprSyntheticOpaqueMVar (.forallE .anonymous α β .default) - (tag := userName ++ `f) - let a₁ ← Meta.mkFreshExprSyntheticOpaqueMVar α - (tag := userName ++ `a₁) - let a₂ ← Meta.mkFreshExprSyntheticOpaqueMVar α - (tag := userName ++ `a₂) - let h ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq a₁ a₂) - (tag := userName ++ `h) - let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) target - let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType - (tag := userName ++ `conduit) - mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h) - let result := [α, a₁, a₂, f, h, conduit] - return result.map (·.mvarId!) - -def evalCongruenceArg: Elab.Tactic.TacticM Unit := do - let goal ← Elab.Tactic.getMainGoal - let nextGoals ← congruenceArg goal - Elab.Tactic.replaceMainGoal nextGoals - -def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do - mvarId.checkNotAssigned `Pantograph.Tactic.congruenceFun - let target ← mvarId.getType - let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq" - let userName := (← mvarId.getDecl).userName - let u ← Meta.mkFreshLevelMVar - let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u) - (tag := userName ++ `α) - let fType := .forallE .anonymous α β .default - let f₁ ← Meta.mkFreshExprSyntheticOpaqueMVar fType - (tag := userName ++ `f₁) - let f₂ ← Meta.mkFreshExprSyntheticOpaqueMVar fType - (tag := userName ++ `f₂) - let a ← Meta.mkFreshExprSyntheticOpaqueMVar α - (tag := userName ++ `a) - let h ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq f₁ f₂) - (tag := userName ++ `h) - let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) target - let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType - (tag := userName ++ `conduit) - mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a) - let result := [α, f₁, f₂, h, a, conduit] - return result.map (·.mvarId!) - -def evalCongruenceFun: Elab.Tactic.TacticM Unit := do - let goal ← Elab.Tactic.getMainGoal - let nextGoals ← congruenceFun goal - Elab.Tactic.replaceMainGoal nextGoals - -def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do - mvarId.checkNotAssigned `Pantograph.Tactic.congruence - let target ← mvarId.getType - let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq" - let userName := (← mvarId.getDecl).userName - let u ← Meta.mkFreshLevelMVar - let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u) - (tag := userName ++ `α) - let fType := .forallE .anonymous α β .default - let f₁ ← Meta.mkFreshExprSyntheticOpaqueMVar fType - (tag := userName ++ `f₁) - let f₂ ← Meta.mkFreshExprSyntheticOpaqueMVar fType - (tag := userName ++ `f₂) - let a₁ ← Meta.mkFreshExprSyntheticOpaqueMVar α - (tag := userName ++ `a₁) - let a₂ ← Meta.mkFreshExprSyntheticOpaqueMVar α - (tag := userName ++ `a₂) - let h₁ ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq f₁ f₂) - (tag := userName ++ `h₁) - let h₂ ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq a₁ a₂) - (tag := userName ++ `h₂) - let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) target - let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType - (tag := userName ++ `conduit) - mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂) - let result := [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit] - return result.map (·.mvarId!) - -def evalCongruence: Elab.Tactic.TacticM Unit := do - let goal ← Elab.Tactic.getMainGoal - let nextGoals ← congruence goal - Elab.Tactic.replaceMainGoal nextGoals - -end Pantograph.Tactic diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean deleted file mode 100644 index 993d287..0000000 --- a/Pantograph/Tactic/MotivatedApply.lean +++ /dev/null @@ -1,106 +0,0 @@ -import Lean - -open Lean - -namespace Pantograph.Tactic - -def getForallArgsBody: Expr → List Expr × Expr - | .forallE _ d b _ => - let (innerArgs, innerBody) := getForallArgsBody b - (d :: innerArgs, innerBody) - | e => ([], e) - -def replaceForallBody: Expr → Expr → Expr - | .forallE param domain body binderInfo, target => - let body := replaceForallBody body target - .forallE param domain body binderInfo - | _, target => target - -structure RecursorWithMotive where - args: List Expr - body: Expr - - -- .bvar index for the motive and major from the body - iMotive: Nat - -namespace RecursorWithMotive - -protected def nArgs (info: RecursorWithMotive): Nat := info.args.length - -protected def getMotiveType (info: RecursorWithMotive): Expr := - let level := info.nArgs - info.iMotive - 1 - let a := info.args.get! level - a - -protected def surrogateMotiveType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do - let motiveType := Expr.instantiateRev info.getMotiveType mvars - let resultantType ← Meta.inferType resultant - return replaceForallBody motiveType resultantType - -protected def conduitType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do - let motiveCall := Expr.instantiateRev info.body mvars - Meta.mkEq motiveCall resultant - -end RecursorWithMotive - -def getRecursorInformation (recursorType: Expr): Option RecursorWithMotive := do - let (args, body) := getForallArgsBody recursorType - if ¬ body.isApp then - .none - let iMotive ← match body.getAppFn with - | .bvar iMotive => pure iMotive - | _ => .none - return { - args, - body, - iMotive, - } - -def collectMotiveArguments (forallBody: Expr): SSet Nat := - match forallBody with - | .app (.bvar i) _ => SSet.empty.insert i - | _ => SSet.empty - -/-- Applies a symbol of the type `∀ (motive: α → Sort u) (a: α)..., (motive α)` -/ -def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.InductionSubgoal) := mvarId.withContext do - mvarId.checkNotAssigned `Pantograph.Tactic.motivatedApply - let recursorType ← Meta.inferType recursor - let resultant ← mvarId.getType - let tag ← mvarId.getTag - - let info ← match getRecursorInformation recursorType with - | .some info => pure info - | .none => throwError "Recursor return type does not correspond with the invocation of a motive: {← Meta.ppExpr recursorType}" - - let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do - if i ≥ info.nArgs then - return prev - else - let argType := info.args.get! i - -- If `argType` has motive references, its goal needs to be placed in it - let argType := argType.instantiateRev prev - let bvarIndex := info.nArgs - i - 1 - let argGoal ← if bvarIndex = info.iMotive then - let surrogateMotiveType ← info.surrogateMotiveType prev resultant - Meta.mkFreshExprSyntheticOpaqueMVar surrogateMotiveType (tag := tag ++ `motive) - else - Meta.mkFreshExprSyntheticOpaqueMVar argType (tag := .anonymous) - let prev := prev ++ [argGoal] - go (i + 1) prev - termination_by info.nArgs - i - let mut newMVars ← go 0 #[] - - -- Create the conduit type which proves the result of the motive is equal to the goal - let conduitType ← info.conduitType newMVars resultant - let goalConduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType (tag := `conduit) - mvarId.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars) - newMVars := newMVars ++ [goalConduit] - - return newMVars.map (λ mvar => { mvarId := mvar.mvarId!}) - -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.replaceMainGoal $ nextGoals.toList.map (·.mvarId) - -end Pantograph.Tactic diff --git a/Pantograph/Tactic/NoConfuse.lean b/Pantograph/Tactic/NoConfuse.lean deleted file mode 100644 index e9ff459..0000000 --- a/Pantograph/Tactic/NoConfuse.lean +++ /dev/null @@ -1,22 +0,0 @@ -import Lean - -open Lean - -namespace Pantograph.Tactic - -def noConfuse (mvarId: MVarId) (h: Expr): MetaM Unit := mvarId.withContext do - mvarId.checkNotAssigned `Pantograph.Tactic.noConfuse - let target ← mvarId.getType - let noConfusion ← Meta.mkNoConfusion (target := target) (h := h) - - unless ← Meta.isDefEq (← Meta.inferType noConfusion) target do - throwError "invalid noConfuse call: The resultant type {← Meta.ppExpr $ ← Meta.inferType noConfusion} cannot be unified with {← Meta.ppExpr target}" - mvarId.assign noConfusion - -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.replaceMainGoal [] - -end Pantograph.Tactic diff --git a/Test/Main.lean b/Test/Main.lean index 18dc9e3..e5cf285 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -54,9 +54,6 @@ def main (args: List String) := do ("Delate", Delate.suite env_default), ("Serial", Serial.suite env_default), ("Tactic/Assign", Tactic.Assign.suite env_default), - ("Tactic/Congruence", Tactic.Congruence.suite env_default), - ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default), - ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default), ("Tactic/Prograde", Tactic.Prograde.suite env_default), ] let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) [] diff --git a/Test/Proofs.lean b/Test/Proofs.lean index bf43bf6..ef8bc09 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -543,179 +543,6 @@ def test_calc: TestM Unit := do ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free buildGoal free target userName? -def test_nat_zero_add: TestM Unit := do - let state? ← startProof (.expr "∀ (n: Nat), n + 0 = n") - let state0 ← match state? with - | .some state => pure state - | .none => do - addTest $ assertUnreachable "Goal could not parse" - return () - let tactic := "intro n" - let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = - #[buildGoal [("n", "Nat")] "n + 0 = n"]) - let recursor := "@Nat.brecOn" - let state2 ← match ← state1.tryMotivatedApply (state1.get! 0) (recursor := recursor) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - let [mvarMotive, mvarMajor, mvarInduct, mvarConduit] := state2.goals | - fail "Incorrect number of goals" - let .num _ major := mvarMajor.name | fail "Incorrect form of mvar id" - addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) = - #[ - buildNamedGoal mvarMotive.name.toString [("n", "Nat")] "Nat → Prop" (.some "motive"), - buildNamedGoal mvarMajor.name.toString [("n", "Nat")] "Nat", - buildNamedGoal mvarInduct.name.toString [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t", - buildNamedGoal mvarConduit.name.toString [("n", "Nat")] s!"?motive ?m.{major} = (n + 0 = n)" (.some "conduit") - ]) - - let tactic := "exact n" - let state3b ← match ← state2.tacticOn (goalId := 1) (tactic := tactic) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check tactic ((← state3b.serializeGoals (options := ← read)).map (·.devolatilize) = - #[]) - let state2b ← match state3b.continue state2 with - | .ok state => pure state - | .error e => do - addTest $ assertUnreachable e - return () - let tactic := "exact (λ x => x + 0 = x)" - let state3c ← match ← state2b.tacticOn (goalId := 0) (tactic := tactic) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check tactic ((← state3c.serializeGoals (options := ← read)).map (·.devolatilize) = - #[]) - let state2c ← match state3c.continue state2b with - | .ok state => pure state - | .error e => do - addTest $ assertUnreachable e - return () - let tactic := "intro t h" - let state3 ← match ← state2c.tacticOn (goalId := 0) (tactic := tactic) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check tactic ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) = - #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"]) - - let tactic := "simp" - let state3d ← match ← state3.tacticOn (goalId := 0) (tactic := tactic) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - let state2d ← match state3d.continue state2c with - | .ok state => pure state - | .error e => do - addTest $ assertUnreachable e - return () - let tactic := "rfl" - let stateF ← match ← state2d.tacticOn (goalId := 0) (tactic := tactic) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check tactic ((← stateF.serializeGoals (options := ← read)) = - #[]) - - let expr := stateF.mctx.eAssignment.find! stateF.root - let (expr, _) := instantiateMVarsCore (mctx := stateF.mctx) (e := expr) - addTest $ LSpec.check "(F root)" stateF.rootExpr?.isSome - -def test_nat_zero_add_alt: TestM Unit := do - let state? ← startProof (.expr "∀ (n: Nat), n + 0 = n") - let state0 ← match state? with - | .some state => pure state - | .none => do - addTest $ assertUnreachable "Goal could not parse" - return () - let tactic := "intro n" - let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = - #[buildGoal [("n", "Nat")] "n + 0 = n"]) - let recursor := "@Nat.brecOn" - let state2 ← match ← state1.tryMotivatedApply (state1.get! 0) (recursor := recursor) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - let [mvarMotive, mvarMajor, mvarInduct, mvarConduit] := state2.goals | - fail "Incorrect number of goals" - let .num _ major := mvarMajor.name | fail "Incorrect form of mvar id" - addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) = - #[ - buildNamedGoal mvarMotive.name.toString [("n", "Nat")] "Nat → Prop" (.some "motive"), - buildNamedGoal mvarMajor.name.toString [("n", "Nat")] "Nat", - buildNamedGoal mvarInduct.name.toString [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t", - buildNamedGoal mvarConduit.name.toString [("n", "Nat")] s!"?motive ?m.{major} = (n + 0 = n)" (.some "conduit") - ]) - - let tactic := "intro x" - let state3m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check tactic ((← state3m.serializeGoals (options := ← read)).map (·.devolatilize) = - #[buildGoal [("n", "Nat"), ("x", "Nat")] "Prop" (.some "motive")]) - let tactic := "apply Eq" - let state3m2 ← match ← state3m.tacticOn (goalId := 0) (tactic := tactic) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - let [eqL, eqR, eqT] := state3m2.goals | fail "Incorrect number of goals" - let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict" - let state2b ← match state3m2.resume [conduit] with - | .ok state => pure state - | .error e => do - addTest $ assertUnreachable e - return () - - let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))" - let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))" - let fvN ← state2b.withContext conduit do - let lctx ← getLCtx - pure $ lctx.getFVarIds.get! 0 |>.name - let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))" - let substOf (mvarId: MVarId) := s!"(:subst (:mv {mvarId.name}) (:fv {fvN}) (:mv {mvarMajor}))" - let .num _ nL := eqL.name | fail "Incorrect form of mvar id" - let .num _ nR := eqR.name | fail "Incorrect form of mvar id" - let nL' := nL + 4 - let nR' := nR + 5 - addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) = - #[ - { - name := mvarConduit.name.toString, - userName? := .some "conduit", - target := { - pp? := .some s!"(?m.{nL'} ?m.{major} = ?m.{nR'} ?m.{major}) = (n + 0 = n)", - sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})", - }, - vars := #[{ - name := fvN.toString, - userName := "n", - type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" }, - }], - } - ]) - def test_tactic_failure_unresolved_goals : TestM Unit := do let state? ← startProof (.expr "∀ (p : Nat → Prop), ∃ (x : Nat), p (0 + x + 0)") let state0 ← match state? with @@ -778,8 +605,6 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("Or.comm", test_or_comm), ("conv", test_conv), ("calc", test_calc), - ("Nat.zero_add", test_nat_zero_add), - ("Nat.zero_add alt", test_nat_zero_add_alt), ("tactic failure with unresolved goals", test_tactic_failure_unresolved_goals), ("tactic failure with synthesize placeholder", test_tactic_failure_synthesize_placeholder), ] diff --git a/Test/Tactic.lean b/Test/Tactic.lean index 6b3e8fd..217edb6 100644 --- a/Test/Tactic.lean +++ b/Test/Tactic.lean @@ -1,5 +1,2 @@ import Test.Tactic.Assign -import Test.Tactic.Congruence -import Test.Tactic.MotivatedApply -import Test.Tactic.NoConfuse import Test.Tactic.Prograde diff --git a/Test/Tactic/Congruence.lean b/Test/Tactic/Congruence.lean deleted file mode 100644 index e861b2f..0000000 --- a/Test/Tactic/Congruence.lean +++ /dev/null @@ -1,88 +0,0 @@ -import LSpec -import Lean -import Test.Common - -open Lean -open Pantograph - -namespace Pantograph.Test.Tactic.Congruence - -def test_congr_arg_list : TestT Elab.TermElabM Unit := do - let expr := "λ {α} (l1 l2 : List α) (h: l1 = l2) => l1.reverse = l2.reverse" - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId! - addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = - [ - (`α, "Sort ?u.30"), - (`a₁, "?α"), - (`a₂, "?α"), - (`f, "?α → List α"), - (`h, "?a₁ = ?a₂"), - (`conduit, "(?f ?a₁ = ?f ?a₂) = (l1.reverse = l2.reverse)"), - ]) - let f := newGoals.get! 3 - let h := newGoals.get! 4 - let c := newGoals.get! 5 - let results ← Meta.withAssignableSyntheticOpaque do f.apply (← parseSentence "List.reverse") - addTest $ LSpec.check "apply" (results.length = 0) - addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂") - addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(List.reverse ?a₁ = List.reverse ?a₂) = (l1.reverse = l2.reverse)") -def test_congr_arg : TestT Elab.TermElabM Unit := do - let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m" - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId! - addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = - [ - (`α, "Sort ?u.73"), - (`a₁, "?α"), - (`a₂, "?α"), - (`f, "?α → Nat"), - (`h, "?a₁ = ?a₂"), - (`conduit, "(?f ?a₁ = ?f ?a₂) = (n * n = m * m)"), - ]) -def test_congr_fun : TestT Elab.TermElabM Unit := do - let expr := "λ (n m: Nat) => (n + m) + (n + m) = (n + m) * 2" - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let newGoals ← runTacticOnMVar Tactic.evalCongruenceFun target.mvarId! - addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = - [ - (`α, "Sort ?u.165"), - (`f₁, "?α → Nat"), - (`f₂, "?α → Nat"), - (`h, "?f₁ = ?f₂"), - (`a, "?α"), - (`conduit, "(?f₁ ?a = ?f₂ ?a) = (n + m + (n + m) = (n + m) * 2)"), - ]) -def test_congr : TestT Elab.TermElabM Unit := do - let expr := "λ (a b: Nat) => a = b" - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let newGoals ← runTacticOnMVar Tactic.evalCongruence target.mvarId! - addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = - [ - (`α, "Sort ?u.10"), - (`f₁, "?α → Nat"), - (`f₂, "?α → Nat"), - (`a₁, "?α"), - (`a₂, "?α"), - (`h₁, "?f₁ = ?f₂"), - (`h₂, "?a₁ = ?a₂"), - (`conduit, "(?f₁ ?a₁ = ?f₂ ?a₂) = (a = b)"), - ]) - -def suite (env: Environment): List (String × IO LSpec.TestSeq) := - [ - ("congrArg List.reverse", test_congr_arg_list), - ("congrArg", test_congr_arg), - ("congrFun", test_congr_fun), - ("congr", test_congr), - ] |>.map (λ (name, t) => (name, runTestTermElabM env t)) - -end Pantograph.Test.Tactic.Congruence diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean deleted file mode 100644 index 2da643e..0000000 --- a/Test/Tactic/MotivatedApply.lean +++ /dev/null @@ -1,113 +0,0 @@ -import LSpec -import Lean -import Test.Common - -open Lean -open Pantograph - -namespace Pantograph.Test.Tactic.MotivatedApply - -def test_type_extract : TestT Elab.TermElabM Unit := do - let recursor ← parseSentence "@Nat.brecOn" - let recursorType ← Meta.inferType recursor - addTest $ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" = - (← exprToStr recursorType)) - let info ← match Tactic.getRecursorInformation recursorType with - | .some info => pure info - | .none => throwError "Failed to extract recursor info" - addTest $ LSpec.check "iMotive" (info.iMotive = 2) - let motiveType := info.getMotiveType - addTest $ LSpec.check "motiveType" ("Nat → Sort ?u.1" = - (← exprToStr motiveType)) - -def test_nat_brec_on : TestT Elab.TermElabM Unit := do - let expr := "λ (n t: Nat) => n + 0 = n" - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let recursor ← match Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `term) - (input := "@Nat.brecOn") - (fileName := ← getFileName) with - | .ok syn => pure syn - | .error error => throwError "Failed to parse: {error}" - -- Apply the tactic - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let tactic := Tactic.evalMotivatedApply recursor - let newGoals ← runTacticOnMVar tactic target.mvarId! - let test := LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = - [ - "Nat → Prop", - "Nat", - "∀ (t : Nat), Nat.below t → ?motive t", - "?motive ?m.74 = (n + 0 = n)", - ]) - addTest test - -def test_list_brec_on : TestT Elab.TermElabM Unit := do - let expr := "λ {α : Type} (l: List α) => l ++ [] = [] ++ l" - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let recursor ← match Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `term) - (input := "@List.brecOn") - (fileName := ← getFileName) with - | .ok syn => pure syn - | .error error => throwError "Failed to parse: {error}" - -- Apply the tactic - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let tactic := Tactic.evalMotivatedApply recursor - let newGoals ← runTacticOnMVar tactic target.mvarId! - addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = - [ - "Type ?u.90", - "List ?m.92 → Prop", - "List ?m.92", - "∀ (t : List ?m.92), List.below t → ?motive t", - "?motive ?m.94 = (l ++ [] = [] ++ l)", - ]) - -def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do - let expr := "λ (n t: Nat) => n + 0 = n" - let recursor ← match Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `term) - (input := "@Nat.brecOn") - (fileName := ← getFileName) with - | .ok syn => pure syn - | .error error => throwError "Failed to parse: {error}" - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - -- Apply the tactic - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let tactic := Tactic.evalMotivatedApply recursor - let newGoals ← runTacticOnMVar tactic target.mvarId! - let majorId := 74 - addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = - [ - "Nat → Prop", - "Nat", - "∀ (t : Nat), Nat.below t → ?motive t", - s!"?motive ?m.{majorId} = (n + 0 = n)", - ])) - let [motive, major, step, conduit] := newGoals | panic! "Incorrect goal number" - addTest $ (LSpec.check "goal name" (major.name.toString = s!"_uniq.{majorId}")) - - -- Assign motive to `λ x => x + _` - let motive_assign ← parseSentence "λ (x: Nat) => @Nat.add x + 0 = _" - motive.assign motive_assign - - addTest $ ← conduit.withContext do - let t := toString (← Meta.ppExpr $ ← conduit.getType) - return LSpec.check "conduit" (t = s!"(Nat.add ?m.{majorId} + 0 = ?m.149 ?m.{majorId}) = (n + 0 = n)") - -def suite (env: Environment): List (String × IO LSpec.TestSeq) := - [ - ("type_extract", test_type_extract), - ("Nat.brecOn", test_nat_brec_on), - ("List.brecOn", test_list_brec_on), - ("Nat.brecOn partial motive instantiation", test_partial_motive_instantiation), - ] |>.map (λ (name, t) => (name, runTestTermElabM env t)) - -end Pantograph.Test.Tactic.MotivatedApply diff --git a/Test/Tactic/NoConfuse.lean b/Test/Tactic/NoConfuse.lean deleted file mode 100644 index 93f0606..0000000 --- a/Test/Tactic/NoConfuse.lean +++ /dev/null @@ -1,72 +0,0 @@ -import LSpec -import Lean -import Test.Common - -open Lean -open Pantograph - -namespace Pantograph.Test.Tactic.NoConfuse - -def test_nat : TestT Elab.TermElabM Unit := do - let expr := "λ (n: Nat) (h: 0 = n + 1) => False" - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let recursor ← match Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `term) - (input := "h") - (fileName := ← getFileName) with - | .ok syn => pure syn - | .error error => throwError "Failed to parse: {error}" - -- Apply the tactic - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let tactic := Tactic.evalNoConfuse recursor - let newGoals ← runTacticOnMVar tactic target.mvarId! - addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = []) - -def test_nat_fail : TestT Elab.TermElabM Unit := do - let expr := "λ (n: Nat) (h: n = n) => False" - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let recursor ← match Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `term) - (input := "h") - (fileName := ← getFileName) with - | .ok syn => pure syn - | .error error => throwError "Failed to parse: {error}" - -- Apply the tactic - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - try - let tactic := Tactic.evalNoConfuse recursor - let _ ← runTacticOnMVar tactic target.mvarId! - addTest $ assertUnreachable "Tactic should fail" - catch _ => - addTest $ LSpec.check "Tactic should fail" true - -def test_list : TestT Elab.TermElabM Unit := do - let expr := "λ (l: List Nat) (h: [] = 1 :: l) => False" - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let recursor ← match Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `term) - (input := "h") - (fileName := ← getFileName) with - | .ok syn => pure syn - | .error error => throwError "Failed to parse: {error}" - -- Apply the tactic - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let tactic := Tactic.evalNoConfuse recursor - let newGoals ← runTacticOnMVar tactic target.mvarId! - addTest $ LSpec.check "goals" - ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = []) - -def suite (env: Environment): List (String × IO LSpec.TestSeq) := - [ - ("Nat", test_nat), - ("Nat fail", test_nat_fail), - ("List", test_list), - ] |>.map (λ (name, t) => (name, runTestTermElabM env t)) - -end Pantograph.Test.Tactic.NoConfuse -- 2.44.1 From 39ec79e6bb11a49d6f0137385e6a70969d3c55c5 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 8 Mar 2025 21:07:15 -0800 Subject: [PATCH 3/6] feat: Monad lifting in `GoalState.withContext` --- Pantograph/Goal.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index aaff02d..43f3e85 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -74,13 +74,14 @@ protected def GoalState.metaState (state: GoalState): Meta.State := protected def GoalState.coreState (state: GoalState): Core.SavedState := state.savedState.term.meta.core -protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do +protected def GoalState.withContext' (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do mvarId.withContext m |>.run' (← read) state.metaState - +protected def GoalState.withContext { m } [MonadControlT MetaM m] [Monad m] (state: GoalState) (mvarId: MVarId) : m α → m α := + Meta.mapMetaM <| state.withContext' mvarId protected def GoalState.withParentContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α := - Meta.mapMetaM <| state.withContext state.parentMVar?.get! + Meta.mapMetaM <| state.withContext' state.parentMVar?.get! protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α := - Meta.mapMetaM <| state.withContext state.root + Meta.mapMetaM <| state.withContext' state.root private def GoalState.mvars (state: GoalState): SSet MVarId := state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k -- 2.44.1 From 5a690c4421f650d1a6fb85f8bc9c28efc7579cb1 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 8 Mar 2025 21:11:34 -0800 Subject: [PATCH 4/6] chore: Use `fetchGit` for `LSpec` input --- flake.nix | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/flake.nix b/flake.nix index af6e4fb..54552c5 100644 --- a/flake.nix +++ b/flake.nix @@ -2,12 +2,11 @@ description = "Pantograph"; inputs = { - nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05"; + nixpkgs.url = "github:nixos/nixpkgs/nixos-24.11"; flake-parts.url = "github:hercules-ci/flake-parts"; - lean4-nix.url = "github:lenianiva/lean4-nix"; - lspec = { - url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab"; - flake = false; + lean4-nix = { + url = "github:lenianiva/lean4-nix"; + inputs.nixpkgs.follows = "nixpkgs"; }; }; @@ -16,7 +15,6 @@ nixpkgs, flake-parts, lean4-nix, - lspec, ... }: flake-parts.lib.mkFlake {inherit inputs;} { @@ -39,8 +37,11 @@ }; lspecLib = pkgs.lean.buildLeanPackage { name = "LSpec"; - roots = ["Main" "LSpec"]; - src = "${lspec}"; + roots = ["LSpec"]; + src = builtins.fetchGit { + url = "https://github.com/argumentcomputer/LSpec.git"; + rev = "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec"; + }; }; project = pkgs.lean.buildLeanPackage { name = "Pantograph"; -- 2.44.1 From 92515ea0f2ba2f38f13779545c646445af0803a6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 8 Mar 2025 21:11:59 -0800 Subject: [PATCH 5/6] fix: Update flake lock --- flake.lock | 75 +++++++++++++++++------------------------------------- 1 file changed, 23 insertions(+), 52 deletions(-) diff --git a/flake.lock b/flake.lock index 4a17f3d..dedddc8 100644 --- a/flake.lock +++ b/flake.lock @@ -5,11 +5,11 @@ "nixpkgs-lib": "nixpkgs-lib" }, "locked": { - "lastModified": 1730504689, - "narHash": "sha256-hgmguH29K2fvs9szpq2r3pz2/8cJd2LPS+b4tfNFCwE=", + "lastModified": 1741352980, + "narHash": "sha256-+u2UunDA4Cl5Fci3m7S643HzKmIDAe+fiXrLqYsR2fs=", "owner": "hercules-ci", "repo": "flake-parts", - "rev": "506278e768c2a08bec68eb62932193e341f55c90", + "rev": "f4330d22f1c5d2ba72d3d22df5597d123fdb60a9", "type": "github" }, "original": { @@ -39,14 +39,16 @@ "lean4-nix": { "inputs": { "flake-parts": "flake-parts_2", - "nixpkgs": "nixpkgs" + "nixpkgs": [ + "nixpkgs" + ] }, "locked": { - "lastModified": 1736388194, - "narHash": "sha256-ymSrd/A8Pw+9FzbxUbR7CkFHLJK1b4SnFFWg/1e0JeE=", + "lastModified": 1741472588, + "narHash": "sha256-XnMeMZKuspEphP+fEq4soc3PY7Nz+gsMPjlsXbobyrA=", "owner": "lenianiva", "repo": "lean4-nix", - "rev": "90f496bc0694fb97bdfa6adedfc2dc2c841a4cf2", + "rev": "cffeb67d58e02b50ccb9acd51b0212dc653ed6ce", "type": "github" }, "original": { @@ -55,49 +57,35 @@ "type": "github" } }, - "lspec": { - "flake": false, - "locked": { - "lastModified": 1728279187, - "narHash": "sha256-ZMqbvCqR/gHXRuIkuo7b0Yp9N1vOQR7xnrcy/SeIBoQ=", - "owner": "argumentcomputer", - "repo": "LSpec", - "rev": "504a8cecf8da601b9466ac727aebb6b511aae4ab", - "type": "github" - }, - "original": { - "owner": "argumentcomputer", - "ref": "504a8cecf8da601b9466ac727aebb6b511aae4ab", - "repo": "LSpec", - "type": "github" - } - }, "nixpkgs": { "locked": { - "lastModified": 1728500571, - "narHash": "sha256-dOymOQ3AfNI4Z337yEwHGohrVQb4yPODCW9MDUyAc4w=", + "lastModified": 1741332913, + "narHash": "sha256-ri1e8ZliWS3Jnp9yqpKApHaOo7KBN33W8ECAKA4teAQ=", "owner": "nixos", "repo": "nixpkgs", - "rev": "d51c28603def282a24fa034bcb007e2bcb5b5dd0", + "rev": "20755fa05115c84be00b04690630cb38f0a203ad", "type": "github" }, "original": { "owner": "nixos", - "ref": "nixos-24.05", + "ref": "nixos-24.11", "repo": "nixpkgs", "type": "github" } }, "nixpkgs-lib": { "locked": { - "lastModified": 1730504152, - "narHash": "sha256-lXvH/vOfb4aGYyvFmZK/HlsNsr/0CVWlwYvo2rxJk3s=", - "type": "tarball", - "url": "https://github.com/NixOS/nixpkgs/archive/cc2f28000298e1269cea6612cd06ec9979dd5d7f.tar.gz" + "lastModified": 1740877520, + "narHash": "sha256-oiwv/ZK/2FhGxrCkQkB83i7GnWXPPLzoqFHpDD3uYpk=", + "owner": "nix-community", + "repo": "nixpkgs.lib", + "rev": "147dee35aab2193b174e4c0868bd80ead5ce755c", + "type": "github" }, "original": { - "type": "tarball", - "url": "https://github.com/NixOS/nixpkgs/archive/cc2f28000298e1269cea6612cd06ec9979dd5d7f.tar.gz" + "owner": "nix-community", + "repo": "nixpkgs.lib", + "type": "github" } }, "nixpkgs-lib_2": { @@ -112,28 +100,11 @@ "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz" } }, - "nixpkgs_2": { - "locked": { - "lastModified": 1731386116, - "narHash": "sha256-lKA770aUmjPHdTaJWnP3yQ9OI1TigenUqVC3wweqZuI=", - "owner": "nixos", - "repo": "nixpkgs", - "rev": "689fed12a013f56d4c4d3f612489634267d86529", - "type": "github" - }, - "original": { - "owner": "nixos", - "ref": "nixos-24.05", - "repo": "nixpkgs", - "type": "github" - } - }, "root": { "inputs": { "flake-parts": "flake-parts", "lean4-nix": "lean4-nix", - "lspec": "lspec", - "nixpkgs": "nixpkgs_2" + "nixpkgs": "nixpkgs" } } }, -- 2.44.1 From 9cf071eefe73c15418523575c028c7b4c0a8e2bf Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 8 Mar 2025 21:16:47 -0800 Subject: [PATCH 6/6] chore: Read manifest for LSpec version --- flake.nix | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/flake.nix b/flake.nix index 54552c5..424f863 100644 --- a/flake.nix +++ b/flake.nix @@ -35,13 +35,12 @@ inherit system; overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)]; }; + manifest = pkgs.lib.importJSON ./lake-manifest.json; + manifest-lspec = builtins.head manifest; lspecLib = pkgs.lean.buildLeanPackage { name = "LSpec"; roots = ["LSpec"]; - src = builtins.fetchGit { - url = "https://github.com/argumentcomputer/LSpec.git"; - rev = "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec"; - }; + src = builtins.fetchGit { inherit (manifest-lspec) url rev; }; }; project = pkgs.lean.buildLeanPackage { name = "Pantograph"; -- 2.44.1