From 31b160665845fe82ca6dc3e9bd5539a1a2bf404f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 25 Jul 2015 14:31:24 -0700 Subject: [PATCH] feat(library/data/bag): add subbag predicate --- library/data/bag.lean | 98 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 98 insertions(+) diff --git a/library/data/bag.lean b/library/data/bag.lean index d07fd8edc..784c58fc3 100644 --- a/library/data/bag.lean +++ b/library/data/bag.lean @@ -34,6 +34,9 @@ quot.lift_on b (λ l, ⟦a::l⟧) lemma insert_empty_eq_singleton (a : A) : insert a empty = singleton a := rfl +definition insert.comm (a₁ a₂ : A) (b : bag A) : insert a₁ (insert a₂ b) = insert a₂ (insert a₁ b) := +quot.induction_on b (λ l, quot.sound !perm.swap) + definition append (b₁ b₂ : bag A) : bag A := quot.lift_on₂ b₁ b₂ (λ l₁ l₂, ⟦l₁++l₂⟧) (λ l₁ l₂ l₃ l₄ h₁ h₂, quot.sound (perm_app h₁ h₂)) @@ -128,6 +131,13 @@ quot.induction_on₂ b₁ b₂ (λ l₁ l₂ (h : ∀ a, count a ⟦l₁⟧ = co ... ~ l++(a::r) : perm_middle ... = s₂ : e₁, quot.sound (gen l₁ l₂ h)) + +definition insert.inj {a : A} {b₁ b₂ : bag A} : insert a b₁ = insert a b₂ → b₁ = b₂ := +assume h, bag.ext (take x, + assert e : count x (insert a b₁) = count x (insert a b₂), by rewrite h, + by_cases + (suppose x = a, begin subst x, rewrite [*count_insert at e], injection e, assumption end) + (suppose x ≠ a, begin rewrite [*count_insert_of_ne this at e], assumption end)) end count section extract @@ -461,6 +471,9 @@ bag.ext (λ a, by rewrite [*count_union, max.comm]) lemma union.assoc (b₁ b₂ b₃ : bag A) : (b₁ ∪ b₂) ∪ b₃ = b₁ ∪ (b₂ ∪ b₃) := bag.ext (λ a, by rewrite [*count_union, max.assoc]) +theorem union.left_comm (s₁ s₂ s₃ : bag A) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃) := +!left_comm union.comm union.assoc s₁ s₂ s₃ + lemma union_self (b : bag A) : b ∪ b = b := bag.ext (λ a, by rewrite [*count_union, max_self]) @@ -477,6 +490,9 @@ bag.ext (λ a, by rewrite [*count_inter, min.comm]) lemma inter.assoc (b₁ b₂ b₃ : bag A) : (b₁ ∩ b₂) ∩ b₃ = b₁ ∩ (b₂ ∩ b₃) := bag.ext (λ a, by rewrite [*count_inter, min.assoc]) +theorem inter.left_comm (s₁ s₂ s₃ : bag A) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) := +!left_comm inter.comm inter.assoc s₁ s₂ s₃ + lemma inter_self (b : bag A) : b ∩ b = b := bag.ext (λ a, by rewrite [*count_inter, min_self]) @@ -528,4 +544,86 @@ calc (b₁ ∪ b₂) ∩ b₃ = b₃ ∩ (b₁ ∪ b₂) : inter.comm ... = (b₁ ∩ b₃) ∪ (b₃ ∩ b₂) : inter.comm ... = (b₁ ∩ b₃) ∪ (b₂ ∩ b₃) : inter.comm end union_inter + +section subbag +variable [decA : decidable_eq A] +include decA + +definition subbag (b₁ b₂ : bag A) := ∀ a, count a b₁ ≤ count a b₂ + +infix ⊆ := subbag + +definition subbag.refl (b : bag A) : b ⊆ b := +take a, !le.refl + +definition subbag.trans {b₁ b₂ b₃ : bag A} : b₁ ⊆ b₂ → b₂ ⊆ b₃ → b₁ ⊆ b₃ := +assume h₁ h₂, take a, le.trans (h₁ a) (h₂ a) + +definition subbag.antisymm {b₁ b₂ : bag A} : b₁ ⊆ b₂ → b₂ ⊆ b₁ → b₁ = b₂ := +assume h₁ h₂, bag.ext (take a, le.antisymm (h₁ a) (h₂ a)) + +definition count_le_of_subbag {b₁ b₂ : bag A} : b₁ ⊆ b₂ → ∀ a, count a b₁ ≤ count a b₂ := +assume h, h + +definition subbag.intro {b₁ b₂ : bag A} : (∀ a, count a b₁ ≤ count a b₂) → b₁ ⊆ b₂ := +assume h, h + +definition empty_subbag (b : bag A) : empty ⊆ b := +subbag.intro (take a, !zero_le) + +definition eq_empty_of_subbag_empty {b : bag A} : b ⊆ empty → b = empty := +assume h, subbag.antisymm h (empty_subbag b) + +definition union_subbag_of_subbag_of_subbag {b₁ b₂ b₃ : bag A} : b₁ ⊆ b₃ → b₂ ⊆ b₃ → b₁ ∪ b₂ ⊆ b₃ := +assume h₁ h₂, subbag.intro (λ a, calc + count a (b₁ ∪ b₂) = max (count a b₁) (count a b₂) : by rewrite count_union + ... ≤ count a b₃ : max_le (h₁ a) (h₂ a)) + +definition subbag_inter_of_subbag_of_subbag {b₁ b₂ b₃ : bag A} : b₁ ⊆ b₂ → b₁ ⊆ b₃ → b₁ ⊆ b₂ ∩ b₃ := +assume h₁ h₂, subbag.intro (λ a, calc + count a b₁ ≤ min (count a b₂) (count a b₃) : le_min (h₁ a) (h₂ a) + ... = count a (b₂ ∩ b₃) : by rewrite count_inter) + +definition subbag_union_left (b₁ b₂ : bag A) : b₁ ⊆ b₁ ∪ b₂ := +subbag.intro (take a, by rewrite [count_union]; apply le_max_left) + +definition subbag_union_right (b₁ b₂ : bag A) : b₂ ⊆ b₁ ∪ b₂ := +subbag.intro (take a, by rewrite [count_union]; apply le_max_right) + +definition inter_subbag_left (b₁ b₂ : bag A) : b₁ ∩ b₂ ⊆ b₁ := +subbag.intro (take a, by rewrite [count_inter]; apply min_le_left) + +definition inter_subbag_right (b₁ b₂ : bag A) : b₁ ∩ b₂ ⊆ b₂ := +subbag.intro (take a, by rewrite [count_inter]; apply min_le_right) + +definition subbag_append_left (b₁ b₂ : bag A) : b₁ ⊆ b₁ ++ b₂ := +subbag.intro (take a, by rewrite [count_append]; apply le_add_right) + +definition subbag_append_right (b₁ b₂ : bag A) : b₂ ⊆ b₁ ++ b₂ := +subbag.intro (take a, by rewrite [count_append]; apply le_add_left) + +definition inter_subbag_union (b₁ b₂ : bag A) : b₁ ∩ b₂ ⊆ b₁ ∪ b₂ := +subbag.trans (inter_subbag_left b₁ b₂) (subbag_union_left b₁ b₂) + +open decidable + +definition union_subbag_append (b₁ b₂ : bag A) : b₁ ∪ b₂ ⊆ b₁ ++ b₂ := +subbag.intro (take a, begin + rewrite [count_append, count_union], unfold max, + exact by_cases + (suppose count a b₁ < count a b₂, by rewrite [if_pos this]; apply le_add_left) + (suppose ¬ count a b₁ < count a b₂, by rewrite [if_neg this]; apply le_add_right) +end) + +definition subbag_insert (a : A) (b : bag A) : b ⊆ insert a b := +subbag.intro (take x, by_cases + (suppose x = a, by rewrite [this, count_insert]; apply le_succ) + (suppose x ≠ a, by rewrite [count_insert_of_ne this])) + +definition mem_of_subbag_of_mem {a : A} {b₁ b₂ : bag A} : b₁ ⊆ b₂ → a ∈ b₁ → a ∈ b₂ := +assume h₁ h₂, +have count a b₁ ≤ count a b₂, from count_le_of_subbag h₁ a, +have count a b₁ > 0, from h₂, +show count a b₂ > 0, from lt_of_lt_of_le `0 < count a b₁` `count a b₁ ≤ count a b₂` +end subbag end bag