Stream: Beginner Questions

Topic: Giving a datatype an "equal" property


view this post on Zulip Umon (Dec 02 2022 at 21:09):

Hey guys,

I'm completely new to Isabelle and having a lot of trouble with types.

I have this function,
fun getArcs::"'a set ⇒ ('a*'a) set" where "getArcs A = {(u,v). (u,v)∈(A×A) ∧ (u≠v)}"
,which is supposed to get me all pairs of a set, except for the ones with the same value in both places.

It compiles fine, but I can't test it.

I thought since 'a is polymorphic, using a set of nats would work, but it doesn't, because it's "not of sort {enum,equal}".
So I tried creating my own datatype, but I ran into the same problem.

Without the u≠v both of those approaches work.

Can someone help me?

view this post on Zulip Umon (Dec 05 2022 at 16:44):

I've managed to narrow the problem down to this:

fun minError::"'a ⇒ 'a set" where
"minError x = {y. y=y}"

(I'm aware this function makes no sense but before it runs into the problem you'd expect, it runs into the error I encountered.)
It's the same if you put y=x at the end instead of y=y.

I suppose the problem is that y doesn't have a type yet? Is there a way to give an element, that's introduced in a set to be returned, a type?

view this post on Zulip Mathias Fleury (Dec 05 2022 at 17:51):

You just have to add the missing sorts to the type annotation:

fun minError::"'a :: {enum, equal} ⇒ 'a set" where
"minError x = {y. y=y}"

view this post on Zulip Umon (Dec 05 2022 at 18:30):

I don't think that works?

Calling value "minError 0" with your function just gives me

Wellsortedness error:
Type 'a not of sort term_of
Cannot derive subsort relation {enum,zero,equal} < term_of

view this post on Zulip Mathias Fleury (Dec 05 2022 at 18:33):

then add term_of

view this post on Zulip Mathias Fleury (Dec 05 2022 at 18:34):

That error message just means: "I want to you user do add XXX to the sorts"

view this post on Zulip Mathias Fleury (Dec 05 2022 at 18:34):

Remark that you can also drop the type annotation completely

view this post on Zulip Mathias Fleury (Dec 05 2022 at 18:35):

fun minError where
"minError x = {y. y=y}"

view this post on Zulip Mathias Fleury (Dec 05 2022 at 18:35):

then there is no type annotation and Isabelle will take care of adding the correct sorts and types

view this post on Zulip Jonathan Julian Huerta y Munive (Dec 05 2022 at 18:58):

It compiles fine, but I can't test it.

I assume by "test" you mean you want to use the value command?

Since you are using a proof assistant you can "test" with a lemma instead:

lemma "getArcs ({True, False}) = {(True, False), (False, True)}"
  by auto

lemma "getArcs ({0::nat, 1, 2}) = {(0, 1), (1,0), (1, 2), (2,1), (0, 2), (2, 0)}"
  by auto

The better approach is to "test" it abstractly:

lemma "(n,n) ∉ getArcs A"
  "n ≠ m ⟹ n ∈ A ⟹ m ∈ A ⟹ (m, n) ∈ getArcs A"
  "n ≠ m ⟹ n ∈ A ⟹ m ∈ A ⟹ (n, m) ∈ getArcs A"
  by auto

view this post on Zulip Umon (Dec 05 2022 at 19:09):

Alright, I'll be doing that going forward.

Thanks a lot, both of you.

view this post on Zulip Jonathan Julian Huerta y Munive (Dec 05 2022 at 19:13):

Since the command value calls the code generator, you are asking Isabelle to compute on sets. Sets can be infinite, requiring us to have extra constraints on the type e.g. enum and equal. If you want to know more about these, they are type classes https://isabelle.in.tum.de/dist/Isabelle2022/doc/classes.pdf. Thus, if you are just starting with Isabelle, I recommend using value for things "clearly" computable (e.g. lists, nats, ints and functions on these).


Last updated: Mar 28 2024 at 08:18 UTC