lift

Stream: general

[Sebastien Gouezel]

Is there a way to lift something providing the proof of the condition using a tactic? I mean, the standard syntax is

  lift n to ℕ using hn

where hn is a proof that n is nonnegative. I'd like to write

  lift n to ℕ using (by simp [h'n])

or whatever, but I can't find a way to do this. Is this syntax just not there?

[Johan Commelin]

Does lift n to ℕ, { by simp [h'n] }, do this? If so, is that close enough to what you want?

[Sebastien Gouezel]

You need an additional swap. This is what I am doing, but I am not completely satisfied by this solution.

[Gabriel Ebner]

Does the (by simp) fail to parse? Looking at the lift source, there is support for arbitrary expressions after the using.

[Eric Rodriguez]

using (show 0 ≤ n, by simp [h'n]) or using (by simp [h'n] : 0 ≤ n)?

[Gabriel Ebner]

I guess somebody needs to modify https://github.com/leanprover-community/mathlib/blob/5360e476391508e092b5a1e5210bd0ed22dc0755/src/tactic/lift.lean#L90

[Gabriel Ebner]

And write prf ← i_to_expr ``((%%(option.get h_some) : %%expected_prf_ty))

[Patrick Massot]

Yes, this code will try to evaluate by simp without knowing what is supposed to be proven.

[Floris van Doorn]

Thanks for the report (and the way to fix it):
#7739