lean2/tests/lean/run/finset.lean

194 lines
7.3 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.

import data.list
open list setoid quot decidable nat
namespace finset
definition eqv {A : Type} (l₁ l₂ : list A) :=
∀ a, a ∈ l₁ ↔ a ∈ l₂
infix `~` := eqv
theorem eqv.refl {A : Type} (l : list A) : l ~ l :=
λ a, !iff.refl
theorem eqv.symm {A : Type} {l₁ l₂ : list A} : l₁ ~ l₂ → l₂ ~ l₁ :=
λ H a, iff.symm (H a)
theorem eqv.trans {A : Type} {l₁ l₂ l₃ : list A} : l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃ :=
λ H₁ H₂ a, iff.trans (H₁ a) (H₂ a)
theorem eqv.is_equivalence (A : Type) : equivalence (@eqv A) :=
and.intro (@eqv.refl A) (and.intro (@eqv.symm A) (@eqv.trans A))
definition norep {A : Type} [H : decidable_eq A] : list A → list A
| [] := []
| (x :: xs) := if x ∈ xs then norep xs else x :: norep xs
definition eqv_norep {A : Type} [H : decidable_eq A] : ∀ l : list A, l ~ norep l
| [] := (λ a, iff.rfl)
| (x :: xs) :=
take y,
assert ih : xs ~ norep xs, from eqv_norep xs,
show y ∈ x :: xs ↔ y ∈ if x ∈ xs then norep xs else x :: norep xs,
begin
apply (@by_cases (x ∈ xs)),
begin
intro xin, rewrite (if_pos xin),
apply iff.intro,
{intro yinxxs, apply (or.elim (iff.mp !mem_cons_iff yinxxs)),
intro yeqx, rewrite -yeqx at xin, exact (iff.mp (ih y) xin),
intro yeqxs, exact (iff.mp (ih y) yeqxs)},
{intro yinnrep, show y ∈ x::xs, from or.inr (iff.mp' (ih y) yinnrep)}
end,
begin
intro xnin, rewrite (if_neg xnin),
apply iff.intro,
{intro yinxxs, apply (or.elim (iff.mp !mem_cons_iff yinxxs)),
intro yeqx, rewrite yeqx, apply mem_cons,
intro yinxs, show y ∈ x:: norep xs, from or.inr (iff.mp (ih y) yinxs)},
{intro yinxnrep, apply (or.elim (iff.mp !mem_cons_iff yinxnrep)),
intro yeqx, rewrite yeqx, apply mem_cons,
intro yinrep, show y ∈ x::xs, from or.inr (iff.mp' (ih y) yinrep)}
end
end
definition sub {A : Type} (l₁ l₂ : list A) := ∀ a, a ∈ l₁ → a ∈ l₂
infix ⊆ := sub
theorem eqv_of_sub_of_sub {A : Type} {l₁ l₂ : list A} : l₁ ⊆ l₂ → l₂ ⊆ l₁ → l₁ ~ l₂ :=
assume h₁ h₂ a, iff.intro (h₁ a) (h₂ a)
theorem sub_of_eqv_left {A : Type} {l₁ l₂ : list A} : l₁ ~ l₂ → l₁ ⊆ l₂ :=
assume h₁ a ainl₁, iff.mp (h₁ a) ainl₁
theorem sub_of_eqv_right {A : Type} {l₁ l₂ : list A} : l₁ ~ l₂ → l₂ ⊆ l₁ :=
assume h₁ a ainl₂, iff.mp' (h₁ a) ainl₂
definition sub_of_cons_sub {A : Type} {a : A} {l₁ l₂ : list A} : a :: l₁ ⊆ l₂ → l₁ ⊆ l₂ :=
assume s, take b, assume binl₁, s b (or.inr binl₁)
definition decidable_sub [instance] {A : Type} [H : decidable_eq A] : ∀ l₁ l₂ : list A, decidable (l₁ ⊆ l₂)
| [] ys := inl (λ a h, absurd h !not_mem_nil)
| (x::xs) ys :=
if xinys : x ∈ ys then
match decidable_sub xs ys with
| (inl xs_sub_ys) := inl (λ y yinxxs, or.elim (iff.mp !mem_cons_iff yinxxs)
(λ yeqx, by rewrite yeqx; exact xinys)
(λ yinxs, xs_sub_ys y yinxs))
| (inr nxs_sub_ys) := inr (λ h, absurd (sub_of_cons_sub h) nxs_sub_ys)
end
else
inr (λ h, absurd (h x !mem_cons) xinys)
example : [(1 : nat), 2, 3] ⊆ [1,3,4,1,2] :=
dec_trivial
definition decidable_eqv [instance] {A : Type} [H : decidable_eq A] : ∀ l₁ l₂ : list A, decidable (l₁ ~ l₂) :=
take l₁ l₂ : list A,
match decidable_sub l₁ l₂ with
| (inl s₁) :=
match decidable_sub l₂ l₁ with
| (inl s₂) := inl (eqv_of_sub_of_sub s₁ s₂)
| (inr n₂) := inr (λ h, absurd (sub_of_eqv_right h) n₂)
end
| (inr n₁) := inr (λ h, absurd (sub_of_eqv_left h) n₁)
end
example : [(1:nat), 2, 3, 2, 2, 2] ~ [1,3,3,1,2] :=
dec_trivial
definition finset_setoid [instance] (A : Type) : setoid (list A) :=
setoid.mk (@eqv A) (eqv.is_equivalence A)
definition finset (A : Type) : Type :=
quot (finset_setoid A)
definition has_decidable_eq [instance] {A : Type} [H : decidable_eq A] : ∀ s₁ s₂ : finset A, decidable (s₁ = s₂) :=
take s₁ s₂, quot.rec_on_subsingleton₂ s₁ s₂
(take l₁ l₂,
match decidable_eqv l₁ l₂ with
| inl e := inl (quot.sound e)
| inr d := inr (λ e, absurd (quot.exact e) d)
end)
definition to_finset {A : Type} (l : list A) : finset A :=
⟦l⟧
definition mem {A : Type} (a : A) (s : finset A) : Prop :=
quot.lift_on s
(λ l : list A, a ∈ l)
(λ l₁ l₂ r, propext (r a))
infix ∈ := mem
theorem mem_list {A : Type} {a : A} {l : list A} : a ∈ l → a ∈ ⟦l⟧ :=
λ H, H
definition empty {A : Type} : finset A :=
⟦nil⟧
notation `∅` := empty
definition union {A : Type} (s₁ s₂ : finset A) : finset A :=
quot.lift_on₂ s₁ s₂
(λ l₁ l₂ : list A, ⟦l₁ ++ l₂⟧)
(λ l₁ l₂ l₃ l₄ r₁ r₂,
begin
apply quot.sound,
intro a,
apply iff.intro,
begin
intro inl₁l₂,
apply (or.elim (mem_or_mem_of_mem_append inl₁l₂)),
intro inl₁, exact (mem_append_of_mem_or_mem (or.inl (iff.mp (r₁ a) inl₁))),
intro inl₂, exact (mem_append_of_mem_or_mem (or.inr (iff.mp (r₂ a) inl₂)))
end,
begin
intro inl₃l₄,
apply (or.elim (mem_or_mem_of_mem_append inl₃l₄)),
intro inl₃, exact (mem_append_of_mem_or_mem (or.inl (iff.mp' (r₁ a) inl₃))),
intro inl₄, exact (mem_append_of_mem_or_mem (or.inr (iff.mp' (r₂ a) inl₄)))
end,
end)
infix `` := union
theorem mem_union_left {A : Type} (s₁ s₂ : finset A) (a : A) : a ∈ s₁ → a ∈ s₁ s₂ :=
quot.ind₂ (λ l₁ l₂ ainl₁, mem_append_left l₂ ainl₁) s₁ s₂
theorem mem_union_right {A : Type} (s₁ s₂ : finset A) (a : A) : a ∈ s₂ → a ∈ s₁ s₂ :=
quot.ind₂ (λ l₁ l₂ ainl₂, mem_append_right l₁ ainl₂) s₁ s₂
theorem union_empty {A : Type} (s : finset A) : s ∅ = s :=
quot.induction_on s (λ l, quot.sound (λ a, by rewrite append_nil_right))
theorem empty_union {A : Type} (s : finset A) : ∅ s = s :=
quot.induction_on s (λ l, quot.sound (λ a, by rewrite append_nil_left))
example : to_finset (1::2::nil) to_finset (2::3::nil) = ⟦1 :: 2 :: 2 :: 3 :: nil⟧ :=
rfl
example : to_finset [(1:nat), 1, 2, 3] = to_finset [2, 3, 1, 2, 2, 3] :=
dec_trivial
example : to_finset [(1:nat), 1, 4, 2, 3] ≠ to_finset [2, 3, 1, 2, 2, 3] :=
dec_trivial
definition clean {A : Type} [H : decidable_eq A] (s : finset A) : finset A :=
quot.lift_on s (λ l, ⟦norep l⟧)
(λ l₁ l₂ e, calc
⟦norep l₁⟧ = ⟦l₁⟧ : quot.sound (eqv_norep l₁)
... = ⟦l₂⟧ : quot.sound e
... = ⟦norep l₂⟧ : quot.sound (eqv_norep l₂))
theorem eq_clean {A : Type} [H : decidable_eq A] : ∀ s : finset A, clean s = s :=
take s, quot.induction_on s (λ l, eq.symm (quot.sound (eqv_norep l)))
theorem eq_of_clean_eq_clean {A : Type} [H : decidable_eq A] : ∀ s₁ s₂ : finset A, clean s₁ = clean s₂ → s₁ = s₂ :=
take s₁ s₂, by rewrite *eq_clean; intro H; apply H
example : to_finset [(1:nat), 1, 2, 3] = to_finset [1, 2, 2, 2, 3, 3] :=
!eq_of_clean_eq_clean rfl
end finset