## Stream: Beginner Questions

### Topic: partition_on

#### Robert Soeldner (Oct 02 2022 at 14:35):

I'm stuck proving properties of `partition_on`, e.g. `‹partition_on X {a,t,p} ⟹ partition_on X {a,e,p} ⟹ t = e›` or even simpler: `‹partition_on X A ⟹ ⋂A = {}`. Is there something I misinterpret, even nitpick finds a counterexample :-/ ?

#### Mathias Fleury (Oct 02 2022 at 14:41):

What is the problem with the counterexample of nitpick?

#### Mathias Fleury (Oct 02 2022 at 14:42):

To understand it: what is the value of `{a,a,b}`? and of `{a,b,b}`?

#### Mathias Fleury (Oct 02 2022 at 14:49):

If you add the assumption `distinct [a,t,p]`, then your property holds by the way

#### Robert Soeldner (Oct 02 2022 at 15:35):

It looks like, I even have a wrong understanding of `disjoint` (used by `partition_on`). My mental assumption was `disjoint {A,B} ⟷ A ∩ B = {}` which is obviously not true.

#### Mathias Fleury (Oct 02 2022 at 15:40):

It is more a notation problem:

``````lemma ‹A≠B ⟹ disjoint {A,B} ⟷ A∩B = {}›
by (auto simp: disjoint_def)
``````

People usually implicitly mean `A≠B` when they writing `{A,B}`.

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

You are right, still this _feels_ strange. What prevents `card (P :: nat set set) ≥ 2 ⟹ disjoint P ⟹ ⋂P = {}` to also pass? Nitpick reports: `P = {{0, 1, 2}}` which should already conflict with the assumption `card (P :: nat set set) ≥ 2`

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

``````lemma ‹card (P :: nat set set) ≥ 2 ⟹ disjoint P ⟹ ⋂P = {}›
nitpick[eval="⋂P" "card (P :: nat set set)"]
(*
Nitpicking formula...
Nitpick found a potentially spurious counterexample:
Free variable:
P = {{0, 1, 2}}
Evaluated terms:
⋂ P = {0, 1, 2}
card P = 2
Nitpick checked 7 of 10 scopes
*)
``````

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

remark that nitpick is already telling you that the counterexample might not be correct

Last updated: Dec 07 2023 at 20:16 UTC