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

refactor(library/data): rename 'countable' to 'encodable', define countable in the usual way, and prove all 'encodable' type is 'countable'

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-19 14:18:49 -07:00
parent f4398115b4
commit 306087b5d3
5 changed files with 380 additions and 358 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

312
library/data/countable.lean
View file

@ -5,313 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
Module: data.countable
Author: Leonardo de Moura
Type class for countable types
Define countable types
-/
import data.fintype data.list data.sum data.nat data.subtype
open option list nat
import algebra.function
open function
structure countable [class] (A : Type) :=
(pickle : A → nat) (unpickle : nat → option A) (picklek : ∀ a, unpickle (pickle a) = some a)
open countable
definition countable_fintype [instance] {A : Type} [h₁ : fintype A] [h₂ : decidable_eq A] : countable A :=
countable.mk
(λ a, find a (elements_of A))
(λ n, nth (elements_of A) n)
(λ a, find_nth (fintype.complete a))
definition countable_nat [instance] : countable nat :=
countable.mk (λ a, a) (λ n, some n) (λ a, rfl)
definition countable_option [instance] {A : Type} [h : countable A] : countable (option A) :=
countable.mk
(λ o, match o with
| some a := succ (pickle a)
| none := 0
end)
(λ n, if n = 0 then some none else some (unpickle A (pred n)))
(λ o,
begin
cases o with [a],
begin esimp end,
begin esimp, rewrite [if_neg !succ_ne_zero, pred_succ, countable.picklek] end
end)
section sum
variables {A B : Type}
variables [h₁ : countable A] [h₂ : countable B]
include h₁ h₂
definition pickle_sum : sum A B → nat
| (sum.inl a) := 2 * pickle a
| (sum.inr b) := 2 * pickle b + 1
definition unpickle_sum (n : nat) : option (sum A B) :=
if n mod 2 = 0 then
match unpickle A (n div 2) with
| some a := some (sum.inl a)
| none := none
end
else
match unpickle B ((n - 1) div 2) with
| some b := some (sum.inr b)
| none := none
end
open decidable
theorem unpickle_pickle_sum : ∀ s : sum A B, unpickle_sum (pickle_sum s) = some s
| (sum.inl a) :=
assert aux : 2 > 0, from dec_trivial,
begin
esimp [pickle_sum, unpickle_sum],
rewrite [mul_mod_right, if_pos (eq.refl 0), mul_div_cancel_left _ aux, countable.picklek]
end
| (sum.inr b) :=
assert aux₁ : 2 > 0, from dec_trivial,
assert aux₂ : 1 mod 2 = 1, by rewrite [modulo_def],
assert aux₃ : 1 ≠ 0, from dec_trivial,
begin
esimp [pickle_sum, unpickle_sum],
rewrite [add.comm, add_mul_mod_self_left aux₁, aux₂, if_neg aux₃, add_sub_cancel_left,
mul_div_cancel_left _ aux₁, countable.picklek]
end
definition countable_sum [instance] : countable (sum A B) :=
countable.mk
(λ s, pickle_sum s)
(λ n, unpickle_sum n)
(λ s, unpickle_pickle_sum s)
end sum
section prod
variables {A B : Type}
variables [h₁ : countable A] [h₂ : countable B]
include h₁ h₂
definition pickle_prod : A × B → nat
| (a, b) := mkpair (pickle a) (pickle b)
definition unpickle_prod (n : nat) : option (A × B) :=
match unpair n with
| (n₁, n₂) :=
match unpickle A n₁ with
| some a :=
match unpickle B n₂ with
| some b := some (a, b)
| none := none
end
| none := none
end
end
theorem unpickle_pickle_prod : ∀ p : A × B, unpickle_prod (pickle_prod p) = some p
| (a, b) :=
begin
esimp [pickle_prod, unpickle_prod, prod.cases_on],
rewrite [unpair_mkpair],
esimp,
rewrite [*countable.picklek]
end
definition countable_product [instance] : countable (A × B) :=
countable.mk
pickle_prod
unpickle_prod
unpickle_pickle_prod
end prod
section list
variables {A : Type}
variables [h : countable A]
include h
definition pickle_list_core : list A → nat
| [] := 0
| (a::l) := mkpair (pickle a) (pickle_list_core l)
theorem pickle_list_core_cons (a : A) (l : list A) : pickle_list_core (a::l) = mkpair (pickle a) (pickle_list_core l) :=
rfl
definition pickle_list (l : list A) : nat :=
mkpair (length l) (pickle_list_core l)
definition unpickle_list_core : nat → nat → option (list A)
| 0 v := some []
| (succ n) v :=
match unpair v with
| (v₁, v₂) :=
match unpickle A v₁ with
| some a :=
match unpickle_list_core n v₂ with
| some l := some (a::l)
| none := none
end
| none := none
end
end
theorem unpickle_list_core_succ (n v : nat) :
unpickle_list_core (succ n) v =
match unpair v with
| (v₁, v₂) :=
match unpickle A v₁ with
| some a :=
match unpickle_list_core n v₂ with
| some l := some (a::l)
| none := none
end
| none := none
end
end
:= rfl
definition unpickle_list (n : nat) : option (list A) :=
match unpair n with
| (l, v) := unpickle_list_core l v
end
theorem unpickle_pickle_list_core : ∀ l : list A, unpickle_list_core (length l) (pickle_list_core l) = some l
| [] := rfl
| (a::l) :=
begin
rewrite [pickle_list_core_cons, length_cons, add_one (length l), unpickle_list_core_succ],
rewrite [unpair_mkpair],
esimp [prod.cases_on],
rewrite [unpickle_pickle_list_core l],
rewrite [countable.picklek],
end
theorem unpickle_pickle_list (l : list A) : unpickle_list (pickle_list l) = some l :=
begin
esimp [pickle_list, unpickle_list],
rewrite [unpair_mkpair],
esimp [prod.cases_on],
apply unpickle_pickle_list_core
end
definition countable_list [instance] : countable (list A) :=
countable.mk
pickle_list
unpickle_list
unpickle_pickle_list
end list
definition countable_of_left_injection
{A B : Type} [h₁ : countable A]
(f : B → A) (finv : A → option B) (linv : ∀ b, finv (f b) = some b) : countable B :=
countable.mk
(λ b, pickle (f b))
(λ n,
match unpickle A n with
| some a := finv a
| none := none
end)
(λ b,
begin
esimp,
rewrite [countable.picklek],
esimp [option.cases_on],
rewrite [linv]
end)
/-
Choice function for countable types and decidable predicates.
We provide the following API
choose {A : Type} {p : A → Prop} [c : countable A] [d : decidable_pred p] : (∃ x, p x) → A :=
choose_spec {A : Type} {p : A → Prop} [c : countable A] [d : decidable_pred p] (ex : ∃ x, p x) : p (choose ex) :=
-/
section find_a
parameters {A : Type} {p : A → Prop} [c : countable A] [d : decidable_pred p]
include c
include d
private definition pn (n : nat) : Prop :=
match unpickle A n with
| some a := p a
| none := false
end
private definition decidable_pn : decidable_pred pn :=
λ n,
match unpickle A n with
| some a := λ e : unpickle A n = some a,
match d a with
| decidable.inl t :=
begin
unfold pn, rewrite e, esimp [option.cases_on],
exact (decidable.inl t)
end
| decidable.inr f :=
begin
unfold pn, rewrite e, esimp [option.cases_on],
exact (decidable.inr f)
end
end
| none := λ e : unpickle A n = none,
begin
unfold pn, rewrite e, esimp [option.cases_on],
exact decidable_false
end
end (eq.refl (unpickle A n))
private definition ex_pn_of_ex : (∃ x, p x) → (∃ x, pn x) :=
assume ex,
obtain (w : A) (pw : p w), from ex,
exists.intro (pickle w)
begin
unfold pn, rewrite [picklek], esimp, exact pw
end
private lemma unpickle_ne_none_of_pn {n : nat} : pn n → unpickle A n ≠ none :=
assume pnn e,
begin
rewrite [▸ (match unpickle A n with | some a := p a | none := false end) at pnn],
rewrite [e at pnn], esimp [option.cases_on] at pnn,
exact (false.elim pnn)
end
open subtype
private lemma of_nat (n : nat) : pn n → { a : A | p a } :=
match unpickle A n with
| some a := λ (e : unpickle A n = some a),
begin
unfold pn, rewrite e, esimp [option.cases_on], intro pa,
exact (tag a pa)
end
| none := λ (e : unpickle A n = none) h, absurd e (unpickle_ne_none_of_pn h)
end (eq.refl (unpickle A n))
private definition find_a : (∃ x, p x) → {a : A | p a} :=
assume ex : ∃ x, p x,
have exn : ∃ x, pn x, from ex_pn_of_ex ex,
let r : nat := @nat.choose pn decidable_pn exn in
have pnr : pn r, from @nat.choose_spec pn decidable_pn exn,
of_nat r pnr
end find_a
namespace countable
open subtype
definition choose {A : Type} {p : A → Prop} [c : countable A] [d : decidable_pred p] : (∃ x, p x) → A :=
assume ex, elt_of (find_a ex)
theorem choose_spec {A : Type} {p : A → Prop} [c : countable A] [d : decidable_pred p] (ex : ∃ x, p x) : p (choose ex) :=
has_property (find_a ex)
theorem axiom_of_choice {A : Type} {B : A → Type} {R : Π x, B x → Prop} [c : Π a, countable (B a)] [d : ∀ x y, decidable (R x y)]
: (∀x, ∃y, R x y) → ∃f, ∀x, R x (f x) :=
assume H,
have H₁ : ∀x, R x (choose (H x)), from take x, choose_spec (H x),
exists.intro _ H₁
theorem skolem {A : Type} {B : A → Type} {P : Π x, B x → Prop} [c : Π a, countable (B a)] [d : ∀ x y, decidable (P x y)]
: (∀x, ∃y, P x y) ↔ ∃f, (∀x, P x (f x)) :=
iff.intro
(assume H : (∀x, ∃y, P x y), axiom_of_choice H)
(assume H : (∃f, (∀x, P x (f x))),
take x, obtain (fw : ∀x, B x) (Hw : ∀x, P x (fw x)), from H,
exists.intro (fw x) (Hw x))
end countable
definition countable (A : Type) : Prop := ∃ f : A → nat, injective f

