## Stream: Beginner Questions

### Topic: Defining and using set of functions

#### Trinh Le Khanh (Oct 22 2020 at 09:35):

Hi everyone, I want to define and use a set of functions to map elements from set X to set Y but I got trouble about using it.
For example, we have two sets as follows:

``````definition X :: "nat set"
where "X = {1, 2}"
definition Y :: "nat set"
where "Y = {3, 4}"
``````

`alpha` is the function map an element of X to an element of Y and `alphaSet` is the set of `alpha`. For instance,

``````alphaSet = {(1,3), (2,4)} or {(1,4), (2,3)} or ...
If alphaSet = {(1,3), (2,4)} then
alpha 1 = 3
alpha 2 = 4
``````

Thus, I defined `alpha` and `alphaSet` as follows:

``````definition alpha :: "nat ⇒ nat" where
"alpha x = (if x ∈ X then (SOME y. y ∈ Y) else 0)"

definition alphaSet :: "(nat ⇒ nat) set " where
"alphaSet = {f. (∀x ∈ X.(f x) ∈ Y)}"
``````

My problem is that how can I generate the values of `alphaSet` (i.e. how to get the set of function)? I tried

``````value "∀x ∈ X. alpha x".      ------- error
lemma test1: "(x ∈ X) ∧ (alpha ∈ alphaSet) ⟹ ((alpha x) ∈ Y)"
``````

but the result is `Failed to finish proof`. Could anyone help me, please? Thank you very much.

#### Mathias Fleury (Oct 22 2020 at 09:48):

value does not work for an obvious reason: It does not type. You are probably looking for `value "alpha ` X"`, which does not work either, because of the SOME. There is no way Isabelle can evaluate this expression, it is not constructive.

#### Mathias Fleury (Oct 22 2020 at 09:49):

About test1: I don't believe that it is out of the reach of someone who has done the Isabelle part of the Concrete Semantics.

#### Mathias Fleury (Oct 22 2020 at 09:49):

(and the lemma is correct)

#### Mathias Fleury (Oct 22 2020 at 09:52):

A constructive way for alpha can involve `sorted_list_of_set` to convert a set to a list and build the mapping explicitly.

#### Trinh Le Khanh (Oct 22 2020 at 10:01):

About test1: I don't believe that it is out of the reach of someone who has done the Isabelle part of the Concrete Semantics.

Yes, I've just done it. I forgot to unfold the definitions of X, Y, alpha, and alphaSet.

A constructive way for alpha can involve `sorted_list_of_set` to convert a set to a list and build the mapping explicitly.

Thank you for your suggestion. I'll try it.

#### Mathias Fleury (Oct 22 2020 at 10:09):

The question is probably if you really need to have an explicit mapping. There should be a theorem somewhere that states that there is an injection between two sets of the same cardinality.

#### Trinh Le Khanh (Oct 22 2020 at 22:33):

Mathias Fleury said:

The question is probably if you really need to have an explicit mapping. There should be a theorem somewhere that states that there is an injection between two sets of the same cardinality.

Yes, actually, I need that: for each `x ∈ X`, create a set Y_x. For example,

``````X = {0, 1}
x ∈ X
x = 0: create Y_0 = {3,4,5}
x = 1: create Y_1 = {6,7}
``````

#### Trinh Le Khanh (Nov 01 2020 at 20:01):

Mathias Fleury said:

The question is probably if you really need to have an explicit mapping. There should be a theorem somewhere that states that there is an injection between two sets of the same cardinality.

Hi Mathias, I got a problem defining a set of functions. I defined `alphaSet` (a set of `alpha` function) as follows:

``````definition SyncExport :: "nat set" (* Export*)
where "SyncExport = {1, 2}"

definition SyncElemExport :: "nat set" (*element Export*)
where "SyncElemExport = {1, 2}"

definition TypeSync :: "nat set" (*port types*)
where "TypeSync = {1, 2}"

