Stream: Coq users

Topic: reflexivity breaks `simpl never` encapsulation


view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Dec 04 2023 at 17:26):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Dec 04 2023 at 21:18):

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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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 )

view this post on Zulip 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?

view this post on Zulip Cyril Cohen (Dec 05 2023 at 11:19):

To me hiding and encapsulation are two distinct problems:

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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Dec 05 2023 at 14:21):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Jun 22 2024 at 15:01 UTC