Stream: Coq users

Topic: Parameterized typeclasses

Chantal Keller (Oct 20 2021 at 16:13):

Hi
I must be missing something, but I do not understand why the following fails (tested with Coq.8.13.2):

Class Inhabited (A : Type) := { inh : A }.

Instance unit_Inhabited : Inhabited unit := { inh := tt }.

Section prod.
  Generalizable Variables A B.
  Context `{EA : Inhabited A, EB : Inhabited B}.

  Instance prod_Inhabited : Inhabited (A*B) :=
    { inh := (inh, inh) }.
End prod.

Lemma dummy {A:Type} `{HA : Inhabited A} : A.
Proof. exact inh. Qed.

Lemma ok : unit.
Proof. apply dummy. Qed.

Lemma ko : unit * unit.
Proof. Fail apply dummy. Abort.

Thanks!

Guillaume Melquiond (Oct 20 2021 at 16:17):

You need to reexport the instance: Existing Instance prod_Inhabited.

Chantal Keller (Oct 20 2021 at 16:18):

Thanks, it works! But what does it mean?

Gaëtan Gilbert (Oct 20 2021 at 16:20):

instance in section is local by default

Guillaume Melquiond (Oct 20 2021 at 16:20):

If you use Instance inside Section, the instance only lives as long as the section. Outside, it is just a plain definition. So, you can register it again using Existing Instance.

Chantal Keller (Oct 20 2021 at 16:24):

Ok, thanks a lot. Maybe the documentation could explain it in the section "Sections and contexts" ;-) Actually now I understand the meaning of #[global], which I guess does the same?

Chantal Keller (Oct 20 2021 at 16:28):

I have another question regarding typeclasses: can the mechanism be called by hand, if I have e.g. such a goal:

Lemma test : Inhabited (unit * unit).

?

Guillaume Melquiond (Oct 20 2021 at 16:31):

typeclasses eauto should do the trick.

Théo Winterhalter (Oct 20 2021 at 16:31):

Or exact _.

Chantal Keller (Oct 20 2021 at 16:33):

Great, many thanks!

Last updated: Oct 13 2024 at 01:02 UTC