From 72d6550a7aa60bf0d23cf3510c4cdde883180432 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 25 Jul 2015 17:44:03 -0700 Subject: [PATCH] feat(library/data/bag): show that subbag predicate is decidable when A has decidable equality --- library/data/bag.lean | 95 ++++++++++++++++++++++++++++++++++--------- 1 file changed, 76 insertions(+), 19 deletions(-) diff --git a/library/data/bag.lean b/library/data/bag.lean index 784c58fc3..5cf77d134 100644 --- a/library/data/bag.lean +++ b/library/data/bag.lean @@ -169,6 +169,17 @@ bag.induction_on b rfl (λ c b ih, by_cases (suppose a = c, begin subst c, rewrite [extract_insert, ih] end) (suppose a ≠ c, begin rewrite [extract_insert_of_ne this, count_insert_of_ne this, ih] end)) + +lemma count_extract_of_ne {a₁ a₂ : A} (h : a₁ ≠ a₂) (b : bag A) : count a₁ (extract a₂ b) = count a₁ b := +bag.induction_on b rfl + (take x b ih, by_cases + (suppose x = a₁, begin subst x, rewrite [extract_insert_of_ne (ne.symm h), *count_insert, ih] end) + (suppose x ≠ a₁, by_cases + (suppose x = a₂, begin subst x, rewrite [extract_insert, ih, count_insert_of_ne h] end) + (suppose x ≠ a₂, begin + rewrite [count_insert_of_ne (ne.symm `x ≠ a₁`), extract_insert_of_ne (ne.symm this)], + rewrite [count_insert_of_ne (ne.symm `x ≠ a₁`), ih] + end))) end extract section erase @@ -553,61 +564,61 @@ definition subbag (b₁ b₂ : bag A) := ∀ a, count a b₁ ≤ count a b₂ infix ⊆ := subbag -definition subbag.refl (b : bag A) : b ⊆ b := +lemma 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₃ := +lemma 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₂ := +lemma 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₂ := +lemma 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₂ := +lemma 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 := +lemma 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 := +lemma 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₃ := +lemma 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₃ := +lemma 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₂ := +lemma 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₂ := +lemma 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₁ := +lemma 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₂ := +lemma 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₂ := +lemma 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₂ := +lemma 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₂ := +lemma 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₂ := +lemma 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 @@ -615,15 +626,61 @@ subbag.intro (take a, begin (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 := +lemma 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₂ := +lemma 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₂` + +lemma extract_subbag (a : A) (b : bag A) : extract a b ⊆ b := +subbag.intro (take x, by_cases + (suppose x = a, by rewrite [this, count_extract]; apply zero_le) + (suppose x ≠ a, by rewrite [count_extract_of_ne this])) + +open bool + +private definition subcount : list A → list A → bool +| [] l₂ := tt +| (a::l₁) l₂ := if list.count a (a::l₁) ≤ list.count a l₂ then subcount l₁ l₂ else ff + +private lemma all_of_subcount_eq_tt : ∀ {l₁ l₂ : list A}, subcount l₁ l₂ = tt → ∀ a, list.count a l₁ ≤ list.count a l₂ +| [] l₂ h := take x, !zero_le +| (a::l₁) l₂ h := take x, + have subcount l₁ l₂ = tt, from by_contradiction (suppose subcount l₁ l₂ ≠ tt, + assert subcount l₁ l₂ = ff, from eq_ff_of_ne_tt this, + begin unfold subcount at h, rewrite [this at h, if_t_t at h], contradiction end), + assert ih : ∀ a, list.count a l₁ ≤ list.count a l₂, from all_of_subcount_eq_tt this, + assert i : list.count a (a::l₁) ≤ list.count a l₂, from by_contradiction (suppose ¬ list.count a (a::l₁) ≤ list.count a l₂, + begin unfold subcount at h, rewrite [if_neg this at h], contradiction end), + by_cases + (suppose x = a, by rewrite this; apply i) + (suppose x ≠ a, by rewrite [list.count_cons_of_ne this]; apply ih) + +private lemma ex_of_subcount_eq_ff : ∀ {l₁ l₂ : list A}, subcount l₁ l₂ = ff → ∃ a, ¬ list.count a l₁ ≤ list.count a l₂ +| [] l₂ h := by contradiction +| (a::l₁) l₂ h := by_cases + (suppose i : list.count a (a::l₁) ≤ list.count a l₂, + have subcount l₁ l₂ = ff, from by_contradiction (suppose subcount l₁ l₂ ≠ ff, + assert subcount l₁ l₂ = tt, from eq_tt_of_ne_ff this, + begin unfold subcount at h, rewrite [if_pos i at h, this at h], contradiction end), + have ih : ∃ a, ¬ list.count a l₁ ≤ list.count a l₂, from ex_of_subcount_eq_ff this, + obtain w hw, from ih, by_cases + (suppose w = a, begin subst w, existsi a, rewrite list.count_cons_eq, apply not_lt_of_ge, apply le_of_lt (lt_of_not_ge hw) end) + (suppose w ≠ a, exists.intro w (by rewrite (list.count_cons_of_ne `w ≠ a`); exact hw))) + (suppose ¬ list.count a (a::l₁) ≤ list.count a l₂, exists.intro a this) + +definition decidable_subbag [instance] (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) := +quot.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂, + match subcount l₁ l₂ with + | tt := suppose subcount l₁ l₂ = tt, inl (all_of_subcount_eq_tt this) + | ff := suppose subcount l₁ l₂ = ff, inr (suppose h : (∀ a, list.count a l₁ ≤ list.count a l₂), + obtain w hw, from ex_of_subcount_eq_ff `subcount l₁ l₂ = ff`, + absurd (h w) hw) + end rfl) end subbag end bag