From 6ffb227cd641f77109c539152e0b38f6d2bfa125 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 22 Apr 2024 10:02:09 -0700
Subject: [PATCH] feat: Conduit modus ponens

---
 Pantograph/Tactic/MotivatedApply.lean | 12 ++++++------
 Test/Proofs.lean                      | 15 +++++++++++++--
 2 files changed, 19 insertions(+), 8 deletions(-)

diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean
index 1201174..821b681 100644
--- a/Pantograph/Tactic/MotivatedApply.lean
+++ b/Pantograph/Tactic/MotivatedApply.lean
@@ -37,7 +37,7 @@ protected def surrogateMotiveType (info: RecursorWithMotive) (resultant: Expr):
   let resultantType ← Meta.inferType resultant
   return replaceForallBody motiveType resultantType
 
-protected def phantomType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
+protected def conduitType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
   let motiveCall := Expr.instantiateRev info.body mvars
   Meta.mkEq motiveCall resultant
 
@@ -92,11 +92,11 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do
       termination_by info.nArgs - i
     let mut newMVars ← go 0 #[]
 
-    goal.assign (mkAppN recursor newMVars)
-
-    let phantomType ← info.phantomType newMVars resultant
-    let goalPhantom ← Meta.mkFreshExprMVar phantomType .syntheticOpaque (userName := `phantom)
-    newMVars := newMVars ++ [goalPhantom]
+    -- Create the conduit type which proves the result of the motive is equal to the goal
+    let conduitType ← info.conduitType newMVars resultant
+    let goalConduit ← Meta.mkFreshExprMVar conduitType .syntheticOpaque (userName := `conduit)
+    goal.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
+    newMVars := newMVars ++ [goalConduit]
 
     let nextGoals ← newMVars.toList.map (·.mvarId!) |>.filterM (not <$> ·.isAssigned)
     pure nextGoals
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 2df0868..429d4d2 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -664,7 +664,7 @@ def test_nat_zero_add: TestM Unit := do
       buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
       buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat",
       buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
-      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "phantom")
+      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
     ])
 
   let tactic := "exact n"
@@ -703,7 +703,18 @@ def test_nat_zero_add: TestM Unit := do
     #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"])
 
   let tactic := "simp"
-  let stateF ← match ← state3.tryTactic (goalId := 0) (tactic := tactic) with
+  let state3d ← match ← state3.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let state2d ← match state3d.continue state2c with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let tactic := "rfl"
+  let stateF ← match ← state2d.tryTactic (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString