Stream: Coq users

Topic: reflexivity breaks `simpl never` encapsulation

Pierre Rousselin (Dec 04 2023 at 16:53):

I guess it is not really the intended goal. I am trying to prevent the students to randomly use simpl.
I've found out about simpl never.

Arguments Nat.add : simpl never.
Lemma plop : 2 + 2 = 4.
Proof.
  simpl. (* so far so good: nothing happens *)
  reflexivity. (* magic, magic *)
Qed.

Is there a way to actually force the students to always use rewrite?

Paolo Giarrusso (Dec 04 2023 at 17:26):

mlock gives you encapsulation: https://github.com/LPCIC/coq-elpi/tree/master/apps/locker

Pierre Rousselin (Dec 04 2023 at 17:38):

Thank you. I'm not sure it's very realistic to use coq-elpi for basic courses. But I will look at it, thanks.
Any hope it could be done without a hacky external translation?

Pierre Roux (Dec 04 2023 at 20:00):

You can always simulate the effect of mlock with a module and a module type to hide the definitions.

Paolo Giarrusso (Dec 04 2023 at 20:29):

That encoding is spelled out here https://github.com/LPCIC/coq-elpi/tree/master/apps/locker#example-of-mlock

Paolo Giarrusso (Dec 04 2023 at 20:31):

For a course... You might indeed have challenges, but the Coq platform comes with coq-elpi. However, mlock used to have issues with implicit arguments in the defined constant until recently (they're on coq-elpi's tracker)

Paolo Giarrusso (Dec 04 2023 at 20:33):

ssreflect has lighter-weight encodings with varying robustness - usually they break convertibility (and reflexivity), but your definition still has a body that can be unfolded. It's probably fine for students.

Paolo Giarrusso (Dec 04 2023 at 20:34):

And FWIW, simpl never isn't even supposed to mean "simpl should never unfold this definition". Coq devs say that's intended, even if I find this terrible naming.

Paolo Giarrusso (Dec 04 2023 at 20:34):

Opaque Nat.add will actually block simpl, but it will not block reflexivity, or apply in the goal.

Karl Palmskog (Dec 04 2023 at 20:43):

for the record, one of the key points of the Platform is to break "dependency aversion", i.e., to allow people to use non-Stdlib to solve practical problems like locking in a casual way

Karl Palmskog (Dec 04 2023 at 20:46):

do students even need to be aware that some file/module they're using is using coq-elpi?

Paolo Giarrusso (Dec 04 2023 at 21:18):

If they install Coq using the platform, they shouldn't need to

Pierre Rousselin (Dec 05 2023 at 06:15):

I'm using jscoq, so it seems there is still one place where it's not convenient.

Cyril Cohen (Dec 05 2023 at 10:49):

Pierre Rousselin said:

Thank you. I'm not sure it's very realistic to use coq-elpi for basic courses. But I will look at it, thanks.
Any hope it could be done without a hacky external translation?

No, not without hacking Coq's kernel, so one would rather program on top of Coq rather than inside it...

Cyril Cohen (Dec 05 2023 at 10:49):

To me it sounds like a XY problem and the proper solution would be to fix jscoq instead (ping @Emilio Jesús Gallego Arias )

Pierre Rousselin (Dec 05 2023 at 11:03):

Then, how unreasonable would it be to hack the kernel to have something like that? Is it theoretically problematic?

My two most recent posts (and quite a few others) always point in the same direction: it seems to me that Coq lacks primitive ways to hide and encapsulate. Require 1 file, and you transitively populate your global context with (literally) thousands of identifiers + Setoid. Hiding a definition is made difficult.

This is not only an issue with teaching. If libraries could enforce things like "This file works with these types, these opaque definitions and only uses these results", without having to redefine everything, wouldn't they be a lot more robust?

Cyril Cohen (Dec 05 2023 at 11:19):

To me hiding and encapsulation are two distinct problems:

• hiding should look the same from Coq's kernel point of view, but affect only the user experience in the display: mostly in Search, but also to a lesser extent to Check, About and Print which should be able to tell the user something is meant to be hidden and recommend looking elsewhere. There I agree Coq fundamentally lacks support, whether it should be added as an external plugin (e.g. elpi programmed, meta-coq programmed or coq-lsp-like programmed) or inside Coq itself should not be that relevant in the presence of the Coq platform and of software that can import it fully.

• "encapsulating" (the way I guess you mean it) is a fundamental operation that blocks reduction, and that has heavy consequences: if you do it after the fact, then things that used to typecheck may not anymore... and the feature to do it asap and export it is already here and has three implementations, namely 1. Lambda abstraction 2. Qed and 3. Module types.

  1. lambda abstraction is what you do when you make primitive abstract interfaces, using structures or classes for example. In the case of your 2 + 2 example, for example in a mathcomp semiRingType, 2 + 2 does not reduce and reflexivity on 2 + 2 = 4 will thus fail. (The usual way to solve this is to push coercions to the top and rely on reduction to solve the goal).
  2. Qed is a way to tell Coq something is opaque, and that's the one which is used in the implementation of lock.
  3. Module types is another way to tell Coq something is opaque, by isolating the implementation and the declared constant via an abstract signature which must continue to typecheck even when we do not have access to the bodies, which guarantees that the above-mentioned problem does not arise when exiting the module. This is what is used behind the implementation of mlock. One potential feature that could be added there is subsequent module reopening, but I do not think it would help you.

My conclusion: if you want 2 + 2 not to compute just don't use nat, use an abstraction of it (I recommend 1. for generality and 3. for simplicity, 2. is just painful)

Cyril Cohen (Dec 05 2023 at 11:29):

PS: simpl never is a directive for simplification heuristics (which is still broken in many cases btw) and will not affect reduction.

Another hack you may want try: forbid reflexivity and any other tactic that rely on it and provide your own set of tactic in a way that does not exploit conversion: e.g. add a layer to reflexivity which first test syntactic equality, call reflexivity if the syntactic match succeeded and fail otherwise. This is a hard exercise to cover all tactics, especially because you might still need conversion here and there to avoid false negatives, and additionally conversion will still leak here and there, just because Coq's kernel cannot not use conversion. The advantage will be that all these tactics will be way faster than the original ones, and may be useful for more than just teaching indeed.

Pierre-Marie Pédrot (Dec 05 2023 at 14:20):

In the world of theory, tactics ought to respect the transparent state, i.e. if you add Opaque plus then reflexivity should fail on 2 + 2 = 4.

Pierre-Marie Pédrot (Dec 05 2023 at 14:21):

As usual, this is broken by most basic tactics because historical reasons.

Pierre-Marie Pédrot (Dec 05 2023 at 14:22):

If one day we manage to pull the unif-all off we could have replacement tactics not break this abstraction barrier.

Pierre Rousselin (Dec 05 2023 at 15:24):

Thank you very much for your answers. So I guess the conclusion is to use module duct tape for the time being and then ... a lot of work.

Emilio Jesús Gallego Arias (Dec 05 2023 at 17:56):

Cyril Cohen said:

To me it sounds like a XY problem and the proper solution would be to fix jscoq instead (ping Emilio Jesús Gallego Arias )

I'm afraid than other than Shachar volunteering when he can, there are 0 resources for jsCoq maintenance scheduled.

Last updated: Oct 13 2024 at 01:02 UTC