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 xP 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.