Paolo Giarrusso (Oct 25 2020 at 15:11): Paolo Giarrusso (Oct 25 2020 at 15:11):Does Software Foundations introduce anywhere the concept of abstraction barriers in proofs?
Paolo Giarrusso (Oct 25 2020 at 15:13):"abstraction barrier" in the sense used in math-comp — each definition D is a (light) abstraction barriers, to be only unfolded in the theory of D, or by simplification and definitional equality, but not elsewhere
Paolo Giarrusso (Oct 25 2020 at 15:14):Many proofs are instead in an "unfold and mash" style: instead of providing theories for your definitions, unfold everything in your context and prove things painfully, maybe with some Ltac for automation.
Paolo Giarrusso (Oct 25 2020 at 15:15):That style _does_ have its uses, especially in syntactic proofs!
Paolo Giarrusso (Oct 25 2020 at 15:15):but other times, your proofs aren't just more fragile, but even bigger than they'd be.
Paolo Giarrusso (Oct 25 2020 at 15:17):At least, that's something I've started to observe over time, while learning about math-comp style — what I write is closer to math-classes/"iris" style, but similar properties apply.
Karl Palmskog (Oct 25 2020 at 15:18):you mean locked definitions, right? Never seen them anywhere but mathcomp, really
Paolo Giarrusso (Oct 25 2020 at 15:19):stdpp/iris use seal instead
Paolo Giarrusso (Oct 25 2020 at 15:19):but no, I did mean definitions
Paolo Giarrusso (Oct 25 2020 at 15:20):they're already opaque to tactics using syntactic matching
Paolo Giarrusso (Oct 25 2020 at 16:02):I was also a bit surprised when @Ralf Jung claimed they're already abstraction barriers, but in the end that makes sense, and it seems also math-comp's practice. Even when you can do a proof by unfolding something, you're encouraged to reuse an appropriate lemma instead.
Christian Doczkal (Oct 26 2020 at 08:40):I am not sure I can fully agree with the assessment of @Paolo Giarrusso . I think that one of the main reasons why one does not see a lot of unfold (i.e., rewrite /def) in mathcomp proofs is that the rewrite tactic of of ssreflect unfolds definitions in the goal if it does not find a visible pattern for the given rewrite rule. As I had to find out when trying to change the definition of rot, this is used all over the place, not just when establishing the basic theory of rotating lists. One might even say that this implicit unfolding of the rewrite tactic actively encourages relying on the concrete definition.
Michael Soegtrop (Oct 27 2020 at 16:20):I had intense discussions on the CUDW 2 years back with various people if Coq should have some integrated facilities to define levels of abstraction and e.g. ensure that simplification stays in this. This is especially important if different experts work together on one topic. But in the end this is quite tricky. E.g. if one works with Z which are defined based on positives one never wants to see anything of these internals unless one is proving a missing lemma about Z. On the other hand one needs to expand the positives based definitions to compute with Z. So a simplification algorithm would have to evaluate either down to a ground term or stop at the level where Z uses positives. The question is how this could be done in an efficient way. One would have to set some sort of backtracking point in evaluation whenever one leaves the currently desired level of abstraction,
I would very much appreciate improvements in this area - say a way to define symbols which belong to a certain level of abstraction - which when working with Z would include the constructors of positives but no functions on positives - and a way to tell Coq to stay at this level if possible.
Paolo Giarrusso (Oct 27 2020 at 23:32):@Michael Soegtrop I don’t know how to satisfy all those requirements fully — Coq’s simpl and cbn, together with Arguments, work toward _some_ of that (modulo the open bugs), but not fully. You can also have level of abstractions with something like locked definitions (in a slightly different setup)
Paolo Giarrusso (Oct 27 2020 at 23:33):at least with stdpp’s sealing pattern, each definition foo gets a separate unfolding lemma, and you can write a tactic that uses a certain list of unfolding lemmas.
Paolo Giarrusso (Oct 27 2020 at 23:34):in turn, the result can use other opaque definitions.
Michael Soegtrop (Oct 28 2020 at 09:53):One option which might improve things e.g. for numbers would be a way to say that certain definitions shall only be unfolded if certain arguments are free of variables or have other term classification properties.
Of cause I can write my own simplification functions which do exactly what I want - that's what I am doing - but this is not exactly nice.
Paolo Giarrusso (Oct 28 2020 at 21:08):"arguments are free of variables" good point, @Abhishek Anand was asking for that the other day
Paolo Giarrusso (Oct 28 2020 at 21:08):Arguments !_ does sth similar for the top-level constructor. Comparing with Hint Mode suggests adding Arguments -_ (I think) for that.
Michael Soegtrop (Oct 29 2020 at 10:12):I think what I would really want is a way to assign points to certain symbols and have a simplification function which minimizes the number of points in the resulting term. Ideally it should be possible to define abstraction layers and assign the points to the combination of symbol and abstraction layer. Then one can hide or show abstraction layers - hiding means the points for that layer are counted during simplification, showing a layer means the points are not counted. To make things easy it should be possible to define points to all defined symbols in a module, preferably after the facts - say "assign x points to all defined symbols in module y" rather than having a declaration like "all following definitions get x points in abstraction layer y". Of cause one has to treat constructor symbols and defined symbols differently. Constructor symbols usually should get 0 points so that a ground term has 0 points.
I didn't think too much about how compute intensive such an algorithm would be. Obviously it is not so that optimizing the arguments of a function call in a cbv evaluation scheme leads to optimal results since an outer function might have to look into structure in hidden abstraction layers in order to perform computation which might entirely remove this level of abstraction - think of the Z defined based on positives example I gave before. I think one would have to deliver a possibly dynamic (request based) list of possible head symbols and resulting point counts. Then one can decide in outer functions at a match if keeping the symbolic match or evaluating up to the head symbol on which the match could be reduced is better. But if this would be optimal, I don't know. Possibly it would be a good enough heuristic.
sameer gupta (Jan 06 2021 at 22:34):Test. I have trouble posting here
http://adam.chlipala.net/cpdt/html/Subset.html
Enrico Tassi (Jan 07 2021 at 07:47):Message received.
Last updated: Sep 23 2023 at 06:01 UTC