Library prosa.util.counting


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.13.0 (January 2021)

----------------------------------------------------------------------------- *)


From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

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

  Lemma count_filter_fun :
     (T: eqType) (l: seq T) P,
      count P l = size (filter P l).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 22)
  
  ============================
  forall (T : eqType) (l : seq T) (P : pred T),
  count P l = size [seq x <- l | P x]

----------------------------------------------------------------------------- *)


  Proof.
    intros T l P.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 25)
  
  T : eqType
  l : seq T
  P : pred T
  ============================
  count P l = size [seq x <- l | P x]

----------------------------------------------------------------------------- *)


    induction l; simpl; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 46)
  
  T : eqType
  a : T
  l : seq T
  P : pred T
  IHl : count P l = size [seq x <- l | P x]
  ============================
  P a + count P l =
  size (if P a then a :: [seq x <- l | P x] else [seq x <- l | P x])

----------------------------------------------------------------------------- *)


    by destruct (P a); [by rewrite add1n /=; f_equal | by rewrite add0n].

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

End Counting.