GitLab

Over the last few days, when reflecting the way we introduce assumptions in our proofs, I came to the conclusion that I am somewhat uneasy with globally setting Generalizable All Variables. Imagine we had a type spropC, an OFE, and then consider the following preamble:

Section something_about_sprop.
  Conext `{authG Σ (exR spropC)}.

Can you spot what's wrong with this? Well, we just assumed that SProp is discrete, which it is not. Ouch.

From my experiments, we can avoid over-eager generalization by adding a !. I have not found conclusive documentation for !, but it seems the least we should do is (a) add ! basically everywhere, and (b) treat the absence of ! as a big fat warning bell during code review. The latter will be hard.

But really, while Generalizable All Variables is very useful for some things (like the general fin map libraries in std++), I think for most code the benefits are slim. I have ported a few files to Generalizable No Variables, and the additional declarations required are negligible IMO. So I think what we should aim for (but that might take a while) is for std++ to no longer set Generalizable All Variables (to avoid inflicting this subtle issue onto unsuspecting users), and to locally set that flag in the (few) files that really benefit.

Or maybe I am overreacting, and things are not that bad. But the thought of accidentally assuming things I don't want to assume makes me nervous. What do you think?