Library prosa.classic.util.counting

Require Import prosa.classic.util.tactics prosa.classic.util.ord_quantifier.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

(* Additional lemmas about counting. *)
Section Counting.

  Lemma count_or :
    ∀ (T: eqType) (l: seq T) P Q,
      count (fun x ⇒ P x || Q x) l ≤ count P l + count Q l.

  Lemma sub_in_count :
    ∀ (T: eqType) (l: seq T) (P1 P2: T → bool),
      (∀ x, x \in l → P1 x → P2 x) →
      count P1 l ≤ count P2 l.

  Lemma count_sub_uniqr :
    ∀ (T: eqType) (l1 l2: seq T) P,
      uniq l1 →
      {subset l1 ≤ l2} →
      count P l1 ≤ count P l2.

  Lemma count_pred_inj :
    ∀ (T: eqType) (l: seq T) (P: T → bool),
      uniq l →
      (∀ x1 x2, P x1 → P x2 → x1 = x2) →
      count P l ≤ 1.

  Lemma count_exists :
    ∀ (T: eqType) (l: seq T) n (P: T → 'I_n → bool),
      uniq l →
      (∀ y x1 x2, P x1 y → P x2 y → x1 = x2) →
      count (fun (y: T) ⇒ [∃ x in 'I_n, P y x]) l ≤ n.

End Counting.