Robert Soeldner (Oct 02 2022 at 14:35): 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
*)
remark that nitpick is already telling you that the counterexample might not be correct
Last updated: Apr 19 2024 at 20:15 UTC