Commit 9a0583c7 authored by Armaël Guéneau's avatar Armaël Guéneau

Remove definition and basic lemmas on count

count has been added to TLC
parent 9289ec98
......@@ -184,20 +184,9 @@ Proof.
rew_listx in M. branches; autos*. }
Qed.
Definition count {A} (P : A -> Prop) (l: list A) :=
length (filter P l).
Definition measure C (L: list int) :=
count (= false) C + length L.
Lemma count_nonneg : forall A P (l: list A),
0 <= count P l.
Proof. intros. unfold count. applys~ length_nonneg. Qed.
Lemma count_cons : forall A (P: A -> Prop) x L,
count P (x :: L) = If P x then 1 + count P L else count P L.
Proof. intros. unfold count. rew_listx. case_if~. rew_listx~. Qed.
(* FIXME: lemmas about read and update are inconsistent.
For example:
- there is LibListZ.read_succ, but not LibListZ.update_succ
......@@ -219,7 +208,7 @@ Proof.
rewrite index_eq_inbound, length_cons in Ii.
rewrite* update_cons_pos. rewrite !count_cons. case_if~.
{ rewrite* IHL. rewrite* index_eq_inbound. }
{ rewrite~ IHL. rewrite* index_eq_inbound. } }
{ rewrite* IHL. rewrite* index_eq_inbound. } }
Qed.
Lemma measure_step : forall C L i,
......
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