Skip to content

Commit

Permalink
[fixes #2178] regularise and specify/systematise, the conventions for…
Browse files Browse the repository at this point in the history 
… symbol usage (#2185)

* regularise and specify/systematise, the conventions for symbol usage

* typos/revisions
  • Loading branch information
@jamesmckinna @andreasabel
jamesmckinna authored and andreasabel committed Jul 10, 2024
1 parent d8cd956 commit 67ff824
Show file tree
Hide file tree
Showing 4 changed files with 216 additions and 178 deletions.
54 changes: 27 additions & 27 deletions CHANGELOG.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -112,21 +112,21 @@ Non-backwards compatible changes
always true and cannot be assumed in user's code.

* Therefore the definitions have been changed as follows to make all their arguments explicit:
- `LeftCancellative _•_`
- From: `∀ x {y z} → (x • y) ≈ (x • z) → y ≈ z`
- To: `∀ x y z → (x • y) ≈ (x • z) → y ≈ z`
- `LeftCancellative _∙_`
- From: `∀ x {y z} → (x ∙ y) ≈ (x ∙ z) → y ≈ z`
- To: `∀ x y z → (x ∙ y) ≈ (x ∙ z) → y ≈ z`

- `RightCancellative _•_`
- From: `∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z`
- To: `∀ x y z → (y • x) ≈ (z • x) → y ≈ z`
- `RightCancellative _∙_`
- From: `∀ {x} y z → (y ∙ x) ≈ (z ∙ x) → y ≈ z`
- To: `∀ x y z → (y ∙ x) ≈ (z ∙ x) → y ≈ z`

- `AlmostLeftCancellative e _•_`
- From: `∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z`
- To: `∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z`
- `AlmostLeftCancellative e _∙_`
- From: `∀ {x} y z → ¬ x ≈ e → (x ∙ y) ≈ (x ∙ z) → y ≈ z`
- To: `∀ x y z → ¬ x ≈ e → (x ∙ y) ≈ (x ∙ z) → y ≈ z`

- `AlmostRightCancellative e _•_`
- From: `∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z`
- To: `∀ x y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z`
- `AlmostRightCancellative e _∙_`
- From: `∀ {x} y z → ¬ x ≈ e → (y ∙ x) ≈ (z ∙ x) → y ≈ z`
- To: `∀ x y z → ¬ x ≈ e → (y ∙ x) ≈ (z ∙ x) → y ≈ z`

* Correspondingly some proofs of the above types will need additional arguments passed explicitly.
Instances can easily be fixed by adding additional underscores, e.g.
Expand Down Expand Up @@ -2152,16 +2152,16 @@ Additions to existing modules

* Added new proofs to `Algebra.Consequences.Propositional`:
```agda
comm+assoc⇒middleFour : Commutative _•_ → Associative _•_ → _•_ MiddleFourExchange _•_
identity+middleFour⇒assoc : Identity e _•_ → _•_ MiddleFourExchange _•_ → Associative _•_
identity+middleFour⇒comm : Identity e _+_ → _•_ MiddleFourExchange _+_ → Commutative _•_
comm+assoc⇒middleFour : Commutative _∙_ → Associative _∙_ → _∙_ MiddleFourExchange _∙_
identity+middleFour⇒assoc : Identity e _∙_ → _∙_ MiddleFourExchange _∙_ → Associative _∙_
identity+middleFour⇒comm : Identity e _+_ → _∙_ MiddleFourExchange _+_ → Commutative _∙_
```

* Added new proofs to `Algebra.Consequences.Setoid`:
```agda
comm+assoc⇒middleFour : Congruent₂ _•_ → Commutative _•_ → Associative _•_ → _•_ MiddleFourExchange _•_
identity+middleFour⇒assoc : Congruent₂ _•_ → Identity e _•_ → _•_ MiddleFourExchange _•_ → Associative _•_
identity+middleFour⇒comm : Congruent₂ _•_ → Identity e _+_ → _•_ MiddleFourExchange _+_ → Commutative _•_
comm+assoc⇒middleFour : Congruent₂ _∙_ → Commutative _∙_ → Associative _∙_ → _∙_ MiddleFourExchange _∙_
identity+middleFour⇒assoc : Congruent₂ _∙_ → Identity e _∙_ → _∙_ MiddleFourExchange _∙_ → Associative _∙_
identity+middleFour⇒comm : Congruent₂ _∙_ → Identity e _+_ → _∙_ MiddleFourExchange _+_ → Commutative _∙_
involutive⇒surjective : Involutive f → Surjective f
selfInverse⇒involutive : SelfInverse f → Involutive f
Expand All @@ -2171,15 +2171,15 @@ Additions to existing modules
selfInverse⇒injective : SelfInverse f → Injective f
selfInverse⇒bijective : SelfInverse f → Bijective f
comm+idˡ⇒id : Commutative _•_ → LeftIdentity e _•_ → Identity e _•_
comm+idʳ⇒id : Commutative _•_ → RightIdentity e _•_ → Identity e _•_
comm+zeˡ⇒ze : Commutative _•_ → LeftZero e _•_ → Zero e _•_
comm+zeʳ⇒ze : Commutative _•_ → RightZero e _•_ → Zero e _•_
comm+invˡ⇒inv : Commutative _•_ → LeftInverse e _⁻¹ _•_ → Inverse e _⁻¹ _•_
comm+invʳ⇒inv : Commutative _•_ → RightInverse e _⁻¹ _•_ → Inverse e _⁻¹ _•_
comm+distrˡ⇒distr : Commutative _•_ → _•_ DistributesOverˡ _◦_ → _•_ DistributesOver _◦_
comm+distrʳ⇒distr : Commutative _•_ → _•_ DistributesOverʳ _◦_ → _•_ DistributesOver _◦_
distrib+absorbs⇒distribˡ : Associative _•_ → Commutative _◦_ → _•_ Absorbs _◦_ → _◦_ Absorbs _•_ → _◦_ DistributesOver _•_ → _•_ DistributesOverˡ _◦_
comm+idˡ⇒id : Commutative _∙_ → LeftIdentity e _∙_ → Identity e _∙_
comm+idʳ⇒id : Commutative _∙_ → RightIdentity e _∙_ → Identity e _∙_
comm+zeˡ⇒ze : Commutative _∙_ → LeftZero e _∙_ → Zero e _∙_
comm+zeʳ⇒ze : Commutative _∙_ → RightZero e _∙_ → Zero e _∙_
comm+invˡ⇒inv : Commutative _∙_ → LeftInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_
comm+invʳ⇒inv : Commutative _∙_ → RightInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_
comm+distrˡ⇒distr : Commutative _∙_ → _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOver _◦_
comm+distrʳ⇒distr : Commutative _∙_ → _∙_ DistributesOverʳ _◦_ → _∙_ DistributesOver _◦_
distrib+absorbs⇒distribˡ : Associative _∙_ → Commutative _◦_ → _∙_ Absorbs _◦_ → _◦_ Absorbs _∙_ → _◦_ DistributesOver _∙_ → _∙_ DistributesOverˡ _◦_
```

* Added new functions to `Algebra.Construct.DirectProduct`:
Expand Down
44 changes: 41 additions & 3 deletions notes/style-guide.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -347,12 +347,12 @@ line of code, indented by two spaces.

#### Variables

* `Level` and `Set`s can always be generalized using the keyword `variable`.
* `Level` and `Set`s can always be generalised using the keyword `variable`.

* A file may only declare variables of other types if those types are used
in the definition of the main type that the file concerns itself with.
At the moment the policy is *not* to generalize over any other types to
minimize the amount of information that users have to keep in their head
At the moment the policy is *not* to generalise over any other types to
minimise the amount of information that users have to keep in their head
concurrently.

* Example 1: the main type in `Data.List.Properties` is `List A` where `A : Set a`.
Expand Down Expand Up @@ -443,6 +443,44 @@ word within a compound word is capitalized except for the first word.
relations should be used over the `¬` symbol (e.g. `m+n≮n` should be
used instead of `¬m+n<n`).

#### Symbols for operators and relations

* The stdlib aims to use a consistent set of notations, governed by a
consistent set of conventions, but sometimes, different
Unicode/emacs-input-method symbols nevertheless can be rendered by
identical-*seeming* symbols, so this is an attempt to document these.

* The typical binary operator in the `Algebra` hierarchy, inheriting
from the root `Structure`/`Bundle` `isMagma`/`Magma`, is written as
infix `∙`, obtained as `\.`, NOT as `\bu2`. Nevertheless, there is
also a 'generic' operator, written as infix `·`, obtained as
`\cdot`. Do NOT attempt to use related, but typographically
indistinguishable, symbols.

* Similarly, 'primed' names and symbols, used to standardise names
apart, or to provide (more) simply-typed versions of
dependently-typed operations, should be written using `\'`, NOT the
unmarked `'` character.

* Likewise, standard infix symbols for eg, divisibility on numeric
datatypes/algebraic structure, should be written `\|`, NOT the
unmarked `|` character. An exception to this is the *strict*
ordering relation, written using `<`, NOT `\<` as might be expected.

* Since v2.0, the `Algebra` hierarchy systematically introduces
consistent symbolic notation for the negated versions of the usual
binary predicates for equality, ordering etc. These are obtained
from the corresponding input sequence by adding `n` to the symbol
name, so that `≤`, obtained as `\le`, becomes `≰` obtained as
`\len`, etc.

* Correspondingly, the flipped symbols (and their negations) for the
converse relations are systematically introduced, eg `≥` as `\ge`
and `≱` as `\gen`.

* Any exceptions to these conventions should be flagged on the GitHub
`agda-stdlib` issue tracker in the usual way.

#### Functions and relations over specific datatypes

* When defining a new relation `P` over a datatype `X` in a `Data.X.Relation` module,
Expand Down
54 changes: 27 additions & 27 deletions src/Algebra/Consequences/Propositional.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,16 +44,16 @@ open Base public
------------------------------------------------------------------------
-- Group-like structures

module _ {_•_ _⁻¹ ε} where
module _ {_∙_ _⁻¹ ε} where

assoc+id+invʳ⇒invˡ-unique : Associative _•_ → Identity ε _•_ →
RightInverse ε _⁻¹ _•_ →
∀ x y → (x • y) ≡ ε → x ≡ (y ⁻¹)
assoc+id+invʳ⇒invˡ-unique : Associative _∙_ → Identity ε _∙_ →
RightInverse ε _⁻¹ _∙_ →
∀ x y → (x ∙ y) ≡ ε → x ≡ (y ⁻¹)
assoc+id+invʳ⇒invˡ-unique = Base.assoc+id+invʳ⇒invˡ-unique (cong₂ _)

assoc+id+invˡ⇒invʳ-unique : Associative _•_ → Identity ε _•_ →
LeftInverse ε _⁻¹ _•_ →
∀ x y → (x • y) ≡ ε → y ≡ (x ⁻¹)
assoc+id+invˡ⇒invʳ-unique : Associative _∙_ → Identity ε _∙_ →
LeftInverse ε _⁻¹ _∙_ →
∀ x y → (x ∙ y) ≡ ε → y ≡ (x ⁻¹)
assoc+id+invˡ⇒invʳ-unique = Base.assoc+id+invˡ⇒invʳ-unique (cong₂ _)

------------------------------------------------------------------------
Expand All @@ -76,43 +76,43 @@ module _ {_+_ _*_ -_ 0#} where
------------------------------------------------------------------------
-- Bisemigroup-like structures

module _ {_•_ _◦_ : Op₂ A} (•-comm : Commutative _•_) where
module _ {_∙_ _◦_ : Op₂ A} (∙-comm : Commutative _∙_) where

comm+distrˡ⇒distrʳ : _•_ DistributesOverˡ _◦_ → _•_ DistributesOverʳ _◦_
comm+distrˡ⇒distrʳ = Base.comm+distrˡ⇒distrʳ (cong₂ _) •-comm
comm+distrˡ⇒distrʳ : _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_
comm+distrˡ⇒distrʳ = Base.comm+distrˡ⇒distrʳ (cong₂ _) ∙-comm

comm+distrʳ⇒distrˡ : _•_ DistributesOverʳ _◦_ → _•_ DistributesOverˡ _◦_
comm+distrʳ⇒distrˡ = Base.comm+distrʳ⇒distrˡ (cong₂ _) •-comm
comm+distrʳ⇒distrˡ : _∙_ DistributesOverʳ _◦_ → _∙_ DistributesOverˡ _◦_
comm+distrʳ⇒distrˡ = Base.comm+distrʳ⇒distrˡ (cong₂ _) ∙-comm

comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y • z)) ≡ ((x ◦ y) • (x ◦ z)))
comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _◦_) •-comm
comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y ∙ z)) ≡ ((x ◦ y) ∙ (x ◦ z)))
comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _◦_) ∙-comm

