Question
Does Opaque foo
indeed subsume Typeclasses Opaque foo
, as you’d expect?
Background
I’m revising this code:
Global Typeclasses Opaque foo.
Global Opaque foo.
If I swap these statements, Typeclasses Opaque
gives “Cannot coerce to_subst to an evaluable reference.”
For “Ideal Coq”, that means Typeclasses Opaque
is redundant, but I’ve learned we don’t have that yet, so it’d be good to know for sure. Docs for either Opaque
, Typeclasses Opaque
and Hint Opaque
say little except document that Opaque
isn’t really opaque:
Opaque has also an effect on the conversion algorithm of Coq, telling it to delay the unfolding of a constant as much as possible when Coq has to check the conversion (see Section Conversion rules) of two distinct applied constants.
We also have a couple of issues on Opaque
, which is why I’m especially uncertain.
opened 05:57PM - 04 Dec 18 UTC
part: elaboration
kind: bug
part: apply
`apply` seems to ignore opacity when no evars are involved
```coq
Definition t… (n : nat) := n.
Global Opaque t.
Parameter P : nat -> Prop.
Goal forall n, P (t n) -> P n.
intros n H. apply H. (* refine H also works *)
Qed.
```
However here, opacity is apparently taken into account by `apply`, but still not by `refine`.
```coq
Definition t (n : nat) := n.
Global Opaque t.
Parameter P : nat -> Prop.
Goal (forall n, P (t n)) -> forall n, P n.
intros H n. Fail apply H. refine (H _).
Qed.
```
opened 12:05PM - 22 Jan 19 UTC
part: modules
kind: bug
#### Version
Coq 8.8.2
#### Operating system
Red Hat Enterprise Linux W… orkstation 7.4
#### Description of the problem
The following code does not behave as expected.
```coq
(** We use the line that appears in the interactive proof mode
to make the output more readable. *)
Ltac line := idtac "______________________________________".
(** At this point, everything is fine. *)
Module Mod0.
Definition def : unit := tt.
Theorem thm : True.
Proof. apply I. Qed.
End Mod0.
Print Mod0.
About Mod0.thm.
(** At this point,
- [Mod0.thm] is opaque,
as it should be (by postulate). *)
Goal True. line. Abort.
Module Mod1.
Include Mod0.
End Mod1.
Print Mod1.
About Mod0.thm.
About Mod1.thm.
(** At this point,
- [Mod0.thm] is opaque,
as it should be (by previous point and postulate), and
- [Mod1.thm] is transparent,
even though it should be opaque (by postulate). *)
Goal True. line. Abort.
Module Mod2.
Include Mod0.
Opaque thm.
End Mod2.
Print Mod2.
About Mod0.thm.
About Mod1.thm.
About Mod2.thm.
(** At this point,
- [Mod0.thm] is opaque,
as it should be (by previous point and postulate),
- [Mod1.thm] is transparent,
as it should be (by previous point),
although it could also be opaque (by postulate), and
- [Mod2.thm] is transparent,
even though it should be transparent-opaque (by previous point) or
opaque (by postulate). *)
Goal True. line. Abort.
Module Mod3.
Include Mod0.
End Mod3.
Opaque Mod3.thm.
Print Mod3.
About Mod0.thm.
About Mod1.thm.
About Mod2.thm.
About Mod3.thm.
(** At this point,
- [Mod0.thm] is opaque,
as it should be (by previous point and postulate),
- [Mod1.thm] and [Mod2.thm] are transparent-opaque,
even though they should be transparent (by previous point) or
opaque (by postulate), and
- [Mod3.thm] is transparent-opaque,
as it should be (by previous point),
although it could also be opaque (by postulate). *)
Goal True. line. Abort.
Module Mod4.
Include Mod0.
Transparent thm.
End Mod4.
Print Mod4.
About Mod0.thm.
About Mod1.thm.
About Mod2.thm.
About Mod3.thm.
About Mod4.thm.
(** At this point,
- [Mod0.thm] is opaque,
as it should be (by previous point and postulate),
- [Mod1.thm], [Mod2.thm] and [Mod3.thm] are transparent-opaque,
as they should be (by previous point),
although they could also be opaque (by postulate), and
- [Mod4.thm] is transparent-opaque,
even though it should be transparent (by previous point) or
an error (by postulate). *)
Goal True. line. Abort.
Module Mod5.
Include Mod0.
End Mod5.
Transparent Mod5.thm.
Print Mod5.
About Mod0.thm.
About Mod1.thm.
About Mod2.thm.
About Mod3.thm.
About Mod4.thm.
About Mod5.thm.
(** At this point,
- [Mod0.thm] is opaque,
as it should be (by previous point and postulate),
- [Mod1.thm], [Mod2.thm], [Mod3.thm] and [Mod4.thm] are transparent,
even though they should be transparent-opaque (by previous point) or
opaque (by postulate), and
- [Mod5.thm] is transparent,
as it should be (by previous point),
although it could also be an error (by postulate). *)
```
#### Notes
Using `Global Opaque` or `Global Transparent` inside a module
has the same effect as using `Opaque` or `Transparent` outside the module.
Using `Local Opaque` or `Local Transparent` inside or outside a module
has no effect.
RalfJ
May 22, 2019, 9:55am
2
AFAIK, yes.
Typeclasses Opaque foo
is a unification hint that will prevent unification occurring during typeclass search when checking which instances to apply from unfolding foo
.
I don’t know the exact effects of Opaque
(there are IIRC still some ways to unfold such terms), but from what I recall it does at least affect all unification.
1 Like