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

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.

added 1 commit

• 8a6f2b36 - Explicitly named variables of induction

Compare with previous version

Thanks for the MR. Could you split it up into two parts:

• One for the general lemmas about last (which I think are good, modulo comments).
• One for the interaction of filter and last (we might need some additional debating there as you already guessed ).

added 1 commit

• f491810c - Some improvements for proposed lemmas and added [last_app]

Compare with previous version

mentioned in merge request !355 (merged)

added 3 commits

• 095fc4ef - Added some useful lemmas for the [last] function
• 87eb1296 - Added explicit names of variables for induction tactic
• f8144839 - Added [last_filter_postfix] lemma

Compare with previous version

added 9 commits

• f8144839...f23a05c3 - 6 commits from branch iris:master
• da8c8ad2 - Added some useful lemmas for the [last] function
• 1f8670d7 - Added [last_filter_postfix] lemma
• e964b0a5 - Fixed duplicate lemma from merge

Compare with previous version

added 1 commit

• ecee5998 - Removed overly specialised lemma

Compare with previous version

added 1 commit

• 25d6b519 - Clean up proof a bit

Compare with previous version

added 1 commit

• ee9589c8 - Added [last_filter_postfix] lemma

Compare with previous version

resolved all threads

added 1 commit

• 513ab0b8 - Cleaned a whitespace

Compare with previous version

added 1 commit

• c5900b79 - Added [head_filter_prefix] lemma, and dependencies

Compare with previous version

added 1 commit

• fe795bf4 - Moved the [head_filter_prefix] and [last_filter_postfix] lemmas

Compare with previous version