Is it possible to make an inductive type "Opaque" for tactics that deal with inductive types? In some sense to make them believe it is not inductive.
split, ... should not work on it after it was made opaque. (
vm_compute should of course still see through). Otherwise, it is not really possible to maintain encapsulation. For example if I have a type
ta defined in some file
A which also defines all functions and lemmas needed to work with object of type
ta including automation tactics. Then the user imports
A, the user can be exposed to the inside of
A inadvertently. For example if the context is:
H : Some ca1 = Some ca2
ca2 being constants of type
ta that are actually declared
Opaque. Then, if the user wants to obtain
ca2 and does
injection will immediately expose the insides to
ca2 (even if they are opaque). In particular if
A provided an automation tactic able to decide that actually
ca1 ≠ ca2.
I agree that in the manual case this can be resolved by manually applying a lemma like:
Lemma Some_inj X (a b : X) : Some a = Some b -> a = b.
But as soon has you have automation tactics that try to do injections in the middle, then you cannot prevent the inside of
ca2 from being exposed, and then the automation with failed because it knows nothing about the inside of object of type
ta and shouldn't have to.
Another way of solving this is to decide that it is a bug for
injection and related tactics to be able to see through opaque definitions. That way the only way they could expose internal code is if it was already present in the context or under a transparent definition
Sealing/locking works on inductives as well, tho it's pretty verbose (and would block vm_compute)
OTOH, Opaque does not achieve any real sort of information hiding, not even for definitions: it doesn't stop the typechecker from unfolding definitions (and can't), and doesn't stop unification (even if it could, modulo backwards compatibility)
coq-elpi has some existing support for locking definitions with less boilerplate
What do you mean by sealing/locking?
And yes blocking
vm_compute is really annoying for my use case
Here I'm talking about
ta = gset _ in
stdpp so we need to compute on it at some point.
I guess that indeed
Opaque should just mean "don't open accidentally", not "you can't open it". This makes me think that just having
Opaque constant as Opaque is probably a better solution than focusing on the inductive type itself
Last updated: Jan 29 2023 at 01:02 UTC