Umon (Dec 02 2022 at 21:09): 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?
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?
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}"
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
then add term_of
Mathias Fleury (Dec 05 2022 at 18:34):That error message just means: "I want to you user do add XXX to the sorts"
Mathias Fleury (Dec 05 2022 at 18:34):Remark that you can also drop the type annotation completely
Mathias Fleury (Dec 05 2022 at 18:35):fun minError where
"minError x = {y. y=y}"
then there is no type annotation and Isabelle will take care of adding the correct sorts and types
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
Alright, I'll be doing that going forward.
Thanks a lot, both of you.
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: Dec 21 2024 at 16:20 UTC