Stream: general

Topic: lift

Sebastien Gouezel (May 28 2021 at 14:22):

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 (May 28 2021 at 14:32):

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

Sebastien Gouezel (May 28 2021 at 15:05):

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

Gabriel Ebner (May 28 2021 at 15:08):

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

Eric Rodriguez (May 28 2021 at 15:08):

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

Gabriel Ebner (May 28 2021 at 15:08):

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

Gabriel Ebner (May 28 2021 at 15:10):

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

Patrick Massot (May 28 2021 at 15:10):

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

Floris van Doorn (May 28 2021 at 17:40):

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

Last updated: Dec 20 2023 at 11:08 UTC