------------------------------------------------------------------------
-- Selectivity

module _ {_•_ : Op₂ A} where
module _ {_∙_ : Op₂ A} where

sel⇒idem : Selective _•_ → Idempotent _•_
sel⇒idem : Selective _∙_ → Idempotent _∙_
sel⇒idem = Base.sel⇒idem _≡_

------------------------------------------------------------------------
-- Middle-Four Exchange

module _ {_•_ : Op₂ A} where
module _ {_∙_ : Op₂ A} where

comm+assoc⇒middleFour : Commutative _•_ → Associative _•_ →
_•_ MiddleFourExchange _•_
comm+assoc⇒middleFour = Base.comm+assoc⇒middleFour (cong₂ _•_)
comm+assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
_∙_ MiddleFourExchange _∙_
comm+assoc⇒middleFour = Base.comm+assoc⇒middleFour (cong₂ _∙_)

identity+middleFour⇒assoc : {e : A} → Identity e _•_ →
_•_ MiddleFourExchange _•_ →
Associative _•_
identity+middleFour⇒assoc = Base.identity+middleFour⇒assoc (cong₂ _•_)
identity+middleFour⇒assoc : {e : A} → Identity e _∙_ →
_∙_ MiddleFourExchange _∙_ →
Associative _∙_
identity+middleFour⇒assoc = Base.identity+middleFour⇒assoc (cong₂ _∙_)

identity+middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
_•_ MiddleFourExchange _+_ →
Commutative _•_
identity+middleFour⇒comm = Base.identity+middleFour⇒comm (cong₂ _•_)
_∙_ MiddleFourExchange _+_ →
Commutative _∙_
identity+middleFour⇒comm = Base.identity+middleFour⇒comm (cong₂ _∙_)

------------------------------------------------------------------------
-- Without Loss of Generality
Expand Down
Loading

0 comments on commit 67ff824

Please sign in to comment.