288 lines
14 KiB
Text
288 lines
14 KiB
Text
/-
|
||
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Author: Leonardo de Moura
|
||
-/
|
||
import data.finset.card
|
||
open nat nat.finset decidable
|
||
open algebra
|
||
|
||
namespace finset
|
||
variable {A : Type}
|
||
|
||
protected definition to_nat (s : finset nat) : nat :=
|
||
nat.finset.Sum s (λ n, 2^n)
|
||
|
||
open finset (to_nat)
|
||
|
||
lemma to_nat_empty : to_nat ∅ = 0 :=
|
||
rfl
|
||
|
||
lemma to_nat_insert {n : nat} {s : finset nat} : n ∉ s → to_nat (insert n s) = 2^n + to_nat s :=
|
||
assume h, Sum_insert_of_not_mem _ h
|
||
|
||
protected definition of_nat (s : nat) : finset nat :=
|
||
{ n ∈ upto (succ s) | odd (s / 2^n) }
|
||
|
||
open finset (of_nat)
|
||
|
||
private lemma of_nat_zero : of_nat 0 = ∅ :=
|
||
rfl
|
||
|
||
private lemma odd_of_mem_of_nat {n : nat} {s : nat} : n ∈ of_nat s → odd (s / 2^n) :=
|
||
assume h, of_mem_sep h
|
||
|
||
private lemma mem_of_nat_of_odd {n : nat} {s : nat} : odd (s / 2^n) → n ∈ of_nat s :=
|
||
assume h,
|
||
have 2^n < succ s, from by_contradiction
|
||
(suppose ¬(2^n < succ s),
|
||
assert 2^n > s, from lt_of_succ_le (le_of_not_gt this),
|
||
assert s / 2^n = 0, from div_eq_zero_of_lt this,
|
||
by rewrite this at h; exact absurd h dec_trivial),
|
||
have n < succ s, from calc
|
||
n ≤ 2^n : le_pow_self dec_trivial n
|
||
... < succ s : this,
|
||
have n ∈ upto (succ s), from mem_upto_of_lt this,
|
||
mem_sep_of_mem this h
|
||
|
||
private lemma succ_mem_of_nat (n : nat) (s : nat) : succ n ∈ of_nat s ↔ n ∈ of_nat (s / 2) :=
|
||
iff.intro
|
||
(suppose succ n ∈ of_nat s,
|
||
assert odd (s / 2^(succ n)), from odd_of_mem_of_nat this,
|
||
have odd ((s / 2) / (2 ^ n)), by rewrite [pow_succ' at this, nat.div_div_eq_div_mul, mul.comm]; assumption,
|
||
show n ∈ of_nat (s / 2), from mem_of_nat_of_odd this)
|
||
(suppose n ∈ of_nat (s / 2),
|
||
assert odd ((s / 2) / (2 ^ n)), from odd_of_mem_of_nat this,
|
||
assert odd (s / 2^(succ n)), by rewrite [pow_succ', mul.comm, -nat.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, nat.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, exact absurd rfl `0 ≠ 0`,
|
||
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 / 2 = (0:nat), from dec_trivial,
|
||
assert aux : _, from calc
|
||
succ m ∈ of_nat (2 * w + 1) ↔ m ∈ of_nat ((2*w+1) / 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 / 2) : by rewrite [mul.comm, nat.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 / 2),
|
||
from iff.mp (not_iff_not_of_iff !succ_mem_of_nat) h,
|
||
assert ih : of_nat (2^n + s / 2) = insert n (of_nat (s / 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 / 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 / 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) / 2) : succ_mem_of_nat
|
||
... ↔ m ∈ of_nat (2^n + s / 2) : by rewrite [add.comm, add_mul_div_self (dec_trivial : 2 > 0), add.comm]
|
||
... ↔ m ∈ insert n (of_nat (s / 2)) : by rewrite ih
|
||
... ↔ succ m ∈ insert (succ n) (of_nat s) : aux,
|
||
gen x)
|
||
|
||
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
|
||
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 / 2) = predimage (of_nat s) :=
|
||
finset.ext (λ n, iff.intro
|
||
(suppose n ∈ of_nat (s / 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) / 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), begin rewrite of_nat_to_nat, exact nains end,
|
||
have even (to_nat s), from iff.mp !even_of_not_zero_mem this,
|
||
obtain (w : nat) (hw : to_nat s = 2*w), from exists_of_even this,
|
||
begin
|
||
rewrite hw,
|
||
have d₁ : 1 / 2 = (0:nat), from dec_trivial,
|
||
show 2 * w / 2 = (1 + 2 * w) / 2, by
|
||
rewrite [add_mul_div_self_left _ _ (dec_trivial : 2 > 0), mul.comm,
|
||
nat.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
|
||
|
||
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 / 2 < n, from div_lt_of_ne_zero this,
|
||
have to_nat (of_nat (n / 2)) = n / 2, from ih _ this,
|
||
have e₁ : to_nat (of_nat n) / 2 = n / 2, from calc
|
||
to_nat (of_nat n) / 2 = to_nat (predimage (of_nat n)) : by rewrite to_nat_predimage
|
||
... = to_nat (of_nat (n / 2)) : by rewrite of_nat_div2
|
||
... = n / 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
|
||
|
||
definition finset_nat_equiv_nat : finset nat ≃ nat :=
|
||
mk to_nat of_nat of_nat_to_nat to_nat_of_nat
|
||
|
||
end finset
|