Is finish considered bad?

Stream: new members

[Sam]

I've noticed (by a quick github search) that use of finish seems very rare in mathlib. However, I'm often using in it my own lemmas when finish works and it's not obvious what else to do.

Is finish considered bad? Should it be avoided in mathlib?

What are some techniques for dealing with situations where finish closes the goal, but it's not clear how to proceed otherwise? I'm aware of show_term, but finish usually spits out something pretty horrendous from that!

[Alex J. Best]

Finish can be a bit slow, so while it's not necessarily banned it often gets golfed out to speed things up. I guess it's a bit situational, but if you are using it for logic goals the tactics like tactic#tauto (and variants) do less than finish so are faster when they do work. If you post some examples we can take a look at alternative proofs.

[Sam]

I always at least try hint when resorting to finish, I think that will reliably tell me whether something like tauto is a valid substitute, won't it? I already only use it as a last resort, although I expect more experienced people know better techniques.

[Matt Diamond]

maybe squeeze_simp could help?

[Matt Diamond]

that tells you what works if simp works, and I believe finish calls the simplifier

[Sam]

I'm already doing a lot of simping. This is situation where simp * at * even isn't getting anywhere. I'll try to find a nice example that doesn't rely on too many other defs.

[Sam]

Here's a simple case where I'm using a finish.

import data.list

universe u

def list.containsp
{α : Type u}
(l : list α)
(p : α → Prop) [decidable_pred p] :=
∃ (a : α), a ∈ l ∧ p a

@[simp]
lemma list.containsp_cons_of_neg
{α : Type u}
{a : α}
{l : list α}
{p : α → Prop} [decidable_pred p]
(q : ¬ p a)
(h: (a::l).containsp p) :
l.containsp p :=
begin
  simp only [list.containsp, list.mem_cons_iff] at h,
  simp only [list.containsp],
  finish,
end

[Sam]

Ignore the name of that lemma, I think that's bad/wrong.

[Sam]

Maybe in this case there's some smart way to handle existentials that I don't know? hint, simp, library_search and suggest all seem like dead-ends as far as I can tell.

[Ruben Van de Velde]

Well, that's finish being too clever by half, imo :)

This works:

@[simp]
lemma list.containsp_cons_of_neg
{α : Type u}
{a : α}
{l : list α}
{p : α → Prop} [decidable_pred p]
(q : ¬ p a)
(h: (a::l).containsp p) :
l.containsp p :=
begin
  simp only [list.containsp, list.mem_cons_iff] at h,
  simp only [list.containsp],
  obtain ⟨b, rfl|hb1, hb2⟩ := h,
  { contradiction },
  { exact ⟨b, hb1, hb2⟩ },
end

[Sam]

Ah, so this is just me being a newb then. I don't think I've encountered obtain yet! I have some reading to do.

[Sam]

So essentially I just need to learn lots more tactics?

[Ruben Van de Velde]

At least several, I'd say - obtain is a version of cases with a little more bells and whistles (like the rfl|hb1 bit)

[Ruben Van de Velde]

I think that's a reason I'm not a fan of finish; if you rely on it for the simple problems, you don't learn as much, and you suddenly have to start learning on the difficult problems :)

[Sam]

Is there a good list of which tactics to focus on learning? I've been using a lot of simp, intro, split, induction, rw, split_ifs, apply, exact, assumption, tauto, finish, and cases. But clearly there are some "obvious" ones that I've missed!

[Sam]

Tbh I've been bruteforcing my way through some of those, I don't fully understand them all yet.

[Kyle Miller]

finish is being phased out of mathlib since it's not being ported to Lean 4.

My understanding is that it uses some Z3-like algorithms (SMT solving), and it uses lemmas with the ematch attribute.

[Kyle Miller]

I'm under the impression that it doesn't use simp

[Damiano Testa]

In terms of tactics, I think that the most common that I use are refine and rcases, the occasional rw and, when I want to fast-forward, convert. (I mentioned tactics that you did not mention, the ones in your list are also common.)

[Kyle Miller]

tactic#tidy is nice as an auto-solver sometimes

[Sam]

Oh, I forgot about tidy! That actually works for the example I posted.

[Sam]

Ah, so no finish in mathlib going forward, good to know! I hadn't realised it was SMT like! That explains the slowness.

[Sam]

