elaborate function with expected type

src/tactic/apply_fun.lean

@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2019 Patrick Massot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Patrick Massot
+-/
+
 import tactic.monotonicity
 import order.basic
 
@@ -6,31 +12,33 @@ open tactic interactive (parse) interactive (loc.ns)
 
 local postfix `?`:9001 := optional
 
-meta def apply_fun_name (e : expr) (h : name) (M : option pexpr) : tactic unit :=
+meta def apply_fun_name (e : pexpr) (h : name) (M : option pexpr) : tactic unit :=
 do {
   H ← get_local h,
   t ← infer_type H,
   match t with
   | `(%%l = %%r) := do
-      tactic.interactive.«have» h none ``(congr_arg %%e %%H),
-      tactic.clear H
+      ltp ← infer_type l,
+      mv ← mk_mvar,
+      to_expr ``(congr_arg (%%e : %%ltp → %%mv) %%H) >>= note h,
+      clear H
   | `(%%l ≤ %%r) := do
        if M.is_some then do
          Hmono ← M >>= tactic.i_to_expr,
-         tactic.interactive.«have» h none ``(%%Hmono %%H)
+         to_expr ``(%%Hmono %%H) >>= note h >> skip
        else do {
          n ← get_unused_name `mono,
-         tactic.interactive.«have» n ``(monotone %%e) none,
+         to_expr ``(monotone %%e) >>= assert n,
          do { intro_lst [`x, `y, `h], `[dsimp, mono], skip } <|> swap,
          Hmono ← get_local n,
-         tactic.interactive.«have» h none ``(%%Hmono %%H) },
-       tactic.clear H
+         to_expr ``(%%Hmono %%H) >>= note h >> skip },
+       clear H
   | _ := skip
   end,
   -- let's try to force β-reduction at `h`
   try (tactic.interactive.dsimp tt [] [] (loc.ns [h])
          {eta := false, beta := true})
-  } <|> fail ("failed to apply " ++ to_string e ++ " at " ++ to_string h)
+} <|> fail ("failed to apply " ++ to_string e ++ " at " ++ to_string h)
 
 namespace tactic.interactive
 /-- Apply a function to some local assumptions which are either equalities or
@@ -42,52 +50,14 @@ namespace tactic.interactive
     prove it. -/
 meta def apply_fun (q : parse texpr) (locs : parse location)
   (lem : parse (tk "using" *> texpr)?) : tactic unit :=
-do e ← tactic.i_to_expr q,
+--do e ← tactic.i_to_expr q,
    match locs with
    | (loc.ns l) := do
       l.mmap' (λ l, match l with
-      | some h :=  apply_fun_name e h lem
+      | some h :=  apply_fun_name q h lem
       | none := skip
       end)
    | wildcard := do ctx ← local_context,
-                    ctx.mmap' (λ h, apply_fun_name e h.local_pp_name lem)
+                    ctx.mmap' (λ h, apply_fun_name q h.local_pp_name lem)
    end
 end tactic.interactive
-
-open function
-
-example (X Y Z : Type) (f : X → Y) (g : Y → Z) (H : injective $ g ∘ f) :
-  injective f :=
-begin
-  intros x x' h,
-  apply_fun g at h,
-  exact H h
-end
-
-example (f : ℕ → ℕ) (a b : ℕ) (monof : monotone f)  (h : a ≤ b) : f a ≤ f b :=
-begin
-  apply_fun f at h,
-  assumption,
-  assumption
-end
-
-example (a b : ℕ) (h : a = b) : a + 1 = b + 1 :=
-begin
-  apply_fun (λ n, n+1) at h,
-  -- check that `h` was β-reduced
-  guard_hyp' h := a + 1 = b + 1,
-  exact h
-end
-
-example (f : ℕ → ℕ) (a b : ℕ) (monof : monotone f)  (h : a ≤ b) : f a ≤ f b :=
-begin
-  apply_fun f at h using monof,
-  assumption
-end
-
--- monotonicity will be proved by `mono` in the next example
-example (a b : ℕ) (h : a ≤ b) : a + 1 ≤ b + 1 :=
-begin
-  apply_fun (λ n, n+1) at h,
-  exact h
-end