Stream: Beginner Questions

Topic: Induction and Contradiction Proofs

view this post on Zulip Shriya M (Aug 22 2024 at 16:43):

  1. For a set system (E, F) (E - a finite set and F - a set of subsets of E) here's a lemma that shows that F is closed under arbitrary unions when F is closed under union and contains the empty set.
definition closed_under_union where "closed_under_union F ⟷ (∀X Y. X ∈ F ∧ Y ∈ F ⟶ X ∪ Y ∈ F)"

lemma closed_under_arbitrary_unions:
  assumes "closed_under_union F" "{} ∈ F" "set_system E F"
  shows "∀A. (finite A ∧ (∀i ∈ A. i ∈ F)) ⟶ (⋃i ∈ A. i) ∈ F"
proof (rule allI)
  fix A
  show "finite A ∧ (∀i∈A. i ∈ F) ⟶ (⋃i∈A. i) ∈ F"
  proof
    assume assum1: "finite A ∧ (∀i∈A. i ∈ F)"
    have "finite E" using assms(3) unfolding set_system_def by simp
    then have "finite F" using assms(3) unfolding set_system_def
      by (meson Sup_le_iff finite_UnionD finite_subset)
    then obtain k where "card F = k" by simp
    have "¬(infinite A)" using assum1 by simp
    show "(⋃i∈A. i) ∈ F"
    proof (induction "card A")
      case 0
      then have "A = {}" using ‹¬(infinite A)› card_eq_0_iff by simp
      then have "(⋃i∈A. i) = {}" by simp
      then show "(⋃i∈A. i) ∈ F" using assms(2) by presburger
    next
      case (Suc x)
      then have "card A = (Suc x)" by simp
      then obtain a where "a ∈ A" by fastforce
      then have "card (A - {a}) = x" using ‹card A = (Suc x)› by simp
      then have "x = card (A - {a})" by simp
      then have "(⋃i∈(A - {a}). i) ∈ F" using ‹x = card A ⟹ (⋃i∈A. i) ∈ F› sorry
      have " a ∈ F" using assum1 ‹a ∈ A› by simp
      have "(⋃i∈A. i) = (⋃i∈(A - {a}). i) ∪ a" using ‹a ∈ A› by auto
      also have "... ∈ F" using ‹(⋃i∈(A-{a}). i) ∈ F› ‹a ∈ F› assms(1) unfolding closed_under_union_def by simp
      finally show ?case by simp
    qed
  qed
qed

The line in the proof marked as 'sorry' (that uses the induction hypothesis, 5th line after case (Suc x)) does not terminate for any of the methods. All statements are true, fully proved and valid. Where am I going wrong?

  1. There are two contradiction proofs (that are a part of bigger theorems) that seem valid but don't get proved for any methods. The first one:
then show "False" using a_prop2 sorry

Here, a_prop2 is the second line, and 'then' refers to the first line:

proof (prove)
using this:
    b ∈ τ (E - A ∪ {a}) ∧ card (τ (E - A ∪ {b})) < card (τ (E - A ∪ {a}))
    ∄b. b ∈ τ (E - A ∪ {a}) ∧ card (τ (E - A ∪ {b})) < card (τ (E - A) ∪ {a})

goal (1 subgoal):
 1. False

The second one is:

then show "False" using B_prop(1) set_prop sorry

Here, B_prop(1) refers to the 2nd line, 'then' refers to 1st line and set_prop refers to the last line.

proof (prove)
using this:
    c B ≤ c (B - {y} ∪ {j ! 0})
    ∀A. A ∈ F ∧ c A ≤ c B
    B - {y} ∪ {j ! 0} ∈ F

goal (1 subgoal):
 1. False

I used sledgehammer as well, but it didn't find a proof for any of the cases above. I'd greatly appreciate any help on this. Thanks!

view this post on Zulip Mathias Fleury (Aug 22 2024 at 18:18):

Let's just took at the first:

    b ∈ τ (E - A ∪ {a}) ∧ card (τ (E - A ∪ {b})) < card (τ (E - A ∪ {a}))
    ∄b. b ∈ τ (E - A ∪ {a}) ∧ card (τ (E - A ∪ {b})) < card (τ (E - A) ∪ {a})

Now let's align the goals to find if there is any difference:

            b ∈ τ (E - A ∪ {a}) ∧ card (τ (E - A ∪ {b})) < card (τ (E - A ∪ {a}))
    ∄b. b ∈ τ (E - A ∪ {a}) ∧ card (τ (E - A ∪ {b})) < card (τ (E - A) ∪ {a})

And oh magic there is! the number of parenthesis at the end is not the same

view this post on Zulip Shriya M (Aug 23 2024 at 02:48):

Thanks, both contradiction errors are clear. But I'm still unclear about the induction one, and can't seem to know where the mistake is.

view this post on Zulip Mathias Fleury (Aug 23 2024 at 05:53):

I do not see where you see a contradiction (<= is not strict)

view this post on Zulip Mathias Fleury (Aug 23 2024 at 05:55):

But general rule: whenever you are convinced there is a trivial reasoning leading to the solution, WRITE IT DOWN in Isabelle. That is exactly where Isabelle is great at: checking proofs.

view this post on Zulip Mathias Fleury (Aug 23 2024 at 05:55):

It would have taken you 2min to write the proof down.

view this post on Zulip Shriya M (Aug 23 2024 at 05:58):

Thanks, I understood the contradiction proofs. What about the induction one?

view this post on Zulip Mathias Fleury (Aug 23 2024 at 06:01):

What is the question?

x = card (A - {a})
x = card A ⟹ (⋃i∈A. i) ∈ F

These do not unify this is clear

view this post on Zulip Mathias Fleury (Aug 23 2024 at 06:03):

I could give a solution, but from a teaching perspective, it is better to let you properly write the induction principle what is fixed and what is not and figure it out yourself

view this post on Zulip Shriya M (Aug 23 2024 at 06:04):

Alright, I will try it. Thank you.

Last updated: Dec 21 2024 at 16:20 UTC