Update experimental branch; allow GHC 9.14

[andreasabel]

• [ fix ] release guide ([ fix ] release guide #2800)

• Backport changes from 2.3 release to 2.4 (Backport changes from 2.3 release to 2.4 #2799)

  • Add back accidentally removed lemmas (Issue2788 Issue2788 #2794))

  • opposite of a Ring [clean version of pr opposite of a Ring #1900] (opposite of a Ring [clean version of pr #1900] #1910)

  • punchOut preserves ordering (punchOut preserves ordering #1913)

  • Wellfounded proof for sum relations (Wellfounded proof for sum relations #1920)

  • last revert undone by hand

  • Remove extra line in CHANGELOG

  • Update CHANGELOG.md

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

  • Update CHANGELOG.md

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

  • Update CHANGELOG.md

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

  • Update CHANGELOG.md

  This was indeed anachronistic from 2.0

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

  • Update CHANGELOG.md

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

  • resolve issues pointed out by James.

  • Update CHANGELOG.md

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

  • remove now obsolete comment

  • last mistake in CHANGELOG, hopefully fixed now.

  ---

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com
  Co-authored-by: Nathan van Doorn nvd1234@gmail.com
  Co-authored-by: Alice Laroche 60161310+Seiryn21@users.noreply.github.com
  Co-authored-by: matthewdaggitt matthewdaggitt@gmail.com

  • Bring v2.3 release changes accross

  • Fix typo

  • Fix whitespace

  ---

  Co-authored-by: Jacques Carette carette@mcmaster.ca
  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com
  Co-authored-by: Nathan van Doorn nvd1234@gmail.com
  Co-authored-by: Alice Laroche 60161310+Seiryn21@users.noreply.github.com

• [ add ] eta law for ¬¬ monad ([ add ] eta law for ¬¬ monad #2803)

  • add: eta law for ¬¬ monad

  • refactor: use eta law for ¬¬ monad

  • fix: trim variables

• [Add] padRight properties to Data.Vec.Properties ([Add] padRight properties to Data.Vec.Properties #2769)

  • padRight final vers

  l

  • Adding padRight proprities

  • Cleaning the drafts

  • cleaning drafts

  • modification after reviews

  • suppr double parentheses

  • moved cast-replicate

  • modif after reviews and changelog

  • changes to changelog

  • Update CHANGELOG.md

  fix-whitespace

  ---

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

• [ add ] style-guide recommendation preferring contradiction over ⊥-elim ([ add ] style-guide recommendation preferring contradiction over ⊥-elim #2798)

  • add: recommendation

  • fix: whitespace

  • Update doc/style-guide.md

  Improved text.

  Co-authored-by: Jacques Carette carette@mcmaster.ca

  • fix: fill-column to 72

  ---

  Co-authored-by: Jacques Carette carette@mcmaster.ca

• More distributivity properties for nats (More distributivity properties for nats #2833)

  • More distributivity properties for nats

  • Simplify proof using existing lemma

  • Use lemma instead of refl

  In principle this lets us translate more easily to an arbitrary semiring

• [ add ] flipped version of Relation.Nullary.Negation.Core.contradiction ([ add ] flipped version of Relation.Nullary.Negation.Core.contradiction #2797)

  • add: flipped version of contradiction

  • add: comment to CHANGELOG

• [ refactor ] Data.Fin.Properties following [ refactor ] application, and perhaps even proof, of Data.Fin.Properties.pigeonhole? #2746 ([ refactor ] Data.Fin.Properties following #2746 #2782)

  • refactor: following [ refactor ] application, and perhaps even proof, of Data.Fin.Properties.pigeonhole? #2746

  • refactor: deploy the flip contradiction workaround

  • refactor: prefer <⇒notInjective over injective⇒≤

  • fix: whitespace

  • fix: DRY with private specialisation

  • refactor: use flipped contradiction

• [ add ] BooleanRing plus Properties ([ add ] BooleanRing plus Properties #2763)

  • add: BooleanRing plus Properties

  • Update CHANGELOG.md

  Removed spurious entry

  • refactor: more general API

  • fix: added note to CHANGELOG

  • refactor: make binomial expansion an explicit step

  • rename: *-isIdempotentMonoid

  • add: *-idempotentMonoid

  • refactor: use Cancellative properties only

  • add: stub properties for CommutativeRing

  • refactor: BooleanRing properties in terms of CommutativeRing and BooleanSemiring

  • refactor: put everything together

  • add: stub properties for CommutativeRing

  • refactor: adjust re-exports

  • add: BooleanAlgebra yields BooleanRing etc.

  • add: more re-exports

  • add: more inherited properties

  • add: more properties towards IsBooleanAlgebra

  • add: yet more properties towards IsBooleanAlgebra

  • add: grinding towards IsBooleanAlgebra

  • add: deMorgan laws

  • add: Semiring properties as home for binomial-expansion

  • more fiddling

  • back to square one

  • fix: finally!

  • fix: remove shadowing of isBooleanRing and booleanRing

  • reset: CHANGELOG for v2.4

  • fix: whitespace

• [bug] replace wrong argument to projection in Algebra.Morphism.Construct.DirectProduct ([bug] replace wrong argument to projection in Algebra.Morphism.Construct.DirectProduct #2822)

  • [bug] fix "wrong" argument to projection

  • add: note on bug fix to CHANGELOG

  ---

  Co-authored-by: jamesmckinna j.mckinna@hw.ac.uk

• Update CI to Agda-2.8.0 and GHC-9.12.2 (Update CI to Agda-2.8.0 and GHC-9.12.2 #2835)

  • Update stack.yaml files to latest minor versions

  • Update CI to Agda-2.8.0 and GHC-9.12.2 (shipped with ubuntu-24.04)

• Factor antisymmetry proof for sublist (Factor antisymmetry proof for sublist #2836)

  • Simplify Sublist/Heterogeneous/antisym: collapse two cases

  • Simplify Sublist/Heterogeneous/antisym: factor out contradiction

  • Review comment: use contradiction

  • Apply suggestions from code review

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

  ---

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

• [ new ] Effect.Monad.Random ([ new ] Effect.Monad.Random #2372)

  • [ new ] Effect.Monad.Random

  Still TODO: instances for transformers

  • [ more ] add lifting along transformer

  • [ test ] for the new mtl-style constraint

  • [ cleanup ] this is not meant to be uploaded

  • [ fix ] declare effect.monad.random as unsafe

  • [ changelog ] listing new modules too

  • fix: CHANGELOG

  ---

  Co-authored-by: Jacques Carette carette@mcmaster.ca
  Co-authored-by: jamesmckinna j.mckinna@hw.ac.uk
  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

• [Add] truncate properties to Data.Vec.Properties ([Add] truncate properties to Data.Vec.Properties #2795)

  • adding truncate's properties

  • update changelog

  • cleaning whitespaces

  • Recleaning

  • corrections after reviews

  • correction of changelog

  • changes after review

• Fix universe level typo (Fix universe level typo in Function.Construct.Constant #2841)

• fix: naming convention ([ deprecate ] names for deMorgan lemmas in Relation.Nullary.Negation #2838)

• [ refactor ] reorganise Relation.Nullary.Negation.Core to make clean separation of properties ([ refactor ] reorganise Relation.Nullary.Negation.Core to make clean separation of properties #2805)

  • refactor: reorganise to make clean separation of properties

  • refactor: remove note

  • refactor: remove import of flip

• deprecate: names for deMorgan lemmas ([ deprecate ] names for deMorgan lemmas in Data.Fin.Properties #2837)

• [ refactor ] Data.Fin.Properties.decFinSubset ([ refactor ] Data.Fin.Properties.decFinSubset #2793)

  • [ refactoring ] decidable Data.Fin.Properties

  • refactor: make variables P, Q local again

  • refactor: use flipped contradiction

  • fix: comment

  • Restored deleted import of Function.Base.flip

• Added README for tests directory (Added README for tests directory #2844)

  • Added README for tests directory

  • Whitespace fix

• [ add ] clean version of Data.Fin.Properties.searchMinimalCounterexample ([ add ] clean version of Data.Fin.Properties.searchMinimalCounterexample #2801)

  • [ add ] clean version of Data.Fin.Properties.searchMinimalCounterexample

  • use: Π[_] syntax

  • refactor: simplify

  • refactor: drastic streamlining

  • refactor: remove redundant import

  • refactor: inlined lemma in ¬∀⇒∃¬

• [ fix ] Relation.Nullary.Decidable.Core names for combinators ([ fix ] Relation.Nullary.Decidable.Core names for combinators #2843)

  • refactor: fixes Use consistent names for Decidable combinators #2842

  • refactor: knock-ons

  • refactor: more knock-ons

  • refactor: resolve merge conflict following [ refactor ] Data.Fin.Properties.decFinSubset #2793

• Add doc/ to the target in Makefile and make the cabal command customizable (Add doc/ to the target in Makefile and make the cabal command customizable #2830)

  • Add stack yaml for GHC 9.10.2 (stackage lts-24.11)

  • Fix Everything.agda targets in Makefile

  • Allow customization of the cabal command

  • Bump CI tag to Agda v2.8.0 (not RCs)

  • Fix CABAL_EXEC variable name

  • Update stack-9.10.2 to 9.10.3

• Add two steps to Release Guide (Add two steps to Release Guide #2850)

  • Create a branch for the release in addition to creating tags
  • Before generating docs, make sure the directory content is the release branch (v2.3 webpage is not quite v2.3 #2848)

• Add various relations over non-empty lists (Add various relations over non-empty lists #2862)

  • Add various relations over non-empty lists

  • Address James' feedback

• Add subgroups and submodules (Add subgroups and submodules #2852)

  • Add subgroups and submodules

  • Let Agda fill in a record for me

  • Try different names for the underlying structure

  • Bimodule rather than module

  • style

• Adds "pushforward" to Relation.Unary (Adds "pushforward" to Relation.Unary #2840)

  • add predicate pushforward

  • update changelog

  • update notation based on discussion

  • Additional description

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

  ---

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

• [ add ] Algebra.Definitions.Central plus Consequences for Identity and Zero ([ add ] Algebra.Definitions.Central plus Consequences for Identity and Zero #2873)

  • add: Algebra.Definitions.Central

  • add: Identity and Zero elements are Central

  • Update src/Algebra/Definitions.agda

  Co-authored-by: Jacques Carette carette@mcmaster.ca

  • fix: line break

  ---

  Co-authored-by: Jacques Carette carette@mcmaster.ca

• [ add ] Relation.Binary.Morphism.Construct.On ([ add ] Relation.Binary.Morphism.Construct.On #2872)

  • add: Relation.Binary.Morphism.Construct.On

  • fix: top-level descriptive comment

  • fix: remove module ι, and better description in CHANGELOG

• fix: [ refactor ] Algebra.Properties.Monoid #2882 ([ rename/deprecate ] Rename Algebra.Properties.Monoid.ε-comm #2883)

• ** [ bug/refactor ] put Algebra.Consequence.Propositional.sel⇒idem in the right place ( [ bug/refactor ] put Algebra.Consequence.Propositional.sel⇒idem in the right place  #2881)**

  • refactor: put lemma in the right place

  • fix: uncommitted edits

  • fix: CHANGELOG

  • fix: qualified module name

• Add map-removeAt to Data.Vec.Properties (Add map-removeAt to Data.Vec.Properties #2899)

  • Add map-removeAt to Data.Vec.Properties

  • Fix whitespace in changelog

• [add] irrelevant & antisym to Pointwise for Data.Vec ([add] irrelevant & antisym to Pointwise for Data.Vec #2902)

  • Add irrelevant & antisym for Vec.Pointwise.Inductive

  • Fix: relax sym & trans to allow different levels

  • Add irrelevant & antisym to Vec.Pointwise.Extensional

  • Update CHANGELOG

• Share the proofs of ×-comm and ⊎-comm of type isomorphisms and add a pairing operation (Share the proofs of ×-comm and ⊎-comm of type isomorphisms and add a pairing operation #2868)

  • Share Sum and Product type isomorphism proof

  • Add pairing of type isomorphism

  • Update CHANGELOG for the new functions

  • cosmetic changes: limit Data.Sum.Base imports

• [ doc ] Add JOSS publication ([ doc ] Add JOSS publication #2903)

• Adding extrema to a non-strict order respects equality (Adding extrema to a non-strict order respects equality #2904)

  • Show adding extrema to a non-strict order respects equality

  • Code-block module names in changelog

  • FIXUP remove empty line from changelog

• [ fix ] test runner to use cabal ([ fix ] the test runner for v2.0-joss-submission #2884) ([ fix ] test runner to use cabal (#2884) #2896)

  • [ fix ] add test runner ([ fix ] the test runner for v2.0-joss-submission #2884)

  • [ test ] update bounds

  This is probably not going to build (missing bytestring / random
  dependencies in the sample cabal file).

  • [ fix ] relax directory constraints, fix deprecated use

  • [ fix ] bytestring dependency

  • [ fix ] random dependency

  • [ fix ] test runner for random should ignore outputs

  • [ fix ] the extra arguments may have spaces in them

  • [ cleanup ]

  • CI: remove JOSS build

  • Test runner: print test name without buffering

  • Script: fix issue leading to nested _build/_build/...

  • [ re [ fix ] test runner to use cabal (#2884) #2896 ] Restrict clock types

  • [ oops ] forgot to fix the re-export

  • [ fix ] typo 🤦

  • [ fix ] this casing is killing me

  ---

  Co-authored-by: G. Allais guillaume.allais@ens-lyon.org

• Adds additional properties to {Left,Right}Module (Adds additional properties to {Left,Right}Module #2906)

  • adds additional properties to LeftModule

  • Update src/Algebra/Module/Properties/LeftModule.agda

  using suggestion

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

  • add subscript to name of lemma

  • add RightModule properties

  • Update src/Algebra/Module/Properties/RightModule.agda

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

  • Update CHANGELOG.md

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

  • Update src/Algebra/Module/Properties/LeftModule.agda

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

  • Update src/Algebra/Module/Properties/LeftModule.agda

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

  • Update src/Algebra/Module/Properties/RightModule.agda

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

  ---

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

• [ new ] unix install script for the standard library ([ new ] unix install script for the standard library #2895)

  • [ new ] install script for the standard library

  • [ cosmetic ] cleanup big cases

  • [ cosmetic ] indentation

  • [ fix ] touch files before grepping them

  • [ doc ] explain option choice

  • [ more ] check dependencies + debug mode

  • [ fix ] be more careful about overwriting dirs

  • [ cosmetic ] more structure

  • [ ergonomics ] make more of an effort

  Keep asking the user until we get a valid Agda executable

  • [ doc ] the installation instruction

  • [ cleanup ] follow the shellcheck advice

  • [ admin ] add a step to the release guide

  • [ more ] gracefully report that wget failed

  • [ cleanup ] wording

  • [ cleanup ] use variable rather than repetition

  • [ doc ] more structure in the README

  • [ fix ] remove redundant full stop

  • [ fix ] defaults-X.Y.Z is not supported yet

  I'll open a PR to Agda to add it to the next releases.

  • [ fix ] nasty typo

• [ add ] properties of Relation.Unary adjoints ([ add ] properties of Relation.Unary adjoints #2866)

  • add: adjoint properties for Adds "pushforward" to Relation.Unary #2840

  • add: functoriality proofs

  • tweak: keep original statement

  • fix: whitespace

  • refactor: functoriality of the adjoints

  • refactor: functoriality of the adjoints, again

  • add: more commentary text

• De Morgan's laws for Pred (De Morgan's laws for Pred #2832)

  • Add De Morgan's law for Pred

  • Add more of De Morgan's laws

  • Don't name unused variables

  • Use curry

• [ fix ] README text ([ fix ] README text #2911)

• refactor: remove redundant private lemma ([ refactor ] remove redundant private lemma in Data.Sum.Algebra #2908)

• Unused implicit at Data.List.Fresh.Relation.Unary.Any.Properties (Unused implicit at Data.List.Fresh.Relation.Unary.Any.Properties #2912)

• [ refactor ] make m ≤ n argument to Data.Vec.Base.{truncate|padRight} irrelevant ([ refactor ] make m ≤ n argument to Data.Vec.Base.{truncate|padRight} irrelevant #2787)

  • refactor: make truncate and padRight take irrelevant argument

  • fix: proofs of properties following [Add] padRight properties to Data.Vec.Properties #2769 and [Add] truncate properties to Data.Vec.Properties #2795; deprecate truncate-irrelevant

  • fix: deprecation in CHANGELOG

  • fix: duplication after resolving merge conflict

  • fix: alignment

  • add: specialised versions of padRight-drop and padRight-take

  • fix: whitespace

  • reset: CHANGELOG

  • restore: new CHANGELOG entries

  • refactor: weaken types of truncate properties

  • fix:CHANGELOG to reflect weakened types

  • fix: whitespace

  • final tweak

  • final tweak

• [ fix ] issue Typo in Rational.Properties.nonPos*nonPos⇒nonPos #2918 ([ fix ] issue #2918 #2920)

  • [ fix ] issue Typo in Rational.Properties.nonPos*nonPos⇒nonPos #2918

  • [ add ] deprecation warning

• [ add ] Data.List.Fresh.Membership.DecSetoid ([ add ] Data.List.Fresh.Membership.DecSetoid #2914)

• [ add ] inequalities for 2 ^ log₂ n ([ add ] inequalities for 2 ^ log₂ n #2925)

  • [ add ] inequalities for 2 ^ log₂ n

  This adds the inequalities 2 ^ ⌊log₂ n ⌋ ≤ n for non-zero n and
  n ≤ 2 ^ ⌈log₂ n ⌉ for all natural numbers n. Similar to the existing
  properties of the logarithm, the main proofs
  that keep track of the accumulators are added to
  Data.Nat.Logarithm.Core. Both use a lemma that 2 * (ℕ.suc n) ≡ 2 + (n + n)
  which is added to Data.Nat.Logarithm.Core as well.

  The respective simplified versions on ⌊log₂_⌋ and ⌈log₂_⌉ are added
  directly to Data.Nat.Logarithm.

  • move 2*suc[n]≡2+n+n to Data.Nat.Properties

  • ℕ.suc -> suc

  • Further ℕ.suc -> suc

  • replace 1 + with suc

  • Switch to equational reasoning

  • Update Changelog

  • RM unused 'trans'

  • Use NonZero instance

  • Update Changelog

  • Update src/Data/Nat/Logarithm.agda

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

  • Update CHANGELOG.md

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

  ---

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

• refactor: remove last uses of inspect ([ refactor ] remove last uses of inspect in Data.Rational.Unnormalised.Properties #2926)

• [ add ] Bool action on a RawMonoid plus properties ([ add ] Bool action on a RawMonoid plus properties #2450)

  • Add new Bool action on a RawMonoid plus properties

  • response to review comments on draft

  • reset: CHANGELOG

  • restore: new CHANGELOG entries

  • change: notation

  • refactor: use new notation, plus add new lemma

  • refactor: tweak notation

  • refactor: proof following Jacques' suggestion

• [ fix ] issue Inline Data.Vec.Functional.map for Better Termination Checking #2905 ([ fix ] issue #2905 #2927)

  • [ fix ] issue Inline Data.Vec.Functional.map for Better Termination Checking #2905

  • fix: words

• fix: issue Don't be so eager to _, especially in the presence of instances #2931 ([ fix ] make Data.Nat.Primality.prime⇒nonZero more strict in its explicit. argument #2932)

• [ fix ] issue 4 proofs suggested for Rational.Properties #2921 ([ add ] no-zero-divisor lemmas to Data.Rational.{Unnormalised.}Properties (issue #2921) #2933)

• fixup: further eta-expansions for Don't be so eager to _, especially in the presence of instances #2931 (Further eta-expansions for #2931 #2935)

• [ refactor ] make step a manifest field of Data.Nat.LCG.Generator ([ refactor ] make step a manifest field of Data.Nat.PseudoRandom.LCG.Generator #2937)

• Add divisibility properties of exponentials (Add divisibility properties of exponentials #2940)

  • Add divisibility of exponentials

  • Make inequality irrelevant

  • Simplify m∣n⇒m^o∣n^o definition by reusing ^-distribʳ-*

  • Fiddling with variable names

• Fix a comment concerning Σ-syntax. (Fix a comment concerning Σ-syntax. #2943)
  The old comment might have pertained to an older version of Agda,
  but it does not apply to contemporary Agda (e.g. 2.8.0).

• [ add ] filter-∩, filter-map and filter-swap for Data.List.Properties ([ add ] filter-∩, filter-map and filter-swap for Data.List.Properties #2942)

  • [ add ] filter-∩ and filter-swap for Data.List.Properties

  • [ add ] filter-map to Data.List.Properties

  • also introduced minor readibility rewrites for filter-∩ and filter-swap

  • [ add ] CHANGELOG entry for filter-map, filter-∩ and filter-swap

  • [ meta-fix ] adjusted changelog formatting

  • [ refactor ] naming convention of arbitrary lists

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

  ---

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

• [ add ] ¬[x≢x] contradiction from irrelevant irreflexive propositional equality ([ add ] ¬[x≢x] contradiction from irrelevant irreflexive propositional equality #2944)

  • add: two irreflexivity proofs

  • add: Setoid irreflexivity proofs

  • add: CHANGELOG entries

  • refcator: propagate ¬[x≢x]

• Added function to show Rational at a decimal precision (Added function to show Rational at a decimal precision #2945)

  • Added function to show Rational at a decimal precision

  • fix Data.Nat.Divisibility heading in changelog

  • Change type of 'atPrecision', reuse showAtPrecision from Rational in Rational.Unnormalised

• [ refactor ] Data.Nat.Properties.∸-suc to make m≤n argument irrelevant ([ refactor ] Data.Nat.Properties.∸-suc to make m≤n argument irrelevant #2939)

  • [ refactor ] [ add ] ∸-suc lemma for natural numbers #2757 to make argument to ∸-suc irrelevant

  • [ refactor ] [ add ] ∸-suc lemma for natural numbers #2757 to make argument to ∸-suc irrelevant

  • refactor: more proofs, plus comment about eta-expansion

• [ add ] Bool-valued strict inequality to Data.Integer.Base, Data.Rational.Base etc. ([ add ] Bool-valued strict inequality to Data.Integer.Base, Data.Rational.Base etc. #2949)

  • [ add ] Bool-valued strict inequality

  • add: relate Boolean and inductive definitions of _<_

• [ fix ] assumption name in Data.Product.Relation.Binary.Lex.Strict ([ fix ] assumption name in Data.Product.Relation.Binary.Lex.Strict #2956)

  • [ fix ] assumption name in Data.Product.Relation.Binary.Lex.Strict

  • refactor: use infix

• [ rename ] decidability for `Relation.Binary.Construct.{Intersection|Union}`` ([ rename ] decidability for Relation.Binary.Construct.{Intersection|Union}` #2955)

  • [ rename ] decidability for Relation.Binary.Construct.Intersection

  • d'oh

• [ add ] Nat lemmas with _∸_, _⊔_ and _⊓_ ([ add ] Nat lemmas with _∸_, _⊔_ and _⊓_ #2924)
  Some stuff that I've needed. I have no idea if those belong here in
  stdlib. I don't know if I've put those in the right place, or named
  them properly. Hence the draft and lack of changlog entry.

• [ refactor ] use variables more systematically in Data.List.Fresh{.*} ([ refactor ] use variables more systematically in Data.List.Fresh{.*} #2916)

  • refactor: use variables more systematically

  • refactor: remove P from variable block

  • refactor: Properties follow easily

  • refactor: propagate the variable style throughout

  • Update src/Data/List/Fresh.agda

  • Update src/Data/List/Fresh.agda

  • Update src/Data/List/Fresh.agda

  • Update src/Data/List/Fresh.agda

  • fix: module name

  • fix: bug in imports

  • refactor: Any.Propertiess

  • fix: quantifier prefix

  • final tweaks

  • Update src/Data/List/Fresh/Relation/Unary/Any.agda

  Use a Unary definition, rather than spell it out explicitly.

  Co-authored-by: G. Allais guillaume.allais@ens-lyon.org

  • refactor: further streamlining steps; plus one deprecation

  • refactor: introduce new notation

  • final tweaks

  • add Guillaume's characterisation, plus one deprecation

  • fix: whitespace

  ---

  Co-authored-by: G. Allais guillaume.allais@ens-lyon.org

• Add tactic-style ring solvers for rational and unnormalised rational numbers (Add tactic-style ring solvers for rational and unnormalised rational numbers #2965)

  • add Data/Rational/Unnormalised/Tactic/RingSolver

  • add Data.Rational.Tactic.RingSolver

  • update changelog - tactic ring solvers for rational numbers in Changelog

  • add README.Data.Rational

  • add README.Data.Rational.Unnormalised

  • solver example in README.Data.Rational.Unnormalised

  • solver example in README.Data.Rational

  • property 0≡?-weak : (p : ℚ) → Maybe (0ℚ ≡ p) moved from RingSolver

  • 0≃?-weak : (p : ℚᵘ) → Maybe (0ℚᵘ ≃ p) moved from RingSolver

  • Fix examples: Use ≡ for Data.Rational.Tactic.RingSolver, and ≃ for Data.Rational.Unnormalised.Tactic.RingSolver

  • Use matching unnormalised constants in README solver example

  ---

  Co-authored-by: lemastero piotr.paradzinski@iohk.io

• refactor: cosmetic reordering ([ refactor ] cosmetic reordering of README imports #2960)

• Add properties that characterize Data.Tree.AVL.Indexed.delete. (Add properties that characterize Data.Tree.AVL.Indexed.delete. #2961)

  • Add properties that characterize Data.Tree.AVL.Indexed.delete.

  These are properties for the core delete on AVL trees and similar to the prexisting properties of insert.

  Lemmas added for delete are delete⁺, delete-tree⁻, delete-key-∈⁻ and delete-key⁻.
  Together these can be used to prove (k′ ∈ delete k t) ⇔ (k′ ≉ k × k′ ∈ t), which fully characterizes delete.

  delete⁺, delete-tree⁻, and delete-key⁻ correspond to Coq.FSets.FSetInterface's remove_2, remove_3, and remove_1, respectively.

  Just like other lemmas in this file, delete⁺, delete-tree⁻, delete-key⁻ generalize k′ ∈ t to Any P t.
  delete-key-∈⁻ is essentally a helper for delete-key⁻, which would be difficult to prove directly.

  Many more lemmas were added for AVL functions that delete depends on.
  These additional lemmas characterize the functions castʳ, joinˡ⁺, joinʳ⁺, joinˡ⁻, joinʳ⁻, headTail, and join.
  Adding all this code to Properties.agda caused make test to overflow past the 4096 MB default heap size.
  This was solved by breaking Properties.agda into multiple files, with roughly one file for each AVL function.

  Added proofs are a similar style the preexisting proofs in Properties.agda.

  • telescoped arguments in Singleton.agda

  • removed unused vars, merged cases using Any.toSum for JoinConstFuns.agda

  • addressed review comments on Join.agda

  • addressed comments in Insert.agda

  • addressed review comments for HeadTail.agda

  • addressed review comments for Delete.agda

  • Moved Data.Tree.AVL.Indexed.Relation.Unary.Any.* into Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.*

  • Simplified proofs by removing subterms that recapitulate the subject function.

  • Changed whitespace to align matches.

  • More alignment.

  • addressed review comments to use var in let and moved implicits to variable block

  • Recorded changes in CHANGELOG.md. Addressed review comments for AnyLookup.

  • Apply suggestion from @jamesmckinna

  Cosmetic tweak to text

  ---

  Co-authored-by: jamesmckinna 31931406+jamesmckinna@users.noreply.github.com

• [ refactor ] fix Rename lemma satisfied to any⇒satisfiable in *.Relation.Unary.Any #2865 for v2.4 ([ refactor ] fix #2865 for v2.4 #2954)

  • [ refactor ] fix Rename lemma satisfied to any⇒satisfiable in *.Relation.Unary.Any #2865

  • refactor: another round of renaming

  • fix: revert changes to List.Relation.Unary.Any

  • add: comment documenting downstream intentions to make changes

  • add: additional content to the deprecation warning

• [ refactor ] Infrastructure for Data.Tree.AVL.Indexed.* ([ refactor ] Infrastructure for Data.Tree.AVL.Indexed.* #2968)

  • add : lemmas about balance factors at height 0

  • add: variables; tighten imports

  • fix: qualified module name Function

  • refactor: introduce typedefs, remove parentheses, streamline functions definitions

  • refactor: use of variables; tighten imports

  • tidy up: use of variables; tighten imports

  • fix: CHANGELOG

  • fix: whitespace

  • fix: remove n as a name for height h

  • add: private lemma tree0

  • refactor: rename and deprecate

  • revert: renaming/deprecation

  • fix: more things

  • fix: more things

  • fix: more things

  • fix: final things?

  • tidy up: Properties.Delete

  • tidy up: Properties.Insert

  • tidy up: Properties.HeadTail

  • tidy up: Properties.Lookup

  • tidy up: Properties.LookupFun

  • tidy up: Properties.Singleton

  • refactor: Properties.Join and consolidate as one module

  • add: freshness predicate _#_

  • refactor: consolidate Lookup

  • refactor: use freshness predicate

  • refactor: standardise bound name for a segment l < k < u

  • refactor: split up Join and JoinLemmas

  • refactor: to use JoinLemmas

  • refactor: standardise bound name for a segment l < k < u

  • refactor: standardise notation

  • refactor: use variables

  • refactor: use freshness predicate

  • refactor: cosmetic tweaks

  • fix: imports in Properties

• Revert "[ refactor ] fix Rename lemma satisfied to any⇒satisfiable in *.Relation.Unary.Any #2865 for v2.4 ([ refactor ] fix #2865 for v2.4 #2954)" (Revert "[ refactor ] fix #2865 for v2.4" #2973)
  This reverts commit 7847620.

• [ add ] injectivity of suc for relation m ≡ n (mod o) for {{NonZero o}} ([ add ] injectivity of suc for relation m ≡ n (mod o) for {{NonZero o}} #2971)

  • [ add ] proof of Carette's Lemma

  • refactor: remove simple lemmas

  • add: one half of the equivalence

  • refactor: in terms of _on_ and _⇒_; introduce name for equality mod o

  • add: new lemmas relating SymClosure and on

  • use: new lemmas

  • rename: according to review comments

  • change notation, following review comments

  • chnage comment text to reflect the analysis better

  • refactor: in terms of wlog

  • refactor: export Jacques' lemma; leave Alex' proof private

  • refactor: comment out the wlog proof; tidy up the presentation

  • removed wlog proof

  • refactor: appeal to Sum elimination, rather than with

  • Remove Zulip reference

  ---

  Co-authored-by: Matthew Daggitt matthewdaggitt@gmail.com

• [ fix ] typo in deprecation warning ([ fix ] typo in deprecation warning #2979)
  Fixes Rational.Unnormalized incorrect warning #2978

• [ fix ] CHANGELOG ahead of v2.4 ([ fix ] CHANGELOG ahead of v2.4 #2974)

  • [ fix ] CHANGELOG

  • fix: 'weird quotes', plus some more reordering

  • fix: stupid unfolding of a definition in lemma statement

• agda-stdlib-utils: allow base-4.22 for GHC 9.14