Defining partial functions · Beginner Questions

Stream: Beginner Questions

Topic: Defining partial functions

Trinh Le Khanh (Nov 09 2020 at 01:17):

Hi,
I wanna define a partial function. It works if I define:

definition f :: "nat ⇒ nat option"
where
"f x = (if x ∈ {1, 2, 3} then Some 0 else None)"

But I want to specify the range of the function f is {5,6}, so I defined:

definition f :: "nat ⇒ nat option"
where
"f x = (if x ∈ {1, 2, 3} then (Some y ∈ {5,6}) else None)"

It caused the error:

Type unification failed: No type arity option :: numeral

Type error in application: incompatible operand type

Operator:  (∈) (Some y) :: ??'a option set ⇒ bool
Operand:   {5, 6} :: ??'b set

I understand that it considers the return value of Some y ∈ {5,6} is bool, right?
So, how to specify the range of the function f?

Mathias Fleury (Nov 09 2020 at 05:51):

On syntax level, you are confusing Some and SOME y. y ∈ {5,6}. What you have should type for Some (SOME y. y ∈ {5,6}).

Mathias Fleury (Nov 09 2020 at 05:55):

On the conceptual level, you are not defining what you intend to.

Assume you fix your definition with Some (SOME y. y ∈ {5,6}). Your function f will be defined by:

  f: 1,2, or 3 -> some value of {5, 6}, the same for 1, 2, and 3
     _               -> None

And again, you cannot know if f(1) is equal to 5 or 6. You cannot distinguish this in Isabelle. However, f(1), f(2), and f(3) are equal to the same value.

Trinh Le Khanh (Nov 09 2020 at 08:41):

As I understand, SOME y. y ∈ {5, 6} means that the value is 5 or 6. So why we have to put Some before SOME y. y ∈ {5, 6}?

Fabian Huch (Nov 09 2020 at 08:43):

Some is the option constructor for your nat option return value.

Mathias Fleury (Nov 09 2020 at 08:45):

In
if x ∈ {1, 2, 3} then PLACEHOLDER else None

None has type nat option. So PLACEHOLDER must have the same type. SOME y. y ∈ {5, 6} has type nat. You need either to convert the nat to nat option by Some. Or change None to something of type nat (like undefined or a default value)

Trinh Le Khanh (Nov 09 2020 at 08:46):

Mathias Fleury said:

In
if x ∈ {1, 2, 3} then PLACEHOLDER else None

None has type nat option. So PLACEHOLDER must have the same type. SOME y. y ∈ {5, 6} has type nat. You need either to convert the nat to nat option by Some. Or change None to something of type nat (like undefined or a default value)

It's very clear. Thank you for your explanation.

Trinh Le Khanh (Nov 09 2020 at 09:13):

For the function:

definition f :: "nat ⇒ nat option"
where
"f x = (if x ∈ {1, 2, 3} then Some(SOME y. y ∈ {5, 6}) else None)"

I check the range of it like this:

lemma "ran f = {5,6}"
  unfolding f_def ran_def
  apply auto
  done

And the result is:

proof (prove)
goal (14 subgoals):
 1. (SOME y. y = 5 ∨ y = 6) ≠ 5 ⟹ (SOME y. y = 5 ∨ y = 6) = 6
 2. (SOME y. y = 5 ∨ y = 6) ≠ 5 ⟹ (SOME y. y = 5 ∨ y = 6) = 6
 3. (SOME y. y = 5 ∨ y = 6) ≠ 5 ⟹ (SOME y. y = 5 ∨ y = 6) = 6
 4. (SOME y. y = 5 ∨ y = 6) ≠ 5 ⟹ (SOME y. y = 5 ∨ y = 6) = 6
 5. (SOME y. y = 5 ∨ y = 6) ≠ 5 ⟹ (SOME y. y = 5 ∨ y = 6) = 6
 6. (SOME y. y = 5 ∨ y = 6) ≠ 5 ⟹ (SOME y. y = 5 ∨ y = 6) = 6
 7. (SOME y. y = 5 ∨ y = 6) ≠ 5 ⟹ (SOME y. y = 5 ∨ y = 6) = 6
 8. (SOME y. y = 5 ∨ y = 6) ≠ 5 ⟹ (SOME y. y = 5 ∨ y = 6) = 6
 9. (SOME y. y = 5 ∨ y = 6) ≠ 5 ⟹ (SOME y. y = 5 ∨ y = 6) = 6
 10. (SOME y. y = 5 ∨ y = 6) ≠ 5 ⟹ (SOME y. y = 5 ∨ y = 6) = 6
