Merge branch 'master' into refactor-heyting

Author: jamesmckinna

CHANGELOG.md

@@ -9,6 +9,10 @@ Highlights
 Bug-fixes
 ---------
 
+* In `Algebra.Apartness.Structures`, renamed `sym` from `IsApartnessRelation`
+  to `#-sym` in order to avoid overloaded projection.
+  `irrefl` and `cotrans` are similarly renamed for the sake of consistency.
+
 Non-backwards compatible changes
 --------------------------------
 
@@ -44,7 +48,7 @@ Deprecated names
   _∤∤_    ↦  _∦_
   ```
 
-* In `Algebra.Module.Consequences
+* In `Algebra.Module.Consequences`
   ```agda
   *ₗ-assoc+comm⇒*ᵣ-assoc      ↦  *ₗ-assoc∧comm⇒*ᵣ-assoc
   *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc   ↦  *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc
@@ -162,6 +166,19 @@ Additions to existing modules
   x-0#≈x : RightIdentity 0# _-_
   ```
 
+* In `Data.List.Properties`:
+  ```agda
+  map-applyUpTo : ∀ (f : ℕ → A) (g : A → B) n → map g (applyUpTo f n) ≡ applyUpTo (g ∘ f) n
+  map-applyDownFrom : ∀ (f : ℕ → A) (g : A → B) n → map g (applyDownFrom f n) ≡ applyDownFrom (g ∘ f) n
+  map-upTo : ∀ (f : ℕ → A) n → map f (upTo n) ≡ applyUpTo f n
+  map-downFrom : ∀ (f : ℕ → A) n → map f (downFrom n) ≡ applyDownFrom f n
+  ```
+
+* In `Data.List.Relation.Binary.Permutation.PropositionalProperties`:
+  ```agda
+  filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
+  ```
+
 * In `Relation.Binary.Properties.DecSetoid`:
   ```agda
   ≉-isTightApartnessRelation : IsTightApartnessRelation _≈_ _#_

src/Algebra/Apartness/Structures.agda

@@ -32,6 +32,12 @@ record IsHeytingCommutativeRing : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
 
   open IsCommutativeRing isCommutativeRing public
   open IsTightApartnessRelation isTightApartnessRelation public
+  open IsApartnessRelation isApartnessRelation public
+    renaming
+      ( irrefl  to #-irrefl
+      ; sym     to #-sym
+      ; cotrans to #-cotrans
+      )
 
   ¬#-isEquivalence : IsEquivalence _¬#_
   ¬#-isEquivalence = AR.¬#-isEquivalence refl isApartnessRelation

src/Algebra/Properties/Magma/Divisibility.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra using (Magma)
+open import Algebra.Bundles using (Magma)
 
 module Algebra.Properties.Magma.Divisibility {a ℓ} (M : Magma a ℓ) where
 

src/Algebra/Properties/Monoid/Divisibility.agda

@@ -6,16 +6,17 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra using (Monoid)
+open import Algebra.Bundles using (Monoid)
+
+module Algebra.Properties.Monoid.Divisibility
+  {a ℓ} (M : Monoid a ℓ) where
+
 open import Data.Product.Base using (_,_)
 open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.Bundles using (Preorder)
 open import Relation.Binary.Structures using (IsPreorder; IsEquivalence)
 open import Relation.Binary.Definitions using (Reflexive)
 
-module Algebra.Properties.Monoid.Divisibility
-  {a ℓ} (M : Monoid a ℓ) where
-
 open Monoid M
 
 ------------------------------------------------------------------------
@@ -60,9 +61,9 @@ infix 4 ε∣_
 
 ∥-isEquivalence : IsEquivalence _∥_
 ∥-isEquivalence = record
-  { refl  = λ {x} → ∥-refl {x}
-  ; sym   = λ {x} {y} → ∥-sym {x} {y}
-  ; trans = λ {x} {y} {z} → ∥-trans {x} {y} {z}
+  { refl  = ∥-refl
+  ; sym   = ∥-sym
+  ; trans = ∥-trans
   }
 
 

src/Algebra/Properties/Semigroup/Divisibility.agda

@@ -6,13 +6,14 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra using (Semigroup)
-open import Data.Product.Base using (_,_)
-open import Relation.Binary.Definitions using (Transitive)
+open import Algebra.Bundles using (Semigroup)
 
 module Algebra.Properties.Semigroup.Divisibility
   {a ℓ} (S : Semigroup a ℓ) where
 
+open import Data.Product.Base using (_,_)
+open import Relation.Binary.Definitions using (Transitive)
+
 open Semigroup S
 
 ------------------------------------------------------------------------

src/Algebra/Properties/Semiring/Divisibility.agda

@@ -6,10 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra using (Semiring)
-import Algebra.Properties.Monoid.Divisibility as MonoidDivisibility
-open import Data.Product.Base using (_,_)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Algebra.Bundles using (Semiring)
 
 module Algebra.Properties.Semiring.Divisibility
   {a ℓ} (R : Semiring a ℓ) where
@@ -19,7 +16,7 @@ open Semiring R
 ------------------------------------------------------------------------
 -- Re-exporting divisibility over monoids
 
-open MonoidDivisibility *-monoid public
+open import Algebra.Properties.Monoid.Divisibility *-monoid public
   renaming (ε∣_ to 1∣_)
 
 ------------------------------------------------------------------------
@@ -37,4 +34,4 @@ x∣y∧y≉0⇒x≉0 : ∀ {x y} → x ∣ y → y ≉ 0# → x ≉ 0#
 x∣y∧y≉0⇒x≉0 x∣y y≉0 x≈0 = y≉0 (0∣x⇒x≈0 (∣-respˡ x≈0 x∣y))
 
 0∤1 : 0# ≉ 1# → 0# ∤ 1#
-0∤1 0≉1 (q , q*0≈1) = 0≉1 (trans (sym (zeroʳ q)) q*0≈1)
+0∤1 0≉1 0∣1 = 0≉1 (sym (0∣x⇒x≈0 0∣1))

src/Algebra/Properties/Semiring/Primality.agda

@@ -1,22 +1,29 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Some theory for CancellativeCommutativeSemiring.
+-- Properties of Coprimality and Irreducibility for Semiring.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra using (Semiring)
-open import Data.Sum.Base using (reduce)
-open import Function.Base using (flip)
-open import Relation.Binary.Definitions using (Symmetric)
+open import Algebra.Bundles using (Semiring)
 
 module Algebra.Properties.Semiring.Primality
   {a ℓ} (R : Semiring a ℓ)
   where
 
+open import Data.Sum.Base using (reduce)
+open import Function.Base using (flip)
+open import Relation.Binary.Definitions using (Symmetric)
+
 open Semiring R renaming (Carrier to A)
 open import Algebra.Properties.Semiring.Divisibility R
+  using (_∣_; ∣-trans; 0∤1)
+
+private
+  variable
+    x p : A
+
 
 ------------------------------------------------------------------------
 -- Re-export primality definitions
@@ -30,12 +37,12 @@ open import Algebra.Definitions.RawSemiring rawSemiring public
 Coprime-sym : Symmetric Coprime
 Coprime-sym coprime = flip coprime
 
-∣1⇒Coprime : ∀ {x} y → x ∣ 1# → Coprime x y
-∣1⇒Coprime {x} y x∣1 z∣x _ = ∣-trans z∣x x∣1
+∣1⇒Coprime : ∀ y → x ∣ 1# → Coprime x y
+∣1⇒Coprime _ x∣1 z∣x _ = ∣-trans z∣x x∣1
 
 ------------------------------------------------------------------------
 -- Properties of Irreducible
 
-Irreducible⇒≉0 : 0# ≉ 1# → ∀ {p} → Irreducible p → p ≉ 0#
+Irreducible⇒≉0 : 0# ≉ 1# → Irreducible p → p ≉ 0#
 Irreducible⇒≉0 0≉1 (mkIrred _ chooseInvertible) p≈0 =
   0∤1 0≉1 (reduce (chooseInvertible (trans p≈0 (sym (zeroˡ 0#)))))

src/Data/List/Properties.agda

@@ -842,6 +842,10 @@ applyUpTo-∷ʳ : ∀ (f : ℕ → A) n → applyUpTo f n ∷ʳ f n ≡ applyUpT
 applyUpTo-∷ʳ f zero = refl
 applyUpTo-∷ʳ f (suc n) = cong (f 0 ∷_) (applyUpTo-∷ʳ (f ∘ suc) n)
 
+map-applyUpTo : ∀ (f : ℕ → A) (g : A → B) n → map g (applyUpTo f n) ≡ applyUpTo (g ∘ f) n
+map-applyUpTo f g zero = refl
+map-applyUpTo f g (suc n) = cong (g (f 0) ∷_) (map-applyUpTo (f ∘ suc) g n)
+
 ------------------------------------------------------------------------
 -- applyDownFrom
 
@@ -859,6 +863,10 @@ module _ (f : ℕ → A) where
   applyDownFrom-∷ʳ zero = refl
   applyDownFrom-∷ʳ (suc n) = cong (f (suc n) ∷_) (applyDownFrom-∷ʳ n)
 
+  map-applyDownFrom : ∀ (g : A → B) n → map g (applyDownFrom f n) ≡ applyDownFrom (g ∘ f) n
+  map-applyDownFrom g zero = refl
+  map-applyDownFrom g (suc n) = cong (g (f n) ∷_) (map-applyDownFrom g n)
+
 ------------------------------------------------------------------------
 -- upTo
 
@@ -871,6 +879,9 @@ lookup-upTo = lookup-applyUpTo id
 upTo-∷ʳ : ∀ n → upTo n ∷ʳ n ≡ upTo (suc n)
 upTo-∷ʳ = applyUpTo-∷ʳ id
 
+map-upTo : ∀ (f : ℕ → A) n → map f (upTo n) ≡ applyUpTo f n
+map-upTo = map-applyUpTo id
+
 ------------------------------------------------------------------------
 -- downFrom
 
@@ -883,6 +894,9 @@ lookup-downFrom = lookup-applyDownFrom id
 downFrom-∷ʳ : ∀ n → applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n)
 downFrom-∷ʳ = applyDownFrom-∷ʳ id
 
+map-downFrom : ∀ (f : ℕ → A) n → map f (downFrom n) ≡ applyDownFrom f n
+map-downFrom = map-applyDownFrom id
+
 ------------------------------------------------------------------------
 -- tabulate
 

src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda

@@ -26,7 +26,7 @@ open import Data.Product.Base using (_,_; _×_; ∃; ∃₂)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Function.Base using (_∘_; _⟨_⟩_; _$_)
 open import Level using (Level)
-open import Relation.Unary using (Pred)
+open import Relation.Unary as Pred using (Pred)
 open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
 open import Relation.Binary.Definitions using (_Respects_; Decidable)
 open import Relation.Binary.PropositionalEquality.Core as ≡
@@ -372,6 +372,21 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where
     x ∷ xs ++ y ∷ ys         ∎
     where open PermutationReasoning
 
+------------------------------------------------------------------------
+-- filter
+
+filter-↭ : ∀ {p} {P : Pred A p} (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
+filter-↭ P? refl = refl
+filter-↭ P? (prep x xs↭ys) with P? x
+... | yes _ = prep x (filter-↭ P? xs↭ys)
+... | no _  = filter-↭ P? xs↭ys
+filter-↭ P? (swap x y xs↭ys) with P? x in eqˣ | P? y in eqʸ
+... | yes _ | yes _ rewrite eqˣ rewrite eqʸ = swap x y (filter-↭ P? xs↭ys)
+... | yes _ | no  _ rewrite eqˣ rewrite eqʸ = prep x (filter-↭ P? xs↭ys)
+... | no _  | yes _ rewrite eqˣ rewrite eqʸ = prep y (filter-↭ P? xs↭ys)
+... | no _  | no _  rewrite eqˣ rewrite eqʸ = filter-↭ P? xs↭ys
+filter-↭ P? (trans xs↭ys ys↭zs) = ↭-trans (filter-↭ P? xs↭ys) (filter-↭ P? ys↭zs)
+
 ------------------------------------------------------------------------
 -- catMaybes