Stream: Coq users

Topic: assert vs have


view this post on Zulip Hugo Herbelin (Jan 26 2022 at 12:14):

Maybe the usual question: why are there assert and have which seem to do rather similar things. How to explain a user how to choose?

view this post on Zulip Ali Caglayan (Jan 26 2022 at 12:15):

One is default coq the other ssreflect 0:-)

view this post on Zulip Hugo Herbelin (Jan 26 2022 at 12:16):

You mean like emacs and vi, Proof General and coqide?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:28):

Basically have has many more features than assert , and assert has nothing over have as far as I can tell. If it was for me I'd just deprecate assert

view this post on Zulip Ali Caglayan (Jan 26 2022 at 12:30):

On the other hand assert does one thing and does it well so is in a sense more reliable. Many bigger proof scripts might require that. I don't know if "have" can fill the same role and I also don't know if people are willing to rely on ssreflect to use it.

view this post on Zulip Ali Caglayan (Jan 26 2022 at 12:32):

So I guess to answer Hugo's question fully: assert can be used, but is more simple. have is a cleverer version which can do all sorts of fancy things too that you might like.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:34):

In what sense is more reliable? have can do the exact thing that assert, in fact it has some extensions that once you are used to them, you can never go back to assert

view this post on Zulip Kenji Maillard (Jan 26 2022 at 12:34):

currently assert supports strict propositions while have does not yet

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:34):

I don't know if eassert is a thing

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:34):

FTR simple tactics are important for efficiency of proof scripts

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:35):

like, you want both a swiss knife and a spoon

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:35):

You mean @Pierre-Marie Pédrot like the 50% speedup people saw in some projects when switching from Coq's rewrite to ssreflect rewrite?

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:35):

rewrite is another beast

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:35):

have has more features but it doesn't make it slower per-se

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:35):

precisely, the vanilla Coq rewrite is too clever for its own good

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:35):

feel free to bench, but I guess they should be equivalent

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:36):

no, it's not about that

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:36):

already Assia's example would be much more painful for me to write with assert

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:36):

it's about having access to low-level primitives you know what they do

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:36):

ssr asser is doing random stuff with patterns and whatnot IIRC

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:36):

When I'm writing proofs I don't care that at all

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:36):

I know what have does

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:36):

making my life much better

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:36):

you're missing the point

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:36):

I don't see where the mistery in in have H : T.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:36):

Because it has more features, features that I can't live without

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:36):

because it has to compute evars, solve stuff and decide accordingly

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:37):

when the low-level assert is mostly O(1)

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:37):

Yes and that's essential

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:37):

not for all use-cases

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:37):

If that were a need have would have a flag to do that

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:37):

no!

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:37):

flags are bad

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:37):

they don't compose well

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:37):

bah that's FUD evidence strongly suggests otherwise

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:37):

once again, no

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:37):

I don't know anyone who would prefer assert after having used have

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:38):

a lot of the contraptions developed by @Jason Gross are trying to work around the built-in cleverness of tactics

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:38):

you're missing the point, again

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:38):

you are maybe talking about destruct

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:38):

neither

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:38):

have is not "clever"

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:38):

it just has more features

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:38):

it is

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:38):

in which way it is "clever"

view this post on Zulip Ali Caglayan (Jan 26 2022 at 12:38):

@Emilio Jesús Gallego Arias We aren't suggesting you use assert everywhere, have is definitely an improvement on the user side. If I have a big fancy proof script that uses assert rather than have, now adding features to have can make that script break. assert on the other hand has a very clear function.

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:38):

the context is Ltac scripts, not proofs

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:39):

have also has a very clear function, how is have H : T not clear?

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:39):

because it computes more stuff and is not O(1)

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:39):

Pierre-Marie Pédrot said:

the context is Ltac scripts, not proofs

LTAC is a terrible thing I'm not gonna accept it as evidence :)

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:39):

whatever

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:39):

when writing OCaml tactics that's the same

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:39):

What was claimed was

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:39):

you don't want to call ssr

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:39):

or Coq's assert either actually

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:40):

that assert is more reliable; modulo the SProp bug

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:40):

you want the low-level stuff that tells you "just push that into the env"

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:40):

there is not evidence for that

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:40):

Pierre-Marie Pédrot said:

or Coq's assert either actually

exactly

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:40):

that point I buy

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:40):

and agree

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:40):

but Coq assert is more predictible

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:40):

in what sense?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:40):

show me an example where it is

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:41):

performance !

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:41):

ssr assert does a lot of stuff behind the scenes

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:41):

we are talking about what?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:41):

2 milliseconds?

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:42):

no!

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:42):

it saves me hours per week

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:42):

then what's the performance delta @Pierre-Marie Pédrot ?

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:42):

you're missing the point, again

view this post on Zulip Ali Caglayan (Jan 26 2022 at 12:42):

Doing have 1000 times in a proof script will mean a 2second increase for 2 millisecond differences

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:43):

this

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:43):

Pierre-Marie Pédrot said:

this

