Merge pull request 'refactor: Cleanup the congruence tactics' (#81) from tactic/congruence into dev

Reviewed-on: #81

Pantograph/Library.lean

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

Pantograph/Serial.lean

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

Test/Tactic/Congruence.lean

@@ -7,6 +7,34 @@ open Pantograph
 
 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 :=
   let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
   runMetaMSeq env do
@@ -72,6 +100,7 @@ def test_congr (env: Environment): 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),
     ("congrFun", test_congr_fun env),
     ("congr", test_congr env),