Skip to content

added new function take-all to stdl #1983

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 8 commits into from
Jun 27, 2023

Conversation

Sofia-Insa
Copy link
Contributor

Added new function take all to stdl Data.List.Properties and declare the change in CHANGELOG.md

Sofia-Insa and others added 2 commits June 14, 2023 13:13
add take-all to stdl Data.List.Propreties
@Sofia-Insa Sofia-Insa changed the title added new function take all to stdl added new function take-all to stdl Jun 14, 2023
Copy link
Contributor

@MatthewDaggitt MatthewDaggitt left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! A few comments.

Sofia-Insa and others added 4 commits June 15, 2023 10:57
Syntaxe of `take-all` adjusted
declaration of `take-al` to the section  **Other minor changes**  / Add new proofs in `Data.List.Properties`
@jamesmckinna
Copy link
Contributor

jamesmckinna commented Jun 18, 2023

Hmmm... as an alternative, consider the following 'Mathematics Made Difficult' style argument: for fixed xs

  • for any n, take n xs is a Prefix of xs
  • moreover, this is functorial (monotone) from the usual ordering on n to the Prefix extension/inclusion ordering (maybe this is more fiddly to prove than it looks)

Each of these seems a worthwhile property to have in the library?

Now, by entirely analogous, but simpler (the cases are in lockstep) reasoning to the lemma here

  • take (length xs) xs = xs

(Ditto. Though it obviously follows from the lemma proved in this PR)

Conclude, via the partial order structure of Prefix?

@JacquesCarette
Copy link
Contributor

So I had a bunch of lemmas (still do) using the ordering structure. But because of bugs in Agda (Cubical leaking) and the weird reduction properties of fromN<, I gave up on that path. It sure makes sense, but since I was trying to get specific things done, it wasn't worth pushing through the pain.

error l instead of l fixed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants