------------------------------------------------------------------------
-- The Agda standard library
--
-- Divisibility over magmas
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (Magma)
module Algebra.Properties.Magma.Divisibility {a ℓ} (M : Magma a ℓ) where
open import Data.Product.Base using (_,_; swap)
open import Relation.Binary.Definitions
using (_Respects_; _Respectsˡ_; _Respectsʳ_; _Respects₂_; Symmetric)
open import Relation.Nullary.Negation.Core using (contradiction)
open Magma M
------------------------------------------------------------------------
-- Re-export divisibility relations publicly
open import Algebra.Definitions.RawMagma rawMagma public
using (_∣_; _∤_; _∥_; _∦_; _∣ˡ_; _∤ˡ_; _∣ʳ_; _∤ʳ_; _,_)
------------------------------------------------------------------------
-- Properties of right divisibility
∣ʳ-respʳ-≈ : _∣ʳ_ Respectsʳ _≈_
∣ʳ-respʳ-≈ y≈z (q , qx≈y) = q , trans qx≈y y≈z
∣ʳ-respˡ-≈ : _∣ʳ_ Respectsˡ _≈_
∣ʳ-respˡ-≈ x≈z (q , qx≈y) = q , trans (∙-congˡ (sym x≈z)) qx≈y
∣ʳ-resp-≈ : _∣ʳ_ Respects₂ _≈_
∣ʳ-resp-≈ = ∣ʳ-respʳ-≈ , ∣ʳ-respˡ-≈
x∣ʳyx : ∀ x y → x ∣ʳ y ∙ x
x∣ʳyx x y = y , refl
xy≈z⇒y∣ʳz : ∀ x y {z} → x ∙ y ≈ z → y ∣ʳ z
xy≈z⇒y∣ʳz x y xy≈z = x , xy≈z
------------------------------------------------------------------------
-- Properties of left divisibility
∣ˡ-respʳ-≈ : _∣ˡ_ Respectsʳ _≈_
∣ˡ-respʳ-≈ y≈z (q , xq≈y) = q , trans xq≈y y≈z
∣ˡ-respˡ-≈ : _∣ˡ_ Respectsˡ _≈_
∣ˡ-respˡ-≈ x≈z (q , xq≈y) = q , trans (∙-congʳ (sym x≈z)) xq≈y
∣ˡ-resp-≈ : _∣ˡ_ Respects₂ _≈_
∣ˡ-resp-≈ = ∣ˡ-respʳ-≈ , ∣ˡ-respˡ-≈
x∣ˡxy : ∀ x y → x ∣ˡ x ∙ y
x∣ˡxy x y = y , refl
xy≈z⇒x∣ˡz : ∀ x y {z} → x ∙ y ≈ z → x ∣ˡ z
xy≈z⇒x∣ˡz x y xy≈z = y , xy≈z
------------------------------------------------------------------------
-- Properties of non-divisibility
∤-respˡ-≈ : _∤_ Respectsˡ _≈_
∤-respˡ-≈ x≈y x∤z y∣ʳz = contradiction (∣ʳ-respˡ-≈ (sym x≈y) y∣ʳz) x∤z
∤-respʳ-≈ : _∤_ Respectsʳ _≈_
∤-respʳ-≈ x≈y z∤x z∣ʳy = contradiction (∣ʳ-respʳ-≈ (sym x≈y) z∣ʳy) z∤x
∤-resp-≈ : _∤_ Respects₂ _≈_
∤-resp-≈ = ∤-respʳ-≈ , ∤-respˡ-≈
------------------------------------------------------------------------
-- Properties of mutual divisibility _∥_
∥-sym : Symmetric _∥_
∥-sym = swap
∥-respˡ-≈ : _∥_ Respectsˡ _≈_
∥-respˡ-≈ x≈z (x∣ʳy , y∣ʳx) = ∣ʳ-respˡ-≈ x≈z x∣ʳy , ∣ʳ-respʳ-≈ x≈z y∣ʳx
∥-respʳ-≈ : _∥_ Respectsʳ _≈_
∥-respʳ-≈ y≈z (x∣ʳy , y∣ʳx) = ∣ʳ-respʳ-≈ y≈z x∣ʳy , ∣ʳ-respˡ-≈ y≈z y∣ʳx
∥-resp-≈ : _∥_ Respects₂ _≈_
∥-resp-≈ = ∥-respʳ-≈ , ∥-respˡ-≈
------------------------------------------------------------------------
-- Properties of mutual non-divisibility _∤∤_
∦-sym : Symmetric _∦_
∦-sym x∦y y∥x = contradiction (∥-sym y∥x) x∦y
∦-respˡ-≈ : _∦_ Respectsˡ _≈_
∦-respˡ-≈ x≈y x∦z y∥z = contradiction (∥-respˡ-≈ (sym x≈y) y∥z) x∦z
∦-respʳ-≈ : _∦_ Respectsʳ _≈_
∦-respʳ-≈ x≈y z∦x z∥y = contradiction (∥-respʳ-≈ (sym x≈y) z∥y) z∦x
∦-resp-≈ : _∦_ Respects₂ _≈_
∦-resp-≈ = ∦-respʳ-≈ , ∦-respˡ-≈
------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
-- Version 2.2
∣-respˡ = ∣ʳ-respˡ-≈
{-# WARNING_ON_USAGE ∣-respˡ
"Warning: ∣-respˡ was deprecated in v2.2.
Please use ∣ʳ-respˡ-≈ instead. "
#-}
∣-respʳ = ∣ʳ-respʳ-≈
{-# WARNING_ON_USAGE ∣-respʳ
"Warning: ∣-respʳ was deprecated in v2.2.
Please use ∣ʳ-respʳ-≈ instead. "
#-}
∣-resp = ∣ʳ-resp-≈
{-# WARNING_ON_USAGE ∣-resp
"Warning: ∣-resp was deprecated in v2.2.
Please use ∣ʳ-resp-≈ instead. "
#-}
-- Version 2.3
∣∣-sym = ∥-sym
{-# WARNING_ON_USAGE ∣∣-sym
"Warning: ∣∣-sym was deprecated in v2.3.
Please use ∥-sym instead. "
#-}
∣∣-respˡ-≈ = ∥-respˡ-≈
{-# WARNING_ON_USAGE ∣∣-respˡ-≈
"Warning: ∣∣-respˡ-≈ was deprecated in v2.3.
Please use ∥-respˡ-≈ instead. "
#-}
∣∣-respʳ-≈ = ∥-respʳ-≈
{-# WARNING_ON_USAGE ∣∣-respʳ-≈
"Warning: ∣∣-respʳ-≈ was deprecated in v2.3.
Please use ∥-respʳ-≈ instead. "
#-}
∣∣-resp-≈ = ∥-resp-≈
{-# WARNING_ON_USAGE ∣∣-resp-≈
"Warning: ∣∣-resp-≈ was deprecated in v2.3.
Please use ∥-resp-≈ instead. "
#-}
∤∤-sym = ∦-sym
{-# WARNING_ON_USAGE ∤∤-sym
"Warning: ∤∤-sym was deprecated in v2.3.
Please use ∦-sym instead. "
#-}
∤∤-respˡ-≈ = ∦-respˡ-≈
{-# WARNING_ON_USAGE ∤∤-respˡ-≈
"Warning: ∤∤-respˡ-≈ was deprecated in v2.3.
Please use ∦-respˡ-≈ instead. "
#-}
∤∤-respʳ-≈ = ∦-respʳ-≈
{-# WARNING_ON_USAGE ∤∤-respʳ-≈
"Warning: ∤∤-respʳ-≈ was deprecated in v2.3.
Please use ∦-respʳ-≈ instead. "
#-}
∤∤-resp-≈ = ∦-resp-≈
{-# WARNING_ON_USAGE ∤∤-resp-≈
"Warning: ∤∤-resp-≈ was deprecated in v2.3.
Please use ∦-resp-≈ instead. "
#-}
∣-respʳ-≈ = ∣ʳ-respʳ-≈
{-# WARNING_ON_USAGE ∣-respʳ-≈
"Warning: ∣-respʳ-≈ was deprecated in v2.3.
Please use ∣ʳ-respʳ-≈ instead. "
#-}
∣-respˡ-≈ = ∣ʳ-respˡ-≈
{-# WARNING_ON_USAGE ∣-respˡ-≈
"Warning: ∣-respˡ-≈ was deprecated in v2.3.
Please use ∣ʳ-respˡ-≈ instead. "
#-}
∣-resp-≈ = ∣ʳ-resp-≈
{-# WARNING_ON_USAGE ∣-resp-≈
"Warning: ∣-resp-≈ was deprecated in v2.3.
Please use ∣ʳ-resp-≈ instead. "
#-}
x∣yx = x∣ʳyx
{-# WARNING_ON_USAGE x∣yx
"Warning: x∣yx was deprecated in v2.3.
Please use x∣ʳyx instead. "
#-}
xy≈z⇒y∣z = xy≈z⇒y∣ʳz
{-# WARNING_ON_USAGE xy≈z⇒y∣z
"Warning: xy≈z⇒y∣z was deprecated in v2.3.
Please use xy≈z⇒y∣ʳz instead. "
#-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4