List.countP.mono_left but strict inequality

Stream: Is there code for X?

[Aatman Supkar]

This can be used to take a list, and argue that if q is satisfied by each entry that satisfies p, then the weak inequality follows. I wish to provide a hypothesis that there exists an index where q is satisfied but p is not, and obtain a strict inequality. Do we have something that does that?

[Yury G. Kudryashov]

@loogle List.countP, _ < _

[loogle]

:search: List.countP_pos, List.countP_pos_iff, and 6 more

[Yury G. Kudryashov]

It looks like the answer is no.

[Edward van de Meent]

I suspect that it will be easiest to prove the contrapositive by induction

[Edward van de Meent]

So assuming the counts are equal and p -> q, all elements satisfying q must satisfy p

[Edward van de Meent]

actually i no longer think that's true... i think an argument making use of List.countP_eq_countP_filter_add might be easier

[Edward van de Meent]

variable {α : Type u} {l : List α} {P Q : α → Bool}

theorem List.countP_lt_countP (hpq : ∀ x ∈ l, P x → Q x) {x:α} (hx: x ∈ l) (hxP : P x = false) (hxQ : Q x):
    l.countP P < l.countP Q := by
  rw [List.countP_eq_countP_filter_add l Q P]
  have : List.countP (Q) (l.filter P) = List.countP P l := by
    rw [List.countP_filter, ←List.countP_attach, ←List.countP_attach (l := l)]
    congr
    ext x
    simp only [Bool.and_iff_right_iff_imp]
    exact hpq x.val x.property
  rw [this]
  simp only [Nat.lt_add_right_iff_pos, List.countP_pos_iff, List.mem_filter, Bool.not_eq_eq_eq_not,
    Bool.not_true]
  exact ⟨x,⟨hx,hxP⟩,hxQ⟩

[Kim Morrison]

I can get this down to

theorem List.countP_lt_countP (hpq : ∀ x ∈ l, P x → Q x) (y:α) (hx: y ∈ l) (hxP : P y = false) (hxQ : Q y) :
    l.countP P < l.countP Q := by
  induction l with
  | nil => grind
  | cons x xs ih =>
    have : xs.countP P ≤ xs.countP Q := countP_le_countP (by grind)
    specialize ih (by grind)
    grind

(on an unreleased version of Lean, sorry).

[Kim Morrison]

(And I hope we can do without the specialize line later.)