feat: let apply_fun use CoeFun and dependent functions (#2890)

Changes `apply_fun` to use the main function application elaborator, then uses `Lean.MVarId.congrN` to solve for a congruence proof. This means that `apply_fun f at h` should work whenever `f` applies to both sides of the equation `h` (even when coercions need to be involved).

Mathlib/Tactic/ApplyFun.lean

@@ -22,40 +22,33 @@ open Lean Parser Tactic Elab Tactic Meta
 
 initialize registerTraceClass `apply_fun
 
-/--
-Helper function to fill implicit arguments with metavariables.
--/
-partial def fillImplicitArgumentsWithFreshMVars (e : Expr) : MetaM Expr := do
-  match ← inferType e with
-  | Expr.forallE _ _ _ .implicit
-  | Expr.forallE _ _ _ .instImplicit => do
-    fillImplicitArgumentsWithFreshMVars (mkApp e (← mkFreshExprMVar none))
-  | _                    => pure e
-
 /-- Apply a function to a hypothesis. -/
-def applyFunHyp (f : Expr) (using? : Option Expr) (h : FVarId) (g : MVarId) :
-    MetaM (List MVarId) := do
+def applyFunHyp (f : TSyntax `term) (using? : Option Expr) (h : FVarId) (g : MVarId) :
+    TacticM (List MVarId) := do
   let d ← h.getDecl
   let (prf, newGoals) ← match (← whnfR (← instantiateMVars d.type)).getAppFnArgs with
-  | (``Eq, #[α, _, _]) => do
-    -- We have to jump through a hoop here!
-    -- At this point Lean may think `f` is a dependently-typed function,
-    -- so we can't just feed it to `congrArg`.
-    -- To solve this, we first fill any implicit arguments for `f` with metavariables,
-    -- and then try to unify with a metavariable `_ : α → _`
-    -- (i.e. an arrow, but with the target as some fresh type metavariable).
-    -- (Arguably `Lean.Meta.mkCongrArg` could do this all itself.)
-    let arrow ← mkFreshExprMVar (← mkArrow α (← mkFreshTypeMVar))
-    let f' ← fillImplicitArgumentsWithFreshMVars f
-    if ¬ (← isDefEq f' arrow) then
-      throwError "Can not use `apply_fun` with a dependently typed function."
-    pure (← mkCongrArg f' d.toExpr, [])
+  | (``Eq, #[_, lhs, rhs]) => do
+    let (eq', gs) ← withCollectingNewGoalsFrom (tagSuffix := `apply_fun) <|
+      withoutRecover <| runTermElab <| do
+        let f ← Term.elabTerm f none
+        let lhs' ← Term.elabAppArgs f #[] #[.expr lhs] none false false
+        let rhs' ← Term.elabAppArgs f #[] #[.expr rhs] none false false
+        unless ← isDefEq (← inferType lhs') (← inferType rhs') do
+          let msg ← mkHasTypeButIsExpectedMsg (← inferType rhs') (← inferType lhs')
+          throwError "In generated equality, right-hand side {msg}"
+        let eq ← mkEq lhs'.headBeta rhs'.headBeta
+        Term.synthesizeSyntheticMVarsUsingDefault
+        instantiateMVars eq
+    let mvar ← mkFreshExprMVar eq'
+    let [] ← mvar.mvarId!.congrN | throwError "`apply_fun` could not construct congruence"
+    pure (mvar, gs)
   | (``LE.le, _) =>
     let (monotone_f, newGoals) ← match using? with
     -- Use the expression passed with `using`
     | some r => pure (r, [])
     -- Create a new `Monotone f` goal
     | none => do
+      let f ← elabTermForApply f
       let ng ← mkFreshExprMVar (← mkAppM ``Monotone #[f])
       -- TODO attempt to solve this goal using `mono` when it has been ported,
       -- via `synthesizeUsing`.
@@ -128,9 +121,10 @@ example (X Y Z : Type) (f : X → Y) (g : Y → Z) (H : Injective <| g ∘ f) :
 syntax (name := applyFun) "apply_fun " term (ppSpace location)? (" using " term)? : tactic
 
 elab_rules : tactic | `(tactic| apply_fun $f $[$loc]? $[using $P]?) => do
-  let f ← elabTermForApply f
   let P ← P.mapM (elabTerm · none)
   withLocation (expandOptLocation (Lean.mkOptionalNode loc))
-    (atLocal := fun h ↦ liftMetaTactic <| applyFunHyp f P h)
-    (atTarget := liftMetaTactic <| applyFunTarget f P)
+    (atLocal := fun h ↦ do replaceMainGoal <| ← applyFunHyp f P h (← getMainGoal))
+    (atTarget := withMainContext do
+      let f ← elabTermForApply f
+      liftMetaTactic fun g => applyFunTarget f P g)
     (failed := fun _ ↦ throwError "apply_fun failed")

test/apply_fun.lean

@@ -17,9 +17,9 @@ example (x : Int) (h : x = 1) : 1 = 1 := by
 
 example (a b : Int) (h : a = b) : a + 1 = b + 1 := by
   -- Make sure that we infer the type of the function only after we see the hypothesis:
-  apply_fun (fun n => n+1) at h
-  -- check that `h` was β-reduced (in Lean3 this required additional work)
-  guard_hyp h : a + 1 = b + 1
+  apply_fun (fun n => n + 1) at h
+  -- check that `h` was β-reduced
+  guard_hyp h :ₛ a + 1 = b + 1
   exact h
 
 -- Verify failure when applying a dependently typed function.
@@ -109,3 +109,46 @@ example : ∀ m n : ℕ, m = n → (m < 2) = (n < 2) := by
   intro m n h
   apply_fun (· < 2) at h
   exact h
+
+example (f : ℕ ≃ ℕ) (a b : ℕ) (h : a = b) : True := by
+  apply_fun f at h
+  guard_hyp h : f a = f b
+  trivial
+
+example (f : ℤ ≃ ℤ) (a b : ℕ) (h : a = b) : True := by
+  apply_fun f at h
+  guard_hyp h : f a = f b
+  trivial
+
+example (f : ℤ ≃ ℤ) (a b : α) (h : a = b) : True := by
+  fail_if_success apply_fun f at h
+  trivial
+
+example (f : ℕ → ℕ) (a b : ℕ) (h : a = b) : True := by
+  apply_fun f at h
+  guard_hyp h : f a = f b
+  trivial
+
+example (f : {i : Nat} → Fin i → ℕ) (a b : Fin 37) (h : a = b) : True := by
+  apply_fun f at h
+  guard_hyp h : f a = f b
+  trivial
+
+example (f : (p : Prop) → [Decidable p] → Nat) (p q : Prop) (h : p = q)
+    (h' : {n m : Nat} → n = m → True) : True := by
+  classical
+  apply_fun f at h
+  apply h'
+  exact h
+
+example (f : (p : Prop) → [Decidable p] → Nat) (p q : Prop) (h : p = q)
+    (h' : {n m : Nat} → n = m → True) : True := by
+  classical
+  apply_fun (fun x [Decidable x] => f x) at h
+  apply h'
+  exact h
+
+example (a b : ℕ) (h : a = b) : True := by
+  apply_fun (fun i => i + ?_) at h
+  · trivial
+  · exact 37