Stream: Beginner Questions

Topic: Finite subset lattice "induction"


view this post on Zulip Florian Sextl (Feb 14 2023 at 07:53):

I want to prove the following lemma:

lemma "⟦finite A; P {}⟧ ⟹ ∃E⊆A. P E ∧ (∄T. T⊆A ∧ P T ∧ E ⊂ T)"

The intuitive proof would be that the subset lattice of A is finite and therefore we can always find a locally maximal subset satisfying P (as at least the empty set satisfies it). It would only be a local maximum as P does not necessarily hold for A.
Unfortunately, I have no idea how to translate this proof idea to Isabelle. Is there any kind of "induction" on finite subset lattices available?
I'd expect to have the empty set as the bottom element as the base case and some kind of induction step going a step up in the lattice.

view this post on Zulip Christian Pardillo Laursen (Feb 15 2023 at 15:26):

You can use fact Finite_Set.finite_has_maximal, which they prove using induction rule finite_psubset_induct. Here's a quick proof of your lemma:

lemma "⟦finite A; P {}⟧ ⟹ ∃E⊆A. P E ∧ (∄T. T⊆A ∧ P T ∧ E ⊂ T)"
proof -
  assume *: "finite A" "P {}"
  have "∃m∈{x. x ⊆ A ∧ P x}. ∀b∈{x. x ⊆ A ∧ P x}. m ⊆ b ⟶ m = b"
    apply (rule finite_has_maximal)
    using * by auto
  then show ?thesis
    by (simp add: psubset_eq, metis)
qed

view this post on Zulip Florian Sextl (Feb 16 2023 at 07:59):

Thank you very much, that's exactly what I was looking for!
I didn't expect the proof to be that straightforward, but finite_has_maximal and finite_psubset_induct are really helpful.


Last updated: Feb 27 2024 at 08:17 UTC