Zulip Chat Archive

Stream: general

Topic: exact this

Patrick Massot (Jul 25 2018 at 22:10):

Today I came across several instance of have := stuff, exact this closing a goal where exact stuff doesn't. I guess this is yet another elaboration subtlety, but I'd like to know if there is a nicer way to do this in one tactic.

Mario Carneiro (Jul 26 2018 at 01:31):

I use Chris's trick: exact (stuff : _)

Patrick Massot (Jul 26 2018 at 07:51):

Thanks!

Patrick Massot (Jul 26 2018 at 15:56):

Could we get a mathlib tactic replacing exact which tries exact and then Chris's trick?

Patrick Massot (Jul 26 2018 at 15:57):

@Sebastian Ullrich : is this a well known bug or a feature?

Sebastian Ullrich (Jul 26 2018 at 15:58):

I'll go with feature

Patrick Massot (Jul 26 2018 at 15:58):

Too easy...

Patrick Massot (Jul 26 2018 at 15:59):

Seriously, what do I miss to understand this thing?

Sebastian Ullrich (Jul 26 2018 at 16:02):

I mean, it's clear that omitting the expected type can lead to different elaboration results in some cases, and in some of these cases, the result without expected type may even be preferable. Whether that is something that could be improved in the elaborator can only be decided on a case by case basis.

Patrick Massot (Jul 26 2018 at 16:05):

I sort of understand this. What I don't get is how (stuff : _) differs from not specifying the expected type of stuff. Here we really mean underscore, this is not an abbreviation for Zulip purposes.

Sebastian Ullrich (Jul 26 2018 at 16:14):

Where do you not specify it? If you use exact stuff, the expected type is the goal.

Sebastian Ullrich (Jul 26 2018 at 16:14):

In both have := stuff and (stuff : _), there is no expected type

Patrick Massot (Jul 26 2018 at 16:23):

I mean exact stuff versus exact (stuff : _), both meant to close the current goal.

Patrick Massot (Jul 26 2018 at 16:23):

Sometimes only the later succeeds

Sebastian Ullrich (Jul 26 2018 at 16:31):

As I said, only in exact stuff do you have an expected type. It's the goal.

Patrick Massot (Jul 26 2018 at 16:31):

Sorry I'm slow.

Patrick Massot (Jul 26 2018 at 16:32):

But it's really really hot here

Sebastian Ullrich (Jul 26 2018 at 16:33):

I'm very grateful to spend the remaining summer in the land of air conditioning :)

Patrick Massot (Jul 26 2018 at 16:33):

USA?

Sebastian Ullrich (Jul 26 2018 at 16:41):

Yes, I'm doing an internship under Leo until October

Patrick Massot (Jul 26 2018 at 16:41):

Oooh, that sounds like a very good idea!

Luis Castillo (Aug 22 2022 at 08:03):

Hi, all! I have a doubt with the exact tactic. My local context is:

hQ: Q ∉ r
H: P = Q
hP: Q ∈ r
⊢ false

and typing "exact hQ hP," closes the goal, but typing "exact hP hQ," does not. I don't understand why. Could sb explain me the difference?

Yaël Dillies (Aug 22 2022 at 08:07):

Q ∉ r is definitionally Q ∈ r → false. Q ∈ r is not definitionally Q ∉ r → false. This requires double negation elimination (docs#not_not)

Last updated: Dec 20 2023 at 11:08 UTC