countp_nodup.lean

import data.finset data.multiset
import tactic
import init.classical
noncomputable theory
open_locale classical
local attribute [instance, priority 10000] classical.prop_decidable -- avoid decidability hell

universe u
variables {α β : Type u}

namespace list
variable (a : α)
variable (l : list α)

theorem countp_cons (p : α → Prop) [∀ a, decidable (p a)] :
    countp p (a :: l) = ite (p a) 1 0 +  countp p l :=
by {by_cases p a; rw countp; simp [h], ring,}

theorem not_mem_of_countp_eq_zero (l : list α) (p : α → Prop) :
    l.countp p = 0 ↔ ∀ a ∈ l, ¬ p a :=
begin
  split,
  { intros hzero a hmem hp,
    induction l with x l ih,
    { simp at hmem, exact hmem, },
    simp [countp_cons] at *,
    cases hmem with hx hl,
    { rw ← hx at hzero, simp [hp] at hzero, exact hzero, },
    exact ih hzero.left hl,},
  intros h,
  induction l with x l ih,
  { simp, },
  simp [countp_cons],
  split,
  { rw ih,
    intros a hmem,
    exact h a (by simp [hmem]), },
  simp [h x],
end

theorem countp_split (l : list α) (p : α → Prop) (q : α → Prop) :
    l.countp p = (l.filter q).countp p + (l.filter (λ a, ¬ q a)).countp p :=
begin
  induction l with x l ih,
  { simp, },
  simp [countp_cons],
  by_cases p x,
  { by_cases q x; simp *, },
  simp [h, ih],
end

theorem countp_le_length {l : list α} {p : α → Prop} : l.countp p ≤ l.length :=
begin
  induction l with x l ih,
  simp,
  by_cases p x; simp [h, ih],
  linarith,
end

theorem length_lt_of_filter_of_mem (l : list α) (p : α → Prop) :
    (∃ a ∈ l, ¬ p a) → (l.filter p).length < l.length :=
begin
  intro h,
  cases h with a h,
  cases h with hmem ha,
  induction l with x l ih,
  { simp at ⊢ hmem,
    exfalso,
    exact hmem, },
  rw ← list.countp_eq_length_filter,
  simp [list.countp_cons],
  by_cases heq : a = x,
  { rw ← heq,
    simp [ha],
    have : countp p l ≤ length l, from countp_le_length,
    linarith,
  },
  have : a ∈ l,
  { simp at hmem,
    cases hmem,
    exact absurd hmem heq,
    exact hmem,
  },
  have : l.countp p < length l, by simp [list.countp_eq_length_filter, ih this],
  have hleite : ite (p x) 1 0 ≤ 1, by by_cases p x; simp *,
  linarith,
end

theorem countp_false_eq_zero {l : list α} : l.countp (λ x, false) = 0 :=
by {induction l with x l ih, simp, simp [ih]}
end list

@[simp]
lemma exists_and (a : α) (p : α → Prop) : (∃ x, p x) ∧ p a ↔ p a :=
by { split; simp, intro hp, split, exact ⟨a, hp⟩, exact hp, }

lemma countp_no_dup_aux (len : ℕ) {r : α → β → Prop}
    (nodup : ∀ (x y : α) (b : β), x ≠ y → ¬ (r x b ∧ r y b))
    : ∀ l1 l2 : list β, l1.length ≤ len → (∀ a : α, l1.countp (r a) = l2.countp (r a)) →
    l1.countp (λ b, ∃ a, r a b) = l2.countp (λ b, ∃ a, r a b) :=
