-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathPigeonhole_principle.lean
122 lines (103 loc) · 3.79 KB
/
Pigeonhole_principle.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
-- Pigeonhole_principle.lean
-- Pigeonhole principle.
-- José A. Alonso Jiménez <https://jaalonso.github.io>
-- Seville, October 7, 2024
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Prove the pigeonhole principle; that is, if S is a finite set and T
-- and U are subsets of S such that the number of elements of S is less
-- than the sum of the number of elements of T and U, then the
-- intersection of T and U is non-empty.
-- ---------------------------------------------------------------------
-- Proof in natural language
-- =========================
-- By contradiction. For this, let's assume that
-- T ∩ U = ∅ (1)
-- and we have to prove that
-- card(T) + card(U) ≤ card(S) (2)
-- The inequality (2) is proved by the following chain of relations:
-- card(T) + card(U) = card(T ∪ U) + card(T ∩ U)
-- = card(T ∪ U) + 0 [by (1)]
-- = card(T ∪ U)
-- ≤ card(S) [because T ⊆ S and U ⊆ S]
-- Proofs with Lean4
-- =================
import Mathlib.Data.Finset.Card
open Finset
variable [DecidableEq α]
variable {s t u : Finset α}
set_option pp.fieldNotation false
-- Proof 1
-- =======
example
(hts : t ⊆ s)
(hus : u ⊆ s)
(hstu : card s < card t + card u)
: Finset.Nonempty (t ∩ u) :=
by
contrapose! hstu
-- hstu : ¬Finset.Nonempty (t ∩ u)
-- ⊢ card t + card u ≤ card s
have h1 : t ∩ u = ∅ := not_nonempty_iff_eq_empty.mp hstu
have h2 : card (t ∩ u) = 0 := card_eq_zero.mpr h1
calc
card t + card u
= card (t ∪ u) + card (t ∩ u) := (card_union_add_card_inter t u).symm
_ = card (t ∪ u) + 0 := congrArg (card (t ∪ u) + .) h2
_ = card (t ∪ u) := add_zero (card (t ∪ u))
_ ≤ card s := card_le_card (union_subset hts hus)
-- Proof 2
-- =======
example
(hts : t ⊆ s)
(hus : u ⊆ s)
(hstu : card s < card t + card u)
: Finset.Nonempty (t ∩ u) :=
by
contrapose! hstu
-- hstu : ¬Finset.Nonempty (t ∩ u)
-- ⊢ card t + card u ≤ card s
calc
card t + card u
= card (t ∪ u) + card (t ∩ u) :=
(card_union_add_card_inter t u).symm
_ = card (t ∪ u) + 0 :=
congrArg (card (t ∪ u) + .) (card_eq_zero.mpr (not_nonempty_iff_eq_empty.mp hstu))
_ = card (t ∪ u) :=
add_zero (card (t ∪ u))
_ ≤ card s :=
card_le_card (union_subset hts hus)
-- Proof 3
-- =======
example
(hts : t ⊆ s)
(hus : u ⊆ s)
(hstu : card s < card t + card u)
: Finset.Nonempty (t ∩ u) :=
by
contrapose! hstu
-- hstu : ¬Finset.Nonempty (t ∩ u)
-- ⊢ card t + card u ≤ card s
calc
card t + card u
= card (t ∪ u) := by simp [← card_union_add_card_inter,
not_nonempty_iff_eq_empty.1 hstu]
_ ≤ card s := by gcongr; exact union_subset hts hus
-- Proof 4
-- =======
example
(hts : t ⊆ s)
(hus : u ⊆ s)
(hstu : card s < card t + card u)
: Finset.Nonempty (t ∩ u) :=
inter_nonempty_of_card_lt_card_add_card hts hus hstu
-- Used lemmas
-- ===========
-- variable (a : ℕ)
-- #check (add_zero a : a + 0 = a)
-- #check (card_eq_zero : card s = 0 ↔ s = ∅)
-- #check (card_le_card : s ⊆ t → card s ≤ card t)
-- #check (card_union_add_card_inter s t : card (s ∪ t) + card (s ∩ t) =card s + card t)
-- #check (inter_nonempty_of_card_lt_card_add_card : t ⊆ s → u ⊆ s → card s < card t + card u → Finset.Nonempty (t ∩ u))
-- #check (not_nonempty_iff_eq_empty : ¬Finset.Nonempty s ↔ s = ∅)
-- #check (union_subset : s ⊆ u → t ⊆ u → s ∪ t ⊆ u)