Hi everybody,

I wrote a function to convert a set to a list

```
fun convert_set_to_list :: "'a set ⇒ 'a list" where
"convert_set_to_list {} = []" |
"convert_set_to_list (insert x A) = [x] @ convert_set_to_list A"
```

the output showed:

```
Non-constructor pattern not allowed in sequential mode.
convert_set_to_list {} = []
```

I found a solution that I should import `Executable_Set`

to use `{}`

directly in this forum: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2008-January/msg00035.html

However, when I type `imports Main "~~/src/HOL/Library/Executable_Set"`

, Isabelle said that `Bad theory import "Draft.Executable_Set"`

This library isn't supported anymore?

- the function does not make sense (sets are not ordered: which element do you take first)
`"HOL-Library.Executable_Set"`

for the import

Mathias Fleury said:

- The function does not make sense (sets are not ordered: which element do you take first)

So, there is no way to convert a general set to a list, right? I know `sorted_list_of_set`

but it just applies for primary types like `nat`

, `int`

.

Mathias Fleury said:

`"HOL-Library.Executable_Set"`

for the import

It also doesn't work `Bad theory import "HOL-Library.Executable_Set"`

To convert a set to a list in an *executable* way you need a way to make the conversion *deterministic*. `sorted_list_of_set`

does it by using the natural order relation.

For executable set: the theory does not exist anymore in `HOL/Library`

. I don't know what changed, but most likely you don't need that import anyway.

Mathias Fleury said:

To convert a set to a list in an

executableway you need a way to make the conversiondeterministic.`sorted_list_of_set`

does it by using the natural order relation.

I'm not clear about `making the conversion *deterministic*`

much. Can you give me some hints, please?

take the set {2,3,4} and the lists:

```
[2,3,4]
[4,2,3]
[2,2,3,3,4]
```

all these lists (and many others) respect the conditions `set xs = {2,3,4}`

. Which one do you pick?

What you tried to write is `SPEC(%xs. set xs = {2,3,4})`

. Now you also expect to see a lists such that you do computations on it. Therefore, you want to restrict `(%xs. set xs = {2,3,4})`

to return a *single* result.

Thank you for your suggestion. I tried

```
definition Ptype :: "nat set"
where "Ptype = {0, 1}"
definition Ptype1 :: "nat set"
where "Ptype1 = {2, 3}"
value "(Ptype × Ptype1)"
value "sorted_list_of_set (SPEC (%xs. set xs = Ptype × Ptype1))"
value "hd (sorted_list_of_set (SPEC (%xs. set xs = Ptype × Ptype1)))"
```

I expect that the last line should return `(0,2)`

- a concrete value, but it returns

```
"hd (sorted_list_of_set
(SPEC
(λu. (∀u∈set u. (0, 2) = u ∨ (0, 3) = u ∨ (1, 2) = u ∨ (1, 3) = u) ∧
(0, 2) ∈ set u ∧ (0, 3) ∈ set u ∧ (1, 2) ∈ set u ∧ (1, 3) ∈ set u)))"
:: "'a"
```

this is an abstract return.

SPEC is not executable. I don't understand what you are even trying here....

above I meant that `SPEC(%xs. set xs = {2,3,4})`

is what you seem to be trying to do in an executable way. You cannot use it directly.

I'm trying to convert a set to a list. For example, we have `A = {{1,2}, {3,4}}`

after converting, it will be the list `B = [{1,2}, {3,4}]`

. Thus, when I call `hd B`

the result is `{1, 2}`

. `sorted_list_of_set`

only works for primary types like `nat`

or `int`

but doesn't work for structed types like `set set`

, `list set`

or `(nat * nat)`

.

I believe that you can instantiate lists with an (lin)order to make sorted_list_of_set work on "nat list list" (something like lenlex?), but I don't see how to make anything work for "set set"

Yes, `nat list list`

is no problem. That's why I want to know is whether any library to convert a general set to a list? But it seems doesn't exist.

sorry I meant "nat list set", not "nat list list"

Trinh Le Khanh said:

Yes,

`nat list list`

is no problem. That's why I want to know is whether any library to convert a general set to a list? But it seems doesn't exist.

No, because it cannot work in HOL.

I have a question: why don't you use lists directly? The automation for them is quite good and you can use `set`

to convert them to a set.