326
library/data/encodable.lean Normal file
View file

@ -0,0 +1,326 @@
/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: data.encodable
Author: Leonardo de Moura
Type class for encodable types.
Note that every encodable type is countable.
-/
import data.fintype data.list data.sum data.nat data.subtype data.countable
open option list nat function
structure encodable [class] (A : Type) :=
(encode : A → nat) (decode : nat → option A) (encodek : ∀ a, decode (encode a) = some a)
open encodable
definition countable_of_encodable {A : Type} : encodable A → countable A :=
assume e : encodable A,
have inj_encode : injective encode, from
λ (a₁ a₂ : A) (h : encode a₁ = encode a₂),
assert aux : decode A (encode a₁) = decode A (encode a₂), by rewrite h,
by rewrite [*encodek at aux]; exact (option.no_confusion aux (λ e, e)),
exists.intro encode inj_encode
definition encodable_fintype [instance] {A : Type} [h₁ : fintype A] [h₂ : decidable_eq A] : encodable A :=
encodable.mk
(λ a, find a (elements_of A))
(λ n, nth (elements_of A) n)
(λ a, find_nth (fintype.complete a))
definition encodable_nat [instance] : encodable nat :=
encodable.mk (λ a, a) (λ n, some n) (λ a, rfl)
definition encodable_option [instance] {A : Type} [h : encodable A] : encodable (option A) :=
encodable.mk
(λ o, match o with
| some a := succ (encode a)
| none := 0
end)
(λ n, if n = 0 then some none else some (decode A (pred n)))
(λ o,
begin
cases o with [a],
begin esimp end,
begin esimp, rewrite [if_neg !succ_ne_zero, pred_succ, encodable.encodek] end
end)
section sum
variables {A B : Type}
variables [h₁ : encodable A] [h₂ : encodable B]
include h₁ h₂
definition encode_sum : sum A B → nat
| (sum.inl a) := 2 * encode a
| (sum.inr b) := 2 * encode b + 1
definition decode_sum (n : nat) : option (sum A B) :=
if n mod 2 = 0 then
match decode A (n div 2) with
| some a := some (sum.inl a)
| none := none
end
else
match decode B ((n - 1) div 2) with
| some b := some (sum.inr b)
| none := none
end
open decidable
theorem decode_encode_sum : ∀ s : sum A B, decode_sum (encode_sum s) = some s
| (sum.inl a) :=
assert aux : 2 > 0, from dec_trivial,
begin
esimp [encode_sum, decode_sum],
rewrite [mul_mod_right, if_pos (eq.refl 0), mul_div_cancel_left _ aux, encodable.encodek]
end
| (sum.inr b) :=
assert aux₁ : 2 > 0, from dec_trivial,
assert aux₂ : 1 mod 2 = 1, by rewrite [modulo_def],
assert aux₃ : 1 ≠ 0, from dec_trivial,
begin
esimp [encode_sum, decode_sum],
rewrite [add.comm, add_mul_mod_self_left aux₁, aux₂, if_neg aux₃, add_sub_cancel_left,
mul_div_cancel_left _ aux₁, encodable.encodek]
end
definition encodable_sum [instance] : encodable (sum A B) :=
encodable.mk
(λ s, encode_sum s)
(λ n, decode_sum n)
(λ s, decode_encode_sum s)
end sum
section prod
variables {A B : Type}
variables [h₁ : encodable A] [h₂ : encodable B]
include h₁ h₂
definition encode_prod : A × B → nat
| (a, b) := mkpair (encode a) (encode b)
definition decode_prod (n : nat) : option (A × B) :=
match unpair n with
| (n₁, n₂) :=
match decode A n₁ with
| some a :=
match decode B n₂ with
| some b := some (a, b)
| none := none
end
| none := none
end
end
theorem decode_encode_prod : ∀ p : A × B, decode_prod (encode_prod p) = some p
| (a, b) :=
begin
esimp [encode_prod, decode_prod, prod.cases_on],
rewrite [unpair_mkpair],
esimp,
rewrite [*encodable.encodek]
end
definition encodable_product [instance] : encodable (A × B) :=
encodable.mk
encode_prod
decode_prod
decode_encode_prod
end prod
section list
variables {A : Type}
variables [h : encodable A]
include h
definition encode_list_core : list A → nat
| [] := 0
| (a::l) := mkpair (encode a) (encode_list_core l)
theorem encode_list_core_cons (a : A) (l : list A) : encode_list_core (a::l) = mkpair (encode a) (encode_list_core l) :=
rfl
definition encode_list (l : list A) : nat :=
mkpair (length l) (encode_list_core l)
definition decode_list_core : nat → nat → option (list A)
| 0 v := some []
| (succ n) v :=
match unpair v with
| (v₁, v₂) :=
match decode A v₁ with
| some a :=
match decode_list_core n v₂ with
| some l := some (a::l)
| none := none
end
| none := none
end
end
theorem decode_list_core_succ (n v : nat) :
decode_list_core (succ n) v =
match unpair v with
| (v₁, v₂) :=
match decode A v₁ with
| some a :=
match decode_list_core n v₂ with
| some l := some (a::l)
| none := none
end
| none := none
end
end
:= rfl
definition decode_list (n : nat) : option (list A) :=
match unpair n with
| (l, v) := decode_list_core l v
end
theorem decode_encode_list_core : ∀ l : list A, decode_list_core (length l) (encode_list_core l) = some l
| [] := rfl
| (a::l) :=
begin
rewrite [encode_list_core_cons, length_cons, add_one (length l), decode_list_core_succ],
rewrite [unpair_mkpair],
esimp [prod.cases_on],
rewrite [decode_encode_list_core l],
rewrite [encodable.encodek],
end
theorem decode_encode_list (l : list A) : decode_list (encode_list l) = some l :=
begin
esimp [encode_list, decode_list],
rewrite [unpair_mkpair],
esimp [prod.cases_on],
apply decode_encode_list_core
end
definition encodable_list [instance] : encodable (list A) :=
encodable.mk
encode_list
decode_list
decode_encode_list
end list
definition encodable_of_left_injection
{A B : Type} [h₁ : encodable A]
(f : B → A) (finv : A → option B) (linv : ∀ b, finv (f b) = some b) : encodable B :=
encodable.mk
(λ b, encode (f b))
(λ n,
match decode A n with
| some a := finv a
| none := none
end)
(λ b,
begin
esimp,
rewrite [encodable.encodek],
esimp [option.cases_on],
rewrite [linv]
end)
/-
Choice function for encodable types and decidable predicates.
We provide the following API
choose {A : Type} {p : A → Prop} [c : encodable A] [d : decidable_pred p] : (∃ x, p x) → A :=
choose_spec {A : Type} {p : A → Prop} [c : encodable A] [d : decidable_pred p] (ex : ∃ x, p x) : p (choose ex) :=
-/
section find_a
parameters {A : Type} {p : A → Prop} [c : encodable A] [d : decidable_pred p]
include c
include d
private definition pn (n : nat) : Prop :=
match decode A n with
| some a := p a
| none := false
end
private definition decidable_pn : decidable_pred pn :=
λ n,
match decode A n with
| some a := λ e : decode A n = some a,
match d a with
| decidable.inl t :=
begin
unfold pn, rewrite e, esimp [option.cases_on],
exact (decidable.inl t)
end
| decidable.inr f :=
begin
unfold pn, rewrite e, esimp [option.cases_on],
exact (decidable.inr f)
end
end
| none := λ e : decode A n = none,
begin
unfold pn, rewrite e, esimp [option.cases_on],
exact decidable_false
end
end (eq.refl (decode A n))
private definition ex_pn_of_ex : (∃ x, p x) → (∃ x, pn x) :=
assume ex,
obtain (w : A) (pw : p w), from ex,
exists.intro (encode w)
begin
unfold pn, rewrite [encodek], esimp, exact pw
end
private lemma decode_ne_none_of_pn {n : nat} : pn n → decode A n ≠ none :=
assume pnn e,
begin
rewrite [▸ (match decode A n with | some a := p a | none := false end) at pnn],
rewrite [e at pnn], esimp [option.cases_on] at pnn,
exact (false.elim pnn)
end
open subtype
private lemma of_nat (n : nat) : pn n → { a : A | p a } :=
match decode A n with
| some a := λ (e : decode A n = some a),
begin
unfold pn, rewrite e, esimp [option.cases_on], intro pa,
exact (tag a pa)
end
| none := λ (e : decode A n = none) h, absurd e (decode_ne_none_of_pn h)
end (eq.refl (decode A n))
private definition find_a : (∃ x, p x) → {a : A | p a} :=
assume ex : ∃ x, p x,
have exn : ∃ x, pn x, from ex_pn_of_ex ex,
let r : nat := @nat.choose pn decidable_pn exn in
have pnr : pn r, from @nat.choose_spec pn decidable_pn exn,
of_nat r pnr
end find_a
namespace encodable
open subtype
definition choose {A : Type} {p : A → Prop} [c : encodable A] [d : decidable_pred p] : (∃ x, p x) → A :=
assume ex, elt_of (find_a ex)
theorem choose_spec {A : Type} {p : A → Prop} [c : encodable A] [d : decidable_pred p] (ex : ∃ x, p x) : p (choose ex) :=
has_property (find_a ex)
theorem axiom_of_choice {A : Type} {B : A → Type} {R : Π x, B x → Prop} [c : Π a, encodable (B a)] [d : ∀ x y, decidable (R x y)]
: (∀x, ∃y, R x y) → ∃f, ∀x, R x (f x) :=
assume H,
have H₁ : ∀x, R x (choose (H x)), from take x, choose_spec (H x),
exists.intro _ H₁
theorem skolem {A : Type} {B : A → Type} {P : Π x, B x → Prop} [c : Π a, encodable (B a)] [d : ∀ x y, decidable (P x y)]
: (∀x, ∃y, P x y) ↔ ∃f, (∀x, P x (f x)) :=
iff.intro
(assume H : (∀x, ∃y, P x y), axiom_of_choice H)
(assume H : (∃f, (∀x, P x (f x))),
take x, obtain (fw : ∀x, B x) (Hw : ∀x, P x (fw x)), from H,
exists.intro (fw x) (Hw x))
end encodable

