feat(library/data/hf): define Hereditarily finite sets
This commit is contained in:
Leonardo de Moura
parent
6fd3affeb1
commit
cee9d6b092
1 changed files with 322 additions and 0 deletions
322
library/data/hf.lean
Normal file
322
library/data/hf.lean
Normal file
|
|
@ -0,0 +1,322 @@
|
|||
/-
|
||||
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Leonardo de Moura
|
||||
|
||||
Hereditarily finite sets: finite sets whose elements are all hereditarily finite sets.
|
||||
|
||||
Remark: all definitions compute, however the performace is quite poor since
|
||||
we implement this module using a bijection from (finset nat) to nat, and
|
||||
this bijection is implemeted using the Ackermann coding.
|
||||
-/
|
||||
import data.nat data.finset.equiv
|
||||
open nat binary
|
||||
open -[notations]finset
|
||||
|
||||
definition hf := nat
|
||||
|
||||
namespace hf
|
||||
protected definition prio : num := num.succ std.priority.default
|
||||
|
||||
protected definition has_decidable_eq [instance] : decidable_eq hf :=
|
||||
nat.has_decidable_eq
|
||||
|
||||
definition of_finset (s : finset hf) : hf :=
|
||||
@equiv.to_fun _ _ finset_nat_equiv_nat s
|
||||
|
||||
definition to_finset (h : hf) : finset hf :=
|
||||
@equiv.inv _ _ finset_nat_equiv_nat h
|
||||
|
||||
definition to_nat (h : hf) : nat :=
|
||||
h
|
||||
|
||||
definition of_nat (n : nat) : hf :=
|
||||
n
|
||||
|
||||
lemma to_finset_of_finset (s : finset hf) : to_finset (of_finset s) = s :=
|
||||
@equiv.left_inv _ _ finset_nat_equiv_nat s
|
||||
|
||||
lemma of_finset_to_finset (s : hf) : of_finset (to_finset s) = s :=
|
||||
@equiv.right_inv _ _ finset_nat_equiv_nat s
|
||||
|
||||
lemma to_finset_inj {s₁ s₂ : hf} : to_finset s₁ = to_finset s₂ → s₁ = s₂ :=
|
||||
λ h, function.injective_of_left_inverse of_finset_to_finset h
|
||||
|
||||
lemma of_finset_inj {s₁ s₂ : finset hf} : of_finset s₁ = of_finset s₂ → s₁ = s₂ :=
|
||||
λ h, function.injective_of_left_inverse to_finset_of_finset h
|
||||
|
||||
/- empty -/
|
||||
definition empty : hf :=
|
||||
of_finset (finset.empty)
|
||||
|
||||
notation `∅` := hf.empty
|
||||
|
||||
/- insert -/
|
||||
definition insert (a s : hf) : hf :=
|
||||
of_finset (finset.insert a (to_finset s))
|
||||
|
||||
/- mem -/
|
||||
definition mem (a : hf) (s : hf) : Prop :=
|
||||
finset.mem a (to_finset s)
|
||||
|
||||
infix `∈` := mem
|
||||
|
||||
definition not_mem (a : hf) (s : hf) : Prop := ¬ a ∈ s
|
||||
|
||||
infix `∉` := not_mem
|
||||
|
||||
lemma not_mem_empty (a : hf) : a ∉ ∅ :=
|
||||
begin unfold [not_mem, mem, empty], rewrite to_finset_of_finset, apply finset.not_mem_empty end
|
||||
|
||||
lemma mem_insert (a s : hf) : a ∈ insert a s :=
|
||||
begin unfold [mem, insert], rewrite to_finset_of_finset, apply finset.mem_insert end
|
||||
|
||||
lemma mem_insert_of_mem (a b s : hf) : a ∈ s → a ∈ insert b s :=
|
||||
begin unfold [mem, insert], intros, rewrite to_finset_of_finset, apply finset.mem_insert_of_mem, assumption end
|
||||
|
||||
lemma eq_or_mem_of_mem_insert (a b s : hf) : a ∈ insert b s → a = b ∨ a ∈ s :=
|
||||
begin unfold [mem, insert], rewrite to_finset_of_finset, intros, apply eq_or_mem_of_mem_insert, assumption end
|
||||
|
||||
theorem mem_of_mem_insert_of_ne {x a : hf} {s : hf} : x ∈ insert a s → x ≠ a → x ∈ s :=
|
||||
begin unfold [mem, insert], rewrite to_finset_of_finset, intros, apply mem_of_mem_insert_of_ne, repeat assumption end
|
||||
|
||||
protected theorem ext {s₁ s₂ : hf} : (∀ a, a ∈ s₁ ↔ a ∈ s₂) → s₁ = s₂ :=
|
||||
assume h,
|
||||
assert to_finset s₁ = to_finset s₂, from finset.ext h,
|
||||
assert of_finset (to_finset s₁) = of_finset (to_finset s₂), by rewrite this,
|
||||
by rewrite [*of_finset_to_finset at this]; exact this
|
||||
|
||||
theorem insert_eq_of_mem {a : hf} {s : hf} : a ∈ s → insert a s = s :=
|
||||
begin unfold mem, intro h, unfold [mem, insert], rewrite (finset.insert_eq_of_mem h), rewrite of_finset_to_finset end
|
||||
|
||||
/- union -/
|
||||
definition union (s₁ s₂ : hf) : hf :=
|
||||
of_finset (finset.union (to_finset s₁) (to_finset s₂))
|
||||
|
||||
infix [priority hf.prio] ∪ := union
|
||||
|
||||
theorem mem_union_left {a : hf} {s₁ : hf} (s₂ : hf) : a ∈ s₁ → a ∈ s₁ ∪ s₂ :=
|
||||
begin unfold mem, intro h, unfold union, rewrite to_finset_of_finset, apply finset.mem_union_left _ h end
|
||||
|
||||
theorem mem_union_l {a : hf} {s₁ : hf} {s₂ : hf} : a ∈ s₁ → a ∈ s₁ ∪ s₂ :=
|
||||
mem_union_left s₂
|
||||
|
||||
theorem mem_union_right {a : hf} {s₂ : hf} (s₁ : hf) : a ∈ s₂ → a ∈ s₁ ∪ s₂ :=
|
||||
begin unfold mem, intro h, unfold union, rewrite to_finset_of_finset, apply finset.mem_union_right _ h end
|
||||
|
||||
theorem mem_union_r {a : hf} {s₂ : hf} {s₁ : hf} : a ∈ s₂ → a ∈ s₁ ∪ s₂ :=
|
||||
mem_union_right s₁
|
||||
|
||||
theorem mem_or_mem_of_mem_union {a : hf} {s₁ s₂ : hf} : a ∈ s₁ ∪ s₂ → a ∈ s₁ ∨ a ∈ s₂ :=
|
||||
begin unfold [mem, union], rewrite to_finset_of_finset, intro h, apply finset.mem_or_mem_of_mem_union h end
|
||||
|
||||
theorem mem_union_iff {a : hf} (s₁ s₂ : hf) : a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂ :=
|
||||
iff.intro
|
||||
(λ h, mem_or_mem_of_mem_union h)
|
||||
(λ d, or.elim d
|
||||
(λ i, mem_union_left _ i)
|
||||
(λ i, mem_union_right _ i))
|
||||
|
||||
theorem mem_union_eq {a : hf} (s₁ s₂ : hf) : (a ∈ s₁ ∪ s₂) = (a ∈ s₁ ∨ a ∈ s₂) :=
|
||||
propext !mem_union_iff
|
||||
|
||||
theorem union.comm (s₁ s₂ : hf) : s₁ ∪ s₂ = s₂ ∪ s₁ :=
|
||||
hf.ext (λ a, by rewrite [*mem_union_eq]; exact or.comm)
|
||||
|
||||
theorem union.assoc (s₁ s₂ s₃ : hf) : (s₁ ∪ s₂) ∪ s₃ = s₁ ∪ (s₂ ∪ s₃) :=
|
||||
hf.ext (λ a, by rewrite [*mem_union_eq]; exact or.assoc)
|
||||
|
||||
theorem union.left_comm (s₁ s₂ s₃ : hf) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃) :=
|
||||
!left_comm union.comm union.assoc s₁ s₂ s₃
|
||||
|
||||
theorem union.right_comm (s₁ s₂ s₃ : hf) : (s₁ ∪ s₂) ∪ s₃ = (s₁ ∪ s₃) ∪ s₂ :=
|
||||
!right_comm union.comm union.assoc s₁ s₂ s₃
|
||||
|
||||
theorem union_self (s : hf) : s ∪ s = s :=
|
||||
hf.ext (λ a, iff.intro
|
||||
(λ ain, or.elim (mem_or_mem_of_mem_union ain) (λ i, i) (λ i, i))
|
||||
(λ i, mem_union_left _ i))
|
||||
|
||||
theorem union_empty (s : hf) : s ∪ ∅ = s :=
|
||||
hf.ext (λ a, iff.intro
|
||||
(suppose a ∈ s ∪ ∅, or.elim (mem_or_mem_of_mem_union this) (λ i, i) (λ i, absurd i !not_mem_empty))
|
||||
(suppose a ∈ s, mem_union_left _ this))
|
||||
|
||||
theorem empty_union (s : hf) : ∅ ∪ s = s :=
|
||||
calc ∅ ∪ s = s ∪ ∅ : union.comm
|
||||
... = s : union_empty
|
||||
|
||||
/- inter -/
|
||||
definition inter (s₁ s₂ : hf) : hf :=
|
||||
of_finset (finset.inter (to_finset s₁) (to_finset s₂))
|
||||
|
||||
infix [priority hf.prio] ∩ := inter
|
||||
|
||||
theorem mem_of_mem_inter_left {a : hf} {s₁ s₂ : hf} : a ∈ s₁ ∩ s₂ → a ∈ s₁ :=
|
||||
begin unfold mem, unfold inter, rewrite to_finset_of_finset, intro h, apply finset.mem_of_mem_inter_left h end
|
||||
|
||||
theorem mem_of_mem_inter_right {a : hf} {s₁ s₂ : hf} : a ∈ s₁ ∩ s₂ → a ∈ s₂ :=
|
||||
begin unfold mem, unfold inter, rewrite to_finset_of_finset, intro h, apply finset.mem_of_mem_inter_right h end
|
||||
|
||||
theorem mem_inter {a : hf} {s₁ s₂ : hf} : a ∈ s₁ → a ∈ s₂ → a ∈ s₁ ∩ s₂ :=
|
||||
begin unfold mem, intro h₁ h₂, unfold inter, rewrite to_finset_of_finset, apply finset.mem_inter h₁ h₂ end
|
||||
|
||||
theorem mem_inter_iff (a : hf) (s₁ s₂ : hf) : a ∈ s₁ ∩ s₂ ↔ a ∈ s₁ ∧ a ∈ s₂ :=
|
||||
iff.intro
|
||||
(λ h, and.intro (mem_of_mem_inter_left h) (mem_of_mem_inter_right h))
|
||||
(λ h, mem_inter (and.elim_left h) (and.elim_right h))
|
||||
|
||||
theorem mem_inter_eq (a : hf) (s₁ s₂ : hf) : (a ∈ s₁ ∩ s₂) = (a ∈ s₁ ∧ a ∈ s₂) :=
|
||||
propext !mem_inter_iff
|
||||
|
||||
theorem inter.comm (s₁ s₂ : hf) : s₁ ∩ s₂ = s₂ ∩ s₁ :=
|
||||
hf.ext (λ a, by rewrite [*mem_inter_eq]; exact and.comm)
|
||||
|
||||
theorem inter.assoc (s₁ s₂ s₃ : hf) : (s₁ ∩ s₂) ∩ s₃ = s₁ ∩ (s₂ ∩ s₃) :=
|
||||
hf.ext (λ a, by rewrite [*mem_inter_eq]; exact and.assoc)
|
||||
|
||||
theorem inter.left_comm (s₁ s₂ s₃ : hf) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) :=
|
||||
!left_comm inter.comm inter.assoc s₁ s₂ s₃
|
||||
|
||||
theorem inter.right_comm (s₁ s₂ s₃ : hf) : (s₁ ∩ s₂) ∩ s₃ = (s₁ ∩ s₃) ∩ s₂ :=
|
||||
!right_comm inter.comm inter.assoc s₁ s₂ s₃
|
||||
|
||||
theorem inter_self (s : hf) : s ∩ s = s :=
|
||||
hf.ext (λ a, iff.intro
|
||||
(λ h, mem_of_mem_inter_right h)
|
||||
(λ h, mem_inter h h))
|
||||
|
||||
theorem inter_empty (s : hf) : s ∩ ∅ = ∅ :=
|
||||
hf.ext (λ a, iff.intro
|
||||
(suppose a ∈ s ∩ ∅, absurd (mem_of_mem_inter_right this) !not_mem_empty)
|
||||
(suppose a ∈ ∅, absurd this !not_mem_empty))
|
||||
|
||||
theorem empty_inter (s : hf) : ∅ ∩ s = ∅ :=
|
||||
calc ∅ ∩ s = s ∩ ∅ : inter.comm
|
||||
... = ∅ : inter_empty
|
||||
|
||||
/- card -/
|
||||
definition card (s : hf) : nat :=
|
||||
finset.card (to_finset s)
|
||||
|
||||
theorem card_empty : card ∅ = 0 :=
|
||||
rfl
|
||||
|
||||
lemma ne_empty_of_card_eq_succ {s : hf} {n : nat} : card s = succ n → s ≠ ∅ :=
|
||||
by intros; substvars; contradiction
|
||||
|
||||
/- erase -/
|
||||
definition erase (a : hf) (s : hf) : hf :=
|
||||
of_finset (erase a (to_finset s))
|
||||
|
||||
theorem mem_erase (a : hf) (s : hf) : a ∉ erase a s :=
|
||||
begin unfold [not_mem, mem, erase], rewrite to_finset_of_finset, apply finset.mem_erase end
|
||||
|
||||
theorem card_erase_of_mem {a : hf} {s : hf} : a ∈ s → card (erase a s) = pred (card s) :=
|
||||
begin unfold mem, intro h, unfold [erase, card], rewrite to_finset_of_finset, apply finset.card_erase_of_mem h end
|
||||
|
||||
theorem card_erase_of_not_mem {a : hf} {s : hf} : a ∉ s → card (erase a s) = card s :=
|
||||
begin unfold [not_mem, mem], intro h, unfold [erase, card], rewrite to_finset_of_finset, apply finset.card_erase_of_not_mem h end
|
||||
|
||||
theorem erase_empty (a : hf) : erase a ∅ = ∅ :=
|
||||
rfl
|
||||
|
||||
theorem ne_of_mem_erase {a b : hf} {s : hf} : b ∈ erase a s → b ≠ a :=
|
||||
by intro h beqa; subst b; exact absurd h !mem_erase
|
||||
|
||||
theorem mem_of_mem_erase {a b : hf} {s : hf} : b ∈ erase a s → b ∈ s :=
|
||||
begin unfold [erase, mem], rewrite to_finset_of_finset, intro h, apply mem_of_mem_erase h end
|
||||
|
||||
theorem mem_erase_of_ne_of_mem {a b : hf} {s : hf} : a ≠ b → a ∈ s → a ∈ erase b s :=
|
||||
begin intro h₁, unfold mem, intro h₂, unfold erase, rewrite to_finset_of_finset, apply mem_erase_of_ne_of_mem h₁ h₂ end
|
||||
|
||||
theorem mem_erase_iff (a b : hf) (s : hf) : a ∈ erase b s ↔ a ∈ s ∧ a ≠ b :=
|
||||
iff.intro
|
||||
(assume H, and.intro (mem_of_mem_erase H) (ne_of_mem_erase H))
|
||||
(assume H, mem_erase_of_ne_of_mem (and.right H) (and.left H))
|
||||
|
||||
theorem mem_erase_eq (a b : hf) (s : hf) : a ∈ erase b s = (a ∈ s ∧ a ≠ b) :=
|
||||
propext !mem_erase_iff
|
||||
|
||||
theorem erase_insert {a : hf} {s : hf} : a ∉ s → erase a (insert a s) = s :=
|
||||
begin
|
||||
unfold [not_mem, mem, erase, insert],
|
||||
intro h, rewrite [to_finset_of_finset, finset.erase_insert h, of_finset_to_finset]
|
||||
end
|
||||
|
||||
theorem insert_erase {a : hf} {s : hf} : a ∈ s → insert a (erase a s) = s :=
|
||||
begin
|
||||
unfold mem, intro h, unfold [insert, erase],
|
||||
rewrite [to_finset_of_finset, finset.insert_erase h, of_finset_to_finset]
|
||||
end
|
||||
|
||||
|
||||
/- subset -/
|
||||
definition subset (s₁ s₂ : hf) : Prop :=
|
||||
finset.subset (to_finset s₁) (to_finset s₂)
|
||||
|
||||
infix [priority hf.prio] `⊆` := subset
|
||||
|
||||
theorem empty_subset (s : hf) : ∅ ⊆ s :=
|
||||
begin unfold [empty, subset], rewrite to_finset_of_finset, apply finset.empty_subset (to_finset s) end
|
||||
|
||||
theorem subset.refl (s : hf) : s ⊆ s :=
|
||||
begin unfold [subset], apply finset.subset.refl (to_finset s) end
|
||||
|
||||
theorem subset.trans {s₁ s₂ s₃ : hf} : s₁ ⊆ s₂ → s₂ ⊆ s₃ → s₁ ⊆ s₃ :=
|
||||
begin unfold [subset], intro h₁ h₂, apply finset.subset.trans h₁ h₂ end
|
||||
|
||||
theorem mem_of_subset_of_mem {s₁ s₂ : hf} {a : hf} : s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂ :=
|
||||
begin unfold [subset, mem], intro h₁ h₂, apply finset.mem_of_subset_of_mem h₁ h₂ end
|
||||
|
||||
theorem subset.antisymm {s₁ s₂ : hf} : s₁ ⊆ s₂ → s₂ ⊆ s₁ → s₁ = s₂ :=
|
||||
begin unfold [subset], intro h₁ h₂, apply to_finset_inj (finset.subset.antisymm h₁ h₂) end
|
||||
|
||||
-- alternative name
|
||||
theorem eq_of_subset_of_subset {s₁ s₂ : hf} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂ :=
|
||||
subset.antisymm H₁ H₂
|
||||
|
||||
theorem subset_of_forall {s₁ s₂ : hf} : (∀x, x ∈ s₁ → x ∈ s₂) → s₁ ⊆ s₂ :=
|
||||
begin unfold [mem, subset], intro h, apply finset.subset_of_forall h end
|
||||
|
||||
theorem subset_insert (s : hf) (a : hf) : s ⊆ insert a s :=
|
||||
begin unfold [subset, insert], rewrite to_finset_of_finset, apply finset.subset_insert (to_finset s) end
|
||||
|
||||
theorem eq_empty_of_subset_empty {x : hf} (H : x ⊆ ∅) : x = ∅ :=
|
||||
subset.antisymm H (empty_subset x)
|
||||
|
||||
theorem subset_empty_iff (x : hf) : x ⊆ ∅ ↔ x = ∅ :=
|
||||
iff.intro eq_empty_of_subset_empty (take xeq, by rewrite xeq; apply subset.refl ∅)
|
||||
|
||||
theorem erase_subset_erase (a : hf) {s t : hf} : s ⊆ t → erase a s ⊆ erase a t :=
|
||||
begin unfold [subset, erase], intro h, rewrite *to_finset_of_finset, apply finset.erase_subset_erase a h end
|
||||
|
||||
theorem erase_subset (a : hf) (s : hf) : erase a s ⊆ s :=
|
||||
begin unfold [subset, erase], rewrite to_finset_of_finset, apply finset.erase_subset a (to_finset s) end
|
||||
|
||||
theorem erase_eq_of_not_mem {a : hf} {s : hf} : a ∉ s → erase a s = s :=
|
||||
begin unfold [not_mem, mem, erase], intro h, rewrite [finset.erase_eq_of_not_mem h, of_finset_to_finset] end
|
||||
|
||||
theorem erase_insert_subset (a : hf) (s : hf) : erase a (insert a s) ⊆ s :=
|
||||
begin unfold [erase, insert, subset], rewrite [*to_finset_of_finset], apply finset.erase_insert_subset a (to_finset s) end
|
||||
|
||||
theorem erase_subset_of_subset_insert {a : hf} {s t : hf} (H : s ⊆ insert a t) : erase a s ⊆ t :=
|
||||
hf.subset.trans (!hf.erase_subset_erase H) (erase_insert_subset a t)
|
||||
|
||||
theorem insert_erase_subset (a : hf) (s : hf) : s ⊆ insert a (erase a s) :=
|
||||
decidable.by_cases
|
||||
(assume ains : a ∈ s, by rewrite [!insert_erase ains]; apply subset.refl)
|
||||
(assume nains : a ∉ s, by rewrite[erase_eq_of_not_mem nains]; apply subset_insert)
|
||||
|
||||
theorem insert_subset_insert (a : hf) {s t : hf} : s ⊆ t → insert a s ⊆ insert a t :=
|
||||
begin
|
||||
unfold [subset, insert], intro h,
|
||||
rewrite *to_finset_of_finset, apply finset.insert_subset_insert a h
|
||||
end
|
||||
|
||||
theorem subset_insert_of_erase_subset {s t : hf} {a : hf} (H : erase a s ⊆ t) : s ⊆ insert a t :=
|
||||
subset.trans (insert_erase_subset a s) (!insert_subset_insert H)
|
||||
|
||||
theorem subset_insert_iff (s t : hf) (a : hf) : s ⊆ insert a t ↔ erase a s ⊆ t :=
|
||||
iff.intro !erase_subset_of_subset_insert !subset_insert_of_erase_subset
|
||||
end hf
|
||||
Loading…
Reference in a new issue