sufficesI

Stream: general

[Yaël Dillies]

Could we have an "instance version" of tactic#suffices? This would complete the have, haveI, suffices square.

[Reid Barton]

Do you have a practical use in mind for it?

[Yaël Dillies]

It has the same applications as haveI. For example I have this proof

  haveI : is_empty {a // b a = k},
  { refine subtype.is_empty_of_false _,
    rintro a rfl,
    exact hbk (finset.mem_image_of_mem _ $ finset.mem_univ _) },
  exact det_is_empty,

This would read slightly better as

  sufficesI : is_empty {a // b a = k},
  { exact det_is_empty },
  refine subtype.is_empty_of_false _,
  rintro a rfl,
  exact hbk (finset.mem_image_of_mem _ $ finset.mem_univ _),

[Reid Barton]

Ideally is_empty would not be a class in the first place, and you could just write apply det_is_empty and then the rest.

[Yaël Dillies]

Sure, but

1. It should be a class
2. My specific problem has little to do with the tactic gap that I just uncovered

[Reid Barton]

But I think this is really a representative example--my biggest problem with type class abuse is precisely that it makes these kinds of proofs more awkward. In the best case you make I duplicates of a bunch of tactics but it's still worse than just proving stuff normally; here you had to spell out the exact is_empty statement you need.

[Reid Barton]

I think what would make the situation more tolerable is something like an apply tactic that turns failed instance searches into new goals

[Yaël Dillies]

We should either have both haveI and sufficesI or none of them, because they fulfill the exact same role. Is your solution to delete haveI?

[Reid Barton]

??

[Yaël Dillies]

There's a mismatch between have and suffices. This mismatch shouldn't exist. What is your solution to it?

[Reid Barton]

Why do I need a solution?

[Reid Barton]

I think adding sufficesI is okay; but it doesn't address the real issue

[Yaël Dillies]

Sure, we can also add applyI which does what you say. I think this would be ideal.

[Adam Topaz]

We have apply_with

[Adam Topaz]

And you can just use suffices : foo, { resetI, bar }.

[Yaël Dillies]

How does one use apply_with?

[Adam Topaz]

apply_with ... { instances := ff }

[Reid Barton]

Does that mean all instance arguments will become new goals? That's probably not ideal either

[Adam Topaz]

Yeah, that's what it does. When I do it I usually have to do any_goal { apply_instance } right after

[Damiano Testa]

It might be that adding a tactic.swap at the end of the haveI tactic would generate the sufficesI tactic.
I'm not at a computer, so cannot check now, though.

[Kyle Miller]

You could use tactic#exactI here:

  suffices : is_empty {a // b a = k},
  { exactI det_is_empty },
  refine subtype.is_empty_of_false _,
  rintro a rfl,
  exact hbk (finset.mem_image_of_mem _ $ finset.mem_univ _),

Or there's

  suffices : is_empty {a // b a = k},
  unfreezingI { exact det_is_empty },
  refine subtype.is_empty_of_false _,
  rintro a rfl,
  exact hbk (finset.mem_image_of_mem _ $ finset.mem_univ _),

but tactic#unfreezingI doesn't focus the goal.

[Kyle Miller]

For longer proofs inside the first suffices goal, you can put tactic#resetI at the beginning. I think the value-add of haveI is that you don't have to do have : foo, { ...}, resetI, ... with the resetI potentially far away from the have.