Skip to content

Add `filter_reverse`, `head_filter_Some`, `last_filter_Some` lemmas

Jonas Kastberg requested to merge jihgfee/stdpp:last_filter_postfix into master

Added the lemma:

Lemma last_filter_postfix P `{!∀ x : A, Decision (P x)} l x
  last (filter P l) = Some x →
  ∃ l1 l2, l = l1 ++ [x] ++ l2 ∧ Forall (λ z, ¬ (P z)) l2.

(and its counterpart for head)

The lemmas seem useful and general enough to fit in stdpp. The last lemma derives the property Forall (λ z, ¬ (P z)) l2 of the postfix of a split l1 ++ [x] ++ l2 for a list l whenever last (filter P l) = Some x.

Edited by Robbert Krebbers

Merge request reports