Stream: Coq users

Topic: opaque function that I didn't set

walker (Apr 16 2023 at 18:40):

I have a very strange situation that I cannot reproduce outside its current big setup:

In some file in the path: theories/common/debruijn/structs.v

There is the following definition:

Definition uprenn (n: nat) := iterate (upren) n.
(*more stuff*)

(*note that this is the last lemma in the whole file*)
Lemma uprenSn n ξ: uprenn n.+1 ξ= upren( uprenn n ξ).
Proof.
by rewrite /uprenn /=. (*note that unfolding works here *)
Qed.

Then in another file in a different path theoris/e0/debruijn/facts.v There is the following:

Lemma uprenn_upn ξ n: @ren Term (uprenn n ξ) = upn n (ren ξ).
Proof.
unfold uprenn. (* goal is:  ren (iterate upren n ξ) = upn n (ren ξ)*)
print uprenn.
(*uprenn = [eta iterate upren]
     : nat -> (nat -> nat) -> nat -> nat

Arguments uprenn n%nat_scope a%function_scope _%nat_scope
*)
Admitted.
(*this is literally the next line, there is no stuff between the two lemmas*)
Lemma upn_comp uprenn σ ξ n:
@upn Term n σ ∘ uprenn n ξ = upn n (σ ∘ ξ).
Proof.
Fail rewrite /uprenn.
(*The command has indeed failed with message:
uprenn is opaque..*)
Fail unfold uprenn.
(*The command has indeed failed with message:
Cannot coerce uprenn to an evaluable reference.*)

I most certainly know that I didn't set uprenn to opaque, and even if I did the command: Transparent upenn doesn't make unfold or
rewrite work. At this point I am not entirely sure what is the problem.

Edit: I thought it is corrupted coq state, so I did make clean followed by make but the problem persists in this particular case.

Gaëtan Gilbert (Apr 16 2023 at 18:46):

Lemma upn_comp uprenn ... means uprenn is a local variable in this lemma

walker (Apr 16 2023 at 18:47):

oh, that should have been upn_comp_uprenn, I spent like an hour trying to see where is the opaque.

walker (Apr 16 2023 at 18:47):

thanks for pointing out the problem

Gaëtan Gilbert (Apr 16 2023 at 18:49):

interesting About uprenn would pick up the local one saying "uprenn is an hypothesis of the local context" but Print uprenn picks up the global one

walker (Apr 16 2023 at 18:50):

yes it does in both case, (I forgot to put in both cases).

walker (Apr 16 2023 at 18:51):

my inner OS engineer kicked in and I kept thinking of compiler bug somewhere that corrupted the internal representation of the function and that was why (at least in my mind) it couldn't unfold.

walker (Apr 16 2023 at 18:52):

thanks a lot for pointing out the issue, this is a thing I could have easily burned hours looking at

Last updated: Oct 04 2023 at 23:01 UTC