`take_app_ge` has unneeded side-condition

Lemma take_app_ge l k n :
  length l ≤ n → take n (l ++ k) = l ++ take (n - length l) k.

length l ≤ n is not needed.

In fact, the stdlib has firstn_app which exactly the above std++ lemma without side-condition.

changed the description

The same problem for drop_app_ge, stdlib has the better skipn_app.

And relatedly, we miss skipn_rev and firstn_rev for the linear-time reverse.

Sounds like we should just have take_app without the side-condition then, and remove take_app_ge?

And relatedly, we miss skipn_rev and firstn_rev for the linear-time reverse.

See !517 (merged)

mentioned in merge request !518 (merged)

It turns out that I was not entirely right, the most general lemma (corresponding to firstn_app) for take and ++ is:

take n (l ++ k) = take n l ++ take (n - length l) k

The existing take_app_ge : take .. = l ++ take .. really needs the length inequality as a side-condition, but can be derived from the most general lemma above.

The merge request !517 (merged) !518 (merged) uses take_app and drop_app for the most general lemmas (without side-conditions), and derives other lemmas from it.

The merge request !517 (merged) uses take_app and drop_app for the most general lemmas (without side-conditions), and derives other lemmas from it.

I assume you mean !518 (merged)?

Yes :).

mentioned in commit c57a2eed

closed with merge request !518 (merged)