New functions take-drop-1 and take-one-more added to Data.List.Properties

[Sofia-Insa]

functions
take-drop-1
take-one-more
added to Data.List.Properties and declared in CHANGELOG.md

Creation of a section take-drop in Data.List.Properties.
Moved take++drop from drop section to take-drop section.

The name of the two new functions are up to debate

[MatthewDaggitt]

Please see comments in #1983 for similar things that need addressing.

[MatthewDaggitt]

I think this equality should the other way around. We usually have the function application on the left and the reduction behaviour on the right.

[jamesmckinna]

The meta-heuristic being

complex => simple(r)

[jamesmckinna]

Not sure that the tabulate really belongs in the lemma statement. What you seem to have us a lemma which combines:

• interaction of take and suc on the one hand;
• semantics of tabulate on the other.

Suggest splitting out the first one. That may also uncouple the dependency on Fin (which would otherwise be needed for tabulate)?

[JacquesCarette]

So I had tried the lemmas without tabulate and succeeded. However, the results were basically unusable.

For example, with take-one-more, the natural statement involves lookup and then you get stuff that involves length l in the type and it ends up being just horrible. Trying to then prove the combined lemma with tabulate (which is the one I really needed) got me deep into subst hell. [I think that lookup's type involves "green slime" if I've got that concept right.]

So yes, both of these should have tabulate in their name. Also, I don't know how to factor them into useful pieces, even though there indeed are theorems where they are factored.

[jamesmckinna]

Hmm. @JacquesCarette i would look at these proofs... but have no spare time to allocate right now. My first thought (don't be the first to groan) is: clearly try to avoid subst hell, but if you have green slime in a type, ... then abstract over it!?

This is what with/views are actually for.

So I'm sorry not to have the time, if I could then try to make this a good didactic example on non-trivial with programming...

Separately: I further can't help thinking that proofs of lemmas about tabulate on lists should 'really' go via the corresponding statements on Data.Vec.Functional, where the Fin n -> A abstraction is the basic notion...?

[jamesmckinna]

OK... I may have to revise my comments above (but I still need to think some more). But in the meantime:

• cast hell is definitely not as bad as subst hell, and we only need cast here...
• ... thus enabling me to refactor the proof of take-one-more as follows

take-suc : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in
           take (suc m) xs ≡ take m xs ∷ʳ lookup xs i
take-suc (x ∷ xs) zero    = refl
take-suc (x ∷ xs) (suc i) = cong (x ∷_) (take-suc xs i)

take-suc-tabulate : ∀ {n} (f : Fin n → A) (i : Fin n) → let m = toℕ i in
                    take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f i
take-suc-tabulate f i rewrite sym (toℕ-cast (sym (length-tabulate f)) i) | sym (lookup-tabulate f i)
  = take-suc (tabulate f) (cast _ i)

Conclusion (partisan/partial, at least on my side): the refactoring is worth doing, and not as bad as @JacquesCarette claims.
UPDATED: the typechecker somehow could re-infer an equational constraint in the final rewrite, so I with-bound that equation eq and that fixed things. Starting to get a little crunchy and annoying, but I think acceptably so. The encapsulation of the cast-based reasoning in the lemma lookup-tabulate is very much your friend here!

[jamesmckinna]

Likewise:

drop-take-suc : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in
           drop m (take (suc m) xs) ≡ [ lookup xs i ]
drop-take-suc (x ∷ xs) zero    = refl
drop-take-suc (x ∷ xs) (suc i) = drop-take-suc xs i

drop-take-suc-tabulate : ∀ {n} (f : Fin n → A) (i : Fin n) → let m = toℕ i in
                  drop m (take (suc m) (tabulate f)) ≡ [ f i ]
drop-take-suc-tabulate f i rewrite sym (toℕ-cast (sym (length-tabulate f)) i) | sym (lookup-tabulate f i)
  = drop-take-suc (tabulate f) (cast _ i)

[MatthewDaggitt]

Apart from that, and the merge conflicts, this now looks good to go. Thanks for the help @jamesmckinna!

[jamesmckinna]

Of course, the multiple appeals to sym during the various rewrites are a very ugly wart (because they adhere to the complex => simple(r) design metaheuristic... sigh).

[MatthewDaggitt]

Sorry forgot to post his review. Once this is addressed, and the merge conflicts are resolved, I'll merge this in 👍