Updated for 46e60fd

docs/Algebra/Literals.agda

@@ -0,0 +1,27 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Algebra.Literals where
+
+open import Algebra
+
+open import Agda.Builtin.FromNat
+open import Agda.Builtin.FromNeg
+open import Level
+
+variable a b : Level
+
+module Semiring-Lit (R : Semiring a b) where
+  open Semiring R
+
+  open import Data.Unit.Polymorphic
+  open import Data.Nat using (ℕ; zero; suc)
+
+  private
+    ℕ→R : ℕ → Carrier
+    ℕ→R zero    = 0#
+    ℕ→R (suc n) = 1# + ℕ→R n
+
+  instance
+    number : Number Carrier
+    number .Number.Constraint = λ _ → ⊤
+    number .fromNat           = λ n → ℕ→R n

docs/Algebra/PairOp.agda

@@ -0,0 +1,55 @@
+{-# OPTIONS --safe #-}
+
+open import Prelude
+
+open import Algebra
+open import Data.Product.Relation.Binary.Pointwise.NonDependent
+open import Relation.Binary
+
+module Algebra.PairOp (X : Type) (ε : X) (_≈_ : Rel X zeroˡ) (_∙_ : Op₂ X) where
+
+_∙ᵖ_ : (X × X) → (X × X) → (X × X)
+(a , b) ∙ᵖ (c , d) = (a ∙ c) , (b ∙ d)
+
+_≈ᵖ_ : Rel (X × X) zeroˡ
+_≈ᵖ_ = Pointwise _≈_ _≈_
+
+pairOpIdentityˡ :
+  Algebra.LeftIdentity _≈_ ε _∙_ → Algebra.LeftIdentity _≈ᵖ_ (ε , ε) _∙ᵖ_
+pairOpIdentityˡ idˡ (a , b) = ×-refl (idˡ a) (idˡ b) {ε , ε}
+
+pairOpIdentityʳ :
+  Algebra.RightIdentity _≈_ ε _∙_ → Algebra.RightIdentity _≈ᵖ_ (ε , ε) _∙ᵖ_
+pairOpIdentityʳ idʳ (a , b) = ×-refl (idʳ a) (idʳ b) {ε , ε}
+
+pairOpIdentity : Algebra.Identity _≈_ ε _∙_ → Algebra.Identity _≈ᵖ_ (ε , ε) _∙ᵖ_
+pairOpIdentity (idˡ , idʳ) = (pairOpIdentityˡ idˡ) , (pairOpIdentityʳ idʳ)
+
+pairOpAssoc : Algebra.Associative  _≈_ _∙_ →  Algebra.Associative _≈ᵖ_ _∙ᵖ_
+pairOpAssoc assoc (a , b) (c , d) (e , f) =
+  ×-refl (assoc a c e) (assoc b d f) {ε , ε}
+
+pairOpIsMonoid : IsMonoid _≈_ _∙_ ε →  IsMonoid _≈ᵖ_ _∙ᵖ_ (ε , ε)
+pairOpIsMonoid record { isSemigroup = isSemigroup ; identity = identity } = record
+  { isSemigroup = record
+    { isMagma = record
+      { isEquivalence = ×-isEquivalence
+          (IsMagma.isEquivalence (IsSemigroup.isMagma isSemigroup))
+          (IsMagma.isEquivalence (IsSemigroup.isMagma isSemigroup))
+      ; ∙-cong = λ (p , q) (p′ , q′)
+          → IsMagma.∙-cong (IsSemigroup.isMagma isSemigroup) p p′
+          , IsMagma.∙-cong (IsSemigroup.isMagma isSemigroup) q q′
+      }
+    ; assoc = pairOpAssoc (IsSemigroup.assoc isSemigroup)
+    }
+  ; identity = pairOpIdentity identity
+  }
+
+pairOpComm : Algebra.Commutative _≈_ _∙_ → Algebra.Commutative _≈ᵖ_ _∙ᵖ_
+pairOpComm comm (a , b) (c , d) =
+  ×-refl (comm a c) (comm b d) {ε , ε}
+
+pairOpRespectsComm :
+  IsCommutativeMonoid _≈_ _∙_ ε → IsCommutativeMonoid _≈ᵖ_ _∙ᵖ_ (ε , ε)
+pairOpRespectsComm record { isMonoid = isMonoid ; comm = comm } = record
+  { isMonoid = pairOpIsMonoid isMonoid ; comm = pairOpComm comm }

docs/Data/Integer/Ext.agda

@@ -0,0 +1,29 @@
+{-# OPTIONS --safe #-}
+
+module Data.Integer.Ext where
+
+open import Data.Integer
+open import Data.Integer.Properties using ([1+m]⊖[1+n]≡m⊖n)
+open import Data.Nat
+open import Data.Product
+open import Data.Sign
+open import Relation.Binary.PropositionalEquality using (_≡_; sym; cong; trans)
+
+ℤtoSignedℕ : ℤ → Sign × ℕ
+ℤtoSignedℕ x = (sign x , ∣ x ∣)
+
+posPart : ℤ → ℕ
+posPart x with ℤtoSignedℕ x
+... | (Sign.+ , x) = x
+... | _            = 0
+
+negPart : ℤ → ℕ
+negPart x with ℤtoSignedℕ x
+... | (Sign.- , x) = x
+... | _            = 0
+
+∸≡posPart⊖ : {m n : ℕ} → (m ∸ n) ≡ posPart (m ⊖ n)
+∸≡posPart⊖ {zero} {zero} = _≡_.refl
+∸≡posPart⊖ {zero} {ℕ.suc n} = _≡_.refl
+∸≡posPart⊖ {ℕ.suc m} {zero} = _≡_.refl
+∸≡posPart⊖ {ℕ.suc m} {ℕ.suc n} = trans (∸≡posPart⊖{m}{n}) (sym (cong posPart (([1+m]⊖[1+n]≡m⊖n m n))))

docs/Data/List/Ext.agda

@@ -0,0 +1,51 @@
+{-# OPTIONS --safe #-}
+module Data.List.Ext where
+
+open import Agda.Primitive using () renaming (Set to Type)
+
+open import Data.List using (List; _++_; map; concatMap; filter)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Membership.Propositional.Properties using (∈-map⁻; ∈-map⁺; ∈-filter⁻; ∈-filter⁺)
+open import Data.Maybe using (Maybe)
+open import Data.Nat using (ℕ)
+open import Data.Product using (∃-syntax; _×_; _,_; proj₁; proj₂)
+open import Function.Bundles using (_⇔_; mk⇔; Equivalence)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Unary using (Decidable)
+open Maybe; open List; open ℕ
+private variable
+  ℓ : Level
+  A B : Type ℓ
+
+-- Looking up an index into the list; fails when out-of-bounds.
+_⁉_ : List A → ℕ → Maybe A
+[]       ⁉ _     = nothing
+(x ∷ _)  ⁉ zero  = just x
+(_ ∷ xs) ⁉ suc n = xs ⁉ n
+
+-- sublists of the given list
+sublists : List A → List (List A)
+sublists []       = [] ∷ []
+sublists (x ∷ xs) = map (x ∷_) (sublists xs) ++ sublists xs
+
+-- insert the given element in every position of the given list
+insert : A → List A → List (List A)
+insert x [] = (x ∷ []) ∷ []
+insert x (y ∷ ys) = (x ∷ y ∷ ys) ∷ map (y ∷_) (insert x ys)
+
+-- permutations of all sublists of the given list
+subpermutations : List A → List (List A)
+subpermutations [] = [] ∷ []
+subpermutations (x ∷ xs) = concatMap (insert x) (subpermutations xs) ++ subpermutations xs
+
+module _ {f : A → B} {l : List A} {b} {P : A → Type} {P? : Decidable P} where
+  ∈ˡ-map-filter⁻ : b ∈ map f (filter P? l) → (∃[ a ] a ∈ l × b ≡ f a × P a)
+  ∈ˡ-map-filter⁻ h with ∈-map⁻ f h
+  ... | a , a∈X , _≡_.refl = a , proj₁ (∈-filter⁻ P? a∈X) , _≡_.refl , proj₂ (∈-filter⁻ P? {xs = l} a∈X)
+
+  ∈ˡ-map-filter⁺ : (∃[ a ] a ∈ l × b ≡ f a × P a) → b ∈ map f (filter P? l)
+  ∈ˡ-map-filter⁺ (a , a∈l , _≡_.refl , Pa) = ∈-map⁺ f (∈-filter⁺ P? a∈l Pa)
+
+  ∈ˡ-map-filter : (∃[ a ] a ∈ l × b ≡ f a × P a) ⇔ b ∈ map f (filter P? l)
+  ∈ˡ-map-filter = mk⇔ ∈ˡ-map-filter⁺ ∈ˡ-map-filter⁻