Solving a puzzle using the Isabelle proof assistant
section ‹A Simple Graph Problem› | |
text ‹ | |
We shall prove the following: "In a finite group of people, some of whom are friends with some | |
of the others there must be at least two people who have the same number of friends." | |
› | |
theory Friends | |
imports Main | |
Finite_Set | |
Relation | |
begin | |
subsection ‹Setup› | |
locale Friends = | |
fixes people::"'a set" -- ‹The set of individuals› | |
and frnd::"'a rel" -- ‹The friendship relation› | |
assumes ass_findom: "finite people" -- ‹Finite number of individuals› | |
and ass_two: "card people > 1" -- ‹At least two individual› | |
and ass_dom: "frnd ⊆ people × people" -- ‹The domain of the friendship relation› | |
and ass_irr: "irrefl frnd" -- ‹Friendship is irreflexive› | |
and ass_sym: "sym frnd" -- ‹Friendship is symmetric› | |
begin | |
subsection ‹The number of friends someone has› | |
definition nfriends::"'a⇒nat" where | |
"nfriends x = card (frnd `` {x})" | |
subsection ‹The range of the @{term "frnd"} relationship.› | |
lemma no_x:"∀ x. frnd `` {x} ⊆ people - {x}" | |
proof | |
fix x | |
show "frnd `` {x} ⊆ people - {x}" | |
proof (-) | |
have s1: "frnd `` {x} ⊆ people" using ass_dom by blast | |
have "x ∉ frnd `` {x}" using ass_irr by (simp add:irrefl_def) | |
thus ?thesis using s1 by blast | |
qed | |
qed | |
subsection ‹The main theorem.› | |
text‹ @{term "nfriends"} is not a injective function on @{term "people"}› | |
theorem "¬ inj_on nfriends people" | |
proof (-) | |
text ‹We do a proof by using the pigeon hole principle. | |
@{term "nfriends"} takes on values between $0$ and $n-1$ | |
where $n$ is the number of individuals (the value $n$ being ruled out by irreflexibility. | |
These are exactly $n$ values. However @{term "nfriends} cannot take on both the values | |
$n-1$ and $0$ since if it takes on the value $n-1$ then there is someone who has | |
everyone else as their friend and so no one can have $0$ friends. Thus | |
@{term "nfriends"} can take on at most $n-1$ values, so it must take on at | |
least one value twice› | |
let ?n = "card people" -- ‹Number of people› | |
let ?frnds_rng = "nfriends ` people" -- ‹The range of the nfriends function› | |
text ‹A rough bound on the range of @{term "nfriends"}› | |
have rng_rough: "?frnds_rng ⊆ {0..?n-1}" | |
proof (-) | |
have "∀x ∈ people. nfriends x ≤ ?n-1" using no_x ass_findom | |
by (metis card_Diff_singleton card_mono finite_Diff nfriends_def) | |
thus ?thesis using atLeastAtMost_iff by blast | |
qed | |
text ‹Two possibilities for a stricter bound.› | |
have rng_cases:"?n-1 ∈ ?frnds_rng ⟶ 0 ∉ ?frnds_rng" | |
proof | |
assume popular_guy:"?n-1 ∈ ?frnds_rng" | |
then show " 0 ∉ ?frnds_rng" | |
proof | |
obtain x where thex:"x∈people ∧ nfriends x = ?n-1" using popular_guy by auto | |
hence "frnd `` {x} = people-{x}" using no_x | |
by (simp add: ass_findom card_subset_eq nfriends_def) | |
hence "∀ z∈people. z ≠ x ⟶ (x,z) ∈ frnd" by blast | |
hence "∀ z ∈ people. z ≠ x ⟶ frnd `` {z} ≠ {}" using ass_sym | |
by (metis Image_singleton_iff empty_iff symE) | |
hence "∀ z ∈ people. z ≠ x ⟶ nfriends z ≠ 0" | |
by (metis ass_findom card_0_eq finite_Diff nfriends_def no_x rev_finite_subset) | |
hence "∀ z ∈ people. nfriends z ≠ 0" using ass_two thex by auto | |
hence "0 ∉ ?frnds_rng" using rng_rough by auto | |
thus ?thesis by blast | |
qed | |
qed | |
text ‹The cardinality result we need to apply the pigeonhole principle holds in either case› | |
have "card ?frnds_rng < ?n" | |
proof (cases "?n-1 ∈ ?frnds_rng") | |
case True | |
hence "0 ∉ ?frnds_rng" using rng_cases by simp | |
hence "?frnds_rng ⊆ {0..?n-1}-{0}" using rng_rough by auto | |
hence st:"card ?frnds_rng ≤ card ({0..?n-1}-{0})" | |
by (meson card_mono finite_Diff finite_atLeastAtMost) | |
have ct:"card ({0..?n-1}-{0})<?n" | |
using ass_two by auto | |
show ?thesis using st ct | |
using le_less_trans by blast | |
next | |
case False | |
hence "?frnds_rng ⊆ {0..?n-1}-{?n-1}" using rng_rough by blast | |
hence sf:"card ?frnds_rng ≤ card ({0..?n-1}-{?n-1})" | |
by (meson card_mono finite_Diff finite_atLeastAtMost) | |
have cf:"card ({0..?n-1}-{?n-1})<?n" | |
using ass_two by auto | |
show ?thesis using sf cf | |
using le_less_trans by blast | |
qed | |
text ‹Finally we can apply the pigeonhole principle› | |
thus ?thesis using pigeonhole by auto | |
qed | |
end | |
end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment