Does Software Foundations introduce anywhere the concept of abstraction barriers in proofs?
"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
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.
That style _does_ have its uses, especially in syntactic proofs!
but other times, your proofs aren't just more fragile, but even bigger than they'd be.
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.
you mean locked definitions, right? Never seen them anywhere but mathcomp, really
but no, I did mean definitions
they're already opaque to tactics using syntactic matching
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.
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
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.
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.
@Michael Soegtrop I don’t know how to satisfy all those requirements fully — Coq’s
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)
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.
in turn, the result can use other opaque definitions.
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.
"arguments are free of variables" good point, @Abhishek Anand was asking for that the other day
Arguments !_ does sth similar for the top-level constructor. Comparing with Hint Mode suggests adding Arguments -_ (I think) for that.
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.
Test. I have trouble posting here
Last updated: Sep 23 2023 at 06:01 UTC