Skip to content

Instantly share code, notes, and snippets.

@jmoy
Last active June 10, 2022 20:56
Show Gist options
  • Save jmoy/59c0ef25196716f1a0f4fd0efae6e099 to your computer and use it in GitHub Desktop.
Save jmoy/59c0ef25196716f1a0f4fd0efae6e099 to your computer and use it in GitHub Desktop.
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