on lib-2.2-rc1

[mechvel]

I have tested it under
Agda 2.7.0.1 built with flags (cabal -f optimise-heavily)
ghc-9.0.2. Debian Linux 12
on my large library of computer algebra.

It works all right.
Please, find my remarks below.

• Algebra.Definitions.RawMagma defines

x ∤∤ y = ¬ x ∣∣ y                                                               

I doubt, may be it is better to denote this ¬∣∣.
Because seeing x ∤∤ y the reader could think of "neither x ∣ y nor y ∣ x".

---

Data.List.Base:

deduplicate : ∀ {R : Rel A p} → B.Decidable R → List A → List A                 

The names take, drop, span, takeWhile, filter ... come from the Haskell library.
And deduplicate corresponds to nub of Haskell library.
Right?
So, I wonder of whether deduplicate needs to be renamed to nub
(also I do not know the mnemonic of the name nub).

It is also needed a proof for the main properties of deduplicate, the ones that explain why this function is needed:
(a) ys = (deduplicate xs) and xs need to be equal as sets (to be subsets of each other),
(b) ys must not have repetitions.

For example, I have in my library

  data AnyRelates (_~_ : Rel A β) :  Pred (List A) (α ⊔ β)                      
       where                                                                    
       here  :  ∀ {x xs} → Any (x ~_) xs → AnyRelates _~_ (x ∷ xs)              
       there :  ∀ {x xs} → AnyRelates _~_ xs → AnyRelates _~_ (x ∷ xs)          
                                                                                                               
AnyRepeats : Pred (List C) (α ⊔ α≈)     -- over a Setoid                          
AnyRepeats = AnyRelates _≈_                                                     
                                                                                
Over DecSetoid:                                                                 
nub :  (xs : List C) → Σ (List C) (\ys → (xs =ₛ ys) × ¬ AnyRepeats ys)          

---

Why is it introduced ∃[ x ] (P x)
while it is provided ∃ (\x → P x) ?
Is the former simpler? It looks like multiplying entities.

---

Data.List.Properties:

product≢0 : All NonZero ns → NonZero (product ns)                               

It is better to treat the thing in a general way.
To introduce IntegralSemiring (a semiring without zero divisor). It is Semiring with the axiom

∀ {x y} → x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0#   -- (I)                                 

For example, ℕ and ℤ/(3) (integers modulo 3) are integral semirings,
while ℕ × ℕ and ℤ/(4) are not.

Then, ℕ and ℤ have the IntegralSemiring instance proved in a simple way.
And
product≢0 : All NonZero xs → NonZero (product xs)
is proved for any IntegralSemiring also in a simple way.

The notion (I) is as important and as simply expressed and as widely used in algebra as, for example, the notion of
Commutative.
In classical algebra the notion IntegralDomain means CommutativeRing with the property (I).
Also it has sense to introduce is the property

LeftZeroDivisor x =  x ≉ 0# × ∃ (\y → y ≉ 0# × x * y ≈ 0#)                      

And the property (I) itself is called "a semiring without zero divisor".
So,

• the term IntegralDomain is occupied in algebra (as mentioned above),
• the Agda library can intoduce IntegralSemiring
  (I do not know of whether this term is occupied)
  or
  SemiringWithoutZeroDivisor
  (which surely does not break anything in classical terminology).

[mechvel]

This is in addition to my last message.
About product:
I suggest these items under the environment of Monoid:

C = Carrier

Π₁ : C → List C → C    -- product of a nonempty list of elements
Π₁ x = foldr _∙_ x

Π : List C → C         -- product of a list of elements
Π = Π₁ ε

Π[x] :  ∀ x → Π (x ∷ []) ≈ x
Π[x] =  _∙ε

Π₁cong ...

Π++ :  (xs : List C) {ys : List C} → Π (xs ++ ys) ≈ Π xs ∙ Π ys
...

So, over R : Semiring, there are the two instances of Π.
One is for the additive monoid of R (+-0-monoid ?),
where Π is renamed to sum, ε to 0#.
Another is for the multiplicative monoid of R (*-ε-monoid ?).

And for IntegralSemiring, it will be simple to prove for its multiplicative monoid

