Zulip Chat Archive

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