Stream: Beginner Questions

Topic: Import Executable_Set

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

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?

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

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

Trinh Le Khanh (Nov 30 2020 at 10:00):

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_setbut 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"

Mathias Fleury (Nov 30 2020 at 11:59):

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.

Mathias Fleury (Nov 30 2020 at 12:03):

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.

Trinh Le Khanh (Nov 30 2020 at 13:00):

Mathias Fleury said:

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.

I'm not clear about making the conversion *deterministic* much. Can you give me some hints, please?

Mathias Fleury (Nov 30 2020 at 13:53):

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?

Mathias Fleury (Nov 30 2020 at 13:56):

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.

Trinh Le Khanh (Nov 30 2020 at 14:30):

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.

Mathias Fleury (Nov 30 2020 at 17:54):

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

Mathias Fleury (Nov 30 2020 at 17:56):

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.

Trinh Le Khanh (Nov 30 2020 at 18:08):

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).

Mathias Fleury (Nov 30 2020 at 19:27):

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"

Trinh Le Khanh (Nov 30 2020 at 19:32):

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.

Mathias Fleury (Nov 30 2020 at 19:33):

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

Mathias Fleury (Nov 30 2020 at 19:34):

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.

Lukas Stevens (Nov 30 2020 at 19:35):

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.

Lukas Stevens (Nov 30 2020 at 19:36):

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

Trinh Le Khanh (Nov 30 2020 at 19:43):

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.

Lukas Stevens (Nov 30 2020 at 19:45):

Lists are always finite

Trinh Le Khanh (Nov 30 2020 at 19:49):

wow, I thought we have to define finite to determine it. Thank you very much.

Trinh Le Khanh (Nov 30 2020 at 23:44):

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 Pi0and the concrete once worked.)

Mathias Fleury (Dec 01 2020 at 10:59):

• 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...)

Mathias Fleury (Dec 01 2020 at 10:59):

(I have nothing to say on the question)

Trinh Le Khanh (Dec 01 2020 at 11:35):

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?

Mathias Fleury (Dec 01 2020 at 11:55):

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

Mathias Fleury (Dec 01 2020 at 11:57):

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.

Mathias Fleury (Dec 01 2020 at 11:59):

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.

Trinh Le Khanh (Dec 01 2020 at 12:05):

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

Mathias Fleury (Dec 01 2020 at 12:10):

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

Mark Wassell (Dec 01 2020 at 14:31):

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.

Trinh Le Khanh (Dec 01 2020 at 16:44):

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)

Mark Wassell (Dec 01 2020 at 17:14):

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)

Trinh Le Khanh (Dec 01 2020 at 19:41):

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: Dec 21 2024 at 08:21 UTC