Commit 6461aa51 authored by Felipe Cerqueira's avatar Felipe Cerqueira

Add new lemmas for counting and sorting

parent 74126db1
......@@ -4,6 +4,15 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* Additional lemmas about counting. *)
Section Counting.
Lemma count_filter_fun :
forall (T: eqType) (l: seq T) P,
count P l = size (filter P l).
Proof.
intros T l P.
induction l; simpl; first by done.
by destruct (P a); [by rewrite add1n /=; f_equal | by rewrite add0n].
Qed.
Lemma count_or :
forall (T: eqType) (l: seq T) P Q,
count (fun x => P x || Q x) l <= count P l + count Q l.
......
......@@ -20,6 +20,18 @@ Section Sorting.
by rewrite addnS ltnS leq_addr.
Qed.
Lemma sort_ordered:
forall {T: eqType} (leT: rel T) (s: seq T) x0 idx,
sorted leT s ->
idx < (size s).-1 ->
leT (nth x0 s idx) (nth x0 s idx.+1).
Proof.
intros T leT s x0 idx SORT LT.
induction s; first by rewrite /= ltn0 in LT.
simpl in SORT, LT; move: SORT => /pathP SORT.
by simpl; apply SORT.
Qed.
Lemma sorted_rcons_prefix :
forall {T: eqType} (leT: rel T) s x,
sorted leT (rcons s x) ->
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment