feat(tactic/lift): elaborate proof with the expected type (#7739)

* also slightly refactor the corresponding function a bit
* add some tests
* move all tests to `tests/lift.lean`

src/tactic/lift.lean

@@ -85,17 +85,16 @@ If the proof was not specified, we create assert it as a local constant.
 (The name of this local constant doesn't matter, since `lift` will remove it from the context.)
 -/
 meta def get_lift_prf (h : option pexpr) (old_tp new_tp inst e : expr)
-  (s : simp_lemmas) (to_unfold : list name) : tactic expr :=
-if h_some : h.is_some then
-  (do prf ← i_to_expr (option.get h_some), prf_ty ← infer_type prf,
+  (s : simp_lemmas) (to_unfold : list name) : tactic expr := do
   expected_prf_ty ← mk_app `can_lift.cond [old_tp, new_tp, inst, e],
-  unify prf_ty expected_prf_ty <|>
-    (do expected_prf_ty2 ← s.dsimplify to_unfold expected_prf_ty,
-      pformat!"lift tactic failed. The type of\n  {prf}\nis\n  {prf_ty}\nbut it is expected to be\n  {expected_prf_ty2}" >>= fail),
-  return prf)
-  else (do prf_nm ← get_unused_name,
-    prf ← mk_app `can_lift.cond [old_tp, new_tp, inst, e] >>= assert prf_nm,
-    dsimp_target s to_unfold {}, swap, return prf)
+  expected_prf_ty ← s.dsimplify to_unfold expected_prf_ty,
+  if h_some : h.is_some then
+    decorate_error "lift tactic failed." $ i_to_expr ``((%%(option.get h_some) : %%expected_prf_ty))
+  else do
+    prf_nm ← get_unused_name,
+    prf ← assert prf_nm expected_prf_ty,
+    swap,
+    return prf
 
 /-- Lift the expression `p` to the type `t`, with proof obligation given by `h`.
   The list `n` is used for the two newly generated names, and to specify whether `h` should

test/lift.lean

@@ -1,5 +1,62 @@
 import tactic.lift
 import data.set.basic
+import data.int.basic
+
+/-! Some tests of the `lift` tactic. -/
+
+example (n m k x z u : ℤ) (hn : 0 < n) (hk : 0 ≤ k + n) (hu : 0 ≤ u)
+  (h : k + n = 2 + x) (f : false) :
+  k + n = m + x :=
+begin
+  lift n to ℕ using le_of_lt hn,
+    guard_target (k + ↑n = m + x), guard_hyp hn : (0 : ℤ) < ↑n,
+  lift m to ℕ,
+    guard_target (k + ↑n = ↑m + x), tactic.swap, guard_target (0 ≤ m), tactic.swap,
+    tactic.num_goals >>= λ n, guard (n = 2),
+  lift (k + n) to ℕ using hk with l hl,
+    guard_hyp l : ℕ, guard_hyp hl : ↑l = k + ↑n, guard_target (↑l = ↑m + x),
+    tactic.success_if_fail (tactic.get_local `hk),
+  lift x to ℕ with y hy,
+    guard_hyp y : ℕ, guard_hyp hy : ↑y = x, guard_target (↑l = ↑m + x),
+  lift z to ℕ with w,
+    guard_hyp w : ℕ, tactic.success_if_fail (tactic.get_local `z),
+  lift u to ℕ using hu with u rfl hu,
+    guard_hyp hu : (0 : ℤ) ≤ ↑u,
+
+  all_goals { exfalso, assumption },
+end
+
+-- test lift of functions
+example (α : Type*) (f : α → ℤ) (hf : ∀ a, 0 ≤ f a) (hf' : ∀ a, f a < 1) (a : α) : 0 ≤ 2 * f a :=
+begin
+  lift f to α → ℕ using hf,
+    guard_target ((0:ℤ) ≤ 2 * (λ i : α, (f i : ℤ)) a),
+    guard_hyp hf' : ∀ a, ((λ i : α, (f i:ℤ)) a) < 1,
+  exact int.coe_nat_nonneg _
+end
+
+instance can_lift_unit : can_lift unit unit :=
+⟨id, λ x, true, λ x _, ⟨x, rfl⟩⟩
+
+/- test whether new instances of `can_lift` are added as simp lemmas -/
+run_cmd do l ← can_lift_attr.get_cache, guard (`can_lift_unit ∈ l)
+
+/- test error messages -/
+example (n : ℤ) (hn : 0 < n) : true :=
+begin
+  success_if_fail_with_msg {lift n to ℕ using hn} "lift tactic failed.
+invalid type ascription, term has type\n  0 < n\nbut is expected to have type\n  0 ≤ n",
+  success_if_fail_with_msg {lift (n : option ℤ) to ℕ}
+    "Failed to find a lift from option ℤ to ℕ. Provide an instance of\n  can_lift (option ℤ) ℕ",
+  trivial
+end
+
+example (n : ℤ) : ℕ :=
+begin
+  success_if_fail_with_msg {lift n to ℕ}
+    "lift tactic failed. Tactic is only applicable when the target is a proposition.",
+  exact 0
+end
 
 instance can_lift_subtype (R : Type*) (P : R → Prop) : can_lift R {x // P x} :=
 { coe := coe,
@@ -17,3 +74,26 @@ by { lift x to {x // P x} using hx with y, trivial }
 /-! Test that `lift` elaborates `s` as a type, not as a set. -/
 example {R : Type*} {s : set R} (x : R) (hx : x ∈ s) : true :=
 by { lift x to s using hx with y, trivial }
+
+example (n : ℤ) (hn : 0 ≤ n) : true :=
+by { lift n to ℕ, trivial, exact hn }
+
+example (n : ℤ) (hn : 0 ≤ n) : true :=
+by { lift n to ℕ using hn, trivial }
+
+example (n : ℤ) (hn : n ≥ 0) : true :=
+by { lift n to ℕ using ge.le _, trivial, guard_target (n ≥ 0), exact hn }
+
+example (n : ℤ) (hn : 0 ≤ 1 * n) : true :=
+begin
+  lift n to ℕ using by { simpa [int.one_mul] using hn } with k,
+  -- the above braces are optional, but it would be bad style to remove them (see next example)
+  guard_hyp hn : 0 ≤ 1 * ((k : ℕ) : ℤ),
+  trivial
+end
+
+example (n : ℤ) (hn : 0 ≤ n ↔ true) : true :=
+begin
+  lift n to ℕ using by { simp [hn] } with k, -- the braces are not optional here
+  trivial
+end

test/tactics.lean

@@ -209,64 +209,6 @@ by {have : α₁, have : α₂, have : α₃, swap, swap,
 
 end swap
 
-section lift
-
-example (n m k x z u : ℤ) (hn : 0 < n) (hk : 0 ≤ k + n) (hu : 0 ≤ u)
-  (h : k + n = 2 + x) (f : false) :
-  k + n = m + x :=
-begin
-  lift n to ℕ using le_of_lt hn,
-    guard_target (k + ↑n = m + x), guard_hyp hn : (0 : ℤ) < ↑n,
-  lift m to ℕ,
-    guard_target (k + ↑n = ↑m + x), tactic.swap, guard_target (0 ≤ m), tactic.swap,
-    tactic.num_goals >>= λ n, guard (n = 2),
-  lift (k + n) to ℕ using hk with l hl,
-    guard_hyp l : ℕ, guard_hyp hl : ↑l = k + ↑n, guard_target (↑l = ↑m + x),
-    tactic.success_if_fail (tactic.get_local `hk),
-  lift x to ℕ with y hy,
-    guard_hyp y : ℕ, guard_hyp hy : ↑y = x, guard_target (↑l = ↑m + x),
-  lift z to ℕ with w,
-    guard_hyp w : ℕ, tactic.success_if_fail (tactic.get_local `z),
-  lift u to ℕ using hu with u rfl hu,
-    guard_hyp hu : (0 : ℤ) ≤ ↑u,
-
-  all_goals { exfalso, assumption },
-end
-
--- test lift of functions
-example (α : Type*) (f : α → ℤ) (hf : ∀ a, 0 ≤ f a) (hf' : ∀ a, f a < 1) (a : α) : 0 ≤ 2 * f a :=
-begin
-  lift f to α → ℕ using hf,
-    guard_target ((0:ℤ) ≤ 2 * (λ i : α, (f i : ℤ)) a),
-    guard_hyp hf' : ∀ a, ((λ i : α, (f i:ℤ)) a) < 1,
-  exact int.coe_nat_nonneg _
-end
-
-instance can_lift_unit : can_lift unit unit :=
-⟨id, λ x, true, λ x _, ⟨x, rfl⟩⟩
-
-/- test whether new instances of `can_lift` are added as simp lemmas -/
-run_cmd do l ← can_lift_attr.get_cache, guard (`can_lift_unit ∈ l)
-
-/- test error messages -/
-example (n : ℤ) (hn : 0 < n) : true :=
-begin
-  success_if_fail_with_msg {lift n to ℕ using hn} "lift tactic failed. The type of\n  hn\nis
-  0 < n\nbut it is expected to be\n  0 ≤ n",
-  success_if_fail_with_msg {lift (n : option ℤ) to ℕ}
-    "Failed to find a lift from option ℤ to ℕ. Provide an instance of\n  can_lift (option ℤ) ℕ",
-  trivial
-end
-
-example (n : ℤ) : ℕ :=
-begin
-  success_if_fail_with_msg {lift n to ℕ}
-    "lift tactic failed. Tactic is only applicable when the target is a proposition.",
-  exact 0
-end
-
-end lift
-
 private meta def get_exception_message (t : lean.parser unit) : lean.parser string
 | s := match t s with
        | result.success a s' := result.success "No exception" s