begin
  -- Strong induction on l1.length.
  induction len with len,
  { -- Just the base case.
    intros l1 l2 hlen hp,
    simp at hlen,
    have : l1 = list.nil, by rw list.eq_nil_of_length_eq_zero hlen,
    rw this at hp ⊢,
    simp at hp ⊢,
    have : ∀ b ∈ l2, ¬ ∃ a, r a b,
    { intros b hmem h,
      cases h with a ha,
      have : ∀ c ∈ l2, ¬ r a c,
      rw ← list.not_mem_of_countp_eq_zero,
      { symmetry,
        exact hp a, },
      exact absurd ha (this b hmem),
    },
    symmetry,
    rw list.not_mem_of_countp_eq_zero,
    exact this, },
  intros l1 l2 hlen h,
  by_cases hex : ∃ a, ∃ b ∈ l1, r a b,
  { -- Case when both sides of the goal are non-zero.
    cases hex with a ha,
    -- There are an equal (and non-zero) number of elements in l1 and l2 satisfying r a.
    -- Split each list into two parts depending, one that satisfies r a, and one that doesn't.
    rw list.countp_split l1 _ (r a),
    rw list.countp_split l2 _ (r a),

    -- First, we know that the parts satisfying r a have equal length,
    -- so cancel them out on both sides.
    repeat {rw @list.countp_filter _ _ _ (λ (b : β), r a b) _ _},
    simp [-list.countp_filter],
    suffices : list.countp (λ (b : β), ∃ (a : α), r a b) (list.filter (λ (a_1 : β), ¬r a a_1) l1) + list.countp (r a) l1 =
    list.countp (λ (b : β), ∃ (a : α), r a b) (list.filter (λ (a_1 : β), ¬r a a_1) l2) + list.countp (r a) l2,
    { convert this }, -- decidability hell, the instances don't match
    simp [h a, -list.countp_filter],
    set l1' := (list.filter (λ (a_1 : β), ¬r a a_1) l1),
    set l2' := (list.filter (λ (a_1 : β), ¬r a a_1) l2),

    -- Now we are left with two strictly smaller lists,
    -- containing only elements not satisfying r a.
    -- We show that the inductive hypothesis holds for this pair of lists.

    have hlen' : l1'.length ≤ len,
    { have : l1'.length < l1.length,
      { apply list.length_lt_of_filter_of_mem,
        simp at ⊢ ha,
        exact ha,
      },
      have : nat.succ l1'.length ≤ nat.succ len,
      { apply nat.succ_le_of_lt,
        apply nat.lt_of_lt_of_le this hlen, },
      exact nat.le_of_succ_le_succ this,
    },

    -- a' ≠ a case
    have heqcountp : ∀ l (a' : α) (hne : a' ≠ a),
        (list.filter (λ (b : β), ¬r a b) l).countp (r a') = l.countp (r a'),
    { intros l a' hne,
      induction l with x l ih,
      simp,
      simp at ih,
      simp [list.countp_cons, ih],
      by_cases r a' x,
      { have : ¬ r a x, { have not_and := nodup a' a x hne, finish [nodup a' a x hne], },
        simp *, },
      simp *,
    },

    -- if a' = a, then both sides are zero, otherwise it's the same as heqcountp.
    have h' : ∀ (a : α), list.countp (r a) l1' = list.countp (r a) l2',
    { intro a',
      by_cases hcase : a' = a,
      { rw hcase,
        simp,
        suffices : list.countp (λ (a : β), false) l1 = list.countp (λ (a : β), false) l2,
        { convert this, }, -- more decidability hell, the instances don't match
        simp [list.countp_false_eq_zero],
      },
      rw heqcountp l1 _ hcase,
      rw heqcountp l2 _ hcase,
      exact h a',
    },
    exact len_ih l1' l2' (by simp [hlen']) h', },
  
  -- Case when both sides of the goal are zero.
  -- We use countp_eq_length_filter and then show that
  -- no element can belong to either of the filtered lists.
  have : ∀ b ∈ l1, ¬ ∃ a, r a b,
  { intros b hmem h,
    cases h with a ha,
    have : ∃ (a : α) (b : β) (H : b ∈ l1), r a b,
    exact ⟨a, ⟨b, ⟨hmem, ha⟩⟩⟩,
    exact absurd this hex, },
  rw list.countp_eq_length_filter,
  rw list.countp_eq_length_filter,
  have : ∀ b, b ∉ list.filter (λ (b : β), ∃ (a : α), r a b) l1,
  { intros b h,
    simp at h,
    exact absurd h.right (this b h.left), },
  rw list.eq_nil_iff_forall_not_mem.mpr this,
  have : ∀ b, b ∉ list.filter (λ (b : β), ∃ (a : α), r a b) l2,
  { intros b h,
    simp at h,
    cases h with hmem hr,
    cases hr with a hr,
    have : list.countp (r a) l2 = 0,
    { rw ← h a,
      have : ∀ b, b ∉ list.filter (r a) l1,
      { intros b h,
        simp at h,
        cases h with hmem hr,
        have : ∃ (a : α) (b : β) (H : b ∈ l1), r a b,
        exact ⟨a, ⟨b, ⟨hmem, hr⟩⟩⟩,
        exact absurd this hex, },
      rw list.countp_eq_length_filter,
      rw list.eq_nil_iff_forall_not_mem.mpr this,
      simp, },
    rw list.countp_eq_length_filter at this,
    have : l2.filter (r a) = [], from list.eq_nil_of_length_eq_zero this,
    have hfilter_mem : b ∈ l2.filter (r a),
    { rw list.mem_filter,
      exact ⟨hmem, hr⟩, },
    rw list.eq_nil_iff_forall_not_mem at this,
    exact absurd hfilter_mem (this b), },
  rw list.eq_nil_iff_forall_not_mem.mpr this,
end

lemma countp_no_dup {l1 l2 : list β} {r : α → β → Prop} (nodup : ∀ (x y : α) (b : β),
    x ≠ y → ¬ (r x b ∧ r y b)) : (∀ a : α, l1.countp (r a) = l2.countp (r a)) →
    l1.countp (λ b, ∃ a, r a b) = l2.countp (λ b, ∃ a, r a b) :=
begin
  set len := l1.length,
  exact countp_no_dup_aux len nodup l1 l2 (by simp [len]),
end