Salvatore Francesco Rossetta (Dec 02 2023 at 20:33): Salvatore Francesco Rossetta (Dec 02 2023 at 20:33):Hello, I am new to Isabelle and I have a Wellsortedness error on "nat" type.
I am using this function (which i cannot change):
fun rank :: "'a Preference_Relation ⇒ 'a ⇒ nat" where
"rank r a = card (above r a)"
which returns the number of ranking of "a" in the Preference Relation (which is a 'a rel) "r" of type 'a.
I tried using it in the simplest way writing:
value "rank {(3,4), (4,5), (5,6)} 5"
but i get this error:
"Wellsortedness error:
Type 'a not of sort {enum,equal}
Cannot derive subsort relation numeral < {enum,equal}"
So i thought the problem was to not explicitly defining the types and I updated my code:
definition my_pr :: "nat Preference_Relation" where
"my_pr = {(3,4), (4,5), (5,6)}"
value "rank my_pr 5"
but I get this error
Wellsortedness error:
Type nat not of sort {enum,equal}
No type arity nat :: enum
Doesn't this mean that nat does not have enum and equals? but I think it does and I cannot understand how to solve it. I looked for some answers here and I only found one which I don't think fits my case but I am a beginner so maybe I just didn't understand. Thanks in advance
Mathias Fleury (Dec 02 2023 at 20:39):nat is not enumerable, because you cannot enumerate all values in finite time
Mathias Fleury (Dec 02 2023 at 20:41):just think of ?x::nat. P x: there is no finite-time solution to know if this holds or not
Mathias Fleury (Dec 02 2023 at 20:47):However in your case, you can reformulate the problem:
definition above_set :: "_ ⇒ 'a ⇒ 'a set"
where "above_set r a ≡ above (set r) a"
lemmas [code] = above_set_def[symmetric]
lemma [code]:
‹above_set [] a = {}›
‹above_set ((x,y)#xs) a = (if x=a then {y} else {}) ∪ above_set xs a›
by (auto simp: above_set_def above_def)
value "(above (set [(3,4), (4,5), (5,6)]) (5::nat))"
but I think there is a better way
Mathias Fleury (Dec 02 2023 at 21:02):Turns out that I do not remember enough how the setup of sets work, to make the following work:
lemma [code]:
‹above (insert x xs) a = (if a=fst x then {snd x} else {}) ∪ above xs a›
‹above {x} a = (if a=fst x then {snd x} else {})›
by (cases x;auto simp: above_set_def above_def)+
Actually, when I paste the second lemma you wrote it's giving me an error
"Set.insert" is not a constructor, on left hand side of equation, in theorem:
above (insert ?x bot_set_inst.bot_set) ?a ≡
if ?a = fst ?x then insert (snd ?x) bot_set_inst.bot_set else bot_set_inst.bot_set
While if I don't, it seems to work and the value command gives as output "6", which is indeed the set above "5"
Mathias Fleury (Dec 04 2023 at 05:54):Yeah that what I meant with the fact that I do not manage to make it work…
Maximilian Schäffeler (Dec 04 2023 at 07:56):I think you meant to do the following:
lemma [code]:
‹above (set []) a = {}›
‹above (set ((x,y)#xs)) a = (if x=a then {y} else {}) ∪ above (set xs) a›
by (auto simp: above_def)
This works because set and coset are constructors for sets in generated code. The setup was done using
code_datatype set coset
See the codegen tutorial for more info on how this works in general. You can also rewrite the function in terms of Set.filter:
lemma [code]: ‹above r a = snd ` Set.filter (λ(x, y). x = a) r›
unfolding above_def by force
Just FYI, there are already some bits of social choice theory in the AFP that you could build on.
Manuel Eberl (Dec 04 2023 at 09:05):Feel free to ask me about them.
Last updated: Apr 27 2024 at 20:14 UTC