Stream: Beginner Questions

Topic: partition_on


view this post on Zulip 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 :-/ ?

view this post on Zulip Mathias Fleury (Oct 02 2022 at 14:41):

What is the problem with the counterexample of nitpick?

view this post on Zulip Mathias Fleury (Oct 02 2022 at 14:42):

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

view this post on Zulip Mathias Fleury (Oct 02 2022 at 14:49):

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

view this post on Zulip 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.

view this post on Zulip 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}.

view this post on Zulip 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

view this post on Zulip 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
*)

view this post on Zulip Mathias Fleury (Oct 03 2022 at 18:28):

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


Last updated: Feb 27 2024 at 08:17 UTC