Dropping or taking from lists on the right #
Taking or removing element from the tail end of a list
Main defintions #
rdrop n
: dropn : ℕ
elements from the tailrtake n
: taken : ℕ
elements from the taildrop_while p
: remove all the elements that satisfy a decidablep : α → Prop
from the tail of a list until hitting the first non-satisfying elementtake_while p
: take all the elements that satisfy a decidablep : α → Prop
from the tail of a list until hitting the first non-satisfying element
Implementation detail #
The two predicate-based methods operate by performing the regular "from-left" operation on
list.reverse
, followed by another list.reverse
, so they are not the most performant.
The other two rely on list.length l
so they still traverse the list twice. One could construct
another function that takes a L : ℕ
and use L - n
. Under a proof condition that
L = l.length
, the function would do the right thing.
Drop elements from the tail end of a list that satisfy p : α → Prop
.
Implemented naively via list.reverse
Equations
- list.rdrop_while p l = (list.drop_while p l.reverse).reverse
@[simp]
theorem
list.rdrop_while_concat
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α)
(x : α) :
list.rdrop_while p (l ++ [x]) = ite (p x) (list.rdrop_while p l) (l ++ [x])
@[simp]
theorem
list.rdrop_while_concat_pos
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α)
(x : α)
(h : p x) :
list.rdrop_while p (l ++ [x]) = list.rdrop_while p l
@[simp]
theorem
list.rdrop_while_concat_neg
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α)
(x : α)
(h : ¬p x) :
list.rdrop_while p (l ++ [x]) = l ++ [x]
theorem
list.rdrop_while_singleton
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(x : α) :
list.rdrop_while p [x] = ite (p x) list.nil [x]
theorem
list.rdrop_while_last_not
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α)
(hl : list.rdrop_while p l ≠ list.nil) :
¬p ((list.rdrop_while p l).last hl)
theorem
list.rdrop_while_prefix
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α) :
list.rdrop_while p l <+: l
@[simp]
theorem
list.rdrop_while_eq_nil_iff
{α : Type u_1}
{p : α → Prop}
[decidable_pred p]
{l : list α} :
list.rdrop_while p l = list.nil ↔ ∀ (x : α), x ∈ l → p x
@[simp]
@[simp]
theorem
list.rdrop_while_eq_self_iff
{α : Type u_1}
{p : α → Prop}
[decidable_pred p]
{l : list α} :
theorem
list.drop_while_idempotent
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α) :
list.drop_while p (list.drop_while p l) = list.drop_while p l
theorem
list.rdrop_while_idempotent
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α) :
list.rdrop_while p (list.rdrop_while p l) = list.rdrop_while p l
Take elements from the tail end of a list that satisfy p : α → Prop
.
Implemented naively via list.reverse
Equations
- list.rtake_while p l = (list.take_while p l.reverse).reverse
@[simp]
theorem
list.rtake_while_concat
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α)
(x : α) :
list.rtake_while p (l ++ [x]) = ite (p x) (list.rtake_while p l ++ [x]) list.nil
@[simp]
theorem
list.rtake_while_concat_pos
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α)
(x : α)
(h : p x) :
list.rtake_while p (l ++ [x]) = list.rtake_while p l ++ [x]
@[simp]
theorem
list.rtake_while_concat_neg
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α)
(x : α)
(h : ¬p x) :
list.rtake_while p (l ++ [x]) = list.nil
theorem
list.rtake_while_suffix
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α) :
list.rtake_while p l <:+ l
@[simp]
theorem
list.rtake_while_eq_self_iff
{α : Type u_1}
{p : α → Prop}
[decidable_pred p]
{l : list α} :
list.rtake_while p l = l ↔ ∀ (x : α), x ∈ l → p x
@[simp]
theorem
list.mem_rtake_while_imp
{α : Type u_1}
{p : α → Prop}
[decidable_pred p]
{l : list α}
{x : α}
(hx : x ∈ list.rtake_while p l) :
p x
theorem
list.rtake_while_idempotent
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α) :
list.rtake_while p (list.rtake_while p l) = list.rtake_while p l