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 :-/ ?

What is the problem with the counterexample of nitpick?

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

? and of `{a,b,b}`

?

If you add the assumption `distinct [a,t,p]`

, then your property holds by the way

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.

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}`

.

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`

```
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
*)
```

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

Last updated: Feb 27 2024 at 08:17 UTC