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.
Sebastian Ertel has marked this topic as resolved.
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.
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.
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.
No problem, we were just led on the very wrong track when searching for the problem. Thanks again for the clarification.
Yes, I apologise for this.
@Théo Winterhalter have you considered module locking, probably using coq-elpi's mlock? That one creates truly opaque constants.
See https://github.com/LPCIC/coq-elpi/tree/master/apps/locker#example-of-mlock
No I wasn't aware of that.
I think this is what MathComp already uses, right? rewrite unlock
and so on
Sure, coq-elpi just saves boilerplate for both styles of math-comp locking.
The selling point of mlock is that it uses the more robust kind of locking without needing all that excessive boilerplate
sigh, is there even any paper on locking? I think we have seen that the knowledge about it can be sparse in the community
Seems like this should be textbook-published
MCB at least has:
The
bigop
constant is “locked” to make the notation steady. To unravel its computational behavior one has to rewrite with theunlock
lemma.
... but not exactly the deepest explanation
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?
The keyword Axiom isn't introducing axioms there: that's a Module Type.
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.
Paolo Giarrusso said:
The keyword Axiom isn't introducing axioms there: that's a Module Type.
Sorry, I read too fast. :sweat_smile:
Indeed it sounds better! Thanks.
Last updated: Oct 13 2024 at 01:02 UTC