From bbc00cbbb80748a53c2741bd2e4ee1415ba92f8d Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 20 May 2024 14:00:04 -0700
Subject: [PATCH] feat: Congruence tactic FFI interface and tests

---
 Pantograph/Goal.lean        | 12 +---------
 Pantograph/Library.lean     | 16 ++++++++++++++
 Test/Tactic/Congruence.lean | 44 +++++++++++++++++++++++++++++++++++++
 3 files changed, 61 insertions(+), 11 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 3a8e2fe..46888e7 100644
--- a/Pantograph/Goal.lean
+++ b/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)
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 20eaa34..e0625e8 100644
--- a/Pantograph/Library.lean
+++ b/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
diff --git a/Test/Tactic/Congruence.lean b/Test/Tactic/Congruence.lean
index 7ef358a..1421263 100644
--- a/Test/Tactic/Congruence.lean
+++ b/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