definition IncSync :: "nat set set" (*port instances of each port type TypeSync*)
where "IncSync = {{5,6}, {7,8,9}}"

definition mapin :: "nat ⇒ nat set" where (*mapin 1 = {5,6}; mapin 2 = {7,8,9}*)
"mapin pt = (if pt ∈ TypeSync then (SOME pIn. pIn ∈ IncSync) else {})"

definition alphaSet :: "(nat ⇒ nat) set " where (*set of functions alpha*)
"alphaSet = {f. ∀x∈TypeSync. (f x) ∈ (mapin x)}"

definition alpha :: "nat ⇒ nat" where (*alpha 1= 5 or alpha 1 = 6*)
"alpha pt = (if pt ∈ TypeSync then (SOME y. y ∈ (mapin pt)) else 0)"
``````

Then, I test the cardinality of `TypeSync` and `IncSync`. They are equal.

``````value "card TypeSync"
value "card IncSync"
``````

But when I want to show the value of the below predicate:

``````value "(∀t∈TypeSync.∀alp∈alphaSet.(P t (alp t)))"
``````

It caused the error:

``````Wellsortedness error
(in code equation alphaSet ≡ {f. ∀x∈TypeSync. f x ∈ mapin x},
with dependency "Pure.dummy_pattern" -> "alphaSet"):
Type nat ⇒ nat not of sort enum
No type arity nat :: enum
``````

As I understand, this error is from the infinite set but I defined `TypeSync` and `IncSync` are finite sets. Do you have any suggestions?

#### Mathias Fleury (Nov 01 2020 at 20:13):

• This is not an explicit construction (you cannot use SOME for that!) and `mapin` cannot be calculated
• The error message hints that `alphaSet` cannot be calculated. Without code setup, it requires enumerating constructing all functions `f` and then filtering them.

#### Trinh Le Khanh (Nov 01 2020 at 21:55):

In the `mapin`, I want that from the `i element` of set A, we take the corresponding element in the set B.
I read the `set` library in Isabelle but they just provide operators `insert` or `empty`. Is there any chance to make an explicit mapping between two sets' elements?

#### Mathias Fleury (Nov 02 2020 at 05:28):

By definition there is no order of elements of sets, but:

Mathias Fleury said:

A constructive way for alpha can involve `sorted_list_of_set` to convert a set to a list and build the mapping explicitly.

allows you to build a list containing the same elements (if the set is finite). Then there is an order on the elements.

#### Mathias Fleury (Nov 02 2020 at 05:40):

