Not an equation - Function · Beginner Questions

function core_module :: "'a::ord Result ⇒ 'b set ⇒ 'b set ⇒ ('a::ord) set ⇒ ('a::ord, 'b set) Seats ⇒ 'b set StructVotes ⇒ 'b set StructVotes ⇒ nat list ⇒ 'b set StructVotes" where
"core_module result party parties indexes seats votes fract_votes params ≡
  let
      ni = (case result of (_, _, x ) ⇒ SOME y. y \<in> x);
      new_seats = assign_seat ni party seats;
      new_fract_votes = (update_votes party new_seats indexes votes fract_votes params)
in
      new_fract_votes"

which gives me the "not an equation" error. However, if i change function to "definition" it works even if, of course, when i try to use it, it doesn't work for the same problem: not an equation. I am having problems looking for the error. Can someone explain what is happening and how i should solve?

Jan van Brügge (Dec 11 2023 at 15:52):

Manuel Eberl (Dec 11 2023 at 15:55):

In general I would recommend not using ≡ except for abbreviations (where you have to use it).

Lukas Stevens (Dec 11 2023 at 18:57):

Any specific reason for that? I always use ≡ for definitions since it allows you to save some parentheses, e.g. if you use a quantifier on the right-hand side.

Manuel Eberl (Dec 12 2023 at 09:23):

No it's fine for that purpose if you really want to. It doesn't make a difference there. But you don't want to use it in lemmas because it doesn't interact with the automation well.

I see pure equality as a technical oddity coming from the internals of Isabelle that isn't really needed for using HOL, similar to the prop type. So I think especially for beginners the best advice is to just not use it to avoid confusion.

Salvatore Francesco Rossetta (Dec 12 2023 at 14:36):

Thanks for the answer. In case this conversation will be useful for others in the future: after changing this equality
I had to wrap the body function in parenthesis to avoid syntax error.

However, I wanted to check if the module works with some "dummy" values in input but i get "No code equation for Eps"

definition myres :: "nat Result" where
"myres = ({1, 2}, {3}, {4, 5})"

definition myparties:: "char list set" where
"myparties = {''a'', ''b'', ''c'', ''d''}"

definition myindexes:: "nat set" where
"myindexes = {1, 2, 3, 4, 5}"

definition myseats :: "(nat, char list set) Seats" where
"myseats n = (if n = 1 then {''a''} else if n = 2 then {''b''} else if n = 3 then {''a''} else {''a'', ''b'', ''c'', ''d''})"

definition myvotes :: "(char list set) StructVotes" where
"myvotes n = (if n = {''a''} then 1 else if n = {''b''} then 2 else if n = {''c''} then 1 else 0)"

definition myfractvotes :: "(char list set) StructVotes" where
"myfractvotes n = (if n = {''a''} then 1 else if n = {''b''} then 2 else if n = {''c''} then 1 else 0)"

definition myparams :: "nat list" where
"myparams = [1, 2, 3, 4, 5]"

value "core_module myres {''a''} myparties myindexes myseats myvotes myfractvotes myparams"

I don't think these are the problem but I can't find the error in the function, if it's there

Manuel Eberl (Dec 12 2023 at 14:46):

Eps is the name of the Hilbert choice operator, which is written as SOME x. …. You are using it in your definition of core_module. There are no code equations for Eps, and there cannot be. The choice operator is an underspecified operation and therefore cannot be implemented.

It seems that your algorithm is nondeterministic in the sense that it nondetereministically chooses an element from this set and then does something with it. However, HOL is not a nondeterministic logic. Functions have one result, and only one. So if you write it down with the SOME operator, you logically get some result, but you don't know which one. That is one way to resolve nondeterminism, and it can occasionally be a useful one in proofs. But for executable code, it's bad, because, well, you cannot execute it.

So, what other options are there? It depends on what you want to achieve. One possibility is to work in the set monad and return a set of all possible results. Another would be to always pick e.g. the smallest element from the set (but then you lose a lot of flexibility). Or you could use a framework that deals with nondeterminism in a more explicit way, like Peter Lammich's refinement framework.

Lukas Stevens (Dec 12 2023 at 14:48):

Another way is to axiomatise the existence of the choice function with a locale. This leaves the implementation of the choice function for later (e.g. choosing the smallest element).

Salvatore Francesco Rossetta (Dec 12 2023 at 14:49):

Thanks for the clear answer, now I understood the problem. To take the smallest value actually would be the best fitting option for my case, so I think I'll follow that strategy.

Stream: Beginner Questions

Topic: Not an equation - Function

Salvatore Francesco Rossetta (Dec 11 2023 at 15:40):