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

refactor(library/data/finset/basic.lean): change order of arguments to induction tactic

Browse source
This commit is contained in:
Jeremy Avigad 2015-05-25 18:37:07 +10:00 committed by Leonardo de Moura
parent fee6ba8749
commit 7c92161e49
3 changed files with 34 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/algebra/group_bigops.lean
View file

@ -130,7 +130,7 @@ section comm_monoid
(∀{x}, x ∈ s → f x = g x) → Prod s f = Prod s g := (∀{x}, x ∈ s → f x = g x) → Prod s f = Prod s g :=
finset.induction_on s finset.induction_on s
(assume H, rfl) (assume H, rfl)
(take s' x, assume H1 : x ∉ s', (take x s', assume H1 : x ∉ s',
assume IH : (∀ {x : A}, x ∈ s' → f x = g x) → Prod s' f = Prod s' g, assume IH : (∀ {x : A}, x ∈ s' → f x = g x) → Prod s' f = Prod s' g,
assume H2 : ∀{y}, y ∈ insert x s' → f y = g y, assume H2 : ∀{y}, y ∈ insert x s' → f y = g y,
assert H3 : ∀y, y ∈ s' → f y = g y, from assert H3 : ∀y, y ∈ s' → f y = g y, from

16
library/data/finset/basic.lean
View file

@ -21,22 +21,22 @@ definition to_nodup_list [h : decidable_eq A] (l : list A) : nodup_list A :=
namespace finset namespace finset
private definition eqv (l₁ l₂ : nodup_list A) := private definition equiv (l₁ l₂ : nodup_list A) :=
perm (elt_of l₁) (elt_of l₂) perm (elt_of l₁) (elt_of l₂)
local infix ~ := eqv local infix ~ := equiv
private definition eqv.refl (l : nodup_list A) : l ~ l := private definition equiv.refl (l : nodup_list A) : l ~ l :=
!perm.refl !perm.refl
private definition eqv.symm {l₁ l₂ : nodup_list A} : l₁ ~ l₂ → l₂ ~ l₁ := private definition equiv.symm {l₁ l₂ : nodup_list A} : l₁ ~ l₂ → l₂ ~ l₁ :=
assume p, perm.symm p assume p, perm.symm p
private definition eqv.trans {l₁ l₂ l₃ : nodup_list A} : l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃ := private definition equiv.trans {l₁ l₂ l₃ : nodup_list A} : l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃ :=
assume p₁ p₂, perm.trans p₁ p₂ assume p₁ p₂, perm.trans p₁ p₂
definition nodup_list_setoid [instance] (A : Type) : setoid (nodup_list A) := definition nodup_list_setoid [instance] (A : Type) : setoid (nodup_list A) :=
setoid.mk (@eqv A) (mk_equivalence (@eqv A) (@eqv.refl A) (@eqv.symm A) (@eqv.trans A)) setoid.mk (@equiv A) (mk_equivalence (@equiv A) (@equiv.refl A) (@equiv.symm A) (@equiv.trans A))
definition finset (A : Type) : Type := definition finset (A : Type) : Type :=
quot (nodup_list_setoid A) quot (nodup_list_setoid A)
@ -196,7 +196,7 @@ quot.induction_on s
protected theorem induction [recursor 6] {P : finset A → Prop} protected theorem induction [recursor 6] {P : finset A → Prop}
(H1 : P empty) (H1 : P empty)
(H2 : ∀⦃s : finset A⦄, ∀{a : A}, a ∉ s → P s → P (insert a s)) : (H2 : ∀ ⦃a : A⦄, ∀{s : finset A}, a ∉ s → P s → P (insert a s)) :
∀s, P s := ∀s, P s :=
take s, take s,
quot.induction_on s quot.induction_on s
@ -221,7 +221,7 @@ quot.induction_on s
protected theorem induction_on {P : finset A → Prop} (s : finset A) protected theorem induction_on {P : finset A → Prop} (s : finset A)
(H1 : P empty) (H1 : P empty)
(H2 : ∀⦃s : finset A⦄, ∀{a : A}, a ∉ s → P s → P (insert a s)) : (H2 : ∀ ⦃a : A⦄, ∀ {s : finset A}, a ∉ s → P s → P (insert a s)) :
P s := P s :=
finset.induction H1 H2 s finset.induction H1 H2 s
end insert end insert

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

@ -16,28 +16,28 @@ 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₂) :=
begin begin
induction s₂ with s₂ a ans2 IH, induction s₂ with a s₂ ans2 IH,
show card s₁ + card (∅:finset A) = card (s₁ ∪ ∅) + card (s₁ ∩ ∅), show card s₁ + card (∅:finset A) = card (s₁ ∪ ∅) + card (s₁ ∩ ∅),
by rewrite [union_empty, card_empty, inter_empty], by rewrite [union_empty, card_empty, inter_empty],
show card s₁ + card (insert a s₂) = card (s₁ ∪ (insert a s₂)) + card (s₁ ∩ (insert a 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'),
begin begin
rewrite [card_insert_of_not_mem ans2, union.comm, -insert_union, union.comm], rewrite [card_insert_of_not_mem ans2, union.comm, -insert_union, union.comm],
rewrite [insert_union, insert_eq_of_mem as1, insert_eq, inter.distrib_left, inter.comm], rewrite [insert_union, insert_eq_of_mem as1, insert_eq, inter.distrib_left, inter.comm],
rewrite [singleton_inter_of_mem as1, -insert_eq, card_insert_of_not_mem H, -*add.assoc], rewrite [singleton_inter_of_mem as1, -insert_eq, card_insert_of_not_mem H, -*add.assoc],
rewrite IH rewrite IH
end) end)
(assume ans1 : a ∉ s₁, (assume ans1 : a ∉ s₁,
assert H : a ∉ s₁ ∪ s₂, from assume H', assert H : a ∉ s₁ ∪ s₂, from assume H',
or.elim (mem_or_mem_of_mem_union H') (assume as1, ans1 as1) (assume as2, ans2 as2), or.elim (mem_or_mem_of_mem_union H') (assume as1, ans1 as1) (assume as2, ans2 as2),
begin begin
rewrite [card_insert_of_not_mem ans2, union.comm, -insert_union, union.comm], rewrite [card_insert_of_not_mem ans2, union.comm, -insert_union, union.comm],
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 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₂) :=
@ -63,7 +63,7 @@ include deceqB
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 := 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 :=
begin begin
induction s with t a H IH, induction s with a t H IH,
{ rewrite [card_empty] }, { rewrite [card_empty] },
{ have H2 : ts t ⊆ ts (insert a t), by rewrite [-subset_eq_to_set_subset]; apply subset_insert, { 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 H3 : card (image f t) = card t, from IH (inj_on_of_inj_on_of_subset H1 H2),
@ -85,7 +85,7 @@ 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 :=
begin begin
induction s with s' a H IH, induction s with a s' H IH,
rewrite [Sum_empty, card_empty, zero_mul], rewrite [Sum_empty, card_empty, zero_mul],
rewrite [Sum_insert_of_not_mem _ H, IH, card_insert_of_not_mem H, add.comm, 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]
@ -102,7 +102,7 @@ theorem card_Union_of_disjoint (s : finset A) (f : A → finset B) :
card (⋃ x ∈ s, f x) = ∑ x ∈ s, card (f x) := card (⋃ x ∈ s, f x) = ∑ x ∈ s, card (f x) :=
finset.induction_on s finset.induction_on s
(assume H, by rewrite [Union_empty, Sum_empty, card_empty]) (assume H, by rewrite [Union_empty, Sum_empty, card_empty])
(take s' a, assume H : a ∉ s', (take a s', assume H : a ∉ s',
assume IH, assume IH,
assume H1 : ∀ {a₁ a₂ : A}, a₁ ∈ insert a s' → a₂ ∈ insert a s' → a₁ ≠ a₂ → f a₁ ∩ f a₂ = ∅, assume H1 : ∀ {a₁ a₂ : A}, a₁ ∈ insert a s' → a₂ ∈ insert a s' → a₁ ≠ a₂ → f a₁ ∩ f a₂ = ∅,
have H2 : ∀ a₁ a₂ : A, a₁ ∈ s' → a₂ ∈ s' → a₁ ≠ a₂ → f a₁ ∩ f a₂ = ∅, from have H2 : ∀ a₁ a₂ : A, a₁ ∈ s' → a₂ ∈ s' → a₁ ≠ a₂ → f a₁ ∩ f a₂ = ∅, from