Thanks for that list @Damiano Testa, I'll make a note to learn those.

[Kyle Miller]

You can do tidy? to have it output the proof it came up with. Sometimes you can hand-edit a reasonable proof out of it.

[Damiano Testa]

Ah, Kyle's mention of tidy made me remember of ext, which is also useful!

[Sam]

In mathlib, would it be considered better to inline tidy?'s result in the code? For the example I posted, it gives this:

  cases h,
  cases h_h,
  cases h_h_left,
  work_on_goal 1 {
    induction h_h_left,
    fsplit,
    work_on_goal 2 {
      fsplit, work_on_goal 1
      { solve_by_elim },
      assumption
    }
  },
  fsplit,
  work_on_goal 2 {
    fsplit,
    work_on_goal 1
    { assumption },
    assumption
  },

Is it reasonable to just put that in the proof? Is it acceptable to leave it just as tidy?

[Sam]

Do these automatic tactics ever have regressions when mathlib updates? That seems like it would be a reason not to use them.

[Damiano Testa]

I have found that the relative proportion of tactics that I use changed quite a bit with time. Initially, I used tidy, simp, dsimp, apply a lot. Later, I started preferring refine to apply to get finer control, I did not try simp/tidy on everything, but just when they were likely to make progress, started replacing rw by carefully reformulating statements to avoid needing it (when possible).

[Damiano Testa]

The chain of cases can likely be replaced by the output of rcases? h: try it out!

[Damiano Testa]

I am making the wild guess that the output of tidy above can be compacted to 3, max 4 lines.

[Damiano Testa]

(I'm not at a computer now, so cannot actually take my own challenge!)

[Sam]

Well we know

  obtain ⟨b, rfl|hb1, hb2⟩ := h,
  { contradiction },
  { exact ⟨b, hb1, hb2⟩ },

is equivalent to that tidy because @Ruben Van de Velde already found it! So yes, 3 lines. I'll give the rcases route a go!

[Damiano Testa]

Ah, i did not realize it was the same example! :face_palm:

[Kyle Miller]

By the way, this is a proof of that too:

begin
  rw list.containsp at h ⊢,
  tidy,
end

[Sam]

Hah. Every time I think I'm getting better at making my proofs more succinct, somebody comes along and shows her verbose I was still being! The versions I wrote today are already better than the ones I wrote yesterday, so progress is in the right direction at least.

[Damiano Testa]

There is always someone on Zulip who has a shorter proof.

[Damiano Testa]

You'd be surprised by how infinite descent plays out with Lean.

[Damiano Testa]

This is what I obtained by using tidy? and then golfing:

begin
  rw [list.containsp] at h ⊢,  -- this can be replace by the two simps that you had
  rcases h with ⟨h, rfl | h1, h2⟩,  -- takes care of the chain of `cases` and some of the `induction`s
  exact (q h2).elim,  -- this is the contradiction
  exact ⟨h, h1, h2⟩,  -- this is the other `split` and then the `assumption`s
end

[Sam]

Nice, thanks! I can't remember how small I got it by golfing, but you definitely did better than I did!

I've left it as tidy for now. Of course by line count that's the smallest, and tidy seems relatively common in mathlib, so is there a good reason to prefer to inline it instead of leaving it as tiny?

[Damiano Testa]

In this specific case, tidy does not call "non-terminal simps", so replacing tidy by the output of tidy? would just be for performance issues. If I remember correctly, though, tidy tries simp and dsimp "in the middle" and non-terminal (d)simps should be avoided.

[Stuart Presnell]

I set myself the project of eliminating the use of finish from the main body of mathlib back in December. I found tidy? was a good substitute in a lot of cases, generating an inelegant proof that I could then edit into a reasonable form, which was a good exercise in learning how to golf a proof.

[Ruben Van de Velde]

This is probably too short to be helpful:

@[simp]
lemma list.containsp_cons_of_neg
{α : Type u}
{a : α}
{l : list α}
{p : α → Prop} [decidable_pred p]
(q : ¬ p a)
(h: (a::l).containsp p) :
l.containsp p :=
begin
  simp only [list.containsp, list.mem_cons_iff] at h,
  simp only [list.containsp],
  exact h.imp (λ b hb, ⟨hb.1.resolve_left (λ hb', q (hb' ▸ hb.2)), hb.2⟩),
end