Hugo Herbelin (Jan 26 2022 at 12:14): 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?
Ali Caglayan (Jan 26 2022 at 12:15):One is default coq the other ssreflect 0:-)
Hugo Herbelin (Jan 26 2022 at 12:16):You mean like emacs and vi, Proof General and coqide?
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
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.
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.
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
Kenji Maillard (Jan 26 2022 at 12:34):currently assert supports strict propositions while have does not yet
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:34):I don't know if eassert is a thing
Pierre-Marie Pédrot (Jan 26 2022 at 12:34):FTR simple tactics are important for efficiency of proof scripts
Pierre-Marie Pédrot (Jan 26 2022 at 12:35):like, you want both a swiss knife and a spoon
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?
Pierre-Marie Pédrot (Jan 26 2022 at 12:35):rewrite is another beast
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:35):have has more features but it doesn't make it slower per-se
Pierre-Marie Pédrot (Jan 26 2022 at 12:35):precisely, the vanilla Coq rewrite is too clever for its own good
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:35):feel free to bench, but I guess they should be equivalent
Pierre-Marie Pédrot (Jan 26 2022 at 12:36):no, it's not about that
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
Pierre-Marie Pédrot (Jan 26 2022 at 12:36):it's about having access to low-level primitives you know what they do
Pierre-Marie Pédrot (Jan 26 2022 at 12:36):ssr asser is doing random stuff with patterns and whatnot IIRC
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:36):When I'm writing proofs I don't care that at all
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:36):I know what have does
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:36):making my life much better
Pierre-Marie Pédrot (Jan 26 2022 at 12:36):you're missing the point
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:36):I don't see where the mistery in in have H : T.
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:36):Because it has more features, features that I can't live without
Pierre-Marie Pédrot (Jan 26 2022 at 12:36):because it has to compute evars, solve stuff and decide accordingly
Pierre-Marie Pédrot (Jan 26 2022 at 12:37):when the low-level assert is mostly O(1)
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:37):Yes and that's essential
Pierre-Marie Pédrot (Jan 26 2022 at 12:37):not for all use-cases
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:37):If that were a need have would have a flag to do that
Pierre-Marie Pédrot (Jan 26 2022 at 12:37):no!
Pierre-Marie Pédrot (Jan 26 2022 at 12:37):flags are bad
Pierre-Marie Pédrot (Jan 26 2022 at 12:37):they don't compose well
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:37):bah that's FUD evidence strongly suggests otherwise
Pierre-Marie Pédrot (Jan 26 2022 at 12:37):once again, no
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:37):I don't know anyone who would prefer assert after having used have
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
Pierre-Marie Pédrot (Jan 26 2022 at 12:38):you're missing the point, again
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:38):you are maybe talking about destruct
Pierre-Marie Pédrot (Jan 26 2022 at 12:38):neither
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:38):have is not "clever"
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:38):it just has more features
Pierre-Marie Pédrot (Jan 26 2022 at 12:38):it is
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:38):in which way it is "clever"
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.
Pierre-Marie Pédrot (Jan 26 2022 at 12:38):the context is Ltac scripts, not proofs
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?
Pierre-Marie Pédrot (Jan 26 2022 at 12:39):because it computes more stuff and is not O(1)
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 :)
Pierre-Marie Pédrot (Jan 26 2022 at 12:39):whatever
Pierre-Marie Pédrot (Jan 26 2022 at 12:39):when writing OCaml tactics that's the same
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:39):What was claimed was
Pierre-Marie Pédrot (Jan 26 2022 at 12:39):you don't want to call ssr
Pierre-Marie Pédrot (Jan 26 2022 at 12:39):or Coq's assert either actually
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:40):that assert is more reliable; modulo the SProp bug
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"
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:40):there is not evidence for that
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:40):Pierre-Marie Pédrot said:
or Coq's assert either actually
exactly
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:40):that point I buy
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:40):and agree
Pierre-Marie Pédrot (Jan 26 2022 at 12:40):but Coq assert is more predictible
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:40):in what sense?
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:40):show me an example where it is
Pierre-Marie Pédrot (Jan 26 2022 at 12:41):performance !
Pierre-Marie Pédrot (Jan 26 2022 at 12:41):ssr assert does a lot of stuff behind the scenes
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:41):we are talking about what?
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:41):2 milliseconds?
Pierre-Marie Pédrot (Jan 26 2022 at 12:42):no!
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:42):it saves me hours per week
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:42):then what's the performance delta @Pierre-Marie Pédrot ?
Pierre-Marie Pédrot (Jan 26 2022 at 12:42):you're missing the point, again
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
Pierre-Marie Pédrot (Jan 26 2022 at 12:43):this
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?
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
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.
Pierre-Marie Pédrot (Jan 26 2022 at 12:43):Coq's assert is dumber than ssr have
Pierre-Marie Pédrot (Jan 26 2022 at 12:43):dumb != worse
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:44):I'm talking about a human using a tactic
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:44):proof automation is a completely different beast
Pierre-Marie Pédrot (Jan 26 2022 at 12:44):which is precisely you missing the point
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:44):and the least of my worries would be assert vs have
Ali Caglayan (Jan 26 2022 at 12:44):Nobody here is claiming that assert is better than have for a user
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
Ali Caglayan (Jan 26 2022 at 12:44):we are just refuting you saying "lets get rid of assert we have have"
Ali Caglayan (Jan 26 2022 at 12:45):assert has uses that have cannot fulfill nor should it need to
Pierre-Marie Pédrot (Jan 26 2022 at 12:45):this tension is pervasive, even within Coq tactics
Pierre-Marie Pédrot (Jan 26 2022 at 12:46):ssr is leaning by design towards expressivity and human proofs
Pierre-Marie Pédrot (Jan 26 2022 at 12:46):in Coq's tactics we have a hodgepodge of both approaches
Pierre-Marie Pédrot (Jan 26 2022 at 12:46):in part because of stupid syntactic considerations mostly Ltac-specific
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:47):Anyways I should know better than to take the bait, sorry folks :)
Ali Caglayan (Jan 26 2022 at 12:47)::-)
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
Théo Zimmermann (Jan 26 2022 at 13:14):Emilio Jesús Gallego Arias said:
I don't know if
eassertis a thing
Yes, it exists.
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.
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.
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.
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.
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.
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 :)
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?
Cyril Cohen (Jan 27 2022 at 15:32):And then, only then we can work on a minimal covering
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!
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?
Paolo Giarrusso (Jan 27 2022 at 16:49):@Julien Puydt humans must cope with Defined terms.
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: Oct 03 2023 at 04:02 UTC