feat(library/data/finset/equiv): show that (finset nat) is isomorphic to nat
This commit is contained in:
Leonardo de Moura
parent
1cacac2789
commit
6fd3affeb1
2 changed files with 242 additions and 5 deletions
library/data
|
|
@ -51,12 +51,232 @@ iff.intro
|
|||
assert odd (s div 2^(succ n)), by rewrite [pow_succ, mul.comm, -div_div_eq_div_mul]; assumption,
|
||||
show succ n ∈ of_nat s, from mem_of_nat_of_odd this)
|
||||
|
||||
/-
|
||||
private lemma odd_of_zero_mem (s : nat) : 0 ∈ of_nat s ↔ odd s :=
|
||||
begin
|
||||
unfold of_nat, rewrite [mem_sep_eq, pow_zero, div_one, mem_upto_eq],
|
||||
show 0 < succ s ∧ odd s ↔ odd s, from
|
||||
iff.intro
|
||||
(assume h, and.right h)
|
||||
(assume h, and.intro (zero_lt_succ s) h)
|
||||
end
|
||||
|
||||
private lemma even_of_not_zero_mem (s : nat) : 0 ∉ of_nat s ↔ even s :=
|
||||
have aux : 0 ∉ of_nat s ↔ ¬odd s, from not_iff_not_of_iff (odd_of_zero_mem s),
|
||||
iff.intro
|
||||
(suppose 0 ∉ of_nat s, even_of_not_odd (iff.mp aux this))
|
||||
(suppose even s, iff.mpr aux (not_odd_of_even this))
|
||||
|
||||
private lemma even_to_nat (s : finset nat) : even (to_nat s) ↔ 0 ∉ s :=
|
||||
finset.induction_on s dec_trivial
|
||||
(λ a s nains ih,
|
||||
begin
|
||||
rewrite [to_nat_insert nains], apply iff.intro,
|
||||
suppose even (2^a + to_nat s), by_cases
|
||||
(suppose e : even (2^a), by_cases
|
||||
(suppose even (to_nat s),
|
||||
assert 0 ∉ s, from iff.mp ih this,
|
||||
suppose 0 ∈ insert a s, or.elim (eq_or_mem_of_mem_insert this)
|
||||
(suppose 0 = a, begin rewrite [-this at e], exact absurd e not_even_one end)
|
||||
(by contradiction))
|
||||
(suppose odd (to_nat s), absurd `even (2^a + to_nat s)` (odd_add_of_even_of_odd `even (2^a)` this)))
|
||||
(suppose o : odd (2^a), by_cases
|
||||
(suppose even (to_nat s), absurd `even (2^a + to_nat s)` (odd_add_of_odd_of_even `odd (2^a)` this))
|
||||
(suppose odd (to_nat s), suppose 0 ∈ insert a s, or.elim (eq_or_mem_of_mem_insert this)
|
||||
(suppose 0 = a,
|
||||
have even (to_nat s), from iff.mpr ih (by rewrite -this at nains; exact nains),
|
||||
absurd this `odd (to_nat s)`)
|
||||
(suppose 0 ∈ s,
|
||||
assert a ≠ 0, from suppose a = 0, by subst a; contradiction,
|
||||
begin
|
||||
cases a with a, contradiction,
|
||||
have odd (2*2^a), by rewrite [pow_succ at o, mul.comm]; exact o,
|
||||
have even (2*2^a), from !even_two_mul,
|
||||
exact absurd `even (2*2^a)` `odd (2*2^a)`
|
||||
end))),
|
||||
suppose 0 ∉ insert a s,
|
||||
have a ≠ 0, from suppose a = 0, absurd (by rewrite this; apply mem_insert) `0 ∉ insert a s`,
|
||||
have 0 ∉ s, from suppose 0 ∈ s, absurd (mem_insert_of_mem _ this) `0 ∉ insert a s`,
|
||||
have even (to_nat s), from iff.mpr ih this,
|
||||
match a with
|
||||
| 0 := suppose a = 0, absurd this `a ≠ 0`
|
||||
| (succ a') := suppose a = succ a',
|
||||
have even (2^(succ a')), by rewrite [pow_succ, mul.comm]; apply even_two_mul,
|
||||
even_add_of_even_of_even this `even (to_nat s)`
|
||||
end rfl
|
||||
end)
|
||||
|
||||
private lemma of_nat_eq_insert_zero {s : nat} : 0 ∉ of_nat s → of_nat (2^0 + s) = insert 0 (of_nat s) :=
|
||||
assume h : 0 ∉ of_nat s,
|
||||
assert even s, from iff.mp (even_of_not_zero_mem s) h,
|
||||
have odd (s+1), from odd_succ_of_even this,
|
||||
assert zmem : 0 ∈ of_nat (s+1), from iff.mpr (odd_of_zero_mem (s+1)) this,
|
||||
obtain w (hw : s = 2*w), from exists_of_even `even s`,
|
||||
begin
|
||||
rewrite [pow_zero, add.comm, hw],
|
||||
show of_nat (2*w+1) = insert 0 (of_nat (2*w)), from
|
||||
finset.ext (λ n,
|
||||
match n with
|
||||
| 0 := iff.intro (λ h, !mem_insert) (λ h, by rewrite [hw at zmem]; exact zmem)
|
||||
| succ m :=
|
||||
assert d₁ : 1 div 2 = 0, from dec_trivial,
|
||||
assert aux : _, from calc
|
||||
succ m ∈ of_nat (2 * w + 1) ↔ m ∈ of_nat ((2*w+1) div 2) : succ_mem_of_nat
|
||||
... ↔ m ∈ of_nat w : by rewrite [add.comm, add_mul_div_self_left _ _ (dec_trivial : 2 > 0), d₁, zero_add]
|
||||
... ↔ m ∈ of_nat (2*w div 2) : by rewrite [mul.comm, mul_div_cancel _ (dec_trivial : 2 > 0)]
|
||||
... ↔ succ m ∈ of_nat (2*w) : succ_mem_of_nat,
|
||||
iff.intro
|
||||
(λ hl, finset.mem_insert_of_mem _ (iff.mp aux hl))
|
||||
(λ hr, or.elim (eq_or_mem_of_mem_insert hr)
|
||||
(by contradiction)
|
||||
(iff.mpr aux))
|
||||
end)
|
||||
end
|
||||
|
||||
private lemma of_nat_eq_insert : ∀ {n s : nat}, n ∉ of_nat s → of_nat (2^n + s) = insert n (of_nat s)
|
||||
| 0 s h := of_nat_eq_insert_zero h
|
||||
| (succ n) s h :=
|
||||
have n ∉ of_nat (s div 2), from iff.mp (not_iff_not_of_iff !succ_mem_of_nat) h,
|
||||
assert ih : of_nat (2^n + s div 2) = insert n (of_nat (s div 2)), from of_nat_eq_insert this,
|
||||
finset.ext (λ x,
|
||||
have gen : ∀ m, m ∈ of_nat (2^(succ n) + s) ↔ m ∈ insert (succ n) (of_nat s)
|
||||
| zero :=
|
||||
have even (2^(succ n)), by rewrite [pow_succ, mul.comm]; apply even_two_mul,
|
||||
have aux₁ : odd (2^(succ n) + s) ↔ odd s, from iff.intro
|
||||
(suppose odd (2^(succ n) + s), by_contradiction
|
||||
(suppose ¬ odd s,
|
||||
have even s, from even_of_not_odd this,
|
||||
have even (2^(succ n) + s), from even_add_of_even_of_even `even (2^(succ n))` this,
|
||||
absurd `odd (2^(succ n) + s)` (not_odd_of_even this)))
|
||||
(suppose odd s, odd_add_of_even_of_odd `even (2^(succ n))` this),
|
||||
have aux₂ : odd s ↔ 0 ∈ insert (succ n) (of_nat s), from iff.intro
|
||||
(suppose odd s, finset.mem_insert_of_mem _ (iff.mpr !odd_of_zero_mem this))
|
||||
(suppose 0 ∈ insert (succ n) (of_nat s), or.elim (eq_or_mem_of_mem_insert this)
|
||||
(by contradiction)
|
||||
(suppose 0 ∈ of_nat s, iff.mp !odd_of_zero_mem this)),
|
||||
calc
|
||||
0 ∈ of_nat (2^(succ n) + s) ↔ odd (2^(succ n) + s) : odd_of_zero_mem
|
||||
... ↔ odd s : aux₁
|
||||
... ↔ 0 ∈ insert (succ n) (of_nat s) : aux₂
|
||||
| (succ m) :=
|
||||
assert aux : m ∈ insert n (of_nat (s div 2)) ↔ succ m ∈ insert (succ n) (of_nat s), from iff.intro
|
||||
(assume hl, or.elim (eq_or_mem_of_mem_insert hl)
|
||||
(suppose m = n, by subst m; apply mem_insert)
|
||||
(suppose m ∈ of_nat (s div 2), finset.mem_insert_of_mem _ (iff.mpr !succ_mem_of_nat this)))
|
||||
(assume hr, or.elim (eq_or_mem_of_mem_insert hr)
|
||||
(suppose succ m = succ n,
|
||||
assert m = n, by injection this; assumption,
|
||||
by subst m; apply mem_insert)
|
||||
(suppose succ m ∈ of_nat s, finset.mem_insert_of_mem _ (iff.mp !succ_mem_of_nat this))),
|
||||
calc
|
||||
succ m ∈ of_nat (2^(succ n) + s) ↔ succ m ∈ of_nat (2^n * 2 + s) : by rewrite pow_succ
|
||||
... ↔ m ∈ of_nat ((2^n * 2 + s) div 2) : succ_mem_of_nat
|
||||
... ↔ m ∈ of_nat (2^n + s div 2) : by rewrite [add.comm, add_mul_div_self (dec_trivial : 2 > 0), add.comm]
|
||||
... ↔ m ∈ insert n (of_nat (s div 2)) : by rewrite ih
|
||||
... ↔ succ m ∈ insert (succ n) (of_nat s) : aux,
|
||||
gen x)
|
||||
|
||||
private lemma of_nat_to_nat (s : finset nat) : of_nat (to_nat s) = s :=
|
||||
finset.induction_on s rfl
|
||||
(λ a s nains ih, by rewrite [to_nat_insert nains, -ih at nains, of_nat_eq_insert nains, ih])
|
||||
|
||||
private definition predimage (s : finset nat) : finset nat :=
|
||||
{ n ∈ image pred s | succ n ∈ s }
|
||||
|
||||
private lemma mem_image_pred_of_succ_mem {n : nat} {s : finset nat} : succ n ∈ s → n ∈ image pred s :=
|
||||
assume h,
|
||||
assert pred (succ n) ∈ image pred s, from mem_image_of_mem _ h,
|
||||
begin rewrite [pred_succ at this], assumption end
|
||||
|
||||
private lemma mem_predimage_of_succ_mem {n : nat} {s : finset nat} : succ n ∈ s → n ∈ predimage s :=
|
||||
assume h, begin unfold predimage, rewrite [mem_sep_eq], exact and.intro (mem_image_pred_of_succ_mem h) h end
|
||||
|
||||
private lemma succ_mem_of_mem_predimage {n : nat} {s : finset nat} : n ∈ predimage s → succ n ∈ s :=
|
||||
begin
|
||||
unfold predimage, rewrite [mem_sep_eq],
|
||||
suppose n ∈ image pred s ∧ succ n ∈ s, and.right this
|
||||
end
|
||||
|
||||
private lemma predimage_insert_zero (s : finset nat) : predimage (insert 0 s) = predimage s :=
|
||||
finset.ext (λ n,
|
||||
begin
|
||||
intro n s nains ih,
|
||||
rewrite (to_nat_insert nains)
|
||||
end
|
||||
-/
|
||||
unfold predimage, rewrite [*mem_sep_eq, image_insert, pred_zero], apply iff.intro,
|
||||
suppose n ∈ insert 0 (image pred s) ∧ succ n ∈ insert 0 s,
|
||||
have succ n ∈ s, from or.elim (eq_or_mem_of_mem_insert (and.right this))
|
||||
(by contradiction)
|
||||
(λ h, h),
|
||||
and.intro (mem_image_pred_of_succ_mem this) this,
|
||||
suppose n ∈ image pred s ∧ succ n ∈ s,
|
||||
obtain h₁ h₂, from this,
|
||||
and.intro (mem_insert_of_mem 0 h₁) (mem_insert_of_mem 0 h₂)
|
||||
end)
|
||||
|
||||
private lemma predimage_insert_succ (n : nat) (s : finset nat) : predimage (insert (succ n) s) = insert n (predimage s) :=
|
||||
finset.ext (λ m,
|
||||
begin
|
||||
unfold predimage, rewrite [*mem_sep_eq, *image_insert, pred_succ, *mem_insert_eq, *mem_sep_eq], apply iff.intro,
|
||||
suppose (m = n ∨ m ∈ image pred s) ∧ (succ m = succ n ∨ succ m ∈ s),
|
||||
obtain h₁ h₂, from this,
|
||||
or.elim h₁
|
||||
(suppose m = n, or.inl this)
|
||||
(suppose m ∈ image pred s, or.elim h₂
|
||||
(suppose succ m = succ n, by injection this; left; assumption)
|
||||
(suppose succ m ∈ s, by right; split; repeat assumption)),
|
||||
suppose m = n ∨ m ∈ image pred s ∧ succ m ∈ s, or.elim this
|
||||
(suppose m = n, and.intro (or.inl this) (or.inl (by subst m)))
|
||||
(suppose m ∈ image pred s ∧ succ m ∈ s,
|
||||
obtain h₁ h₂, from this,
|
||||
and.intro (or.inr h₁) (or.inr h₂))
|
||||
end)
|
||||
|
||||
private lemma of_nat_div2 (s : nat) : of_nat (s div 2) = predimage (of_nat s) :=
|
||||
finset.ext (λ n, iff.intro
|
||||
(suppose n ∈ of_nat (s div 2),
|
||||
have succ n ∈ of_nat s, from iff.mpr !succ_mem_of_nat this,
|
||||
mem_predimage_of_succ_mem this)
|
||||
(suppose n ∈ predimage (of_nat s),
|
||||
have succ n ∈ of_nat s, from succ_mem_of_mem_predimage this,
|
||||
iff.mp !succ_mem_of_nat this))
|
||||
|
||||
private lemma to_nat_predimage (s : finset nat) : to_nat (predimage s) = (to_nat s) div 2 :=
|
||||
begin
|
||||
induction s with a s nains ih,
|
||||
reflexivity,
|
||||
cases a with a,
|
||||
{ rewrite [predimage_insert_zero, ih, to_nat_insert nains, pow_zero],
|
||||
have 0 ∉ of_nat (to_nat s), by rewrite of_nat_to_nat; assumption,
|
||||
have even (to_nat s), from iff.mp !even_of_not_zero_mem this,
|
||||
obtain w (hw : to_nat s = 2*w), from exists_of_even this,
|
||||
begin
|
||||
rewrite hw,
|
||||
have d₁ : 1 div 2 = 0, from dec_trivial,
|
||||
show 2 * w div 2 = (1 + 2 * w) div 2, by
|
||||
rewrite [add_mul_div_self_left _ _ (dec_trivial : 2 > 0), mul.comm,
|
||||
mul_div_cancel _ (dec_trivial : 2 > 0), d₁, zero_add]
|
||||
end },
|
||||
{ have a ∉ predimage s, from suppose a ∈ predimage s, absurd (succ_mem_of_mem_predimage this) nains,
|
||||
rewrite [predimage_insert_succ, to_nat_insert nains, pow_succ, add.comm,
|
||||
add_mul_div_self (dec_trivial : 2 > 0), -ih, to_nat_insert this, add.comm] }
|
||||
end
|
||||
|
||||
private lemma to_nat_of_nat (s : nat) : to_nat (of_nat s) = s :=
|
||||
nat.strong_induction_on s
|
||||
(λ n ih, by_cases
|
||||
(suppose n = 0, by rewrite this)
|
||||
(suppose n ≠ 0,
|
||||
have n div 2 < n, from div_lt_of_ne_zero this,
|
||||
have to_nat (of_nat (n div 2)) = n div 2, from ih _ this,
|
||||
have e₁ : to_nat (of_nat n) div 2 = n div 2, from calc
|
||||
to_nat (of_nat n) div 2 = to_nat (predimage (of_nat n)) : by rewrite to_nat_predimage
|
||||
... = to_nat (of_nat (n div 2)) : by rewrite of_nat_div2
|
||||
... = n div 2 : this,
|
||||
have e₂ : even (to_nat (of_nat n)) ↔ even n, from calc
|
||||
even (to_nat (of_nat n)) ↔ 0 ∉ of_nat n : even_to_nat
|
||||
... ↔ even n : even_of_not_zero_mem,
|
||||
eq_of_div2_of_even e₁ e₂))
|
||||
|
||||
open equiv
|
||||
|
||||
lemma finset_nat_equiv_nat : finset nat ≃ nat :=
|
||||
mk to_nat of_nat of_nat_to_nat to_nat_of_nat
|
||||
|
||||
end finset
|
||||
|
|
|
|||
|
|
@ -594,4 +594,21 @@ begin
|
|||
rewrite [mul_zero, *div_zero],
|
||||
apply div_div_aux a (succ b) (succ c) dec_trivial dec_trivial
|
||||
end
|
||||
|
||||
lemma div_lt_of_ne_zero : ∀ {n : nat}, n ≠ 0 → n div 2 < n
|
||||
| 0 h := absurd rfl h
|
||||
| (succ n) h :=
|
||||
begin
|
||||
apply div_lt_of_lt_mul,
|
||||
rewrite [-add_one, mul.right_distrib],
|
||||
change n + 1 < (n * 1 + n) + (1 + 1),
|
||||
rewrite [mul_one, -add.assoc],
|
||||
apply add_lt_add_right,
|
||||
show n < n + n + 1,
|
||||
begin
|
||||
rewrite [add.assoc, -add_zero n at {1}],
|
||||
apply add_lt_add_left,
|
||||
apply zero_lt_succ
|
||||
end
|
||||
end
|
||||
end nat
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue