lean2/library/data/fintype.lean

204 lines
8.6 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/-
Copyright (c) 2015 Leonardo de Moura. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
Finite type (type class).
-/
import data.list data.bool
open list bool unit decidable option function
structure fintype [class] (A : Type) : Type :=
(elems : list A) (unique : nodup elems) (complete : ∀ a, a ∈ elems)
definition elements_of (A : Type) [h : fintype A] : list A :=
@fintype.elems A h
definition fintype_unit [instance] : fintype unit :=
fintype.mk [star] dec_trivial (λ u, match u with star := dec_trivial end)
definition fintype_bool [instance] : fintype bool :=
fintype.mk [ff, tt]
dec_trivial
(λ b, match b with | tt := dec_trivial | ff := dec_trivial end)
definition fintype_product [instance] {A B : Type} : Π [h₁ : fintype A] [h₂ : fintype B], fintype (A × B)
| (fintype.mk e₁ u₁ c₁) (fintype.mk e₂ u₂ c₂) :=
fintype.mk
(product e₁ e₂)
(nodup_product u₁ u₂)
(λ p,
match p with
(a, b) := mem_product (c₁ a) (c₂ b)
end)
/- auxiliary function for finding 'a' s.t. f a ≠ g a -/
section find_discr
variables {A B : Type}
variable [h : decidable_eq B]
include h
definition find_discr (f g : A → B) : list A → option A
| [] := none
| (a::l) := if f a = g a then find_discr l else some a
theorem find_discr_nil (f g : A → B) : find_discr f g [] = none :=
rfl
theorem find_discr_cons_of_ne {f g : A → B} {a : A} (l : list A) : f a ≠ g a → find_discr f g (a::l) = some a :=
assume ne, if_neg ne
theorem find_discr_cons_of_eq {f g : A → B} {a : A} (l : list A) : f a = g a → find_discr f g (a::l) = find_discr f g l :=
assume eq, if_pos eq
theorem ne_of_find_discr_eq_some {f g : A → B} {a : A} : ∀ {l}, find_discr f g l = some a → f a ≠ g a
| [] e := by contradiction
| (x::l) e := by_cases
(λ h : f x = g x,
have aux : find_discr f g l = some a, by rewrite [find_discr_cons_of_eq l h at e]; exact e,
ne_of_find_discr_eq_some aux)
(λ h : f x ≠ g x,
have aux : some x = some a, by rewrite [find_discr_cons_of_ne l h at e]; exact e,
option.no_confusion aux (λ xeqa : x = a, eq.rec_on xeqa h))
theorem all_eq_of_find_discr_eq_none {f g : A → B} : ∀ {l}, find_discr f g l = none → ∀ a, a ∈ l → f a = g a
| [] e a i := absurd i !not_mem_nil
| (x::l) e a i := by_cases
(λ fx_eq_gx : f x = g x,
have aux : find_discr f g l = none, by rewrite [find_discr_cons_of_eq l fx_eq_gx at e]; exact e,
or.elim (eq_or_mem_of_mem_cons i)
(λ aeqx : a = x, by rewrite [-aeqx at fx_eq_gx]; exact fx_eq_gx)
(λ ainl : a ∈ l, all_eq_of_find_discr_eq_none aux a ainl))
(λ fx_ne_gx : f x ≠ g x,
by rewrite [find_discr_cons_of_ne l fx_ne_gx at e]; contradiction)
end find_discr
definition decidable_eq_fun [instance] {A B : Type} [h₁ : fintype A] [h₂ : decidable_eq B] : decidable_eq (A → B) :=
λ f g,
match h₁ with
| fintype.mk e u c :=
match find_discr f g e with
| some a := λ h : find_discr f g e = some a, inr (λ f_eq_g : f = g, absurd (by rewrite f_eq_g; reflexivity) (ne_of_find_discr_eq_some h))
| none := λ h : find_discr f g e = none, inl (show f = g, from funext (λ a : A, all_eq_of_find_discr_eq_none h a (c a)))
end rfl
end
section check_pred
variables {A : Type}
definition check_pred (p : A → Prop) [h : decidable_pred p] : list A → bool
| [] := tt
| (a::l) := if p a then check_pred l else ff
definition check_pred_cons_of_pos {p : A → Prop} [h : decidable_pred p] {a : A} (l : list A) : p a → check_pred p (a::l) = check_pred p l :=
assume pa, if_pos pa
definition check_pred_cons_of_neg {p : A → Prop} [h : decidable_pred p] {a : A} (l : list A) : ¬ p a → check_pred p (a::l) = ff :=
assume npa, if_neg npa
definition all_of_check_pred_eq_tt {p : A → Prop} [h : decidable_pred p] : ∀ {l : list A}, check_pred p l = tt → ∀ {a}, a ∈ l → p a
| [] eqtt a ainl := absurd ainl !not_mem_nil
| (b::l) eqtt a ainbl := by_cases
(λ pb : p b, or.elim (eq_or_mem_of_mem_cons ainbl)
(λ aeqb : a = b, by rewrite [aeqb]; exact pb)
(λ ainl : a ∈ l,
have eqtt₁ : check_pred p l = tt, by rewrite [check_pred_cons_of_pos _ pb at eqtt]; exact eqtt,
all_of_check_pred_eq_tt eqtt₁ ainl))
(λ npb : ¬ p b,
by rewrite [check_pred_cons_of_neg _ npb at eqtt]; exact (bool.no_confusion eqtt))
definition ex_of_check_pred_eq_ff {p : A → Prop} [h : decidable_pred p] : ∀ {l : list A}, check_pred p l = ff → ∃ w, ¬ p w
| [] eqtt := bool.no_confusion eqtt
| (a::l) eqtt := by_cases
(λ pa : p a,
have eqtt₁ : check_pred p l = ff, by rewrite [check_pred_cons_of_pos _ pa at eqtt]; exact eqtt,
ex_of_check_pred_eq_ff eqtt₁)
(λ npa : ¬ p a, exists.intro a npa)
end check_pred
definition decidable_forall_finite [instance] {A : Type} {p : A → Prop} [h₁ : fintype A] [h₂ : decidable_pred p]
: decidable (∀ x : A, p x) :=
match h₁ with
| fintype.mk e u c :=
match check_pred p e with
| tt := λ h : check_pred p e = tt, inl (λ a : A, all_of_check_pred_eq_tt h (c a))
| ff := λ h : check_pred p e = ff,
inr (λ n : (∀ x, p x),
obtain (a : A) (w : ¬ p a), from ex_of_check_pred_eq_ff h,
absurd (n a) w)
end rfl
end
definition decidable_exists_finite [instance] {A : Type} {p : A → Prop} [h₁ : fintype A] [h₂ : decidable_pred p]
: decidable (∃ x : A, p x) :=
match h₁ with
| fintype.mk e u c :=
match check_pred (λ a, ¬ p a) e with
| tt := λ h : check_pred (λ a, ¬ p a) e = tt, inr (λ ex : (∃ x, p x),
obtain x px, from ex,
absurd px (all_of_check_pred_eq_tt h (c x)))
| ff := λ h : check_pred (λ a, ¬ p a) e = ff, inl (
assert aux₁ : ∃ x, ¬¬p x, from ex_of_check_pred_eq_ff h,
obtain x nnpx, from aux₁, exists.intro x (not_not_elim nnpx))
end rfl
end
open list.as_type
-- Auxiliary function for returning a list with all elements of the type: (list.as_type l)
-- Remark ⟪s⟫ is notation for (list.as_type l)
-- We use this function to define the instance for (fintype ⟪s⟫)
private definition ltype_elems {A : Type} {s : list A} : Π {l : list A}, l ⊆ s → list ⟪s⟫
| [] h := []
| (a::l) h := lval a (h a !mem_cons) :: ltype_elems (sub_of_cons_sub h)
private theorem mem_of_mem_ltype_elems {A : Type} {a : A} {s : list A}
: Π {l : list A} {h : l ⊆ s} {m : a ∈ s}, mk a m ∈ ltype_elems h → a ∈ l
| [] h m lin := absurd lin !not_mem_nil
| (b::l) h m lin := or.elim (eq_or_mem_of_mem_cons lin)
(λ leq : mk a m = mk b (h b (mem_cons b l)),
as_type.no_confusion leq (λ aeqb em, by rewrite [aeqb]; exact !mem_cons))
(λ linl : mk a m ∈ ltype_elems (sub_of_cons_sub h),
have ainl : a ∈ l, from mem_of_mem_ltype_elems linl,
mem_cons_of_mem _ ainl)
private theorem nodup_ltype_elems {A : Type} {s : list A} : Π {l : list A} (d : nodup l) (h : l ⊆ s), nodup (ltype_elems h)
| [] d h := nodup_nil
| (a::l) d h :=
have d₁ : nodup l, from nodup_of_nodup_cons d,
have nainl : a ∉ l, from not_mem_of_nodup_cons d,
let h₁ : l ⊆ s := sub_of_cons_sub h in
have d₂ : nodup (ltype_elems h₁), from nodup_ltype_elems d₁ h₁,
have nin : mk a (h a (mem_cons a l)) ∉ ltype_elems h₁, from
assume ab, absurd (mem_of_mem_ltype_elems ab) nainl,
nodup_cons nin d₂
private theorem mem_ltype_elems {A : Type} {s : list A} {a : ⟪s⟫}
: Π {l : list A} (h : l ⊆ s), value a ∈ l → a ∈ ltype_elems h
| [] h vainl := absurd vainl !not_mem_nil
| (b::l) h vainbl := or.elim (eq_or_mem_of_mem_cons vainbl)
(λ vaeqb : value a = b,
begin
revert vaeqb h,
-- TODO(Leo): check why 'cases a with va, ma' produces an incorrect proof
eapply as_type.cases_on a,
intro va ma vaeqb,
rewrite -vaeqb, intro h,
apply mem_cons
end)
(λ vainl : value a ∈ l,
have s₁ : l ⊆ s, from sub_of_cons_sub h,
have aux : a ∈ ltype_elems (sub_of_cons_sub h), from mem_ltype_elems s₁ vainl,
mem_cons_of_mem _ aux)
definition fintype_list_as_type [instance] {A : Type} [h : decidable_eq A] {s : list A} : fintype ⟪s⟫ :=
let nds : list A := erase_dup s in
have sub₁ : nds ⊆ s, from erase_dup_sub s,
have sub₂ : s ⊆ nds, from sub_erase_dup s,
have dnds : nodup nds, from nodup_erase_dup s,
let e : list ⟪s⟫ := ltype_elems sub₁ in
fintype.mk
e
(nodup_ltype_elems dnds sub₁)
(λ a : ⟪s⟫, show a ∈ e, from
have vains : value a ∈ s, from is_member a,
have vainnds : value a ∈ nds, from sub₂ vains,
mem_ltype_elems sub₁ vainnds)