Stream: Beginner Questions

Topic: Fix 'a with typeclass


view this post on Zulip Max Nowak (Jun 21 2021 at 13:27):

I introduce variables with fix A :: "'a set", which I later use and need 'a to have a specific typeclass. Is there a way to fix variables with the additional restriction that they are in a typeclass?

view this post on Zulip Manuel Eberl (Jun 21 2021 at 13:28):

fix A :: "`a :: myclass set"

view this post on Zulip Max Nowak (Jun 21 2021 at 13:30):

Now I get the following though:
Sort constraint linorder inconsistent with default type for type variable "'a"

view this post on Zulip Manuel Eberl (Jun 21 2021 at 13:32):

Then you already have a type 'a in your context that doesn't have that type class.

view this post on Zulip Manuel Eberl (Jun 21 2021 at 13:32):

So you probably have to annotate it with that type class even earlier.

view this post on Zulip Manuel Eberl (Jun 21 2021 at 13:33):

Come to think of it, I don't think I can think of any common situation where it would be required to add a type class annotation to a fix command.

view this post on Zulip Manuel Eberl (Jun 21 2021 at 13:33):

If you don't understand what you need to do, you should perhaps post some more context so that we can see what it is that you are attempting to do.

view this post on Zulip Max Nowak (Jun 21 2021 at 13:37):

Yeah I have a (in linorder) on my lemma, and yet it complains that 'a isn't of sort linorder.
My lemma:

lemma (in linorder): "myprop myfunc"
  unfolding myprop_def
proof (safe)
  fix A :: "'a set"
  have "..." using other_lemma[of A] (* <-- error here that A is not of sort linorder*)
qed

I hope that's enough code.

view this post on Zulip Manuel Eberl (Jun 21 2021 at 13:38):

Ah, yes, this is an oddity of the way type classes work in Isabelle. When you are in the linorder context, you do not actually have the sort linorder on the type variable 'a and there is no way to get it.

view this post on Zulip Manuel Eberl (Jun 21 2021 at 13:38):

Ideally, you should prove your other_lemma also in a linorder context (i.e. with in linorder) so that you can use it here.

view this post on Zulip Manuel Eberl (Jun 21 2021 at 13:39):

If that is not possible for some reason, you will have to prove everything that builds on it also outside the linorder context, with an explicit linorder sort annotation.

view this post on Zulip Max Nowak (Jun 21 2021 at 13:40):

Explicit sort annotation such as 'a :: linorder? Just making sure, since I'm not a pro on sorts.

view this post on Zulip Manuel Eberl (Jun 21 2021 at 13:40):

Yes.

view this post on Zulip Max Nowak (Jun 21 2021 at 13:40):

Thanks, you helped me :). I'll choose the latter.

view this post on Zulip Max Nowak (Jun 21 2021 at 13:48):

Yay the error is gone. Time to party.


Last updated: Feb 27 2024 at 08:17 UTC