Sebastian Ertel (Sep 03 2023 at 19:21): Sebastian Ertel (Sep 03 2023 at 19:21):r_reflexivity_alt did not work and reported the same (lock) error.
rpost_weaken_rule does the job:
Lemma KG_real_vs_KG_true :
KG_ind true ≈₀ KG_ind false.
Proof.
eapply eq_rel_perf_ind_eq.
simplify_eq_rel x.
all: ssprove_code_simpl.
Fail eapply rsame_head.
Fail eapply rsame_head_alt.
eapply rpost_weaken_rule.
1:{ eapply rreflexivity_rule. }
intros.
move: H1; case eq_a0: a₀ => [b₀ s₀]; move => eq_a1 //=.
move: eq_a1; case eq_a1: a₁ => [b₁ s₁]; move => eq_b_s.
by [injection eq_b_s => eq_s eq_b].
Qed.
Why did this problem arise?
It seems like none of the other SSProve examples had this problem.
Notification Bot (Sep 03 2023 at 19:22):Sebastian Ertel has marked this topic as resolved.
Théo Winterhalter (Sep 03 2023 at 19:41):It's because the post-condition do not match with what is expected so unification fail. This is why I tried to have most rule end with pre and post being variables.
Sebastian Ertel (Sep 04 2023 at 07:05):Ah ok. So the problem was really not the locking but the unification of pre and post. Got it.
Thanks a lot for your help.
Théo Winterhalter (Sep 04 2023 at 07:26):Yes, the problem is that unification fails, but it tries to unfold many things which results in this stupid error message. I tried to solve this issue but never managed.
Sebastian Ertel (Sep 04 2023 at 07:45):No problem, we were just led on the very wrong track when searching for the problem. Thanks again for the clarification.
Théo Winterhalter (Sep 04 2023 at 09:14):Yes, I apologise for this.
Paolo Giarrusso (Sep 04 2023 at 10:46):@Théo Winterhalter have you considered module locking, probably using coq-elpi's mlock? That one creates truly opaque constants.
Paolo Giarrusso (Sep 04 2023 at 10:49):See https://github.com/LPCIC/coq-elpi/tree/master/apps/locker#example-of-mlock
Théo Winterhalter (Sep 04 2023 at 11:03):No I wasn't aware of that.
Karl Palmskog (Sep 04 2023 at 11:05):I think this is what MathComp already uses, right? rewrite unlock and so on
Paolo Giarrusso (Sep 04 2023 at 11:29):Sure, coq-elpi just saves boilerplate for both styles of math-comp locking.
Paolo Giarrusso (Sep 04 2023 at 11:30):The selling point of mlock is that it uses the more robust kind of locking without needing all that excessive boilerplate
Karl Palmskog (Sep 04 2023 at 11:31):sigh, is there even any paper on locking? I think we have seen that the knowledge about it can be sparse in the community
Paolo Giarrusso (Sep 04 2023 at 11:34):Seems like this should be textbook-published
Karl Palmskog (Sep 04 2023 at 11:38):MCB at least has:
The
bigopconstant is “locked” to make the notation steady. To unravel its computational behavior one has to rewrite with theunlocklemma.
Karl Palmskog (Sep 04 2023 at 11:39):... but not exactly the deepest explanation
Théo Winterhalter (Sep 04 2023 at 13:23):Paolo Giarrusso said:
See https://github.com/LPCIC/coq-elpi/tree/master/apps/locker#example-of-mlock
Wait, this introduces axioms? It's not great is it?
Paolo Giarrusso (Sep 05 2023 at 05:04):The keyword Axiom isn't introducing axioms there: that's a Module Type.
Paolo Giarrusso (Sep 05 2023 at 05:08):The way this is used, that creates constant with a body, but such that the body is completely invisible to clients (as if it were an axiom) even if it's visible to say coqchk.
https://coq.inria.fr/library/Coq.ssr.ssreflect.html motivates a bit the pattern:
we also use Module Type ascription to create truly opaque constants,
because simple expansion of constants to reveal an unreducible term
doubles the time complexity of a negative comparison. Such opaque
constants can be expanded generically with the unlock rewrite rule.
See the definition of card and subset in fintype for examples of this.
Théo Winterhalter (Sep 05 2023 at 05:59):Paolo Giarrusso said:
The keyword Axiom isn't introducing axioms there: that's a Module Type.
Sorry, I read too fast. :sweat_smile:
Théo Winterhalter (Sep 05 2023 at 06:00):Indeed it sounds better! Thanks.
Last updated: Oct 13 2024 at 01:02 UTC