Library prosa.util.counting
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
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 25)
============================
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 28)
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 51)
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.