Induction over sigma in filters

Stream: new members

[Aria Miuk]

Hello, could anyone please point me in a good direction wrt. a proof using dependent types - I am not quite used to working with them. It seems to me my approach from non--dependent scenario is completely inapplicable within the realm of dependent types.

The basic version of the theorem is as follows. (I shall just use Lean for brevity.)

import data.list
open list

variables
    {α : Type} {l : list α} [decidable_eq α]
    {P : α → Prop} [decidable_pred P]
    {Q : α → Prop} [decidable_pred Q]
    {R : α → Prop} [decidable_pred R]

lemma filter_partition (h : ∀x, ¬Q x ↔ R x) :
    length (filter P l) = length (filter P (filter Q l)) + length (filter P (filter R l)) :=
begin
  induction l with hd,
    {simp only [add_zero, list.filter_nil, list.length]},
    {
      by_cases h₁ : R hd,
        {
          have : ¬Q hd, from (h _).2 h₁,
          by_cases h₂ : P hd; simp*,
        },
        {
          have : Q hd, from (not_iff_comm.1 (h _)).1 h₁,
          by_cases h₂ : P hd; simp*
        }
    }
end

I included the proof to show what idea doesn't seem to translate (as far as I can tell) into the following version.

lemma filter_partition_dependent
  {P : {x // x ∈ l} → Prop} [decidable_pred P]
  (h : ∀x, ¬Q x ↔ R x) :
  length (filter (λ (x : {x // x ∈ l}), P x) (attach l)) =
  length (filter (λ (x : {x // x ∈ filter Q l}), P ⟨x.1, mem_of_mem_filter x.2⟩) (attach (filter Q l))) +
  length (filter (λ (x : {x // x ∈ filter R l}), P ⟨x.1, mem_of_mem_filter x.2⟩) (attach (filter R l))) :=
begin
  resetI, induction l with hd tl ih,
    {simp [attach]},
    {
      -- ih : ∀ {P : {x // x ∈ tl} → Prop}
    }
end

This version is not much different. I promoted the original P : α → Prop to P : {x // x ∈ l} → Prop,
which means I had to use attached versions of lists. The filtered lists also need a proof that a ∈ filter p l → a ∈ l.

The problem is that the original proof by induction on l (with hd :: tl in the inductive case) appears to no longer work, because the inductive hypothesis wants P : {x // x ∈ tl} → Prop and I only have P : {x // x ∈ hd :: tl} → Prop.
I tried synthesizing one from P but the conclusion still has the original P that also considers the head.
I can't think of a way to actually successfully use induction here - do I need some filter congruence lemmas?
These seem to only work in "homogeneous" settings with filtering predicates of equivalent types.

Could someone please suggest an alternative way to prove this? Or am I missing something here, have I managed to make the theorem false?
Here's also a link to the web editor which conveniently contains a minimal compilable example - I am not sure how Zulip handles long URLs so I made a pastebin of the link. https://pastebin.com/raw/grX324K2

[Kevin Buzzard]

I am not a computer scientist but I think I'd be tempted to look for a result in the library of the following form: if L : list X and there's a map f: X -> Y and a predicate Q on Y then map f (filter (Q o f) L) = filter Q (map f L), and then use the fact that list.map doesn't change length, let Q be "if x is in l then P(x) else false" and muddle on from there.

[Aria Miuk]

Thank you Kevin, I will give it a try! I've been very much "stuck" in the inductive mindset as conceptually it seems like the most obvious thing to do. Surely tagging along "that" obvious properly shouldn't change the way the proof can be done but the more I struggle with it, the more impossible the inductive proof seems to be. Actually understanding why this happens could come in handy.

[Mario Carneiro]

You can't prove things about attach by induction. You have to generalize it, in the same way that attach itself is generalized, to pmap

[Aria Miuk]

Is this a common "theme" within the realm of dependent types? I can't even formulate this question more specifically - it just appears to be clear that this is not specific to attach only.

[Mario Carneiro]

I think something like this will work:

lemma filter_partition_dependent'
  {β} {P : β → Prop} [decidable_pred P]
  (h : ∀x, ¬Q x ↔ R x)
  (p : α → Prop) (f : ∀ a, p a → β)
  {β₁} (i₁ : β₁ → β) (p₁ : α → Prop) (f₁ : ∀ a, p₁ a → β₁)
  {β₂} (i₂ : β₂ → β) (p₂ : α → Prop) (f₂ : ∀ a, p₂ a → β₂) :
  ∀ (H : ∀ (a : α), a ∈ l → p a)
    (H₁ : ∀ (a : α), a ∈ filter Q l → p₁ a)
    (H₂ : ∀ (a : α), a ∈ filter R l → p₂ a),
  length (filter P (pmap f l H)) =
  length (filter (λ x, P (i₁ x)) (pmap f₁ (filter Q l) H₁)) +
  length (filter (λ x, P (i₂ x)) (pmap f₂ (filter R l) H₂)) :=

[Mario Carneiro]

there may be more hypotheses needed

[Mario Carneiro]

But this is assuming you actually want a direct inductive proof. It is quite likely that Kevin's suggestion of stringing together other lemmas will work here

[Aria Miuk]

Interesting. Thanks everyone kindly for the suggestions, very appreciated.

[Mario Carneiro]

Note that this is a direct generalization of the target statement, like so:

lemma filter_partition_dependent
  {P : {x // x ∈ l} → Prop} [decidable_pred P]
  (h : ∀x, ¬Q x ↔ R x) :
  length (filter P (attach l)) =
  length (filter (λ (x : {x // x ∈ filter Q l}), P ⟨x.1, mem_of_mem_filter x.2⟩) (attach (filter Q l))) +
  length (filter (λ (x : {x // x ∈ filter R l}), P ⟨x.1, mem_of_mem_filter x.2⟩) (attach (filter R l))) :=
filter_partition_dependent' h _ _ _ _ _ _ _ _ _ _ _

[Aria Miuk]

I am not sure how I feel about dependent type right now, there's a lot to process. I read a quote on Coq along the lines of "Coq has a very powerful type system. But don't use it." and perhaps I am starting to see as to why that would be the case.

[Mario Carneiro]

I can get behind that quote