walker (Oct 14 2022 at 09:01): walker (Oct 14 2022 at 09:01):So I am trying to do the following:
Variable A: Type.
Variable B: Type.
Variable A_Eq: EqDecision A.
Variable A_Co: Countable A.
But Countable A requires EqDecision A and coq complains saying:
Unable to satisfy the following constraints:
?EqDecision0 : "EqDecision A"
I want to use A in to create lemmas that assume that Countable A
Li-yao (Oct 14 2022 at 09:06):Are you using Variable outside of a section? Try inside a section.
Gaëtan Gilbert (Oct 14 2022 at 09:09):outside a section use Axiom for A and B, and Declare Instance for A_Eq ad A_Co
walker (Oct 14 2022 at 09:19):Gaëtan Gilbert said:
outside a section use Axiom for A and B, and Declare Instance for A_Eq ad A_Co
That feels strange, I always assumed that axiom is a footgun. does that mean that Vairbale is also equally dangerous ?
Li-yao (Oct 14 2022 at 09:24):When used outside any section, Variable is the same as Axiom.
Li-yao (Oct 14 2022 at 09:26):But you also get a warning about not using Variable that way because you probably don't mean it.
walker (Oct 14 2022 at 09:27):I see. understood
Notification Bot (Oct 14 2022 at 09:27):walker has marked this topic as resolved.
Paolo Giarrusso (Oct 14 2022 at 13:18):More idiomatic and concise ways include either:
Context `{Countable A}.
or
Context `{!EqDecision A, !Countable A}.
in sections; stdpp uses Context a lot
walker (Oct 14 2022 at 16:54):1 extra question, what does the ! mean ?
Gaëtan Gilbert (Oct 14 2022 at 16:58):it means do not create a fresh typeclass for any typeclass argument
so for EqDecision it does nothing, but for Countable without the ! it would add another EqDecision hypothesis and use that instead of the manually declared one
(! is a modifier for ` )
Gaëtan Gilbert (Oct 14 2022 at 16:59):so
Context `{!EqDecision A, !Countable A}.
is equivalent to
Context `{Countable A}.
And if you bind two typeclasses that "inherit" from e.g. EqDecision, you almost always want to use the ! form; I've never seen a case where binding multiple EqDecision instances is reasonable.
Last updated: Apr 20 2024 at 05:01 UTC