refactor: Cleanup the congruence tactics #81

Merged
aniva merged 4 commits from tactic/congruence into dev 2024-06-23 13:35:36 -07:00
3 changed files with 40 additions and 10 deletions

View File

@ -204,15 +204,16 @@ def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Core
def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): 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 SyntheticTactic where
| congruenceArg | congruenceArg
| congruenceFun | congruenceFun
| congruence | congruence
@[export pantograph_goal_tactic_execute_m] /-- Executes a synthetic tactic which has no arguments -/
def goalTacticExecute (state: GoalState) (goalId: Nat) (tacticExecute: TacticExecute): CoreM TacticResult := @[export pantograph_goal_synthetic_tactic_m]
def goalSyntheticTactic (state: GoalState) (goalId: Nat) (case: SyntheticTactic): CoreM TacticResult :=
runTermElabM do runTermElabM do
state.restoreElabM state.restoreElabM
state.execute goalId $ match tacticExecute with state.execute goalId $ match case with
| .congruenceArg => Tactic.congruenceArg | .congruenceArg => Tactic.congruenceArg
| .congruenceFun => Tactic.congruenceFun | .congruenceFun => Tactic.congruenceFun
| .congruence => Tactic.congruence | .congruence => Tactic.congruence

View File

@ -307,11 +307,11 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
let goals := goals.toSSet let goals := goals.toSSet
let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) => let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
!(goals.contains mvarId || mvarId == root) && options.printAll) !(goals.contains mvarId || mvarId == root) && options.printAll)
|>.mapM (fun (mvarId, decl) => do |>.mapM (fun (mvarId, decl) => do
let pref := if goalState.newMVars.contains mvarId then "~" else " " let pref := if goalState.newMVars.contains mvarId then "~" else " "
printMVar pref mvarId decl printMVar pref mvarId decl
) )
pure $ result ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join) pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
where where
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
let resultFVars: List String ← let resultFVars: List String ←
@ -337,7 +337,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
else pure $ value else pure $ value
pure s!"\n := {← Meta.ppExpr value}" pure s!"\n := {← Meta.ppExpr value}"
else if let .some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then else if let .some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then
pure s!"\n := $ {mvarIdPending.name}" pure s!"\n ::= {mvarIdPending.name}"
else else
pure "" pure ""
else else

View File

@ -7,6 +7,34 @@ open Pantograph
namespace Pantograph.Test.Tactic.Congruence namespace Pantograph.Test.Tactic.Congruence
def test_congr_arg_list (env: Environment): IO LSpec.TestSeq :=
let expr := "λ {α} (l1 l2 : List α) (h: l1 = l2) => l1.reverse = l2.reverse"
runMetaMSeq env do
let expr ← parseSentence expr
Meta.lambdaTelescope expr $ λ _ body => do
let mut tests := LSpec.TestSeq.done
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
let (newGoals, test) ← runTermElabMInMeta do
let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
let test := 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)"),
])
return (newGoals, test)
tests := tests ++ test
let f := newGoals.get! 3
let h := newGoals.get! 4
let c := newGoals.get! 5
let results ← f.apply (← parseSentence "List.reverse")
tests := tests ++ (LSpec.check "apply" (results.length = 0))
tests := tests ++ (LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂"))
tests := tests ++ (LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)"))
return tests
def test_congr_arg (env: Environment): IO LSpec.TestSeq := def test_congr_arg (env: Environment): IO LSpec.TestSeq :=
let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m" let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
runMetaMSeq env do runMetaMSeq env do
@ -72,6 +100,7 @@ def test_congr (env: Environment): IO LSpec.TestSeq :=
def suite (env: Environment): List (String × IO LSpec.TestSeq) := def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[ [
("congrArg List.reverse", test_congr_arg_list env),
("congrArg", test_congr_arg env), ("congrArg", test_congr_arg env),
("congrFun", test_congr_fun env), ("congrFun", test_congr_fun env),
("congr", test_congr env), ("congr", test_congr env),