∀ {xs} → All (_≉ 0#) xs → Π xs ≉ 0#.

[mechvel]

Also consider
Data.List.Membership.Setoid.Properties:

 ∉[] : ∀ {x} → x ∉ []

Is not it better _∉[] : ∀ x → x ∉ []
?
For example: (1 ∉[]) is read leterally as 1 is not in [].

[JacquesCarette]

Hmm, if ∉[] is new to 2.2, then I agree with Sergei that having this be postfix would be nicer.

[MatthewDaggitt]

• None of _∤∤_, deduplicate, ∃[ x ] (P x) were introduced in v2.2. Therefore while you're welcome to open separate issues to discuss each of these, they will not be changed for v2.2.

• product≢0 : All NonZero ns → NonZero (product ns) - while I agree that it would be good to develop the theory in terms of an appropriate algebraic structure, unfortunately the library is not currently set up to do so. We would need someone to be motivated to make those contributions, but regardless those changes would also not make it into v2.2.

• Agreed ∉[] probably should be _∉[] and can be changed for the release of v2.2

[jamesmckinna]

Previously, @MatthewDaggitt wrote:

* Agreed `∉[]` probably should be `_∉[]` and can be changed for the release of v2.2

I think I do agree also, but two comments regarding this:

• from the point of view of the typechecker, the quantifier can easily be left implicit (and perhaps should); the choice to make the operator postfix changes that to explicit quantification;
• from the point of view of the user, I can see arguments in both directions as to what should be explicit: the occurrence of the argument in the term x ∉[], or only/simply in the type x ∉ []? The former may be justified from a UX perspective as a redundant recoding, provided we accept the need for explicit mention of such terms as (sub)proofs, while the latter makes sense for 'documentation'.

I'm in two minds about the second: is it the case that all/most (for suitable definitions of such quantifiers) named uses of λ() as a proof term, we should encourage/enforce such redundant recoding?

UPDATED: see #2545

If we do merge the associated PR, should we also make the one use of the lemma in the library, viz. in Data.List.Relation.Binary.Subset.Setoid.Properties also have explicit quantification (at least: of x, if not also of xs?):

  ∷⊈[] : ∀ {x xs} → x ∷ xs ⊈ []
  ∷⊈[] p = Membershipₚ._∉[] S _ $ p (here refl)

[jamesmckinna]

Suggest closing this issue after the discussion on #2545 ?

[mechvel]

∷⊈[] : ∀ {x xs} → x ∷ xs ⊈ []

I thought that as x and xs are not bound by any property, it is better to make them explicit.
But I believe the library developers know better.

Suggest closing this issue after the discussion on
#2545 ?

Let the library team decide.

[MatthewDaggitt]

I thought that as x and xs are not bound by any property, it is better to make them explicit.
But I believe the library developers know better.

Yes, but the problem as @jamesmckinna identified is that when the library modules are not fully parameterised then the misfix notation no longer works. In general, the notation we choose should work for both.

[JacquesCarette]

Yes, but the problem as @jamesmckinna identified is that when the library modules are not fully parameterised then the misfix notation no longer works. In general, the notation we choose should work for both.

See #2549 where I disagree with that conclusion.

[jamesmckinna]

∷⊈[] : ∀ {x xs} → x ∷ xs ⊈ []

I thought that as x and xs are not bound by any property, it is better to make them explicit. But I believe the library developers know better.

Thanks @mechvel .

Your choice of words here is interesting, as you say that " x and xs are not bound by any property", but I, on behalf of the typechecker, feel forced to disagree: x and xs are precisely bound by the property x ∷ xs ⊆ [] which is the antecedent of the definitional expansion of x ∷ xs ⊈ []. Much of the power of unification-based type inference/checking comes precisely from being able to avoid spelling out explicitly arguments which can be resynthesised during typechecking, as here. But such a perspective does seem to be in tension with a more orthodox 'mathematical' reading of (statements expressed in) the language of type theory.

It really does seem to be the case that the routine (semantic) expression of ¬ A as A → ⊥, which leads to the above analysis, is at odds with the 'mathematical'/informal'/'syntactic' reading of x ∷ xs ⊈ [] as a positive atomic predicate instance, in which it would make sense to say that x and xs are 'unconstrained', so should be made explicit. As someone originally trained as a mathematician, my instincts incline me towards your reading; but as the type theorist/library developer that I have become, I am very much more firmly on the typechecker's side!
.