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 21 2024 at 16:20 UTC