agda pr 7349 #2441

* Eliminate many propositional equality imports * Fix merge conflict in Data.Bool.Properties Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org> --------- Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>

To fix agda/agda#6654, we've decided that large indices will no longer be allowed by default. There is an infective flag `--large-indices` to bring them back, but none of the uses of large indices in the standard library were essential: to avoid complicated mutually-recursive PRs across repos, I adjusted the levels to check with `--no-large-indices` instead of adding the flag to the modules that used them.

* Simplify some `Relation.Binary` imports * Format * Better naming scheme * Fix tests * Merge issues

* Simplify leftover `Function` imports * `Function` -> `Function.Base` Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org> --------- Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>

* Simplify more `Data.Product` import to `Data.Product.Base` * Missed an import

…#2019) * Simplify import of `Data.List.Relation.Binary.Pointwise` in agda-stdl * rectifications on Data.List.Relation.Binary.Pointwise import * rectifications on Data.List.Relation.Binary.Pointwise import * Delete weights-README.dot * Delete weight.png * Delete README.dot

* Simplify more `Data.Product` import to `Data.Product.Base` * Simplify more `Data.Product` import to `Data.Product.Base` * Indent

…1986)

A useful improvement to consistency of names,

* `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 <31931406+jamesmckinna@users.noreply.github.com>

…1287] (#1928)

Co-authored-by: Sofia El Boufi--Crouzet <136095087+Sofia-Insa@users.noreply.github.com>

…*` (#2118)

…2049)

…fRec` (#2084)

This reverts commit 91fd951.

…y` to `Relation.Binary.Lattice` (#2131)

… `Relation.Binary.*` (#2095)

…es (#2000)

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.

…2159)

…les (#2162)

* spellcheck; `fix-whitespace`; unfixed: a few alignment issues; typo `predications` to `predicates` in `Relation.Unary.Relation.Binary.Equality`

* 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 <matthewdaggitt@gmail.com>

… symbol usage (#2185) * regularise and specify/systematise, the conventions for symbol usage * typos/revisions

* Move `T?` to `Relation.Nullary.Decidable.Core` * Var name fix * Some refactoring * Fix failing tests and address remaining comments * Fix style-guide

* Make decdable versions of sublist functions the default * Remove imports Bool.Properties * Address comments

* [ 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 <matthewdaggitt@gmail.com>

…ME.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 <guillaume.allais@ens-lyon.org>

Connex allows both relations to hold, so the old comment was wrong.

* Add Function.Consequences.Setoid * Fix comment * Fix re-export bug * Finally fixed bug I hope * Removed rogue comment * More tidying up

…2205) * deprecating `isPropositional` * tighten `import`s * bumped Agda version number in comment

…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 <matthewdaggitt@gmail.com>

…yle-guide` conventions (#2206) * fixes issue #2168 * added more names for deprecation, plus `hiding` them in `Propositional`

* Fix names in IsSemilattice * Add reference to changes to Semilattice to CHANGELOG

* 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 * remove spurious/ambiguous `import` --------- Co-authored-by: jamesmckinna <j.mckinna@hw.ac.uk>

* 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 <guillaume.allais@ens-lyon.org>

* Final admin changes for v2.0 release * Fix Agda versions

* added tabulate+< * renamed tabulate function --------- Co-authored-by: Guilherme <alvares@chalmers.se> Co-authored-by: MatthewDaggitt <matthewdaggitt@gmail.com>

* 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 <alvares@chalmers.se> Co-authored-by: MatthewDaggitt <matthewdaggitt@gmail.com>

…d` (#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 * corrected major version number

* 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 <piotr.paradzinski@iohk.io> Co-authored-by: MatthewDaggitt <matthewdaggitt@gmail.com>

* fixes issue #2237 * leftover from #2182: subtle naming 'bug'/anomaly

* 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 debfec1. * Move definitions up. Fix comments.

* added paragraph on coupled contributions * typo

* 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 debfec1. * Move definitions up. Fix comments. * fix CHANGELOG to report the correct syntax.

…2256) * removed all external use of `less-than-or-equal` beyond `Data.Nat.*` * use of `variable`s

* 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

* Index module morphisms by raw bundles * Use synonyms for RawModule's RawBimodule etc * Update changelog * Update constructed morphisms * Fix Algebra.Module.Morphism.ModuleHomomorphism

* added stub content on programming idioms * added para on qualified import names

@MatthewDaggitt

* fixes #2091 * revised along the lines of @MatthewDaggitt's suggestions --------- Co-authored-by: MatthewDaggitt <matthewdaggitt@gmail.com>

* 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

* `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.*`

Also import this module in doc/README.agda so that it is covered by CI. Closes #2278.

* `Data.List.Relation.Relation.Binary.BagAndSetEquality` * `Relation.Binary.Reasoning.*` * preorder reasoning * setoid reasoning * alignment

* Qualified import of `Data.Product.Base as Product` * more modules affected

* 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 * added one line to CHANGELOG * added permutation properties * Added Base to imports Co-authored-by: Nathan van Doorn <nvd1234@gmail.com> * Added Base to import Co-authored-by: Nathan van Doorn <nvd1234@gmail.com> * Added core to import Co-authored-by: Nathan van Doorn <nvd1234@gmail.com> * 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 <nvd1234@gmail.com> Co-authored-by: Guilherme <alvares@chalmers.se>

* 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 as Sum` * resolve merge conflict in favour of #2293

* [ new ] associativity of Appending * Removed unneeded variable * Renamed Product module --------- Co-authored-by: MatthewDaggitt <matthewdaggitt@gmail.com>

* [ 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 <matthewdaggitt@gmail.com>

* fixing #2280 * re-export constructor via pattern synonym * updated `README` * refactor: better disambiguation; added a note in `CHANGELOG`

* Function setoid is back. * make all changes asked for in review * fix indentation

* recommendation from #2294 * spellcheck * comma --------- Co-authored-by: MatthewDaggitt <matthewdaggitt@gmail.com>

* make `mkRawMonad` and `mkRawApplicative` universe-polymorphic * fix unresolved metas --------- Co-authored-by: Gan Shen <gan@kresge-100-64-83-91.resnet.ucsc.edu>

* Some properties of upTo and downFrom * Rename things per review comments * Fix changelog typo

* tidying up `README` imports * address Matthew's review comments

* 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 <matthewdaggitt@gmail.com>

* 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 <matthewdaggitt@gmail.com>

…lations (#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 <matthewdaggitt@gmail.com> * [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 <matthewdaggitt@gmail.com> Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org> Co-authored-by: Amélia <me@amelia.how> Co-authored-by: Nathan van Doorn <nvd1234@gmail.com> Co-authored-by: James Wood <laMudri@gmail.com> Co-authored-by: Andreas Abel <andreas.abel@ifi.lmu.de>

* 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 <matthewdaggitt@gmail.com>

* 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 <guillaume.allais@ens-lyon.org> Co-authored-by: MatthewDaggitt <matthewdaggitt@gmail.com>

* easy refactorings for better abstraction * tweaking irrefutable `with`

* added structure and bundle; tidied up * added structure and bundle; tidied up * fix order of entries * blank line * standardise `variable` names * alignment

* ⌞_⌟ 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 <matthewdaggitt@gmail.com>

… on `List.Properties` (#2323) * simplifed proof; removed dependency on `List.Properties` * corrected module long name in comment

* 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`

#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

…ion.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

Co-authored-by: MatthewDaggitt <matthewdaggitt@gmail.com>

* minor refactor: use Data.Unit.Polymorphic instead of an explicit Lift. * additional tweak: use contradiction where possible.

* 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.

* 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.

* 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 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 <guillaume.allais@ens-lyon.org>

* added `RawNNO` * [fix #2273] Add `NNO`-related modules * start again, fail better... * rectify names * tighten `import`s * rectify names: `CHANGELOG` --------- Co-authored-by: MatthewDaggitt <matthewdaggitt@gmail.com>

@jamesmckinna

* 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

…2354) * systematic use of `DecidableEquality` * tweak

@JacquesCarette

…) (#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 <guillaume.allais@ens-lyon.org> * @gallais 's comments * Update src/Data/List/Base.agda Oops! Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org> --------- Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>

…Semiring (#2370) * Closes #2315 * whitespace

* [ 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

* 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.

#2364) * `with`-free definition of `unfold` * fixed previous commit

* 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, 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 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

* 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 <matthewdaggitt@gmail.com>

…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. 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 <guillaume.allais@ens-lyon.org> * Update src/Data/Fin/Base.agda layout for readability Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org> * Update src/Data/List/Fresh/Relation/Unary/All.agda layout for readability Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org> --------- Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>

* [ new ] ¹-anti-homo‿- * Update CHANGELOG.md Co-authored-by: Nathan van Doorn <nvd1234@gmail.com> * Update src/Algebra/Properties/Group.agda Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> * Update CHANGELOG.md Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> * [ more ] symmetric lemma * [ new ] ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x --------- Co-authored-by: MatthewDaggitt <matthewdaggitt@gmail.com> Co-authored-by: Nathan van Doorn <nvd1234@gmail.com> Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

This has to be in scope for desugaring `do` blocks that don't bind intermediate results.

…ry.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 * removed redundant `Membership` instances * fix merge conflict error

…#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 <andreas.abel@ifi.lmu.de>

* Pointwise `Algebra` * temporary commit * better `CHANGELOG` entry? * begin removing redundant `module` implementation * finish removing redundant `module` implementation * make `liftRel` implicitly quantified

* 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

) * 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 <31931406+jamesmckinna@users.noreply.github.com> Co-authored-by: James McKinna <J.McKinna@hw.ac.uk>

* Haskell CI (for GenerateEverything) and dependencies bumped to GHC 9.10.1 * CI: bump some versions, satisfy some shellcheck complaints

* 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

* refactored from #2350 * enriched the `module` contents in response to review comments

* 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.

* 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 <31931406+jamesmckinna@users.noreply.github.com>

) * refactor towards `if_then_else_` * layout * `let` into `where`

* 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`

* `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 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 93e9e0f. * Revert "fix things as per Matthew's review - though this remains a breaking change." This reverts commit d1cae72. * Revert "fix whitespace" This reverts commit 81230ec. * Revert "port over two modules" This reverts commit 6619f11. * 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 <J.McKinna@hw.ac.uk>

…es` (#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`

* [ 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 year * Remove extraneous 'i' --------- Co-authored-by: Lex van der Stoep <lex.vanderstoep@imc.com>

* 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

…ary.Decidable.Core` (#2405) * fixes #2059 on the model of #2336 * fixed `import` dependencies * simplified `import` dependencies * final tweak * `CHANGELOG`

* 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 <guillaume.allais@ens-lyon.org> * 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 256a505. * `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 <guillaume.allais@ens-lyon.org> Co-authored-by: James McKinna <J.McKinna@hw.ac.uk> Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

* fixes #2411 * now via local -defined auxiliaries

* Tidy up CHANGELOG in preparation for v2.1 release candidate * Fixed WHITESPACE * Fixed James' feedback and improved alphabetical order

* fixes #2400: use explicit quantification * fix knock-ons

…2123) (#2365)" (#2423) This reverts commit 438f9ed. Specifically, it restores `with`-based definitions of the `Decidable`-definable functions on `List`s, incl. `filter` Fixes #2415

couple fixes for changelog rendering

….AST.Instances

… constructor

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

agda pr 7349 #2441

agda pr 7349 #2441

Commits on Jul 10, 2024