Thibaut Pérami (Nov 05 2022 at 12:16): Thibaut Pérami (Nov 05 2022 at 12:16):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.
In particular injection, inversion, destruct, 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
With ca1 and ca2 being constants of type ta that are actually declared Opaque. Then, if the user wants to obtain ca1 = ca2 and does injection H, injection will immediately expose the insides to ca1 and 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 ca1 and 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
Paolo Giarrusso (Nov 05 2022 at 12:25):Sealing/locking works on inductives as well, tho it's pretty verbose (and would block vm_compute)
Paolo Giarrusso (Nov 05 2022 at 12:27):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)
Paolo Giarrusso (Nov 05 2022 at 12:28):coq-elpi has some existing support for locking definitions with less boilerplate
Thibaut Pérami (Nov 05 2022 at 12:34):What do you mean by sealing/locking?
Thibaut Pérami (Nov 05 2022 at 12:34):And yes blocking vm_compute is really annoying for my use case
Thibaut Pérami (Nov 05 2022 at 12:35):Here I'm talking about ta = gset _ in stdpp so we need to compute on it at some point.
Thibaut Pérami (Nov 05 2022 at 12:38):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 injection treat Opaque constant as Opaque is probably a better solution than focusing on the inductive type itself
Paolo Giarrusso (Nov 05 2022 at 13:13):locking: https://github.com/LPCIC/coq-elpi/tree/68f51f56291953171586a124892705736a131b45/apps/locker
Last updated: Sep 23 2023 at 14:01 UTC