apply at!

Game/Levels/AdvAddition/L03apply.lean

@@ -32,7 +32,7 @@ but Lean is smart enough to figure out the inputs to `succ_inj`.
 ### Example
 
 If the goal is `a * b = 7`, then `apply succ_inj` will turn the
-goal into `succ (a * b) = succ 7`
+goal into `succ (a * b) = succ 7`.
 "
 NewTactic apply
 

Game/Levels/AdvAddition/L04succ_inj1.lean

@@ -9,29 +9,6 @@ namespace MyNat
 
 LemmaTab "Peano"
 
-TacticDoc apply "
-## Summary
-
-If `t : P → Q` is a proof that $P\\implies Q$, and `h : P` is a proof of `P`,
-then `apply t at h` will change `h` to a proof of `Q`. The idea is that if
-you know `P` is true, then you can deduce from `t` that `Q` is true.
-
-If the goal is `Q`, then `apply t` will \"argue backwards\" and change the
-goal to `P`. The idea here is that if you want to prove `Q`, then it suffices
-to prove `P`, so you can reduce the goal to proving `P`.
-
-### Example:
-
-If you have a hypothesis `h : succ (a + 37) = succ (b + 42)`
-then `apply succ_inj at h` will change `h` to `a + 37 = b + 42`.
-
-### Example
-
-If the goal is `a * b = 7`, then `apply succ_inj` will turn the
-goal into `succ (a * b) = succ 7`
-"
-NewTactic apply
-
 Introduction
 "
 If `a` and `b` are numbers, then `succ_inj a b` is a proof

Game/Levels/AdvAddition/L05succ_inj2.lean

@@ -31,6 +31,7 @@ Statement (x : ℕ) (h : x + 1 = 4) : x = 3 := by
 Conclusion "Many people find `apply t at h` easy, but some find `apply t` confusing.
 If you find it confusing, then just argue forwards."
 
+-- **TODO** more levels! Put them elsewhere.
 -- next: intro intro level.
 theorem t1 (x y t : ℕ) : x + t = y + t → x = y := by
   induction t with d hd
@@ -39,18 +40,18 @@ theorem t1 (x y t : ℕ) : x + t = y + t → x = y := by
   assumption
   intro h
   rw [add_succ, add_succ] at h
-  --apply succ_inj at h **TODO**
-  replace h := succ_inj _ _ h
+  apply succ_inj at h
   apply hd at h
   assumption
 
 example (x y : ℕ) : x + t = t → x = 0 := by
   intro h
   nth_rewrite 2 [← zero_add t] at h
-  --apply t1 at h **TODO**
-  replace h := t1 _ _ _ h
+  apply t1 at h
   assumption
 
+axiom succ_ne_zero (x : ℕ) : succ x ≠ 0
+
 example (x y : ℕ) : x + y = 0 → x = 0 := by
   induction y with d hd
   intro h
@@ -59,6 +60,5 @@ example (x y : ℕ) : x + y = 0 → x = 0 := by
   clear hd
   rw [add_succ]
   intro h
-  -- apply succ_ne_zero at h
-  have h2 : False := sorry
+  apply succ_ne_zero at h
   contradiction

Game/Tactic/Apply.lean

@@ -1,19 +1,45 @@
-import Mathlib.Tactic.Replace
-import Std -- TODO: This is mathlib4#7080
+import Mathlib.Tactic
+import Lean
 
-open Lean Elab Tactic
+namespace Mathlib.Tactic
+open Lean Meta Elab Tactic Term
 
-/--
-If `(h : A)` is a proof of `A` and `f : A → B` an implication then
-`apply f at h` turns `h` into a proof of `B`.
+elab "apply" t:term "at" i:ident : tactic => withMainContext do
+  let fn ← Term.elabTerm t none
+  let fnTp ← inferType fn
+  let (ms, _, foutTp) ← forallMetaTelescopeReducing fnTp (some 1)
+  unless ms.size == 1 do throwError "oops!"
+  let finTp ← inferType ms[0]!
+  let ldecl ← (← getLCtx).findFromUserName? i.getId
+  let (mvs, outTp) ← show TacticM (Array Expr × Expr) from do
+    let mut mvs := #[ms[0]!]
+    let mut cmpTp := finTp
+    let mut outTp := foutTp
+    while !(← isDefEq cmpTp ldecl.type) do
+      let (ms, _, newfoutTp) ← forallMetaTelescopeReducing outTp (some 1)
+      unless ms.size == 1 do throwError "oops!"
+      mvs := mvs ++ ms
+      cmpTp ← inferType ms[0]!
+      outTp := newfoutTp
+    mvs := mvs.pop
+    return (mvs, outTp)
+  let mainGoal ← getMainGoal
+  let mainGoal ← mainGoal.tryClear ldecl.fvarId
+  let mainGoal ← mainGoal.assert ldecl.userName outTp (mkAppN fn (mvs.push ldecl.toExpr))
+  let (_, mainGoal) ← mainGoal.intro1P
+  replaceMainGoal <| [mainGoal] ++ mvs.toList.map fun e => e.mvarId!
 
-This is a game-specific implementation and not an official Lean tactic.
-It is equivalent to the tactic `replace h := f h`.
--/
-syntax (name := applyAt) "apply" ident " at " ident : tactic
+example (A B C : Prop) (ha : A) (f : A → B) (g : B → C) : C := by
+  apply f at ha -- ha : B
+  apply g at ha
+  exact ha
 
-elab_rules : tactic | `(tactic| apply $thm at $hyp) => do
-  evalTactic (← `(tactic| replace $hyp := $thm $hyp))
+open Nat
+
+example (a b : Nat) (h : succ a = succ b) : a = b := by
+  let succ_inj2 (a b : Nat) : succ a = succ b → a = b := by simp
+  apply succ_inj2 at h
+  exact h
 
 -- Test
 example (A B C : Prop) (ha : A) (f : A → B) (g : B → C) : C := by