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?
"HOL-Library.Executable_Set"
for the importMathias 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 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?
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.)
(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: Dec 07 2024 at 16:22 UTC