Email Gateway (Aug 22 2022 at 10:47): Email Gateway (Aug 22 2022 at 10:47):From: "C. Diekmann" <diekmann@in.tum.de>
Hi everyone,
with lists, I can do case distinctions, which I cannot do with sets.
Is there any good advice to express case distinctions on sets?
Here is my example. With lists, I can write the following:
case [x←xs. P x] of [] => None
| [y] => Some y
| _ => undefined
I would like to write this down for xs being a set. To prove
equivalence, I will use "set xs". Unfortunately, I cannot use "case"
with a set. The best I could come up with is the following:
let matching_entries = {x ∈ set xs. P x} in
if matching_entries = {} then None else
if ∃y. matching_entries = {y} then Some (the_elem matching_entries) else
undefined
Is there a nicer and better way to express this?
If xs is distinct, both versions are equivalent (though the proof was
horrible). For the proof I needed some helper lemmas, for example the
following:
lemma "distinct xs ⟹ {x. x ∈ set xs ∧ P x} = {x} ⟹
[x←xs . P x] = [x]"
apply(induction xs)
apply(simp)
apply(simp)
apply(case_tac "x=a")
apply simp_all
apply (smt DiffD2 Diff_insert_absorb filter_False insert_compr mem_Collect_eq)
by (smt Collect_cong ball_empty insert_iff mem_Collect_eq)
The lemma seems pretty obvious to me so I didn't want to invest much
time into it. This was the best proof I could come up with. Why can't
the built-in tools such as blast solve this lemma instantly? I could
not replace those two smt calls with other one-line methods. What is
it that makes this lemma so hard for Isabelle?
Thanks for your advice,
Cornelius
Email Gateway (Aug 22 2022 at 10:47):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Cornelius,
You can simplify your definitions if you split the filtering from the section of the
elements. It looks as if you are trying to lift the operation "pick the unique element in
a set" into the option monad. So just lift this operaton:
definition the_elem_option :: "'a set => 'a option"
where "the_elem_option A = (if EX1 x. x : A then Some (the_elem A) else None)"
Note that this specification is tighter than yours as the result is None if there are
several elements in the set. If you wanted the function to be undefined in a mathematical
sense, then this approach is likely to make your life hard anyway, because working with
underspecified functions usually causes quite some pain.
Moreover, I've replaces EX x. A = {x} with EX1 x. x : A, because the latter involves more
primitive operations on sets than the former. Intuitively, I'd expect better automation
for the latter, but I have not tested it.
In general, I recommend that you work only at the level of abstraction that fits your
needs. If you want sets (without order on the elements), then stick to the type set (or
fset, if you need finiteness) and never talk about lists. If you need the order of the
elements in the list, then work with lists and convert them to sets when needed, but do
not try to lift the operations from lists to sets when they rely on the order---this
normally directly leads to ugly, messy, tedious proofs.
Picking an element from a set is hard for the automated tools, because it involves a
tricky mix of rewriting and resolution. Blast can only deal with resolution, but not
rewriting, so blast usually does not work well for proofs involving equality. Conversely,
the simplifier cannot deal well with underspecified functions (like the_elem).
Hope this helps,
Andreas
Last updated: Nov 21 2024 at 12:39 UTC