michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/data/finset/card): test 'induction' tactic at finset

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-19 15:56:51 -07:00
parent 5f628d5080
commit 1665ee39e8
1 changed files with 27 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

59
library/data/finset/card.lean
View file

@ -15,13 +15,11 @@ variables [deceqA : decidable_eq A] [deceqB : decidable_eq B]
include deceqA include deceqA
theorem card_add_card (s₁ s₂ : finset A) : card s₁ + card s₂ = card (s₁ ∪ s₂) + card (s₁ ∩ s₂) := theorem card_add_card (s₁ s₂ : finset A) : card s₁ + card s₂ = card (s₁ ∪ s₂) + card (s₁ ∩ s₂) :=
finset.induction_on s₂ begin
(show card s₁ + card ∅ = card (s₁ ∪ ∅) + card (s₁ ∩ ∅), induction s₂ with s₂ a ans2 IH,
by rewrite [union_empty, card_empty, inter_empty]) show card s₁ + card (∅:finset A) = card (s₁ ∪ ∅) + card (s₁ ∩ ∅),
(take s₂ a, by rewrite [union_empty, card_empty, inter_empty],
assume ans2: a ∉ s₂, show card s₁ + card (insert a s₂) = card (s₁ ∪ (insert a s₂)) + card (s₁ ∩ (insert a s₂)),
assume IH : card s₁ + card s₂ = card (s₁ ∪ s₂) + card (s₁ ∩ s₂),
show card s₁ + card (insert a s₂) = card (s₁ ∪ (insert a s₂)) + card (s₁ ∩ (insert a s₂)),
from decidable.by_cases from decidable.by_cases
(assume as1 : a ∈ s₁, (assume as1 : a ∈ s₁,
assert H : a ∉ s₁ ∩ s₂, from assume H', ans2 (mem_of_mem_inter_right H'), assert H : a ∉ s₁ ∩ s₂, from assume H', ans2 (mem_of_mem_inter_right H'),
@ -39,7 +37,8 @@ finset.induction_on s₂
rewrite [card_insert_of_not_mem H, insert_eq, inter.distrib_left, inter.comm], rewrite [card_insert_of_not_mem H, insert_eq, inter.distrib_left, inter.comm],
rewrite [singleton_inter_of_not_mem ans1, empty_union, add.right_comm], rewrite [singleton_inter_of_not_mem ans1, empty_union, add.right_comm],
rewrite [-add.assoc, IH] rewrite [-add.assoc, IH]
end)) end)
end
theorem card_union (s₁ s₂ : finset A) : card (s₁ ∪ s₂) = card s₁ + card s₂ - card (s₁ ∩ s₂) := theorem card_union (s₁ s₂ : finset A) : card (s₁ ∪ s₂) = card s₁ + card s₂ - card (s₁ ∩ s₂) :=
calc calc
@ -62,39 +61,35 @@ section card_image
open set open set
include deceqB include deceqB
theorem card_image_eq_of_inj_on {f : A → B} {s : finset A} : theorem card_image_eq_of_inj_on {f : A → B} {s : finset A} (H1 : inj_on f (ts s)) : card (image f s) = card s :=
inj_on f (ts s) → card (image f s) = card s := begin
finset.induction_on s induction s with t a H IH,
(assume H : inj_on f (ts empty), calc { rewrite [card_empty] },
card (image f empty) = 0 : card_empty { have H2 : ts t ⊆ ts (insert a t), by rewrite [-subset_eq_to_set_subset]; apply subset_insert,
... = card empty : card_empty) have H3 : card (image f t) = card t, from IH (inj_on_of_inj_on_of_subset H1 H2),
(take t a, have H4 : f a ∉ image f t,
assume H : a ∉ t,
assume IH : inj_on f (ts t) → card (image f t) = card t,
assume H1 : inj_on f (ts (insert a t)),
have H2 : ts t ⊆ ts (insert a t), by rewrite [-subset_eq_to_set_subset]; apply subset_insert,
have H3 : card (image f t) = card t, from IH (inj_on_of_inj_on_of_subset H1 H2),
have H4 : f a ∉ image f t,
proof proof
assume H5 : f a ∈ image f t, assume H5 : f a ∈ image f t,
obtain x (H6l : x ∈ t) (H6r : f x = f a), from exists_of_mem_image H5, obtain x (H6l : x ∈ t) (H6r : f x = f a), from exists_of_mem_image H5,
have H7 : x = a, from H1 (mem_insert_of_mem _ H6l) !mem_insert H6r, have H7 : x = a, from H1 (mem_insert_of_mem _ H6l) !mem_insert H6r,
show false, from H (H7 ▸ H6l) show false, from H (H7 ▸ H6l)
qed, qed,
calc calc
card (image f (insert a t)) = card (insert (f a) (image f t)) : image_insert card (image f (insert a t)) = card (insert (f a) (image f t)) : image_insert
... = card (image f t) + 1 : card_insert_of_not_mem H4 ... = card (image f t) + 1 : card_insert_of_not_mem H4
... = card t + 1 : H3 ... = card t + 1 : H3
... = card (insert a t) : card_insert_of_not_mem H) ... = card (insert a t) : card_insert_of_not_mem H
}
end
end card_image end card_image
theorem Sum_const_eq_card_mul (s : finset A) (n : nat) : (∑ x ∈ s, n) = card s * n := theorem Sum_const_eq_card_mul (s : finset A) (n : nat) : (∑ x ∈ s, n) = card s * n :=
finset.induction_on s begin
(by rewrite [Sum_empty, card_empty, zero_mul]) induction s with s' a H IH,
(take s' a, assume H : a ∉ s', rewrite [Sum_empty, card_empty, zero_mul],
assume IH, rewrite [Sum_insert_of_not_mem _ H, IH, card_insert_of_not_mem H, add.comm,
by rewrite [Sum_insert_of_not_mem _ H, IH, card_insert_of_not_mem H, add.comm, mul.right_distrib, one_mul]
mul.right_distrib, one_mul]) end
theorem Sum_one_eq_card (s : finset A) : (∑ x ∈ s, (1 : nat)) = card s := theorem Sum_one_eq_card (s : finset A) : (∑ x ∈ s, (1 : nat)) = card s :=
eq.trans !Sum_const_eq_card_mul !mul_one eq.trans !Sum_const_eq_card_mul !mul_one