A total of 14 subgoals...

I think that subgoals should be proved by simp because

P ⟹ Q ≡ ¬P ∨ Q ≡
(SOME y. y = 5 ∨ y = 6) = 5 ∨ (SOME y. y = 5 ∨ y = 6) = 6

So why this lemma cannot be proved?

Mathias Fleury (Nov 09 2020 at 09:18):

you need to help simp, for example with using someI[of \<open>%y. y \<in> {5,6}\<close>, of 5]
your realize that your lemma is wrong, right?

Mathias Fleury (Nov 09 2020 at 09:19):

It is wrong due to:

Mathias Fleury said:

f(1), f(2), and f(3) are equal to the same value.

Mathias Fleury (Nov 09 2020 at 09:45):

I think most of the conversion comes from the fact that you don't understand some. You are confusing it with non-determinism, which is the wrong way of seeing it.

Hilbert choice takes a predicate as argument. If there is no way to make the predicate true, some non-specified constant is returned. Otherwise, it returns some non-specified constant fulfilling the predicate.

What does non-specified mean? It means that you cannot know which elements is returned and the element changes every time Isabelle is restarted (roughly speaking).

What is the difference with non-determinism? Well, the returned is _always_ the same within one Isabelle execution. That means that (SOME y::nat. y = 5 ∨ y = 6) will return the same element as (SOME y::nat. y = 5 ∨ y = 6), (SOME y::nat. y = 5 ∨ y = 6), and (SOME y::nat. y = 5 ∨ y = 6). This is not the same as non-determinsm, where calling the C function rand(), rand(), rand(), and rand(), can return different values [1].

What does that mean for your use case? It means that you need to do recursion to be construct the mapping and _exclude the elements mapped so far_. This is also entails that your current approach does not work.

[1] other examples include file parsing, reading environment values, looking at a thermometer, ...

Trinh Le Khanh (Nov 09 2020 at 10:16):

So, when I use Some, the return values of each running time are different, right?

Mathias Fleury (Nov 09 2020 at 10:23):

(SOME y::nat. y = 5 ∨ y = 6) = (SOME y::nat. y = 5 ∨ y = 6) is always true, so no.

Mathias Fleury (Nov 09 2020 at 10:23):

Unlike a C version likerand() == rand().

Trinh Le Khanh (Nov 09 2020 at 10:50):

Mathias Fleury said:

you need to help simp, for example with using someI[of \<open>%y. y \<in> {5,6}\<close>, of 5]

your realize that your lemma is wrong, right?

After applying it, the output is:

proof (prove)
using this:
  5 ∈ {5, 6} ⟹ (SOME y. y ∈ {5, 6}) ∈ {5, 6}

goal (1 subgoal):
 1. {b. ∃a. (if a ∈ {1, 2, 3} then Some (SOME y. y ∈ {5, 6}) else None) = Some b} = {5, 6}

Actually, I don't know what's wrong. Can you explain it?

Mathias Fleury (Nov 09 2020 at 10:51):

using someI[of \<open>%y. y \<in> {5,6}\<close>, of 5] apply simp

Trinh Le Khanh (Nov 09 2020 at 11:35):

The output is:

