proposition: Lemma filter_absorb_map: forall A (f : A -> A) (g : A -> bool) L, (forall x, (g (f x) = g x) /\ ((g (f x) = false) \/ f x = x)) -> filter g (map f L) = filter g L.
proof: Proof. induction L; auto; intros. simpl. case_eq (g (f a)); intro. destruct (H a). rewrite H0 in H2. destruct H2. discriminate. rewrite H1 in *. rewrite H0. rewrite H2, IHL; trivial. destruct (H a). rewrite H1 in H0. rewrite H0. apply IHL; auto. Qed.
imports: RelationClasses VST.floyd.proofauto CertiGraph.lib.List_ext CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.binary_heap_malloc_spec CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel