Add prime factorization and its properties #1969
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
I'd missed this when copy-pasting from my old code in a separate repo
gallais
reviewed
May 15, 2023
Taneb
force-pushed
the
prime-factorization
branch
from
a7a0b65 to
7ec3801
Compare
src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
Outdated
Show resolved
Hide resolved
|
Also needs a CHANGELOG entry |
| ------------------------------------------------------------------------ | ||
| -- Core definition | ||
|
|
||
| record PrimeFactorisation (n : ℕ) : Set where |
There was a problem hiding this comment.
The 'traditional' notion of PrimeFactorisation uses a list of (multiplicity, prime) pairs and has the extra invariant that all primes are distinct.
I am not suggesting you change this definition - but you should probably comment on your design choice, so that this aspect doesn't puzzle a maintainer years down the road.
| factorisation≥1 {[]} [] = s≤s z≤n | ||
| factorisation≥1 {suc a ∷ as} (pa ∷ asPrime) = *-mono-≤ {1} {1 + a} (s≤s z≤n) (factorisation≥1 asPrime) | ||
|
|
||
| factorisationPullToFront : ∀ {as} {p} → Prime p → p ∣ product as → All Prime as → ∃[ as′ ] as ↭ (p ∷ as′) |
There was a problem hiding this comment.
Wouldn't it be 'simpler' if this took a PrimeFactorisation as input instead of the pieces it contains?
Also it feels like this could be proven more simply:
- prove p is a member of the list as
- then there's a permutation that puts it at the front.
This would be straightforward if you already knew it was a PrimeFactorisation.
There was a problem hiding this comment.
I've simplified it a bit. I don't think I do want it to take a PrimeFactorisation, because it recurses on the list, which would be a little more awkward. But maybe I'm wrong here, I'll think about it more
jamesmckinna
requested changes
Dec 26, 2023
It feels like we're importing half the module anyway
jamesmckinna
reviewed
Feb 1, 2024
Following up on this here... why not factor this proof as one for a commutative monoid operation, and then instantiate to |
|
Addressed some of the feedback. @Taneb if you're willing to write something brief about @JacquesCarette's comment on the unique multiplicity representation I'm happy to merge this in. |
|
@jamesmckinna any chance you could turn your thumbs up into an "approve"? 😄 |
jamesmckinna
approved these changes
Mar 16, 2024
Apologies for holding things up through inattention and too much nit-picking! Now DONE, and hitting 'merge'... |
andreasabel
pushed a commit
that referenced
this pull request
Jul 10, 2024
* Add prime factorization and its properties * Add missing header comment I'd missed this when copy-pasting from my old code in a separate repo * Remove completely trivial lemma * Use equational reasoning in quotient|n proof * Fix typo in module header * Factorization => Factorisation * Use Nat lemma in extend-|/ * [ cleanup ] part of the proof * [ cleanup ] finishing up the job * [ cleanup ] a little bit more * [ cleanup ] the import list * [ fix ] header style * [ fix ] broken merge: missing import * Move Data.Nat.Rough to Data.Nat.Primality.Rough * Rename productPreserves↭⇒≡ to product-↭ * Use proof of Prime=>NonZero * Open reasoning once in factoriseRec * Rename Factorisation => PrimeFactorisation * Move wheres around * Tidy up Rough a bit * Move quotient|n to top of file * Replace factorisationPullToFront with slightly more generally useful factorisationHasAllPrimeFactors and a bit of logic * Fix import after merge * Clean up proof of 2-rough-n * Make argument to 2-rough-n implicit * Rename 2-rough-n to 2-rough * Complete merge, rewrite factorisation logic a bit Rewrite partially based on suggestions from James McKinna * Short circuit when candidate is greater than square root of product * Remove redefined lemma * Minor simplifications * Remove private pattern synonyms * Change name of lemma * Typo * Remove using list from import It feels like we're importing half the module anyway * Clean up proof * Fixes after merge * Addressed some feedback * Fix previous merge --------- Co-authored-by: Guillaume Allais <[email protected]> Co-authored-by: MatthewDaggitt <[email protected]>
Closed
github-merge-queue bot
pushed a commit
that referenced
this pull request
Sep 7, 2024
* Bump stdlib and agda version in installation guide (#2027)
* Simplify more `Data.Product` imports to `Data.Product.Base` (#2036)
* Simplify more `Data.Product` import to `Data.Product.Base`
* Simplify more `Data.Product` import to `Data.Product.Base`
* Indent
* Wrapping Comments & Fixing Code Delimiters (#2015)
* Add new pattern synonym `divides-refl` to `Data.Nat.Divisibility.Core`
* Simplify more `Relation.Binary` imports (#2034)
* Rename and deprecate `excluded-middle` (#2026)
* Simplified `String` imports (#2016)
* Change `Function.Definitions` to use strict inverses (#1156)
* Proofs `take/drop/head -map-commute` added to Data.List.Properties (#1986)
* Simplified `Vec` import (#2018)
* More `Data.Product` simplifications (#2039)
* Added Unnormalised Rational Field Structure (#1959)
* More simplifications for `Relation.Binary` imports (#2038)
* Move just a few more things over to new Function hierarchy. (#2044)
* Final `Data.Product` import simplifications (#2052)
* Added properties of Heyting Commutative Ring (#1968)
* Add more properties for `xor` (#2035)
* Additional lemmas about lists and vectors (#2020)
* Removed redundant `import`s from `Data.Bool.Base` (#2062)
* Tidying up `Data.String` (#2061)
* More `Relation.Binary` simplifications (#2053)
* Add `drop-drop` in `Data.List.Properties` (#2043)
* Rename `push-function-into-if`
* agda-stdlib-utils/AllNonAsciiChars: use List1.head instead of List.head
* Bump resolvers in stack-{9.4.5,9.6.2}.yaml
* Bump Haskell CI to GHC 9.8.0 and 9.4.6; allow text-2.1
* Rename `take-drop-id` and `take++drop` (#2069)
A useful improvement to consistency of names,
* Add `find`, `findIndex`, and `findIndices` for `Data.List` (#2042)
* `find*` functions for `Data.List`
both decidable predicate and boolean function variants
* Back to `Maybe.map`
* New type for findIndices
* Add comments
* Respect style guide
---------
Co-authored-by: jamesmckinna <[email protected]>
* Final `Relation.Binary` simplifications (#2068)
* Spellchecked `CHANGELOG` (#2078)
* #2075: Remove symmetry assumption from lexicographic well-foundedness (#2077)
* Make sure RawRing defines rawRingWithoutOne (#1967)
* Direct products and minor fixes (#1909)
* Refine imports in `Reflection.AST` (#2072)
* Add some `_∷ʳ_` properties to `Data.Vec.Properties` (#2041)
* Monadic join (#2079)
* Move `≡-setoid` to `Function.Indexed.Relation.Binary.Equality` (#2047)
* Making (more) arguments implicit in lexicographic ordering lemmas
* `WellFounded` proofs for transitive closure (#2082)
* Add properties of Vector operations `reverse`, `_++_` and `fromList` (#2045)
* Rename `minor changes` section in CHANGELOG
* Improve implementation of `splitAt`, `take` and `drop` in `Data.List`. (#2056)
* Add a recursive view of `Fin n` (#1923)
* Use new style `Function` hierarchy everywhere. (#1895)
* Fix typo and whitespace violation (#2104)
* Add Kleene Algebra morphism with composition and identity construct (#1936)
* Added foldr of permutation of Commutative Monoid (#1944)
* Add `begin-irrefl` reasoning combinator (#1470)
* Refactor some lookup and truncation lemmas (#2101)
* Add style-guide note about local suffix (#2109)
* Weakened pre-conditions of grouped map lemmas (#2108)
* Undeprecate inspect idiom (#2107)
* Add some lemmas related to renamings and substitutions (#1750)
* Proof of the Binomial Theorem for `(Commutative)Semiring` [supersedes #1287] (#1928)
* Modernise `Relation.Nullary` code (#2110)
* Add new fixities (#2116)
Co-authored-by: Sofia El Boufi--Crouzet <[email protected]>
* Adds setoid export to `Algebra.Bundles.SemiringWithoutOne`
* #453: added `Dense` relations and `DenseLinearOrder` (#2111)
* Rectifies the negated equality symbol in `Data.Rational.Unnormalised.*` (#2118)
* Sync insert, remove, and update functionalities for `List` and `Vec` (#2049)
* De-symmetrising `Relation.Binary.Bundles.Preorder._∼_` (#2099)
* Redefines `Data.Nat.Base._≤″_` (#1948)
* Sync `iterate` and `replicate` for `List` and `Vec` (#2051)
* Changes explicit argument `y` to implicit in `Induction.WellFounded.WfRec` (#2084)
* Re-export numeric subclass instances
* Revert "Re-export numeric subclass instances"
This reverts commit 91fd951c117311b2beb2db4a582c4f152eac787d.
* Add (propositional) equational reasoning combinators for vectors (#2067)
* Strict and non-strict transitive property names (#2089)
* Re-export numeric subclass instances (#2122)
* Added Irreflexivity and Asymmetry of WellFounded Relations (#2119)
* Fix argument order of composition operators (#2121)
* Make size parameter on 'replicate' explicit (#2120)
* [fixes #2130] Moving `Properties.HeytingAlgebra` from `Relation.Binary` to `Relation.Binary.Lattice` (#2131)
* [fixes #2127] Fixes #1930 `import` bug (#2128)
* [fixes #1214] Add negated ordering relation symbols systematically to `Relation.Binary.*` (#2095)
* Refactoring (inversion) properties of `_<_` on `Nat`, plus consequences (#2000)
* Bump CI tests to Agda-2.6.4 (#2134)
* Remove `Algebra.Ordered` (#2133)
* [ fix ] missing name in LICENCE file (#2139)
* Add new blocking primitives to `Reflection.TCM` (#1972)
* Change definition of `IsStrictTotalOrder` (#2137)
* Add _<$>_ operator for Function bundle (#2144)
* [ fix #2086 ] new web deployment strategy (#2147)
* [ admin ] fix sorting logic (#2151)
With the previous script we were sorting entries of the form
html/vX.Y.Z/index.html but the order is such that vX.Y/ < vX.Y.Z/
and so we were ending up with v1.7 coming after v1.7.3.
This fixes that by using sed to get rid of the html/ prefix
and the /index.html suffix before the sorting phase.
* Add coincidence law to modules (#1898)
* Make reasoning modular by adding new `Reasoning.Syntax` module (#2152)
* Fixes typos identified in #2154 (#2158)
* tackles #2124 as regards `case_return_of_` (#2157)
* Rename preorder ~ relation reasoning combinators (#2156)
* Move ≡-Reasoning from Core to Properties and implement using syntax (#2159)
* Add consistent deprecation warnings to old function hierarchy (#2163)
* Rename symmetric reasoning combinators. Minimal set of changes (#2160)
* Restore 'return' as an alias for 'pure' (#2164)
* [ fix #2153 ] Properly re-export specialised combinators (#2161)
* Connect `LeftInverse` with (`Split`)`Surjection` (#2054)
* Added remaining flipped and negated relations to binary relation bundles (#2162)
* Tidy up CHANGELOG in preparation for release candidate (#2165)
* Spellcheck CHANGELOG (#2167)
* spellcheck; `fix-whitespace`; unfixed: a few alignment issues; typo `predications` to `predicates` in `Relation.Unary.Relation.Binary.Equality`
* Fixed Agda version typo in README (#2176)
* Fixed in deprecation warning for `<-transˡ` (#2173)
* Bump Haskell CI (original!) to latest minor GHC versions (#2187)
* [fixes #2175] Documentation misc. typos etc. for RC1 (#2183)
* missing comma!
* corrected reference to `README.Design.Decidability`
* typo: capitalisation
* updated `installation-guide`
* added word to `NonZero` section heading
* Run workflows on any PR
* Add merge-group trigger to workflows
---------
Co-authored-by: MatthewDaggitt <[email protected]>
* [fixes #2178] regularise and specify/systematise, the conventions for symbol usage (#2185)
* regularise and specify/systematise, the conventions for symbol usage
* typos/revisions
* Move `T?` to `Relation.Nullary.Decidable.Core` (#2189)
* Move `T?` to `Relation.Nullary.Decidable.Core`
* Var name fix
* Some refactoring
* Fix failing tests and address remaining comments
* Fix style-guide
* Make decidable versions of sublist functions the default (#2186)
* Make decdable versions of sublist functions the default
* Remove imports Bool.Properties
* Address comments
* [ fix #1743 ] move README to `doc/` directory (#2184)
* [ admin ] dev playground
* [ fix #1743 ] move README to doc/ directory
* [ fix ] whitespace violations
* [ ci ] update to cope with new doc/ directory
* [ cleanup ] remove stale reference to travis.yml
* [ admin ] update README-related instructions
* [ admin ] fix build badges
* [ fix ] `make test` build
* Moved contents of notes/ to doc/
* Added CHANGELOG entry
---------
Co-authored-by: MatthewDaggitt <[email protected]>
* documentation: fix link to `installation-guide`, `README.agda`, `README.md`... (#2197)
* fix link to `installation-guide`
* catching another reference to `notes/`
* note on instance brackets
* `HACKING` guide
* added Gurmeet Singh's changes
* [ fix ] links in README.md
---------
Co-authored-by: Guillaume Allais <[email protected]>
* easy deprecation; leftover from `v1.6` perhaps? (#2203)
* fix Connex comment (#2204)
Connex allows both relations to hold, so the old comment was wrong.
* Add `Function.Consequences.Setoid` (#2191)
* Add Function.Consequences.Setoid
* Fix comment
* Fix re-export bug
* Finally fixed bug I hope
* Removed rogue comment
* More tidying up
* Deprecating `Relation.Binary.PropositionalEquality.isPropositional` (#2205)
* deprecating `isPropositional`
* tighten `import`s
* bumped Agda version number in comment
* definition of `Irreducible` and `Rough`; refactoring of `Prime` and `Composite` cf. #2180 (#2181)
* definition of `Irreducible`; refactoring of `Prime` and `Composite`
* tidying up old cruft
* knock-on consequences: `Coprimality`
* considerable refactoring of `Primality`
* knock-on consequences: `Coprimality`
* refactoring: no appeal to `Data.Nat.Induction`
* refactoring: renamed `SmoothAt` and its constructor; added pattern synonym; proved `Decidable Irreducible`; misc. tweaks
* knock-on consequences: `Coprimality`
* refactoring: removed `NonZero` analysis; misc. tweaks
* knock-on consequences: `Coprimality`; tightened `import`s
* knock-on consequences: `Coprimality`; tightened `import`s
* refactoring: every number is `1-rough`
* knock-on consequences: `Coprimality`; use of smart constructor
* refactoring: every number is `0-rough`; streamlining; inverse to `prime`; documentation
* attempt to optimise for a nearly-common case pseudo-constructor
* fiddling now
* refactoring: better use of `primality` API
* `Rough` is bounded
* removed unnecessary implicits
* comment
* refactoring: comprehensive shift over to `NonTrivial` instances
* refactoring: oops!
* tidying up: removed infixes
* tidying up: restored `rough⇒≤`
* further refinements; added `NonTrivial` proofs
* tidying up
* moving definitions to `Data.Nat.Base`
* propagated changes; many more explicit s required?
* `NonTrivial` is `Recomputable`
* all instances of `NonTrivial` now irrelevant; weird to need `NonTrivial 2` explicitly
* tidying up `Coprimality`, eg with `variable`s
* `NonTrivial` is `Decidable`
* systematise proofs of `Decidable` properties via the `UpTo` predicates
* explicit quantifier now in `composite≢`
* Nathan's simplification
* interaction of `NonZero` and `NonTrivial` instances
* divisor now a record field; final lemmas: closure under divisibility; plus partial `CHANGELOG` entries
* '(non-)instances' become '(counter-)examples'
* stylistics
* removed `k` as a variable/parameter
* renamed fields and smart constructors
* moved smart constructors; made a local definition
* tidying up
* refactoring per review comments: equivalence of `UpTo` predicates; making more things `private`
* tidying up: names congruent to ordering relation
* removed variable `k`; removed old proof in favour of new one with `NonZero` instance
* removed `recomputable` in favour of a private lemma
* regularised use of instance brackets
* made instances more explicit
* made instances more explicit
* blank line
* made `nonTrivial⇒nonZero` take an explicit argument in lieu of being able to make it an `instance`
* regularised use of instance brackets
* regularised use of instance brackets
* trimming
* tidied up `Coprimality` entries
* Make HasBoundedNonTrivialDivisor infix
* Make NonTrivial into a record to fix instance resolution bug
* Move HasNonTrivialDivisor to Divisibility.Core and hide UpTo lemmas
* Rearrange file to follow standard ordering of lemmas in the rest of the library
* Move UpTo predicates into decidability proofs
* No-op refactoring to curb excessively long lines
* Make a couple of names consistent with style-guide
* new definition of `Prime`
* renamed fundamental definition
* one last reference in `CHANGELOG`
* more better words; one fewer definition
* tidied up `Definitions` section; rejigged order of proofs of properties to reflect definitional order
* refactored proof of `prime⇒irreducible`
* finishing touches
* missing lemma from irrelevant instance list
* regularised final proof to use `contradiction`
* added fixity `infix 10`
* added fixity `infix 10`; made `composite` a pattern synonym; knock-on improvements
* comprehensive `CHNAGELOG` entry; whitespace fixes
* Rename 1<2+ to sz<ss
* Rename hasNonTrivialDivisor relation
* Updated CHANGELOG
---------
Co-authored-by: MatthewDaggitt <[email protected]>
* [fixes #2168] Change names in `Algebra.Consequences.*` to reflect `style-guide` conventions (#2206)
* fixes issue #2168
* added more names for deprecation, plus `hiding` them in `Propositional`
* Add biased versions of Function structures (#2210)
* Fixes #2166 by fixing names in `IsSemilattice` (#2211)
* Fix names in IsSemilattice
* Add reference to changes to Semilattice to CHANGELOG
* remove final references to `Category.*` (#2214)
* Fix #2195 by removing redundant zero from IsRing (#2209)
* Fix #2195 by removing redundant zero from IsRing
* Moved proofs eariler to IsSemiringWithoutOne
* Updated CHANGELOG
* Fix bug
* Refactored Properties.Ring
* Fix renaming
* Fix #2216 by making divisibility definitions records (#2217)
* Fix #2216 by making divisibility definitions records
* remove spurious/ambiguous `import`
---------
Co-authored-by: jamesmckinna <[email protected]>
* Fix deprecated modules (#2224)
* Fix deprecated modules
* [ ci ] Also build deprecated modules
* [ ci ] ignore user warnings in test
* [ ci ] fix filtering logic
Deprecation and safety are not the same thing
---------
Co-authored-by: Guillaume Allais <[email protected]>
* Final admin changes for v2.0 release (#2225)
* Final admin changes for v2.0 release
* Fix Agda versions
* Fix typo in raise deprecation message (#2226)
* Setup for v2.1 (#2227)
* Added tabulate+< (#2190)
* added tabulate+<
* renamed tabulate function
---------
Co-authored-by: Guilherme <[email protected]>
Co-authored-by: MatthewDaggitt <[email protected]>
* Added pointwise and catmaybe in Lists (#2222)
* added pointwise and catmaybe
* added pointwise to any
* added cat maybe all
* changed pointwise definition
* changed files name
* fixed changelogs and properties
* changed Any solution
* changed pointwise to catMaybe
---------
Co-authored-by: Guilherme <[email protected]>
Co-authored-by: MatthewDaggitt <[email protected]>
* [fixes #1711] Refactoring `Data.Nat.Divisibility` and `Data.Nat.DivMod` (#2182)
* added new definitions to `_∣_`
* `CHANGELOG`
* don't declare `quotient≢0` as an `instance`
* replace use of `subst` with one of `trans`
* what's sauce for the goose...
* switch to a `rewrite`-based solution...
* tightened `import`s
* simplified dependenciess
* simplified dependencies; `CHANGELOG`
* removed `module` abstractions
* delegated proof of `quotient≢0` to `Data.Nat.Properties`
* removed redundant property
* cosmetic review changes; others to follow
* better proof of `quotient>1`
* `where` clause layout
* leaving in the flipped equality; moved everything else
* new lemmas moved from `Core`; knock-on consequences; lots of tidying up
* tidying up; `CHANGELOG`
* cosmetic tweaks
* reverted to simple version
* problems with exporting `quotient`
* added last lemma: defining equation for `_/_`
* improved `CHANGELOG`
* revert: simplified imports
* improved `CHANGELOG`
* endpoint of simplifying the proof of `*-pres-∣`
* simplified the proof of `n/m≡quotient`
* simplified the proof of `∣m+n∣m⇒∣n`
* simplified the proof of `∣m∸n∣n⇒∣m`
* simplified `import`s
* simplified a lot of proofs, esp. wrt `divides-refl` and `NonZero` reasoning
* simplified more proofs, esp. wrt `divides-refl` reasoning
* simplified `import`s
* moved `equalityᵒ` proof out of `Core`
* `CHANGELOG`
* temporary fix: further `NonZero` refactoring advised!
* regularised use of instance brackets
* further instance simplification
* further streamlining
* tidied up `CHANGELOG`
* simplified `NonZero` pattern matching
* regularised use of instance brackets
* simplified proof of `/-*-interchange`
* simplified proof of `/-*-interchange`
* ... permitting the migration of `*-pres-∣` to `Data.Nat.Divisibility`
* tweaked proof of `/-*-interchange`
* narrowed `import`s
* simplified proof; renamed new proofs
* Capitalisation
* streamlined `import`s; streamlined proof of decidability
* spurious duplication after merge
* missing symbol import
* replaced one use of `1 < m` with `{{NonTrivial m}}`
* fixed `CHANGELOG`
* removed use of identifier `k`
* refactoring: more use of `NonTrivial` instances
* knock-on consequences: simplified function
* two new lemmas
* refactoring: use of `connex` in proofs
* new lemmas about `pred`
* new lemmas about monus
* refactoring: use of the new properties, simplifying pattern analysis
* whitespace
* questionable? revision after comments on #2221
* silly argument name typo; remove parens
* tidied up imports of `Relation.Nullary`
* removed spurious `instance`
* localised appeals to `Reasoning`
* further use of `variable`s
* tidied up `record` name in comment
* cosmetic
* reconciled implicit/explicit arguments in various monus lemmas
* fixed knock-on change re monus; reverted change to `m/n<m`
* reverted change to `m/n≢0⇒n≤m`
* reverted breaking changes involving `NonZero` inference
* revised `CHANGELOG`
* restored deleted proof
* fix whitespace
* renaming: `DivMod.nonZeroDivisor`
* localised use of `≤-Reasoning`
* reverted export; removed anonymous module
* revert commit re `yes/no`
* renamed flipped equality
* tweaked comment
* added alias for `equality`
* [fixes #2232] (#2233)
* fixes #2232
* corrected major version number
* Add `map` to `Data.String.Base` (#2208)
* add map to Data.String
* Add test for Data.String map
* CHANGELOG.md add map to list of new functions in Data.String.Base
* precise import of Data.String to avoid conflict on map
* Fix import statements
---------
Co-authored-by: lemastero <[email protected]>
Co-authored-by: MatthewDaggitt <[email protected]>
* fixes issue #2237 (#2238)
* fixes issue #2237
* leftover from #2182: subtle naming 'bug'/anomaly
* Bring back a convenient short-cut for infix Func (#2239)
* Bring back a convenient short-cut for infix Func
* change name as per suggestion from Matthew
* propagate use of shortcut to where it increases readability
* Revert "propagate use of shortcut to where it increases readability"
This reverts commit debfec19a0b6ad93cadce4e88f559790b287a316.
* Move definitions up. Fix comments.
* fixes #2234 (#2241)
* Update `HACKING` (#2242)
* added paragraph on coupled contributions
* typo
* Bring back shortcut [fix CHANGELOG] (#2246)
* Bring back a convenient short-cut for infix Func
* change name as per suggestion from Matthew
* propagate use of shortcut to where it increases readability
* Revert "propagate use of shortcut to where it increases readability"
This reverts commit debfec19a0b6ad93cadce4e88f559790b287a316.
* Move definitions up. Fix comments.
* fix CHANGELOG to report the correct syntax.
* fix toList-replicate's statement about vectors (#2261)
* Remove all external use of `less-than-or-equal` beyond `Data.Nat.*` (#2256)
* removed all external use of `less-than-or-equal` beyond `Data.Nat.*`
* use of `variable`s
* Raw modules bundles (#2263)
* Raw bundles for modules
* Export raw bundles from module bundles
* Update chnagelog
* Remove redundant field
* Reexport raw bundles, add raw bundles for zero
* Add missing reexports, raw bundles for direct product
* Raw bundles for tensor unit
* Update changelog again
* Remove unused open
* Fix typo
* Put a few more definitions in the fake record modules for RawModule and RawSemimodule
* Parametrize module morphisms by raw bundles (#2265)
* Index module morphisms by raw bundles
* Use synonyms for RawModule's RawBimodule etc
* Update changelog
* Update constructed morphisms
* Fix Algebra.Module.Morphism.ModuleHomomorphism
* add lemma (#2271)
* additions to `style-guide` (#2270)
* added stub content on programming idioms
* added para on qualified import names
* fixes issue #1688 (#2254)
* Systematise relational definitions at all arities (#2259)
* fixes #2091
* revised along the lines of @MatthewDaggitt's suggestions
---------
Co-authored-by: MatthewDaggitt <[email protected]>
* lemmas about semiring structure induced by `_× x` (#2272)
* tidying up proofs of, and using, semiring structure induced by `_× x`
* reinstated lemma about `0#`
* fixed name clash
* added companion lemma for `1#`
* new lemma, plus refactoring
* removed anonymous `module`
* don't inline use of the lemma
* revised deprecation warning
* Qualified import of `Data.Nat` fixing #2280 (#2281)
* `Algebra.Properties.Semiring.Binomial`
* `Codata.Sized.Cowriter`
* `Data.Char.Properties`
* `Data.Difference*`
* `Data.Fin.*`
* `Data.Float.Properties`
* `Data.Graph.Acyclic`
* `Data.Integer.Divisibility`: still need to disambiguate `Divisibility`?
* `Data.List.Extrema.Nat`
* `Data.List.Relation.Binary.*`
* `Data.Nat.Binary.*`
* `Data.Rational.Base`
* `Data.String`
* `Data.Vec.*`
* `Data.Word`
* `Induction.Lexicographic`
* `Reflection.AST`
* `Tactic.*`
* `Text.*`
* Fix import in README.Data.Fin.Substitution.UntypedLambda (#2279)
Also import this module in doc/README.agda so that it is covered by CI.
Closes #2278.
* Qualified import of reasoning modules fixing #2280 (#2282)
* `Data.List.Relation.Relation.Binary.BagAndSetEquality`
* `Relation.Binary.Reasoning.*`
* preorder reasoning
* setoid reasoning
* alignment
* Qualified import of `Data.Product.Base` fixing #2280 (#2284)
* Qualified import of `Data.Product.Base as Product`
* more modules affected
* standardise use of `Properties` modules (#2283)
* missing code endquote (#2286)
* manual fix for #1380 (#2285)
* fixed `sized-types` error in orphan module (#2295)
* Qualified import of `PropositionalEquality` etc. fixing #2280 (#2293)
* Qualified import of `PropositionalEquality` fixing #2280
* Qualified import of `PropositionalEquality.Core` fixing #2280
* Qualified import of `HeterogeneousEquality.Core` fixing #2280
* simplified imports; fixed `README` link
* simplified imports
* Added functional vector permutation (#2066)
* added functional vector permutation
* added one line to CHANGELOG
* added permutation properties
* Added Base to imports
Co-authored-by: Nathan van Doorn <[email protected]>
* Added Base to import
Co-authored-by: Nathan van Doorn <[email protected]>
* Added core to import
Co-authored-by: Nathan van Doorn <[email protected]>
* added definitions
* removed unnecessary zs
* renamed types in changelog
* removed unnecessary code
* added more to changelog
* added end of changelog
---------
Co-authored-by: Nathan van Doorn <[email protected]>
Co-authored-by: Guilherme <[email protected]>
* Nagata's "idealization of a module" construction (#2244)
* Nagata's construction
* removed redundant `zero`
* first round of Jacques' review comments
* proved the additional properties
* some of Matthew's suggestions, plus more vertical whitespace, less horizontal; more comments
* Matthew's suggestion: using `private` modules
* Matthew's suggestion: lifting out left-/right- sublemmas
* standardised names, as far as possible
* Matthew's suggestion: lifting out left-/right- sublemmas
* fixed constraint problem with ambiguous symbol; renamed ideal lemmas
* renamed module
* renamed module in `CHANGELOG`
* added generalised annihilation lemma
* typos
* use correct rexported names
* now as a paramterised module instead
* or did you intend this?
* fix whitespace
* aligned one step of reasoning
* more re-alignment of reasoning steps
* more re-alignment of reasoning steps
* Matthew's review comments
* blanklines
* Qualified import of `Data.Sum.Base` fixing #2280 (#2290)
* Qualified import of `Data.Sum.Base as Sum`
* resolve merge conflict in favour of #2293
* [ new ] associativity of Appending (#2023)
* [ new ] associativity of Appending
* Removed unneeded variable
* Renamed Product module
---------
Co-authored-by: MatthewDaggitt <[email protected]>
* [ new ] symmetric core of a binary relation (#2071)
* [ new ] symmetric core of a binary relation
* [ fix ] name clashes
* [ more ] respond to McKinna's comments
* [ rename ] fields to lhs≤rhs and rhs≤lhs
* [ more ] incorporate parts of McKinna's review
* [ minor ] remove implicit argument application from transitive
* [ edit ] pull out isEquivalence and do some renaming
* [ minor ] respond to easy comments
* [ refactor ] remove IsProset, and move Proset to main hierarchy
* Eliminate Proset
* Fixed CHANGELOG typo
---------
Co-authored-by: MatthewDaggitt <[email protected]>
* refactored proofs from #2023 (#2301)
* Qualified imports in `Data.Integer.Divisibility` fixing #2280 (#2294)
* fixing #2280
* re-export constructor via pattern synonym
* updated `README`
* refactor: better disambiguation; added a note in `CHANGELOG`
* guideline for `-Reasoning` module imports (#2309)
* Function setoid is back. (#2240)
* Function setoid is back.
* make all changes asked for in review
* fix indentation
* Style guide: avoid `renaming` on qualified import cf. #2294 (#2308)
* recommendation from #2294
* spellcheck
* comma
---------
Co-authored-by: MatthewDaggitt <[email protected]>
* make `mkRawMonad` and `mkRawApplicative` universe-polymorphic (#2314)
* make `mkRawMonad` and `mkRawApplicative` universe-polymorphic
* fix unresolved metas
---------
Co-authored-by: Gan Shen <[email protected]>
* Some properties of upTo and downFrom (#2316)
* Some properties of upTo and downFrom
* Rename things per review comments
* Fix changelog typo
* Tidy up `README` imports #2280 (#2313)
* tidying up `README` imports
* address Matthew's review comments
* Add unique morphisms from/to `Initial` and `Terminal` algebras (#2296)
* added unique morphisms
* refactored for uniformity's sake
* exploit the uniformity
* add missing instances
* finish up, for now
* `CHANGELOG`
* `CHANGELOG`
* `TheMorphism`
* comment
* comment
* comment
* `The` to `Unique`
* lifted out istantiated `import`
* blank line
* note on instantiated `import`s
* parametrise on the `Raw` bundle
* parametrise on the `Raw` bundle
* Rerranged to get rid of lots of boilerplate
---------
Co-authored-by: MatthewDaggitt <[email protected]>
* Setoid version of indexed containers. (#1511)
* Setoid version of indexed containers.
Following the structure for non-indexed containers.
* An example for indexed containers: multi-sorted algebras.
This tests the new setoid version of indexed containers.
* Brought code up to date
* Added CHANGELOG entry
---------
Co-authored-by: MatthewDaggitt <[email protected]>
* 'No infinite descent' for (`Acc`essible elements of) `WellFounded` relations (#2126)
* basic result
* added missing lemma; is there a better name for this?
* renamed lemma
* final tidying up; `CHANGELOG`
* final tidying up
* missing `CHANGELOG` entry
* `InfiniteDescent` definition and proof
* revised `InfiniteDescent` definition and proof
* major revision: renames things, plus additional corollaries
* spacing
* added `NoSmallestCounterExample` principles for `Stable` predicates
* refactoring; move `Stable` to `Relation.Unary`
* refactoring; remove explicit definition of `CounterExample`
* refactoring; rename qualified `import`
* [fixes #2130] Moving `Properties.HeytingAlgebra` from `Relation.Binary` to `Relation.Binary.Lattice` (#2131)
* [fixes #2127] Fixes #1930 `import` bug (#2128)
* [fixes #1214] Add negated ordering relation symbols systematically to `Relation.Binary.*` (#2095)
* Refactoring (inversion) properties of `_<_` on `Nat`, plus consequences (#2000)
* Bump CI tests to Agda-2.6.4 (#2134)
* Remove `Algebra.Ordered` (#2133)
* [ fix ] missing name in LICENCE file (#2139)
* Add new blocking primitives to `Reflection.TCM` (#1972)
* Change definition of `IsStrictTotalOrder` (#2137)
* Add _<$>_ operator for Function bundle (#2144)
* [ fix #2086 ] new web deployment strategy (#2147)
* [ admin ] fix sorting logic (#2151)
With the previous script we were sorting entries of the form
html/vX.Y.Z/index.html but the order is such that vX.Y/ < vX.Y.Z/
and so we were ending up with v1.7 coming after v1.7.3.
This fixes that by using sed to get rid of the html/ prefix
and the /index.html suffix before the sorting phase.
* Add coincidence law to modules (#1898)
* Make reasoning modular by adding new `Reasoning.Syntax` module (#2152)
* Fixes typos identified in #2154 (#2158)
* tackles #2124 as regards `case_return_of_` (#2157)
* Rename preorder ~ relation reasoning combinators (#2156)
* Move ≡-Reasoning from Core to Properties and implement using syntax (#2159)
* Add consistent deprecation warnings to old function hierarchy (#2163)
* Rename symmetric reasoning combinators. Minimal set of changes (#2160)
* Restore 'return' as an alias for 'pure' (#2164)
* [ fix #2153 ] Properly re-export specialised combinators (#2161)
* Connect `LeftInverse` with (`Split`)`Surjection` (#2054)
* Added remaining flipped and negated relations to binary relation bundles (#2162)
* Tidy up CHANGELOG in preparation for release candidate (#2165)
* Spellcheck CHANGELOG (#2167)
* spellcheck; `fix-whitespace`; unfixed: a few alignment issues; typo `predications` to `predicates` in `Relation.Unary.Relation.Binary.Equality`
* Fixed Agda version typo in README (#2176)
* Fixed in deprecation warning for `<-transˡ` (#2173)
* Bump Haskell CI (original!) to latest minor GHC versions (#2187)
* [fixes #2175] Documentation misc. typos etc. for RC1 (#2183)
* missing comma!
* corrected reference to `README.Design.Decidability`
* typo: capitalisation
* updated `installation-guide`
* added word to `NonZero` section heading
* Run workflows on any PR
* Add merge-group trigger to workflows
---------
Co-authored-by: MatthewDaggitt <[email protected]>
* [fixes #2178] regularise and specify/systematise, the conventions for symbol usage (#2185)
* regularise and specify/systematise, the conventions for symbol usage
* typos/revisions
* Move `T?` to `Relation.Nullary.Decidable.Core` (#2189)
* Move `T?` to `Relation.Nullary.Decidable.Core`
* Var name fix
* Some refactoring
* Fix failing tests and address remaining comments
* Fix style-guide
* Make decidable versions of sublist functions the default (#2186)
* Make decdable versions of sublist functions the default
* Remove imports Bool.Properties
* Address comments
* new `CHANGELOG`
* resolved merge conflict
* resolved merge conflict, this time
* revised in line with review comments
* tweaked `export`s; does that fix things now?
* Fix merge mistake
* Refactored to remove a indirection and nested modules
* Touch up names
* Reintroduce anonymous module for descent
* cosmetics asper final comment
---------
Co-authored-by: MatthewDaggitt <[email protected]>
Co-authored-by: G. Allais <[email protected]>
Co-authored-by: Amélia <[email protected]>
Co-authored-by: Nathan van Doorn <[email protected]>
Co-authored-by: James Wood <[email protected]>
Co-authored-by: Andreas Abel <[email protected]>
* Add new operations (cf. `RawQuasigroup`) to `IsGroup` (#2251)
* added new operations to `IsGroup`
* fixed notations
* fixed `CHANGELOG`
* refactoring `Group` properties: added `isQuasigroup` and `isLoop`
* refactoring `*-helper` lemmas
* fixed `CHANGELOG`
* lemma relating quasigroup operations and `Commutative` property
* simplified proof
* added converse property to \¬Algebra.Properties.AbelianGroup`
* moved lemma
* indentation; congruence lemmas
* untangled operation definitions
* untangled operation definitions in `CHANGELOG`
* fixed names
* reflexive reasoning; tightened imports
* refactoring to push properties into `Loop`, and re-export them from there and `Quasigroup`
* further refactoring
* final refactoring
* Minor naming tweaks
---------
Co-authored-by: MatthewDaggitt <[email protected]>
* Add prime factorization and its properties (#1969)
* Add prime factorization and its properties
* Add missing header comment
I'd missed this when copy-pasting from my old code in a separate repo
* Remove completely trivial lemma
* Use equational reasoning in quotient|n proof
* Fix typo in module header
* Factorization => Factorisation
* Use Nat lemma in extend-|/
* [ cleanup ] part of the proof
* [ cleanup ] finishing up the job
* [ cleanup ] a little bit more
* [ cleanup ] the import list
* [ fix ] header style
* [ fix ] broken merge: missing import
* Move Data.Nat.Rough to Data.Nat.Primality.Rough
* Rename productPreserves↭⇒≡ to product-↭
* Use proof of Prime=>NonZero
* Open reasoning once in factoriseRec
* Rename Factorisation => PrimeFactorisation
* Move wheres around
* Tidy up Rough a bit
* Move quotient|n to top of file
* Replace factorisationPullToFront with slightly more generally useful factorisationHasAllPrimeFactors and a bit of logic
* Fix import after merge
* Clean up proof of 2-rough-n
* Make argument to 2-rough-n implicit
* Rename 2-rough-n to 2-rough
* Complete merge, rewrite factorisation logic a bit
Rewrite partially based on suggestions from James McKinna
* Short circuit when candidate is greater than square root of product
* Remove redefined lemma
* Minor simplifications
* Remove private pattern synonyms
* Change name of lemma
* Typo
* Remove using list from import
It feels like we're importing half the module anyway
* Clean up proof
* Fixes after merge
* Addressed some feedback
* Fix previous merge
---------
Co-authored-by: Guillaume Allais <[email protected]>
Co-authored-by: MatthewDaggitt <[email protected]>
* Refactor `Data.List.Relation.Binary.BagAndSetEquality` (#2321)
* easy refactorings for better abstraction
* tweaking irrefutable `with`
* Tidy up functional vector permutation #2066 (#2312)
* added structure and bundle; tidied up
* added structure and bundle; tidied up
* fix order of entries
* blank line
* standardise `variable` names
* alignment
* A tweak for the cong! tactic (#2310)
* ⌞_⌟ for marking spots to rewrite.
* Added documentation.
* In case of failure, try swapping the RHS with the LHS. Fixes ≡˘⟨ ... ⟩.
* Added comments.
* More clarity. Less redundancy.
* Fixed performance regression.
* Changelog entry.
* cong!-specific combinators instead of catchTC.
* Support other reasoning modules.
* Clarifying comment.
* Slight performance boost.
* Go back to catchTC.
* Fix example after merge.
* Use renamed backward step.
* Language tweaks.
---------
Co-authored-by: MatthewDaggitt <[email protected]>
* Simplify `Data.List.Relation.Unary.Any.Properties`: remove dependency on `List.Properties` (#2323)
* simplifed proof; removed dependency on `List.Properties`
* corrected module long name in comment
* Refactor `Data.Integer.Divisibility.Signed` (#2307)
* removed extra space
* refactor to introduce new `Data.Integer.Properties`
* refactor proofs to use new properties; streamline reasoning
* remove final blank line
* first review comment: missing annotation
* removed two new lemmas: `i*j≢0⇒i≢0` and `i*j≢0⇒j≢0`
* Sublists: generalize disjoint-union-is-cospan to upper-bound-is-cospan (#2320)
* Sublists: generalize disjoint-union-is-cospan to upper-bound-is-cospan
The disjointness assumption is superfluous.
* Move sublist cospan stuff to new module SubList.Propositional.Slice
* CHANGELOG
* Include CHANGELOG in fix-whitespace and whitespace fixes (#2325)
* Fix standard-library.agda-lib (#2326)
* Predicate transformers: Reconciling `Induction.RecStruct` with `Relation.Unary.PredicateTransformer.PT` (#2140)
* reconciling `Induction.RecStruct` with `Relation.Unary.PredicateTransformer.PT`
* relaxing `PredicateTransformer` levels
* `CHANGELOG`; `fix-whitespace`
* added `variable`s; plus tweaked comments`
* restored `FreeMonad`
* restored `Predicate`
* removed linebreaks
* Github action to check for whitespace violations (#2328)
Co-authored-by: MatthewDaggitt <[email protected]>
* [refactor] Relation.Nulllary.Decidable.Core (#2329)
* minor refactor: use Data.Unit.Polymorphic instead of an explicit Lift.
* additional tweak: use contradiction where possible.
* Some design documentation (here: level polymorphism) (#2322)
* add some design documentation corresponding to issue #312. (Redo of bad 957)
* more documentation about LevelPolymorphism
* more documentation precision
* document issues wrt Relation.Unary, both in design doc and in file itself.
* mark variables private in Data.Container.FreeMonad (#2332)
* Move pointwise equality to `.Core` module (#2335)
* Closes #2331.
Also makes a few changes of imports that are related. Many of the places
which look like this improvement might also help use other things from
`Relation.Binary.PropositionalEquality` that should *not* be moved to `.Core`.
(But it might make sense to split them off into their own lighter weight module.)
* don't import Data.Nullary itself since its sub-modules were already imported, just redistribute the using properly.
* fix warning: it was pointing to a record that did not exist. (#2344)
* Tighten imports some more (#2343)
* no need to use Function when only import is from Function.Base
* Use Function.Base when it suffices
* use Data.Product.Base as much as possible. Make imports more precise in many of the files touched. Split an example off into a README instead of using more imports just for its sake.
* more tightening of imports.
* a few more tightening imports
* Tighten imports (#2334)
* tighten imports in some files, and make imports explicit in others. Driven by staring at a partial dependency graph.
* more tightening of imports
* and even more tightening of imports
* some explicit for precision
---------
Co-authored-by: G. Allais <[email protected]>
* [fixes #2273] Add `SuccessorSet` and associated boilerplate (#2277)
* added `RawNNO`
* [fix #2273] Add `NNO`-related modules
* start again, fail better...
* rectify names
* tighten `import`s
* rectify names: `CHANGELOG`
---------
Co-authored-by: MatthewDaggitt <[email protected]>
* Tighten imports, last big versoin (#2347)
* more tightening of imports. Mostly driven by Data.Bool, Data.Nat and Data.Char.
* more tightening of imports
* mostly Data.Unit
* slightly tighten imports.
* remove import of unused Lift)
* fix all 3 things noticed by @jamesmckinna
* Systematise use of `Relation.Binary.Definitions.DecidableEquality` (#2354)
* systematic use of `DecidableEquality`
* tweak
* Added missing v1.7.3 CHANGELOG (#2356)
* Improve `Data.List.Base.mapMaybe` (#2359; deprecate use of `with` #2123) (#2361)
* `with`-free definitions plus tests
* `CHANGELOG`
* use `foldr` on @JacquesCarette 's solution
* tidied up unsolved metas
* factrored out comparison as removable module `MapMaybeTest`
* tidied up; removed `mapMaybeTest`
* tidied up; removed v2.1 deprecation section
* tidy up long line
* Update src/Data/List/Base.agda
Co-authored-by: G. Allais <[email protected]>
* @gallais 's comments
* Update src/Data/List/Base.agda
Oops!
Co-authored-by: G. Allais <[email protected]>
---------
Co-authored-by: G. Allais <[email protected]>
* Add a consequence of definition straight to IsCancellativeCommutativeSemiring (#2370)
* Closes #2315
* whitespace
* [ new ] System.Random bindings (#2368)
* [ new ] System.Random bindings
* [ more ] Show functions, test
* [ fix ] Nat bug, more random generators, test case
* [ fix ] missing file + local gitignore
* [ fix ] forgot to update the CHANGELOG
* Another tweak to cong! (#2340)
* Disallow meta variables in goals - they break anti-unification.
* Postpone checking for metas.
* CHANGELOG entry, unit tests, code tweak.
* Move blockOnMetas to a new Reflection.TCM.Utilities module.
* Improve `Data.List.Base.unfold` (#2359; deprecate use of `with` #2123) (#2364)
* `with`-free definition of `unfold`
* fixed previous commit
* fix #2253 (#2357)
* Remove uses of `Data.Nat.Solver` from a number of places (#2337)
* tighten imports in some files, and make imports explicit in others. Driven by staring at a partial dependency graph.
* more tightening of imports
* and even more tightening of imports
* some explicit for precision
* new Nat Lemmas to use instead of Solve in Data.Integer.Properties
* use direct proofs instead of solver for all Nat proofs in these files
* two more uses of Data.Nat.Solver for rather simple proofs, now made direct.
* fix whitespace violations
* remove some unneeded parens
* minor fixups based on review
* Relation.Binary.PropositionalEquality over-use, (#2345)
* Relation.Binary.PropositionalEquality over-use, can usually be .Core and/or .Properties
* unused import
* another large batch of dependency cleanup, mostly cenetered on Relation.Binary.PropositionalEquality.
* another big batch of making imports more precise.
* last big batch. After this will come some tweaks based on reviews.
* fix things pointed out in review; add CHANGELOG.
* Update DecPropositional.agda
Bad merge
* proper merge
* [ new ] IO buffering, and loops (#2367)
* [ new ] IO conditionals & loops
* [ new ] stdin, stdout, stderr, buffering, etc.
* [ fix ] and test for the new IO primitives
* [ fix ] compilation
* [ fix ] more import fixing
* [ done (?) ] with compilation fixes
* [ test ] add test to runner
* [ doc ] explain the loop
* [ compat ] add deprecated stub
* [ fix ] my silly mistake
* [ doc ] list re-exports in CHANGELOG
* [ cleanup ] imports in the Effect.Monad modules (#2371)
* Add proofs to Data.List.Properties (#2355)
* Add map commutation with other operations
map commutes with most list operations in some way,
and I initially made a section just for these proofs,
but later decided to spread them into each section
for consistency.
* Add congruence to operations that miss it
* Add flip & comm proofs to align[With] & [un]zip[With]
For the case of zipWith, the existing comm proof
can be provided in terms of cong and flip.
For the case of unzip[With], the comm proof has
little use and the flip proof is better named "swap".
* Remove unbound parameter
The alignWith section begins with a
module _ {f g : These A B → C} where
but g is only used by the first function.
* Add properties for take
* Proof of zip[With] and unzip[With] being inverses
* fixup! don't put list parameters in modules
* fixup! typo in changelog entry
* fixup! use equational reasoning in place of trans
* Add interaction with ++ in two more operations
* fixup! foldl-cong: don't take d ≡ e
* prove properties about catMaybes
now that catMaybes is no longer defined in
terms of mapMaybe, properties about mapMaybe
need to be proven for catMaybe as well
* move mapMaybe properties down
see next commit (given that mapMaybe-concatMap
now depends on map-concatMap, it has to be
moved down)
* simplify mapMaybe proofs
since mapMaybe is now defined in terms
of catMaybes and map, we can derive its
proofs from the proofs of those rather
than using induction directly
---------
Co-authored-by: MatthewDaggitt <[email protected]>
* Improve `Data.List.Base` (fix #2359; deprecate use of `with` #2123) (#2365)
* refactor towards `if_then_else_` and away from `yes`/`no`
* reverted chnages to `derun` proofs
* undo last reversion!
* layout
* A number of `with` are not really needed (#2363)
* a number of 'with' are not really needed. Many, many more were, so left as is.
* whitespace
* deal with a few outstanding comments.
* actually re-introduce a 'with' as it is actually clearer.
* with fits better here too.
* tweak things a little from review by James.
* Update src/Codata/Sized/Cowriter.agda
layout for readability
Co-authored-by: G. Allais <[email protected]>
* Update src/Data/Fin/Base.agda
layout for readability
Co-authored-by: G. Allais <[email protected]>
* Update src/Data/List/Fresh/Relation/Unary/All.agda
layout for readability
Co-authored-by: G. Allais <[email protected]>
---------
Co-authored-by: G. Allais <[email protected]>
* [ new ] ⁻¹-anti-homo-(// | \\) (#2349)
* [ new ] ¹-anti-homo‿-
* Update CHANGELOG.md
Co-authored-by: Nathan van Doorn <[email protected]>
* Update src/Algebra/Properties/Group.agda
Co-authored-by: jamesmckinna <[email protected]>
* Update CHANGELOG.md
Co-authored-by: jamesmckinna <[email protected]>
* [ more ] symmetric lemma
* [ new ] ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x
---------
Co-authored-by: MatthewDaggitt <[email protected]>
Co-authored-by: Nathan van Doorn <[email protected]>
Co-authored-by: jamesmckinna <[email protected]>
* Add `_>>_` for `IO.Primitive.Core` (#2374)
This has to be in scope for desugaring `do` blocks that don't bind
intermediate results.
* refactored to lift out `isEquivalence` (#2382)
* `Data.List.Base.reverse` is self adjoint wrt `Data.List.Relation.Binary.Subset.Setoid._⊆_` (#2378)
* `reverse` is `SelfInverse`
* use `Injective` for `reverse-injective`
* fixes #2353
* combinatory form
* removed redundant implicits
* added comment on unit/counit of the adjunction
* fixes #2375 (#2377)
* fixes #2375
* removed redundant `Membership` instances
* fix merge conflict error
* Add `Data.List.Relation.Binary.Sublist.Setoid` categorical properties (#2385)
* refactor: `variable` declarations and `contradiction`
* refactor: one more `contradiction`
* left- and right-unit lemmas
* left- and right-unit lemmas
* `CHANGELOG`
* `CHANGELOG`
* associativity; fixes #816
* Use cong2 to save rewrites
* Make splits for ⊆-assoc exact, simplifying the [] case
* Simplify ⊆-assoc not using rewrite
* Remove now unused private helper
* fix up names and `assoc` orientation; misc. cleanup
* new proofs can now move upwards
* delegate proofs to `Setoid.Properties`
---------
Co-authored-by: Andreas Abel <[email protected]>
* Pointwise `Algebra` (#2381)
* Pointwise `Algebra`
* temporary commit
* better `CHANGELOG` entry?
* begin removing redundant `module` implementation
* finish removing redundant `module` implementation
* make `liftRel` implicitly quantified
* Algebra fixity (#2386)
* put the fixity recommendations into the style guide
* mixing fixity declaration
* was missing a case
* use the new case
* add fixities for everything in Algebra
* incorporate some suggestions for extra cases
* Decidable Setoid -> Apartness Relation and Rational Heyting Field (#2194)
* new stuff
* forgot to add bundles for rational instance of Heyting*
* one more (obvious) simplification
* a few more simplifications
* comments on DecSetoid properties from jamesmckinna
* not working, but partially there
* woo!
* fix anonymous instance
* fix errant whitespace
* `fix-whitespace`
* rectified wrt `contradiction`
* rectified `DecSetoid` properties
* rectified `Group` properties
* inlined lemma; tidied up
---------
Co-authored-by: jamesmckinna <[email protected]>
Co-authored-by: James McKinna <[email protected]>
* CI bumps: ghc 9.10, action versions, Agda to 2.6.4.3 (#2398)
* Haskell CI (for GenerateEverything) and dependencies bumped to GHC 9.10.1
* CI: bump some versions, satisfy some shellcheck complaints
* Refactor `Data.List.Base.scan*` and their properties (#2395)
* refactor `scanr` etc.
* restore `inits` etc. but lazier; plus knock-on consequences
* more refactoring; plus knock-on consequences
* tidy up
* refactored into `Base`
* ... and `Properties`
* fix-up `inits` and `tails`
* fix up `import`s
* knock-ons
* Andreas's suggestions
* further, better, refactoring is possible
* yet further, better, refactoring is possible: remove explicit equational reasoning!
* Update CHANGELOG.md
Fix deprecated names
* Update Base.agda
Fix deprecations
* Update Properties.agda
Fix deprecations
* Update CHANGELOG.md
Fix deprecated names
* fixes #2390 (#2392)
* Add the `Setoid`-based `Monoid` on `(List, [], _++_)` (#2393)
* refactored from #2350
* enriched the `module` contents in response to review comments
* Lists: decidability of Subset+Disjoint relations (#2399)
* fixes #906 (#2401)
* More list properties about `catMaybes/mapMaybe` (#2389)
* More list properties about `catMaybes/mapMaybe`
- Follow-up to PR #2361
- Ported from my [formal-prelude](https://github.com/omelkonian/formal-prelude/tree/c10fe94876a7378088f2e4cf68d9b18858dcc256)
* Revert irrefutable `with`s for inductive hypotheses.
* Very dependent map (#2373)
* add some 'very dependent' maps to Data.Product. More documentation to come later.
* and document
* make imports more precise
* minimal properties of very-dependen map and zipWith. Structured to make it easy to add more.
* whitespace
* implement new names and suggestions about using pattern-matching in the type
* whitespace in CHANGELOG
* small cleanup based on latest round of comments
* and fix the names in the comments too.
---------
Co-authored-by: jamesmckinna <[email protected]>
* Improve `Data.List.Base` (fix #2359; deprecate use of with #2123) (#2366)
* refactor towards `if_then_else_`
* layout
* `let` into `where`
* Adds `Relation.Nullary.Recomputable` plus consequences (#2243)
* prototype for fixing #2199
* delegate to `Relation.Nullary.Negation.Core.weak-contradiction`
* refactoring: lift out `Recomputable` in its own right
* forgot to add this module
* refactoring: tweak
* tidying up; added `CHANGELOG`
* more tidying up
* streamlined `import`s
* removed `Recomputable` from `Relation.Nullary`
* fixed multiple definitions in `Relation.Unary`
* reorder `CHANGELOG` entries after merge
* `contradiciton` via `weak-contradiction`
* irrefutable `with`
* use `of`
* only use *irrelevant* `⊥-elim-irr`
* tightened `import`s
* removed `irr-contradiction`
* inspired by #2329
* conjecture: all uses of `contradiction` can be made weak
* second thoughts: reverted last round of chnages
* lazier pattern analysis cf. #2055
* dependencies: uncoupled from `Recomputable`
* moved `⊥` and `¬ A` properties to this one place
* removed `contradictionᵒ` and rephrased everything in terms of `weak-contradiction`
* knock-on consequences; simplified `import`s
* narrow `import`s
* narrow `import`s; irrefutable `with`
* narrow `import`s; `CHANGELOG`
* narrow `import`s
* response to review comments
* irrelevance of `recompute`
* knock-on, plus proof of `UIP` from #2149
* knock-ons from renaming
* knock-on from renaming
* pushed proof `recompute-constant` to `Recomputable`
* Refactor `List.Membership.*` and `List.Relation.Unary.Any` (#2324)
* `contradiction` against `⊥-elim`
* tightened `import`s
* added two operations `∃∈` and `∀∈`
* added to `CHANGELOG`
* knock-on for the `Propositional` case
* refactor `lose∘find` and `find∘lose` in terms of new lemmas `∃∈-Any∘find` and `find∘∃∈-Any`
* `CHANGELOG`
* reorder
* knock-on viscosity
* knock-on viscosity; plus refactoring of `×↔` for intelligibility
* knock-on viscosity
* tightened `import`s
* misc. import and other tweaks
* misc. import and other tweaks
* misc. import and other tweaks
* removed spurious module name
* better definition of `find`
* make intermediate terms explicit in proof of `to∘from`
* tweaks
* Update Setoid.agda
Remove redundant import of `index` from `Any`
* Update Setoid.agda
Removed more redundant `import`ed operations
* Update Properties.agda
Another redundant `import`
* Update Properties.agda
Another redundant `import`ed operation
* `with` into `let`
* `with` into `let`
* `with` into `let`
* `with` into `let`
* indentation
* fix `universal-U`
* added `map-cong`
* deprecate `map-compose` in favour of `map-∘`
* explicit `let` in statement of `find∘map`
* knock-on viscosity: hide `map-cong`
* use of `Product.map₁`
* revert use of `Product.map₁`
* inlined lemmas!
* alpha conversion and further inlining!
* correctted use of `Product.map₂`
* added `syntax` declarations for the new combinators
* remove`⊥-elim`
* reordered `CHANGELOG`
* revise combinator names
* tighten `import`s
* tighten `import`s
* fixed merge conflict bug
* removed new syntax
* knock-on
* Port two Endomorphism submodules over to new Function hierarchy (#2342)
* port over two modules
* and add to CHANGELOG
* fix whitespace
* fix warning: it was pointing to a record that did not exist.
* fix things as per Matthew's review - though this remains a breaking change.
* take care of comments from James.
* adjust CHANGELOG for what will be implemented shortly
* Revert "take care of comments from James."
This reverts commit 93e9e0fdf482164c0fb7e709ef8799fbc3fa0385.
* Revert "fix things as per Matthew's review - though this remains a breaking change."
This reverts commit d1cae72dcb3b44d4ba3c7290f3535544be32ab1e.
* Revert "fix whitespace"
This reverts commit 81230ecf0c8ff634433c9d17d53c9d2e8b3c1fd2.
* Revert "port over two modules"
This reverts commit 6619f114346e86ead3cf62b1170ab23d31056b48.
* rename these
* fix tiny merge issue
* get deprecations right (remove where not needed, make more global where needed)
* style guide - missing blank lines
* fix a bad merge
* fixed deprecations
* fix #2394
* minor tweaks
---------
Co-authored-by: James McKinna <[email protected]>
* Add `IsIdempotentMonoid` and `IsCommutativeBand` to `Algebra.Structures` (#2402)
* fix #2138
* fixed `Structures`; added `Bundles`
* added fields; plus redefined `IsSemilattice` and `IsBoundedSemilattice` as aliases
* `fix-whitespace`
* reexported `comm`
* fixed `Lattice.Bundles`
* knock-on
* added text about redefinition of `Is(Bounded)Semilattice`
* add manifest fields to `IsIdempotentSemiring`
* final missing `Bundles`
* `CHANGELOG`
* [ new ] Word8, Bytestring, Bytestring builder (#2376)
* [ admin ] deprecate Word -> Word64
* [ new ] a type of bytes
* [ new ] Bytestrings and builders
* [ test ] for bytestrings, builders, word conversion, show, etc.
* [ ci ] bump ghc & cabal numbers
* [ fix ] actually set the bits ya weapon
* [ ci ] bump options to match makefile
* [ ci ] more heap
* [ more ] add hexadecimal show functions too
* Update LICENSE (#2409)
* Update LICENSE year
* Remove extraneous 'i'
---------
Co-authored-by: Lex van der Stoep <[email protected]>
* Remove (almost!) all external use of `_≤″_` beyond `Data.Nat.*` (#2262)
* additional proofs and patterns in `Data.Nat.Properties`
* added two projections; refactored `pad*` operations
* `CHANGELOG`
* removed one more use
* removed final uses of `<″-offset` outside `Data.Nat.Base|Properties`
* rename `≤-proof` to `m≤n⇒∃[o]m+o≡n`
* removed new pattern synonyms
* interim commit: deprecate everything!
* add guarded monus; make arguments more irrelevant
* fixed up `CHANGELOG`
* propagate use of irrelevance
* tidy up deprecations; reinstate `s<″s⁻¹` for `Data.Fin.Properties`
* tightened up the deprecation story
* paragraph on use of `pattern` synonyms
* removed `import`
* Update CHANGELOG.md
Fix refs to Algebra.Definitions.RawMagma
* Update Base.agda
Fix refs. to Algebra.Definitions.RawMagma
* inlined guarded monus definition in property
* remove comment about guarded monus
* Refactor `Data.Sum.{to|from}Dec` via move+deprecate in `Relation.Nullary.Decidable.Core` (#2405)
* fixes #2059 on the model of #2336
* fixed `import` dependencies
* simplified `import` dependencies
* final tweak
* `CHANGELOG`
* Implement move-via-deprecate of `decToMaybe` as per #2330 (#2336)
* Make the main home of `decToMaybe` be `Relation.Nullary.Decidable.Core`, but
deprecate the one in `Data.Maybe.Base` instead of removing it entirely.
Fix the library accordingly.
Note that this forces `Relation.Nullary.Decidable.Core` to use `Agda.Builtin.Maybe`
to avoid a cyclic import. This can be fixed once the deprecation is done.
* Update src/Relation/Nullary/Decidable/Core.agda
Good idea.
Co-authored-by: G. Allais <[email protected]>
* simplified the deprecation
* `CHANGELOG`
* narrowed import too far
* tweak a couple of the solvers for consistency, as per suggestions.
* chnage to `public` re-export of `Relation.Nullary.Decidable.Core.decToMaybe`
* Revert "chnage to `public` re-export of `Relation.Nullary.Decidable.Core.decToMaybe`"
This reverts commit 256a50589dacab913c69f4db5b4570b46cf440d7.
* `fix-whitespace`
* simplify `import`s
* make consistent with `Idempotent` case
* tidy up
* instead of an alias, open public so that Agda knows these really are the same. This is a better deprecation strategy.
* rename(provisional)+deprecate
* knock-on
* knock-on: refactor via `dec⇒maybe`
* deprecation via delegation
* fix `CHANGELOG`
---------
Co-authored-by: G. Allais <[email protected]>
Co-authored-by: James McKinna <[email protected]>
Co-authored-by: jamesmckinna <[email protected]>
* fixes #2411 (#2413)
* fixes #2411
* now via local -defined auxiliaries
* Tidy up CHANGELOG in preparation for v2.1 release candidate (#2412)
* Tidy up CHANGELOG in preparation for v2.1 release candidate
* Fixed WHITESPACE
* Fixed James' feedback and improved alphabetical order
* [v2.1-rc1] fixes #2400: use explicit quantification instead (#2429)
* fixes #2400: use explicit quantification
* fix knock-ons
* Revert "Improve `Data.List.Base` (fix #2359; deprecate use of `with` #2123) (#2365)" (#2423)
This reverts commit 438f9ed4c30751be35718297bbe0c8ec7d3fb669.
Specifically, it restores `with`-based definitions of the
`Decidable`-definable functions on `List`s, incl. `filter`
Fixes #2415
* implicit to explicit in `liftRel` (#2433)
* fix changelog (#2435)
couple fixes for changelog rendering
* Export missing IsDecEquivalence instance for Quantity from Reflection.AST.Instances
* Add missing `showQuantity` function to Reflection.AST.Show
* Compatibility with Agda PR #7322: add quantity to reflected syntax of constructor
* Bump CI for experimental to latest Agda master
* Final admin changes
* Added v2.1.1 CHANGELOG entry
* Fix #2462 by removing duplicate infix definition
* Updated remaining documentation for v2.1.1 release
* Update CHANGELOG.md typo
* Update CHANGELOG.md
* Update installation-guide.md
* Update src/Reflection/AST/Definition.agda
Fix typo
* Update CITATION.cff
bring the date forward to today
---------
Co-authored-by: Saransh Chopra <[email protected]>
Co-authored-by: Maximilien Tirard <[email protected]>
Co-authored-by: jamesmckinna <[email protected]>
Co-authored-by: Sofia El Boufi--Crouzet <[email protected]>
Co-authored-by: Alex Rice <[email protected]>
Co-authored-by: Guilherme Silva <[email protected]>
Co-authored-by: Jacques Carette <[email protected]>
Co-authored-by: Ambroise <[email protected]>
Co-authored-by: Andreas Abel <[email protected]>
Co-authored-by: Nathan van Doorn <[email protected]>
Co-authored-by: Akshobhya K M <[email protected]>
Co-authored-by: shuhung <[email protected]>
Co-authored-by: fredins <[email protected]>
Co-authored-by: Nils Anders Danielsson <[email protected]>
Co-authored-by: Ioannis Markakis <[email protected]>
Co-authored-by: G. Allais <[email protected]>
Co-authored-by: Amélia <[email protected]>
Co-authored-by: James Wood <[email protected]>
Co-authored-by: Jesin <[email protected]>
Co-authored-by: jamesmckinna <[email protected]>
Co-authored-by: Guilherme <[email protected]>
Co-authored-by: Piotr Paradziński <[email protected]>
Co-authored-by: lemastero <[email protected]>
Co-authored-by: Gan Shen <[email protected]>
Co-authored-by: Gan Shen <[email protected]>
Co-authored-by: Uncle Betty <[email protected]>
Co-authored-by: Chris <[email protected]>
Co-authored-by: Alba Mendez <[email protected]>
Co-authored-by: Naïm Favier <[email protected]>
Co-authored-by: Orestis Melkonian <[email protected]>
Co-authored-by: Lex van der Stoep <[email protected]>
Co-authored-by: Lex van der Stoep <[email protected]>
Co-authored-by: Jesper Cockx <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR proves that every non-zero natural number has a unique (up to permutation) prime factorization.
To this end, it also adds a definition of "rough" numbers (numbers which don't have prime factors below a bound)
This is something that I think is important to have a proof for, but I think it needs considerable improvement before it meets the quality criterion for this library, and I can't see how to improve it, so I'd appreciate feedback.
The factorization algorithm is trial division. It does not currently short-circuit when it checks a factor greater than the square root of the number being factorized, which would significantly improve its speed in some cases, but makes the code a bit more complicated.