lift tries to clear hypotheses

Stream: metaprogramming / tactics

[Yaël Dillies]

Would it be possible to make lift not fail if it cannot clear an hypothesis? It is still useful even if the lifting condition hypothesis appears in another hypothesis.

import data.set.finite

example {α : Type*} {s : set α} (hs : s.finite) : hs.to_finset = ∅ :=
begin
  lift s to finset α using hs,
/-
clear tactic failed, target type depends on 'hs'
state:
α : Type ?,
s : finset α,
hs : ↑s.finite
⊢ hs.to_finset = ∅
-/
end

[Yaël Dillies]

Of course, I can just do lift s to finset α using id hs but we might as well fix it to the source.

[Damiano Testa]

If you replace these two lines

https://github.com/leanprover-community/mathlib/blob/10b4e499f43088dd3bb7b5796184ad5216648ab1/src/tactic/lift.lean#L135-L136
namely

  if h_prf_nm : prf_nm.is_some ∧ n.nth 2 ≠ prf_nm then
    get_local (option.get h_prf_nm.1) >>= clear else skip,

with

    new ← get_unused_name,
    if n.nth 2 ≠ prf_nm then get_local (option.get_or_else prf_nm new) >>= clear <|> skip else skip,

you probably obtain the behaviour that you want. I tested it in your case and also on this example with smaller imports that compiles faster:

import tactic.lift

def foo {n : ℤ} (h : 0 ≤ n) := h = h

example {n : ℤ} (h : 0 ≤ n) : foo h :=
begin
  lift n to ℕ using h,  --  now succeeds
  unfold foo,
end

I am not too happy with the "new" name and admittedly the proposal above checks less than what it did earlier, but since the alternative was skipping anyway, it may be ok...

[Damiano Testa]

#17869, to see if anything else breaks and if anyone else has comments!

I made the removal of the issue with clear slightly more robust as well.
EDIT: I changed the previous message to reflect the slightly tighter change.

[Eric Wieser]

Note that this already works if you use lift s to finset α using hs with _ _ hs

[Kevin Buzzard]

@Damiano Testa can you port lift to mathlib 4? Right now any changes to lean 3 tactics are just making the port process harder.

[Damiano Testa]

Kevin, I am going to seriously start with helping the porting process starting from next week: tomorrow is the last day of term and I am very short on time for a few more hours!

[Scott Morrison]

There is actually a PR open: https://github.com/leanprover-community/mathlib4/pull/723 by Yury, that is badly overdue for a review.