From 036fab0ad6a5e137059c634e9931ea7e1724c060 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 11 Apr 2024 16:11:06 -0700 Subject: [PATCH 1/4] fix: Prevent incorrect inheritance of calc rhs --- Pantograph/Goal.lean | 10 ++++++++-- Test/Proofs.lean | 3 +++ 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index fbb850a..75dc3f3 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -325,6 +325,11 @@ protected def GoalState.convExit (state: GoalState): catch exception => return .failure #[← exception.toMessageData.toString] +protected def GoalState.calcPrevRhsOf? (state: GoalState) (goalId: Nat) := + if goalId == 1 then + state.calcPrevRhs? + else + .none protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): Elab.TermElabM TacticResult := do state.restoreElabM @@ -340,20 +345,21 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): (fileName := filename) with | .ok syn => pure syn | .error error => return .parseError error + let calcPrevRhs? := state.calcPrevRhsOf? goalId try goal.withContext do let target ← instantiateMVars (← goal.getDecl).type let tag := (← goal.getDecl).userName let mut step ← Elab.Term.elabType <| ← do - if let some prevRhs := state.calcPrevRhs? then + if let some prevRhs := calcPrevRhs? then Elab.Term.annotateFirstHoleWithType pred (← Meta.inferType prevRhs) else pure pred let some (_, lhs, rhs) ← Elab.Term.getCalcRelation? step | throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}" - if let some prevRhs := state.calcPrevRhs? then + if let some prevRhs := calcPrevRhs? then unless (← Meta.isDefEqGuarded lhs prevRhs) do throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- " diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 9ede63e..1b1b9de 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -510,6 +510,8 @@ def test_calc: TestM Unit := do interiorGoal [] "a + b = b + c" (.some "calc"), interiorGoal [] "b + c = c + d" ]) + addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? 0 |>.isNone) + addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? 1 |>.isSome) let tactic := "apply h1" let state2m ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with @@ -532,6 +534,7 @@ def test_calc: TestM Unit := do #[ interiorGoal [] "b + c = c + d" (.some "calc") ]) + addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? 0 |>.isNone) let tactic := "apply h2" let state4m ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with | .success state => pure state From dc6e79def7a00e1d4a2e936a09e578c851b45bc4 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 11 Apr 2024 16:18:04 -0700 Subject: [PATCH 2/4] doc: Update error message in interaction --- Pantograph.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Pantograph.lean b/Pantograph.lean index a0580d2..f59bc11 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -129,7 +129,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do pure ( Except.ok (← goalConv goalState args.goalId)) | .none, .none, .none, .none, .some false => do pure ( Except.ok (← goalConvExit goalState)) - | _, _, _, _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr, have} must be supplied") + | _, _, _, _, _ => pure (Except.error <| + errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied") match nextGoalState? with | .error error => return .error error | .ok (.success nextGoalState) => From e834765896497e64ef0e30be576843792029f4ac Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 11 Apr 2024 16:25:17 -0700 Subject: [PATCH 3/4] refactor: Code simplification --- Pantograph/Goal.lean | 37 ++++++++++++++++++------------------- 1 file changed, 18 insertions(+), 19 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 75dc3f3..a27f765 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -164,22 +164,21 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr): let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray let errors ← (messages.map Message.data).mapM fun md => md.toString return .failure errors - else - let prevMCtx := state.savedState.term.meta.meta.mctx - let nextMCtx ← getMCtx - -- Generate a list of mvarIds that exist in the parent state; Also test the - -- assertion that the types have not changed on any mvars. - let newMVars := newMVarSet prevMCtx nextMCtx - let nextGoals ← newMVars.toList.filterM (λ mvar => do pure !(← mvar.isAssigned)) - return .success { - root := state.root, - savedState := { - term := ← MonadBacktrack.saveState, - tactic := { goals := nextGoals } - }, - newMVars, - parentMVar? := .some goal, - } + let prevMCtx := state.savedState.term.meta.meta.mctx + let nextMCtx ← getMCtx + -- Generate a list of mvarIds that exist in the parent state; Also test the + -- assertion that the types have not changed on any mvars. + let newMVars := newMVarSet prevMCtx nextMCtx + let nextGoals ← newMVars.toList.filterM (λ mvar => do pure !(← mvar.isAssigned)) + return .success { + root := state.root, + savedState := { + term := ← MonadBacktrack.saveState, + tactic := { goals := nextGoals } + }, + newMVars, + parentMVar? := .some goal, + } catch exception => return .failure #[← exception.toMessageData.toString] @@ -346,10 +345,10 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): | .ok syn => pure syn | .error error => return .parseError error let calcPrevRhs? := state.calcPrevRhsOf? goalId + let target ← instantiateMVars (← goal.getDecl).type + let tag := (← goal.getDecl).userName try goal.withContext do - let target ← instantiateMVars (← goal.getDecl).type - let tag := (← goal.getDecl).userName let mut step ← Elab.Term.elabType <| ← do if let some prevRhs := calcPrevRhs? then @@ -377,7 +376,7 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): -- The calc tactic either solves the main goal or leaves another relation. -- Replace the main goal, and save the new goal if necessary - if ¬(← Meta.isDefEq proofType target) then + unless ← Meta.isDefEq proofType target do let rec throwFailed := throwError "'calc' tactic failed, has type{indentExpr proofType}\nbut it is expected to have type{indentExpr target}" let some (_, _, rhs) ← Elab.Term.getCalcRelation? proofType | throwFailed From a864c4d3ff72360b397ecc450805163627b91755 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 11 Apr 2024 16:29:47 -0700 Subject: [PATCH 4/4] refactor: Code simplification --- Pantograph/Goal.lean | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index a27f765..f1c2503 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -48,8 +48,8 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do let root := goal.mvarId! let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root]} return { - savedState, root, + savedState, newMVars := SSet.insert .empty root, parentMVar? := .none, } @@ -126,7 +126,7 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri (fileName := filename) with | .ok stx => pure $ stx | .error error => return .parseError error - match (← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic)) with + match ← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic) with | .error errors => return .failure errors | .ok nextSavedState => @@ -149,13 +149,12 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr): let goalType ← goal.getType try -- For some reason this is needed. One of the unit tests will fail if this isn't here - let error?: Option String ← goal.withContext (do + let error?: Option String ← goal.withContext do let exprType ← Meta.inferType expr if ← Meta.isDefEq goalType exprType then pure .none else do return .some s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} != {← Meta.ppExpr goalType}" - ) if let .some error := error? then return .parseError error goal.checkNotAssigned `GoalState.assign @@ -221,7 +220,7 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St let binderName := binderName.toName try -- Implemented similarly to the intro tactic - let nextGoals: List MVarId ← goal.withContext $ (do + let nextGoals: List MVarId ← goal.withContext do let type ← Elab.Term.elabType (stx := type) let lctx ← MonadLCtx.getLCtx @@ -234,15 +233,14 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St let fvar := mkFVar fvarId let mvarUpstream ← withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do - Meta.withNewLocalInstances #[fvar] 0 (do + Meta.withNewLocalInstances #[fvar] 0 do let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous) let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream goal.assign expr - pure mvarUpstream) + pure mvarUpstream pure [mvarBranch.mvarId!, mvarUpstream.mvarId!] - ) return .success { root := state.root, savedState := { @@ -359,7 +357,7 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): let some (_, lhs, rhs) ← Elab.Term.getCalcRelation? step | throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}" if let some prevRhs := calcPrevRhs? then - unless (← Meta.isDefEqGuarded lhs prevRhs) do + unless ← Meta.isDefEqGuarded lhs prevRhs do throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- " -- Creates a mvar to represent the proof that the calc tactic solves the @@ -384,7 +382,7 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): let lastStep := mkApp2 r rhs rhs' let lastStepGoal ← Meta.mkFreshExprSyntheticOpaqueMVar lastStep tag (proof, proofType) ← Elab.Term.mkCalcTrans proof proofType lastStepGoal lastStep - unless (← Meta.isDefEq proofType target) do throwFailed + unless ← Meta.isDefEq proofType target do throwFailed remainder := .some lastStepGoal.mvarId! goal.assign proof