Along that line (don't name the function `t` in your development!):

``````fun t where
‹t (x # xs) (y # ys) = (t xs ys) (x := y)› |
‹t _ _ = (λx. 0)›

definition explicit_mapping :: ‹nat set ⇒ nat set ⇒ (nat ⇒ nat)› where
‹explicit_mapping xs ys = t (sorted_list_of_set xs) (sorted_list_of_set ys)›

value ‹explicit_mapping {1, 2, 3} {4, 5, 6}›
``````

And here a completely random lemma:

``````lemma t_maps_to_existing:
‹length xs = length ys ⟹ x ∈ set xs ⟹ (t xs ys) x ∈ set ys›
by (induction xs ys rule: list_induct2) auto

(*why is that not in the library?*)
lemma length_sorted_list_of_set[simp]:
‹finite xs ⟹ length (sorted_list_of_set xs) = card xs›
by (metis distinct_card distinct_sorted_list_of_set set_sorted_list_of_set)

lemma
‹finite xs ⟹ finite ys ⟹ card xs = card ys ⟹ x ∈ xs ⟹ explicit_mapping xs ys x ∈ ys›
using t_maps_to_existing[of ‹sorted_list_of_set xs› ‹sorted_list_of_set ys› x]
by (auto simp: explicit_mapping_def)
``````

#### Mathias Fleury (Nov 02 2020 at 05:42):

But again: do you need to build the mapping explicitly or is it sufficient for you to show that one exists?

#### Mathias Fleury (Nov 02 2020 at 05:44):

In the latter case, you can use the function `finite_same_card_bij`.

#### Trinh Le Khanh (Nov 02 2020 at 09:36):

Mathias Fleury said:

In the latter case, you can use the function `finite_same_card_bij`.

Thank you for your comment. This command

``````value ‹explicit_mapping {1, 2, 3} {4, 5, 6}›
``````

returns

``````"_"
:: "nat ⇒ nat"
``````

not

``````(1=>4), (2=>5), (3=>6)
``````

I think the result should be the latter right?

In the latter case, you can use the function `finite_same_card_bij`.

You mean that I can use it when proving lemmas and theorems not defining the mapping, right? Besides, defining the mapping using `SOME` is incorrect. I should change the definition, right?

#### Mathias Fleury (Nov 02 2020 at 10:32):

I am convinced you can change the definitions to change `explicit_mapping` from a function (like it is now) to whatever you want.

#### Mathias Fleury (Nov 02 2020 at 10:33):

``````You mean that I can use it when proving lemmas and theorems not defining the mapping, right? Besides, defining the mapping using SOME is incorrect. I should change the definition, right?
``````

No, using SOME means you cannot compute it, so `value` cannot work. If you don't need the concrete mapping and don't need value, you can use some.

#### Trinh Le Khanh (Nov 02 2020 at 14:02):

So, I keep my definition as follows:

``````definition PType :: "nat set" (*port types*)
where "PType = {1, 2}"

definition PIns :: "nat set set" (*port instances of each port type PType*)
where "PIns = {{5,6}, {7,8,9}}"

definition mapin :: "nat ⇒ nat set" where (*mapin 1 = {5,6}; mapin 2 = {7,8,9}*)
"mapin pt = (if pt ∈ PType then (SOME pIn. pIn ∈ PIns) else {})"

definition alphaSet :: "(nat ⇒ nat) set " where (*set of functions alpha*)
"alphaSet = {f. ∀x∈PType. (f x) ∈ (mapin x)}"
``````

Then, I create a lemma using `finite_same_card_bij` but it unprovable (it stayed in proving forever)

``````lemma test31: "(∀t∈PType.(∀alp∈alphaSet.(P t (alp t) ⟶ (∀l1∈(mapin t)-{alp t}.¬P t l1))))
⟹ (∀t∈PType.(∃alp∈alphaSet.∀l1∈(mapin t)-{alp t}. ¬P t l1))"
unfolding PType_def mapin_def PIns_def alpha_def alphaSet_def
using finite_same_card_bij
apply blast
done
``````

In Math, it should be equal because

``````(P 2 7 ⟶ ¬P 2 8 ∧ ¬P 2 9) ∧ (P 2 8 ⟶ ¬P 2 7 ∧ ¬P 2 9) ∧ (P 2 9 ⟶ ¬P 2 8 ∧ ¬P 2 7)
⟷ (¬P 2 8 ∧ ¬P 2 9)∨(¬P 2 7 ∧ ¬P 2 9)∨(¬P 2 8 ∧ ¬P 2 7)
``````

#### Mathias Fleury (Nov 02 2020 at 14:47):

You misunderstand what `SOME` means. It is an arbitrary choice. Unless that choice is unique, you _cannot say anything_ about its value. In particular `mapin 1 = {5, 6}` might be true but might also be false.

You are in exactly one of those cases:

``````      mapin 1 = {5, 6} and mapin 2 = {7, 8, 9}
or mapin 1 = {5, 6}  and mapin 2 = {5, 6}
or mapin 1 = {7, 8, 9}  and mapin 2 = {5, 6}
or mapin 1 = {7, 8, 9}  and mapin 2 = {7, 8, 9}
``````

YOU HAVE NO WAY TO KNOW WHICH OF THOSE CASES IS TRUE.

Last updated: Aug 15 2022 at 02:13 UTC