proof (prove)
goal (1 subgoal):
 1. (SOME y. y = 5 ∨ y = 6) = 5 ∨ (SOME y. y = 5 ∨ y = 6) = 6 ⟹
    {b. ∃a. (a = Suc 0 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧
            (a = 2 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧
            (a = 3 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧ (a = Suc 0 ∨ a = 2 ∨ a = 3)} =
    {5, 6}

it equals to

 {b. ∃a.(a = Suc 0 ∨ a = 2 ∨ a = 3) ∧ (SOME y. y = 5 ∨ y = 6) = b)} = {5,6}

I think it's TRUE.

Mathias Fleury (Nov 09 2020 at 11:39):

No it is not.

Mathias Fleury (Nov 09 2020 at 11:40):

We know that (SOME y. y = 5 ∨ y = 6) is either 5 or 6, but let's call it N.

Mathias Fleury (Nov 09 2020 at 11:42):

your set is:

{b. ∃a.(a = Suc 0 ∨ a = 2 ∨ a = 3) ∧ N = b}

By miniscoping this is the same as:

{b. (∃a.(a = Suc 0 ∨ a = 2 ∨ a = 3) )∧ N = b}

Now, ∃a.(a = Suc 0 ∨ a = 2 ∨ a = 3) is true. So we can simplify the set to:

{b. True ∧ N = b}

Therefore, the set is equal to

{N}

Mathias Fleury (Nov 09 2020 at 11:42):

And {N} is not equal to {5,6}

Mathias Fleury (Nov 09 2020 at 11:43):

As I said before, the choice value does not change. It is always the same.

Trinh Le Khanh (Nov 09 2020 at 11:50):

As I understand your explanation, y should be {5} or {6} not {5,6} right?
If so, it's true for the command:

"f x = (if x ∈ {1, 2, 3} then Some(SOME y. y ∈ {5, 6}) else None)"

but in the lemma, I check the range of the function. So if y = {5} or {6} so the ran f = {5, 6} right?

Mathias Fleury (Nov 09 2020 at 11:51):

Let's be precise first: y is 5 or 6, not {5} or {6}

Trinh Le Khanh (Nov 09 2020 at 11:52):

ah yes, my bad, I'm following the set then made this mistake.

Mathias Fleury (Nov 09 2020 at 11:52):

Your definition is equivalent to:

f x = (if x ∈ {1, 2, 3} then Some N else None)

Mathias Fleury (Nov 09 2020 at 11:53):

The N is constant. It has a single value. It does not change never. NEVER.

Mathias Fleury (Nov 09 2020 at 11:55):

So ran f = {N}. Either ran f = {5} or ran f = {6} holds. That is all you can say.

But many things don't hold: ran f = {5,6} never holds. Same for ran f = {4}.

Mathias Fleury (Nov 09 2020 at 12:01):

Maybe this view helps you more: SOME y. y ∈ {5, 6} is a constant. But it is constant only I (technically, the model) knows. But it is only a constant.

Trinh Le Khanh (Nov 09 2020 at 12:11):

Mathias Fleury said:

So ran f = {N}. Either ran f = {5} or ran f = {6} holds. That is all you can say.

But many things don't hold: ran f = {5,6} never holds. Same for ran f = {4}.

Following your explanation, I changed the lemma to:

lemma "ran f = {5} ∨ ran f = {6}"
  unfolding f_def ran_def
  apply simp
  done

and it's still unprovable

Failed to finish proof:
goal (1 subgoal):
 1. {b. ∃a. (a = Suc 0 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧
            (a = 2 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧
            (a = 3 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧ (a = Suc 0 ∨ a = 2 ∨ a = 3)} =
    {5} ∨
    {b. ∃a. (a = Suc 0 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧
            (a = 2 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧
            (a = 3 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧ (a = Suc 0 ∨ a = 2 ∨ a = 3)} =
    {6}

Mathias Fleury (Nov 09 2020 at 12:15):

In that case, it is provable. simp is not strong enough…

Mathias Fleury (Nov 09 2020 at 12:15):

lemma
  defines  ‹N == (SOME y :: nat. y = 5 ∨ y = 6)›
  shows
‹{b::nat. ∃a. (a = Suc 0 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧
            (a = 2 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧
            (a = 3 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧ (a = Suc 0 ∨ a = 2 ∨ a = 3)} =
    {5} ∨
    {b. ∃a. (a = Suc 0 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧
            (a = 2 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧
            (a = 3 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧ (a = Suc 0 ∨ a = 2 ∨ a = 3)} =
    {6::nat}
›
  using someI[of \<open>%y::nat. y = 5 ∨ y = 6\<close>, of 5]
  unfolding N_def[symmetric]
  by auto

Trinh Le Khanh (Nov 09 2020 at 12:21):

But it seems went too far from my purpose. I intend to check the range of the function f x = (if x ∈ {1, 2, 3} then Some(SOME y. y ∈ {5, 6}) else None).
I mean that if y is either 5 or 6, the range is {5,6}

Mathias Fleury (Nov 09 2020 at 12:36):

Thee range is the set of all possible values from f

Mathias Fleury (Nov 09 2020 at 12:36):

you have either 5 or 6, but not both

Mathias Fleury (Nov 09 2020 at 12:40):

let's try to be more formal, maybe that helps.

There is a model of HOL where N is 5. In that world, ran f = {5}.

There is another model of HOL where N is 6. In that world, ran f = {6}.

In Isabelle you are in one of those two models (and you don't know which).

Trinh Le Khanh (Nov 09 2020 at 12:44):

Yes, that's why I tried this lemma:

lemma "ran f = {5} ∨ ran f = {6}"
  unfolding f_def ran_def
  apply auto
  done

It should be proved without adding defines and shows parts.

Mathias Fleury (Nov 09 2020 at 12:46):

Generally, SOME tends to confuse auto and make thinks more complicated

Mathias Fleury (Nov 09 2020 at 12:47):

Therefore I replaced the SOME... by N and called auto. The defines just makes that possible

Mathias Fleury (Nov 09 2020 at 12:48):

Trinh Le Khanh said:

It should be proved without adding defines and shows parts.

There is no guarantee on what auto can and cannot ...

Mathias Fleury (Nov 09 2020 at 12:50):

Actually you don't need the defines:

lemma
‹{b::nat. ∃a. (a = Suc 0 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧
            (a = 2 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧
            (a = 3 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧ (a = Suc 0 ∨ a = 2 ∨ a = 3)} =
    {5} ∨
    {b. ∃a. (a = Suc 0 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧
            (a = 2 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧
            (a = 3 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧ (a = Suc 0 ∨ a = 2 ∨ a = 3)} =
    {6::nat}
›
  using someI[of \<open>%y::nat. y = 5 ∨ y = 6\<close>, of 5]
  by auto

Trinh Le Khanh (Nov 09 2020 at 13:07):

Maybe I still confuse about the proving process. I summary that, from the lemma:

lemma "ran f = {5} ∨ ran f = {6}"
  unfolding f_def ran_def
  apply simp

I got the subgoal:

goal (1 subgoal):
 1. {b. ∃a. (a = Suc 0 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧
            (a = 2 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧
            (a = 3 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧ (a = Suc 0 ∨ a = 2 ∨ a = 3)} =
    {5} ∨
    {b. ∃a. (a = Suc 0 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧
            (a = 2 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧
            (a = 3 ⟶ (SOME y. y = 5 ∨ y = 6) = b) ∧ (a = Suc 0 ∨ a = 2 ∨ a = 3)} =
    {6}

Then, I remove my lemma and create a lemma for this subgoal as you presented. Right?
If so, we just prove the subgoal, it doesn't mean that the lemma is proved.

Mathias Fleury (Nov 09 2020 at 13:09):

lemma "ran f = {5} ∨ ran f = {6}"
  unfolding f_def ran_def
  using someI[of ‹λy::nat. y = 5 ∨ y = 6›, of 5]
  by auto

Trinh Le Khanh (Nov 09 2020 at 13:41):

Thank you. I also try using someI[of ‹λy::nat. y ∈ {5,6}›] and it worked. I have one more question, how do you know what rule should be applied for the proving? For instance, someI in this lemma.

Last updated: Apr 18 2024 at 12:27 UTC