Stream: Coq users

Topic: Example of `Hint Transparent` and `Hint Opaque`

Ali Caglayan (Sep 20 2021 at 11:43):

I am trying to write a test for Hint Transparent and Hint Opaque but I am having trouble coming up with a situation which only works in either case. It seems to me that hint search is disregarding the opaqueness, or perhaps I don't really understand what is going on?

Ali Caglayan (Sep 20 2021 at 11:44):

So if anybody has a small example demonstrating how this works that would be great!

Ali Caglayan (Sep 20 2021 at 12:19):

For examples I tried something like this:

Axiom A : Type.
Axiom P : A -> Type.
Definition Q := P.

Existing Class P.
Existing Class Q.

Axiom a : A.
Axiom pa : P a.
#[local] Existing Instance pa.

Goal sigT P.
Proof.
  eexists.
  typeclasses eauto.
Qed.

#[local] Typeclasses Transparent Q.

Goal sigT Q.
Proof.
  eexists.
  typeclasses eauto.

Ali Caglayan (Sep 20 2021 at 12:20):

But for whatever reason the second goal doesn't work, am I missing something?

Ali Caglayan (Sep 20 2021 at 12:22):

Sorry ignore the #[local] for typeclasses transparent, that was something I was hacking.

Gaëtan Gilbert (Sep 20 2021 at 12:25):

transparency is used for

Definition b := a.

Check _ : P b.

Typeclasses Opaque b.

Check _ : P b.

but not when deciding what class we're looking at

Ali Caglayan (Sep 20 2021 at 12:32):

Aha Ok!

Last updated: Apr 20 2024 at 06:02 UTC