## Stream: Beginner Questions

### Topic: ✔ partition_on

#### Robert Soeldner (Oct 03 2022 at 18:37):

I still struggle with this example, `card {{0, 1, 2}}` is 1 whereby nitpick reports 2 ...

#### Mathias Fleury (Oct 03 2022 at 18:44):

``````lemma
assumes ‹card (P :: nat set set) ≥ 2›
‹disjoint P›
shows ‹⋂P = {}›
proof -
have ‹finite P›
using assms(1) le_simps(2) by force
then obtain a b P' where
H: ‹a ≠ b› ‹a ∉ P'› ‹b ∉ P'› and
P: ‹P = {a,b} ∪ P'› and
fin: ‹finite P'›
using assms apply (induction P rule: finite_induct)
subgoal by auto
subgoal premises p for a A
using p apply auto
by (induction A rule: finite_induct)
(auto, metis, metis)
done
show ?thesis
using fin H assms(2) unfolding P
apply (induction P' rule: finite_induct)
apply (auto simp: disjoint_def)
done
qed
``````

#### Mathias Fleury (Oct 03 2022 at 18:45):

so it holds actually, it is really a wrong counterexample

#### Mathias Fleury (Oct 03 2022 at 18:46):

(the proof can clearly be improved… `auto, metis, metis` is a don't do that)

#### Mathias Fleury (Oct 03 2022 at 18:51):

(and the obtain a b should actually come from two case distinctions… but the default case distinction is missing the `a ∉ P'` in the assumption)

#### Robert Soeldner (Oct 03 2022 at 18:54):

Thank you! Actually, the counterexample drove me crazy. Very hard for me to distinguish and identify the issue. Highly appreciate your support here :-)

#### Notification Bot (Oct 03 2022 at 18:54):

Robert Soeldner has marked this topic as resolved.

#### Mathias Fleury (Oct 03 2022 at 19:10):

Usually when you see "potentially spurious counterexample", the counterexample is really spurious

#### Manuel Eberl (Oct 09 2022 at 21:22):

Note that disjoint_family_on is often better than disjoint

#### Manuel Eberl (Oct 09 2022 at 21:22):

I.e. working with indexed families of sets instead of sets of sets

Last updated: Dec 07 2023 at 08:19 UTC