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.

`Lemma upn_comp uprenn ...`

means `uprenn`

is a local variable in this lemma

oh, that should have been `upn_comp_uprenn`

, I spent like an hour trying to see where is the opaque.

thanks for pointing out the problem

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

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

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.

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

Last updated: Jun 24 2024 at 14:01 UTC