Lists also have induction rules that are more convenient to work with compared to finite sets.

Ah, it depends on my problem. Suppose we have some *Type* (e.g. Windows, Mac OS) and each of them have a set of concrete *Instances* (e.g. {w98, xp, w7}, {Catalina, Big Sur}).

Firstly, I defined them as lists and it works. Then, I run to a general case, in which we define *Type* and *Instances* in an abstract view. For example:

```
lemma test_smt:
assumes "finite Types"
```

I mean, Types and Instances are finite sets (we don't care about concrete values). We seem cannot define a `finite list`

like this.

Lists are always finite

wow, I thought we have to define `finite`

to determine it. Thank you very much.

I wrote this lemma but it unprovable, can you check it a little bit?

```
fun pair_mapping :: "'a list ⇒ 'b list list ⇒ ('a * 'b) list" where
"pair_mapping [] [] = []" |
"pair_mapping (x # xs) [] = []" |
"pair_mapping [] (y # ys) = []" |
"pair_mapping (x # xs) (y # ys) = pair_ns x y @ pair_mapping xs ys"
fun set_ins_of_type :: "'a ⇒ 'a list ⇒ 'a list list ⇒ 'a set" where
"set_ins_of_type k PT PI = (if k ∈ (set PT) then set (lookup k (pair_mapping PT PI)) else {})"
(*---------more complex------------*)
lemma test_complex:
assumes "(Pt :: 'a list) ≠ []"
assumes "(PIns :: 'a list list) ≠ []"
assumes "length Pt = length PIns"
assumes "∀x ∈ set PIns. x ≠ []"
shows "(∀k ∈ set Pt.∀h∈ (set_ins_of_type k Pt PIns). P k h ⟶ (∀h1∈ (set_ins_of_type k Pt PIns)-{h}. ¬P k h1)) ⟹
(∀k ∈ set Pt.∃h∈ (set_ins_of_type k Pt PIns).∀h1∈ (set_ins_of_type k Pt PIns)-{h}. ¬P k h1)"
using [[simp_trace]] assms
sledgehammer (*all the provers timed out*)
```

Then, I back to a concrete example but this lemma is also unprovable.

```
(*---------test types------------*)
definition Pt0 :: "nat list"
where "Pt0 = [0, 1]"
definition Pi0 :: "nat list list"
where "Pi0 = [[2,3], [4,5]]"
lemma "∀k ∈ set Pt0.∀h∈ (set_ins_of_type k Pt0 Pi0). P k h ⟶ (∀h1∈ (set_ins_of_type k Pt0 Pi0)-{h}. ¬P k h1)
⟹ ∀k ∈ set Pt0.∃h∈ (set_ins_of_type k Pt0 Pi0).∀h1∈ (set_ins_of_type k Pt0 Pi0)-{h}. ¬P k h1"
unfolding Pt0_def Pi0_def
using [[simp_trace]]
sledgehammer
```

Then I used `value`

to compute the LHS and RHS of the lemma separately and make a new lemma for them. It worked

```
value "∀k ∈ set Pt0.∀h∈ (set_ins_of_type k Pt0 Pi0). P k h ⟶ (∀h1∈ (set_ins_of_type k Pt0 Pi0)-{h}. ¬P k h1)"
value "∀k ∈ set Pt0.∃h∈ (set_ins_of_type k Pt0 Pi0).∀h1∈ (set_ins_of_type k Pt0 Pi0)-{h}. ¬P k h1"
lemma concrete: "(((P 0 2 ⟶ ¬ P 0 3) ∧ (P 0 3 ⟶ ¬ P 0 2)) ∧ (P 1 4 ⟶ ¬ P 1 5) ∧ (P 1 5 ⟶ ¬ P 1 4)) ⟹ ((¬ P 0 3 ∨ ¬ P 0 2) ∧ (¬ P 1 5 ∨ ¬ P 1 4))"
by blast
```

I don't know why the lemma using variables doesn't work but the concrete once does. (I also made a large number of each element in the list `Pi0`

and the concrete once worked.)

- supply [[simp_trace]]` before sledgehammer makes no sense
- sledgehammer is not magic: you still have to prove things by hand (and in your case you still have the loop in the simplifier, which you should probably investigate...)

(I have nothing to say on the question)

Mathias Fleury said:

(I have nothing to say on the question)

I'm sorry if the question looks stupid but actually, I have no direction to understand why it was. Could you give me some hints to find the answer?

Let me answer with another question: why would any tactic be able to solve your goal?

Even if lectures make it look like everything can be solved by a magic combination of `induction`

and `auto`

, this is not the case in general. It is impossible to translate a proof in Isabelle that you don't really understand. Even if you find the proof trivial and Isabelle fails, you have to decompose into even simpler steps. And if those steps are still too complicated, you have to do even smaller steps.

Usually the simpler steps hint as lemmas you have to prove. Maybe those steps will allow to have a proof like `by (auto ...)`

. Maybe not.

Mathias Fleury said:

Let me answer with another question: why would any tactic be able to solve your goal?

because it's small enough to be proved by provers, right?

As I understand, I should split the lemma into small cases and prove them manually, right? looks like this:

```
proof (induct xs arbitrary: ys zs)
case Nil then show ?case by simp
next
case (Cons x xs ys zs) then show ?case by (cases ys, simp_all)
(cases zs, simp_all)
qed
```

I would not have started by an induction, but I also spent less than 2s of thinking about it.

I could be wrong but it would seem that you are trying to prove a specific case of this:

```
lemma
assumes "S ∉ {}" and "∀X ∈ S. X ≠ {}"
assumes "∀X ∈ S. ∀x ∈ X. P x ⟶ (∀y ∈ X - { x }. ¬ P y)"
shows "∀X ∈ S. ∃x ∈ X. ∀y ∈ X - { x }. ¬ P y"
```

which is easily provable.

Mark Wassell said:

I could be wrong but it would seem that you are trying to prove a specific case of this:

`lemma assumes "S ∉ {}" and "∀X ∈ S. X ≠ {}" assumes "∀X ∈ S. ∀x ∈ X. P x ⟶ (∀y ∈ X - { x }. ¬ P y)" shows "∀X ∈ S. ∃x ∈ X. ∀y ∈ X - { x }. ¬ P y"`

which is easily provable.

Thank you for concerning my problem.

If the predicate has a single parameter like `P x, Q y`

, I can prove it easily as follows:

```
lemma test_simplest:
assumes "finite Pt" and "Pt ≠ {}"
shows "(∀x ∈ Pt. P x ⟶ (∀x1 ∈ Pt - {x}. ¬P x1)) ⟹ (∃x∈Pt.∀x1∈Pt-{x}. ¬P x1)"
using [[simp_trace]] assms
sledgehammer
by blast
```

My case is a little bit more complex with two or more parameters like `P x y`

or `Q x y z`

and the value of the latter one is depended on the value of the previous (e.g. `z`

depends on `y`

, and `y`

depends on `x`

)

Mathematically you are working with a set of indexed sets: your list Pt is providing the index and PIns the elements of the indexed set. Here is a more complicated lemma that is closer to what you need. Here the predicate takes two parameters

```
lemma test_simplest3:
fixes S:: "('a * ('b set)) set"
assumes "S ∉ {}" and "∀X ∈ S. snd X ≠ {}"
assumes "∀X ∈ S. ∀x ∈ snd X. P (fst X) x ⟶ (∀y ∈ (snd X - { x }). ¬ P (fst X) y)"
shows "∀X ∈ S. ∃x ∈ snd X. ∀y ∈ snd X - { x }. ¬ P (fst X) y"
using assms
by (metis Diff_iff equals0I)
```

Mark Wassell said:

Mathematically you are working with a set of indexed sets: your list Pt is providing the index and PIns the elements of the indexed set. Here is a more complicated lemma that is closer to what you need. Here the predicate takes two parameters

`lemma test_simplest3: fixes S:: "('a * ('b set)) set" assumes "S ∉ {}" and "∀X ∈ S. snd X ≠ {}" assumes "∀X ∈ S. ∀x ∈ snd X. P (fst X) x ⟶ (∀y ∈ (snd X - { x }). ¬ P (fst X) y)" shows "∀X ∈ S. ∃x ∈ snd X. ∀y ∈ snd X - { x }. ¬ P (fst X) y" using assms by (metis Diff_iff equals0I)`

That's amazing. I realize that I'm solving my problem in a complex way by defining separately `'a`

and `'b set`

and calculating everything on them. Thank you so much.

Last updated: Oct 13 2024 at 01:36 UTC