45
library/data/examples/notcountable.lean
View file

@ -1,45 +0,0 @@
/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: data.examples.uncountable
Author: Leonardo de Moura
Small example showing that (nat → nat) is not countable.
-/
import data.countable
open nat countable option
section
hypothesis nat_nat_countable : countable (nat → nat)
private definition unpickle_fun (n : nat) : option (nat → nat) :=
@unpickle (nat → nat) nat_nat_countable n
private definition pickle_fun (f : nat → nat) : nat :=
@pickle (nat → nat) nat_nat_countable f
private lemma picklek_fun : ∀ f : nat → nat, unpickle_fun (pickle_fun f) = some f :=
λ f, !picklek
private definition f (n : nat) : nat :=
match unpickle_fun n with
| some g := succ (g n)
| none := 0
end
private definition v : nat := pickle_fun f
private lemma f_eq : succ (f v) = f v :=
begin
change (succ (f v) =
match unpickle_fun (pickle_fun f) with
| some g := succ (g v)
| none := 0
end),
rewrite picklek_fun
end
end
theorem not_countable_nat_arrow_nat : (countable (nat → nat)) → false :=
assume h, absurd (f_eq h) succ_ne_self

45
library/data/examples/notencodable.lean Normal file
View file

@ -0,0 +1,45 @@
/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: data.examples.unencodable
Author: Leonardo de Moura
Small example showing that (nat → nat) is not encodable.
-/
import data.encodable
open nat encodable option
section
hypothesis nat_nat_encodable : encodable (nat → nat)
private definition decode_fun (n : nat) : option (nat → nat) :=
@decode (nat → nat) nat_nat_encodable n
private definition encode_fun (f : nat → nat) : nat :=
@encode (nat → nat) nat_nat_encodable f
private lemma encodek_fun : ∀ f : nat → nat, decode_fun (encode_fun f) = some f :=
λ f, !encodek
private definition f (n : nat) : nat :=
match decode_fun n with
| some g := succ (g n)
| none := 0
end
private definition v : nat := encode_fun f
private lemma f_eq : succ (f v) = f v :=
begin
change (succ (f v) =
match decode_fun (encode_fun f) with
| some g := succ (g v)
| none := 0
end),
rewrite encodek_fun
end
end
theorem not_encodable_nat_arrow_nat : (encodable (nat → nat)) → false :=
assume h, absurd (f_eq h) succ_ne_self

10
tests/lean/run/pickle1.lean
View file

@ -1,7 +1,7 @@
import data.countable
open countable decidable bool prod list nat option
import data.encodable
open encodable decidable bool prod list nat option
variable l : list (nat × bool)
check pickle l
eval pickle [2, 1]
example : unpickle (list nat) (pickle [1, 1]) = some [1, 1] :=
check encode l
eval encode [2, 1]
example : decode (list nat) (encode [1, 1]) = some [1, 1] :=
rfl