Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Add a couple lemmas about product in Data.List.Properties #2460

Merged
merged 8 commits into from
Aug 22, 2024
Merged

Add a couple lemmas about product in Data.List.Properties #2460

merged 8 commits into from
Aug 22, 2024

Conversation

dolio
Copy link
Contributor

@dolio dolio commented Aug 15, 2024

These are a couple of lemmas I found useful when trying to formalize Euclid's proof of the infinitude of primes.

  • the product of non-zero naturals is non-zero
  • any element of a list of non-zero naturals is less-or-equal to the product of the list

Hopefully I didn't just miss these somewhere else, but the divisibility result above this was about the only theorem I could find about product.

JacquesCarette
JacquesCarette requested changes Aug 16, 2024
View reviewed changes
@jamesmckinna
Copy link
Contributor

And: CHANGELOG entries please!

jamesmckinna
jamesmckinna reviewed Aug 16, 2024
View reviewed changes
jamesmckinna
jamesmckinna reviewed Aug 16, 2024
View reviewed changes
jamesmckinna
jamesmckinna approved these changes Aug 16, 2024
View reviewed changes
Copy link
Contributor

@jamesmckinna jamesmckinna left a comment •
edited
Loading

Choose a reason for hiding this comment

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

This seems fine as it is, but my nitpicks above might streamline things a bit, aesthetically at least?

@jamesmckinna
Copy link
Contributor

jamesmckinna commented Aug 16, 2024 •
edited
Loading

NB. It looks as though you have forked the main repo and then done this PR directly on your master branch... it's much better (cleaner; more robust; easier to handle mutliple PRs simultaneously) to do PRs independently on separate branches off your master branch... as described in section 5 of HACKING...

dolio added 2 commits August 16, 2024 17:38
@dolio
Various product proof adjustments
333f990 
- Renamed nonEmpty-product to product≢0
- Swapped argument order of ∈⇒≤product
- Factored the ordering proofs out into Data.Nat.Properties
- Removed the custom product≢0 proof in Primality
@dolio
Fix a CHANGELOG oversight
8367e67
@jamesmckinna
Copy link
Contributor

Thanks for a very nice first PR! (NB better to fix up your git branches before the next one... ;-))
A couple of final refinements, and we should be good to go!
@JacquesCarette are you happy with the refactoring?

@JacquesCarette JacquesCarette added this pull request to the merge queue Aug 20, 2024
@MatthewDaggitt MatthewDaggitt added this to the v2.2 milestone Aug 20, 2024
@MatthewDaggitt MatthewDaggitt removed this pull request from the merge queue due to a manual request Aug 20, 2024
@JacquesCarette JacquesCarette added this pull request to the merge queue Aug 22, 2024
Merged via the queue into agda:master with commit 355ac25 Aug 22, 2024
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@MatthewDaggitt MatthewDaggitt MatthewDaggitt left review comments

@jamesmckinna jamesmckinna jamesmckinna approved these changes

@JacquesCarette JacquesCarette JacquesCarette approved these changes

Assignees
No one assigned
Labels
addition
Projects
None yet
Milestone
v2.2
Development

Successfully merging this pull request may close these issues.
4 participants
@dolio @jamesmckinna @JacquesCarette @MatthewDaggitt