didn't you just said that assert shouldn't be used in that case?

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:43):

and it's not linear because it depends on the size of the term and whatnot

view this post on Zulip Janno (Jan 26 2022 at 12:43):

I think assert is also more predictable in the shape of the goal it produces. ssrtactics (including have) turn TC instances that couldn't be found into quantifiers. assert simply complains about them missing instead of giving a goal that looks different than what you expected.

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:43):

Coq's assert is dumber than ssr have

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:43):

dumb != worse

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:44):

I'm talking about a human using a tactic

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:44):

proof automation is a completely different beast

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:44):

which is precisely you missing the point

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:44):

and the least of my worries would be assert vs have

view this post on Zulip Ali Caglayan (Jan 26 2022 at 12:44):

Nobody here is claiming that assert is better than have for a user

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:44):

I would worry more to start with about the engine taking a linear amount of memory on the number of proof steps

view this post on Zulip Ali Caglayan (Jan 26 2022 at 12:44):

we are just refuting you saying "lets get rid of assert we have have"

view this post on Zulip Ali Caglayan (Jan 26 2022 at 12:45):

assert has uses that have cannot fulfill nor should it need to

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:45):

this tension is pervasive, even within Coq tactics

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:46):

ssr is leaning by design towards expressivity and human proofs

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:46):

in Coq's tactics we have a hodgepodge of both approaches

view this post on Zulip Pierre-Marie Pédrot (Jan 26 2022 at 12:46):

in part because of stupid syntactic considerations mostly Ltac-specific

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:47):

Anyways I should know better than to take the bait, sorry folks :)

view this post on Zulip Ali Caglayan (Jan 26 2022 at 12:47):

:-)

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:48):

For me the original "How to explain a user how to choose?" was understood as a user writing a proof like the one shown here

view this post on Zulip Théo Zimmermann (Jan 26 2022 at 13:14):

Emilio Jesús Gallego Arias said:

I don't know if eassert is a thing

Yes, it exists.

view this post on Zulip Hugo Herbelin (Jan 26 2022 at 13:22):

As said in another post (which now moved in another thread), discussing about have vs assert from a user point of view is a trap, as if we were customers of Coq while we are actually developers of Coq. The real question is about where we want to put our energy and I don't think that we can go anywhere interesting by using our energy in non-concluding flames rather than trying to gather the best of what we know to do, necessary step to go beyond what we currently exists and not be stuck.

view this post on Zulip Enrico Tassi (Jan 26 2022 at 13:47):

I think that one misconception here is that basic tactics, like assert or have, have been given the status of "basic building blocks" for larger pieces of automation. They are not designed for that, even assert is too high level and has too few flags. It is better explained on other tactics, like ring: when writing proof automation I'd better know if the tactic failed because the goal is outside the supported domain, or because the goal is false. Running the tactic and try something else on failure is not a nice API.

view this post on Zulip Enrico Tassi (Jan 26 2022 at 13:48):

So IMO you should not compare have and assert on that respect, they both suck IMO for that purpose.

view this post on Zulip Paolo Giarrusso (Jan 26 2022 at 15:46):

Not just for automation, @Enrico Tassi , but also for Defined terms. I've seen sometimes that translating a proof script from plain ltac to ssreflect sometimes introduces extra noise.

view this post on Zulip Enrico Tassi (Jan 26 2022 at 16:40):

I agree, there is little care in ssr into making proof terms nice, it is not really an objective of ssr.

view this post on Zulip Hugo Herbelin (Jan 27 2022 at 14:31):

Enrico Tassi said:

I agree, there is little care in ssr into making proof terms nice, it is not really an objective of ssr.

That could precisely be a point where the two implementations could learn the one from the others :)

view this post on Zulip Cyril Cohen (Jan 27 2022 at 15:30):

It seems from this discussion that "user" is not uniquely defined :wink:. Maybe we should partition users by class (e.g "ltac users" vs "human readable scripts don't care about the term" vs "human readable scripts and terms"), dispatch all existing tactics in these groups, deprecate the ones that are subsumed by another in any of these classes and then write one doc per class?

view this post on Zulip Cyril Cohen (Jan 27 2022 at 15:32):

And then, only then we can work on a minimal covering

view this post on Zulip Julien Puydt (Jan 27 2022 at 16:25):

Well, computer power doubles every few months while brains are mostly the same since hundred of thousands of years -- I say: let the computers cope with big terms and prefer readable proofs!

view this post on Zulip Karl Palmskog (Jan 27 2022 at 16:27):

I can understand that the core team is concerned with tactic languages (or proof languages) working well. But should individual tactics really be a focus for core?

view this post on Zulip Paolo Giarrusso (Jan 27 2022 at 16:49):

@Julien Puydt humans must cope with Defined terms.

view this post on Zulip Paolo Giarrusso (Jan 27 2022 at 16:51):

@Julien Puydt and computer power can't solve exponential problems like those from Coq... (Technically, you also have O(n^6) problems, and superexponential ones).


Last updated: Feb 01 2023 at 13:03 UTC