feat: Congruence tactic FFI interface and tests

Pantograph/Goal.lean

@@ -76,7 +76,7 @@ private def GoalState.mvars (state: GoalState): SSet MVarId :=
   state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
 protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
   state.savedState.term.meta.restore
-private def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
+protected def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
   state.savedState.term.restore
 private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do
   state.savedState.restore
@@ -518,11 +518,6 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
 protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
-  let goal ← match state.savedState.tactic.goals.get? goalId with
-    | .some goal => pure goal
-    | .none => return .indexError goalId
-  goal.checkNotAssigned `GoalState.tryMotivatedApply
-
   let recursor ← match Parser.runParserCategory
     (env := state.env)
     (catName := `term)
@@ -534,11 +529,6 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
 protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
-  let goal ← match state.savedState.tactic.goals.get? goalId with
-    | .some goal => pure goal
-    | .none => return .indexError goalId
-  goal.checkNotAssigned `GoalState.tryMotivatedApply
-
   let recursor ← match Parser.runParserCategory
     (env := state.env)
     (catName := `term)

Pantograph/Library.lean

@@ -204,4 +204,20 @@ def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean
 def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Lean.CoreM TacticResult :=
   runTermElabM <| state.tryNoConfuse goalId eq
 
+inductive TacticExecute where
+  | congruenceArg
+  | congruenceFun
+  | congruence
+@[export pantograph_goal_tactic_execute_m]
+def goalTacticExecute (state: GoalState) (goalId: Nat) (tacticExecute: TacticExecute): Lean.CoreM TacticResult :=
+  runTermElabM do
+    state.restoreElabM
+    let tactic := match tacticExecute with
+      | .congruenceArg => Tactic.congruenceArg
+      | .congruenceFun => Tactic.congruenceFun
+      | .congruence => Tactic.congruence
+    state.execute goalId tactic
+
+
+
 end Pantograph

Test/Tactic/Congruence.lean

@@ -27,10 +27,54 @@ def test_congr_arg (env: Environment): IO LSpec.TestSeq :=
           ])
       tests := tests ++ test
       return tests
+def test_congr_fun (env: Environment): IO LSpec.TestSeq :=
+  let expr := "λ (n m: Nat) => (n + m) + (n + m) = (n + m) * 2"
+  runMetaMSeq env do
+    let expr ← parseSentence expr
+    Meta.lambdaTelescope expr $ λ _ body => do
+      let mut tests := LSpec.TestSeq.done
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      let test ← runTermElabMInMeta do
+        let newGoals ← runTacticOnMVar Tactic.congruenceFun target.mvarId!
+        pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+          [
+            (`α, "Sort ?u.159"),
+            (`f₁, "?α → Nat"),
+            (`f₂, "?α → Nat"),
+            (`h, "?f₁ = ?f₂"),
+            (`a, "?α"),
+            (`conduit, "(?f₁ ?a = ?f₂ ?a) = (n + m + (n + m) = (n + m) * 2)"),
+          ])
+      tests := tests ++ test
+      return tests
+def test_congr (env: Environment): IO LSpec.TestSeq :=
+  let expr := "λ (a b: Nat) => a = b"
+  runMetaMSeq env do
+    let expr ← parseSentence expr
+    Meta.lambdaTelescope expr $ λ _ body => do
+      let mut tests := LSpec.TestSeq.done
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      let test ← runTermElabMInMeta do
+        let newGoals ← runTacticOnMVar Tactic.congruence target.mvarId!
+        pure $ 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)"),
+          ])
+      tests := tests ++ test
+      return tests
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
     ("congrArg", test_congr_arg env),
+    ("congrFun", test_congr_fun env),
+    ("congr", test_congr env),
   ]
 
 end Pantograph.Test.Tactic.Congruence