From 2ac71e51d2fa41902a235b27f0ccc3ed15dbf99f Mon Sep 17 00:00:00 2001 From: Chris Date: Wed, 22 May 2024 02:58:28 +0100 Subject: [PATCH] Decidable Setoid -> Apartness Relation and Rational Heyting Field (#2194) * new stuff * forgot to add bundles for rational instance of Heyting* * one more (obvious) simplification * a few more simplifications * comments on DecSetoid properties from jamesmckinna * not working, but partially there * woo! * fix anonymous instance * fix errant whitespace * `fix-whitespace` * rectified wrt `contradiction` * rectified `DecSetoid` properties * rectified `Group` properties * inlined lemma; tidied up --------- Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Co-authored-by: James McKinna --- CHANGELOG.md | 23 ++++++- src/Algebra/Properties/Group.agda | 12 ++++ src/Data/Rational/Properties.agda | 60 ++++++++++++++++++- src/Relation/Binary/Properties/DecSetoid.agda | 43 +++++++++++++ src/Relation/Binary/Properties/Setoid.agda | 7 ++- 5 files changed, 139 insertions(+), 6 deletions(-) create mode 100644 src/Relation/Binary/Properties/DecSetoid.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 30dc56b3d0..29839632c7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -145,6 +145,11 @@ New modules Relation.Binary.Construct.Interior.Symmetric ``` +* Properties of `Setoid`s with decidable equality relation: + ``` + Relation.Binary.Properties.DecSetoid + ``` + * Pointwise and equality relations over indexed containers: ```agda Data.Container.Indexed.Relation.Binary.Pointwise @@ -262,6 +267,8 @@ Additions to existing modules //-rightDivides : RightDivides _∙_ _//_ ⁻¹-selfInverse : SelfInverse _⁻¹ + x∙y⁻¹≈ε⇒x≈y : ∀ x y → (x ∙ y ⁻¹) ≈ ε → x ≈ y + x≈y⇒x∙y⁻¹≈ε : ∀ {x y} → x ≈ y → (x ∙ y ⁻¹) ≈ ε \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x ⁻¹-anti-homo-// : (x // y) ⁻¹ ≈ y // x @@ -499,9 +506,22 @@ Additions to existing modules product-↭ : product Preserves _↭_ ⟶ _≡_ ``` +* In `Data.Rational.Properties`: + ```agda + 1≢0 : 1ℚ ≢ 0ℚ + + #⇒invertible : p ≢ q → Invertible 1ℚ _*_ (p - q) + invertible⇒# : Invertible 1ℚ _*_ (p - q) → p ≢ q + + isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ + isHeytingField : IsHeytingField _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ + heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ + heytingField : HeytingField 0ℓ 0ℓ 0ℓ + ``` + * Added new functions in `Data.String.Base`: ```agda - map : (Char → Char) → String → String + map : (Char → Char) → String → String between : String → String → String → String ``` @@ -562,6 +582,7 @@ Additions to existing modules * Added new proofs in `Relation.Binary.Properties.Setoid`: ```agda + ≉-irrefl : Irreflexive _≈_ _≉_ ≈;≈⇒≈ : _≈_ ; _≈_ ⇒ _≈_ ≈⇒≈;≈ : _≈_ ⇒ _≈_ ; _≈_ ``` diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda index bac2c84d31..bade624b3c 100644 --- a/src/Algebra/Properties/Group.agda +++ b/src/Algebra/Properties/Group.agda @@ -115,6 +115,18 @@ inverseʳ-unique x y eq = trans (y≈x\\z x y ε eq) (identityʳ _) ⁻¹-involutive : Involutive _⁻¹ ⁻¹-involutive = selfInverse⇒involutive ⁻¹-selfInverse +x∙y⁻¹≈ε⇒x≈y : ∀ x y → (x ∙ y ⁻¹) ≈ ε → x ≈ y +x∙y⁻¹≈ε⇒x≈y x y x∙y⁻¹≈ε = begin + x ≈⟨ inverseˡ-unique x (y ⁻¹) x∙y⁻¹≈ε ⟩ + y ⁻¹ ⁻¹ ≈⟨ ⁻¹-involutive y ⟩ + y ∎ + +x≈y⇒x∙y⁻¹≈ε : ∀ {x y} → x ≈ y → (x ∙ y ⁻¹) ≈ ε +x≈y⇒x∙y⁻¹≈ε {x} {y} x≈y = begin + x ∙ y ⁻¹ ≈⟨ ∙-congʳ x≈y ⟩ + y ∙ y ⁻¹ ≈⟨ inverseʳ y ⟩ + ε ∎ + ⁻¹-injective : Injective _≈_ _≈_ _⁻¹ ⁻¹-injective = selfInverse⇒injective ⁻¹-selfInverse diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index a00ef23f82..fb186be08d 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -9,6 +9,7 @@ module Data.Rational.Properties where +open import Algebra.Apartness open import Algebra.Construct.NaturalChoice.Base import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp @@ -21,6 +22,7 @@ import Algebra.Morphism.GroupMonomorphism as GroupMonomorphisms import Algebra.Morphism.RingMonomorphism as RingMonomorphisms import Algebra.Lattice.Morphism.LatticeMonomorphism as LatticeMonomorphisms import Algebra.Properties.CommutativeSemigroup as CommSemigroupProperties +import Algebra.Properties.Group as GroupProperties open import Data.Bool.Base using (T; true; false) open import Data.Integer.Base as ℤ using (ℤ; +_; -[1+_]; +[1+_]; +0; 0ℤ; 1ℤ; _◃_) open import Data.Integer.Coprimality using (coprime-divisor) @@ -49,16 +51,18 @@ open import Function.Base using (_∘_; _∘′_; _∘₂_; _$_; flip) open import Function.Definitions using (Injective) open import Level using (0ℓ) open import Relation.Binary +open import Relation.Binary.Morphism.Structures +import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphisms +import Relation.Binary.Properties.DecSetoid as DecSetoidProperties open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂; sym; trans; _≢_; subst; subst₂; resp₂) open import Relation.Binary.PropositionalEquality.Properties using (setoid; decSetoid; module ≡-Reasoning; isEquivalence) -open import Relation.Binary.Morphism.Structures -import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphisms +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +open import Relation.Binary.Reasoning.Syntax using (module ≃-syntax) open import Relation.Nullary.Decidable.Core as Dec using (yes; no; recompute; map′; _×-dec_) open import Relation.Nullary.Negation.Core using (¬_; contradiction) -open import Relation.Binary.Reasoning.Syntax using (module ≃-syntax) open import Algebra.Definitions {A = ℚ} _≡_ open import Algebra.Structures {A = ℚ} _≡_ @@ -97,6 +101,9 @@ mkℚ n₁ d₁ _ ≟ mkℚ n₂ d₂ _ = map′ ≡-decSetoid : DecSetoid 0ℓ 0ℓ ≡-decSetoid = decSetoid _≟_ +1≢0 : 1ℚ ≢ 0ℚ +1≢0 = λ () + ------------------------------------------------------------------------ -- mkℚ+ ------------------------------------------------------------------------ @@ -1239,6 +1246,53 @@ neg-distribʳ-* = +-*-Monomorphism.neg-distribʳ-* ℚᵘ.+-0-isGroup ℚᵘ.*-i { isCommutativeRing = +-*-isCommutativeRing } + +------------------------------------------------------------------------ +-- HeytingField structures and bundles + +module _ where + open CommutativeRing +-*-commutativeRing + using (+-group; zeroˡ; *-congʳ; isCommutativeRing) + + open GroupProperties +-group + open DecSetoidProperties ≡-decSetoid + + #⇒invertible : p ≢ q → Invertible 1ℚ _*_ (p - q) + #⇒invertible {p} {q} p≢q = let r = p - q in 1/ r , *-inverseˡ r , *-inverseʳ r + where instance _ = ≢-nonZero (p≢q ∘ (x∙y⁻¹≈ε⇒x≈y p q)) + + invertible⇒# : Invertible 1ℚ _*_ (p - q) → p ≢ q + invertible⇒# {p} {q} (1/[p-q] , _ , [p-q]/[p-q]≡1) p≡q = contradiction 1≡0 1≢0 + where + open ≈-Reasoning ≡-setoid + 1≡0 : 1ℚ ≡ 0ℚ + 1≡0 = begin + 1ℚ ≈⟨ [p-q]/[p-q]≡1 ⟨ + (p - q) * 1/[p-q] ≈⟨ *-congʳ (x≈y⇒x∙y⁻¹≈ε p≡q) ⟩ + 0ℚ * 1/[p-q] ≈⟨ zeroˡ 1/[p-q] ⟩ + 0ℚ ∎ + + isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ + isHeytingCommutativeRing = record + { isCommutativeRing = isCommutativeRing + ; isApartnessRelation = ≉-isApartnessRelation + ; #⇒invertible = #⇒invertible + ; invertible⇒# = invertible⇒# + } + + isHeytingField : IsHeytingField _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ + isHeytingField = record + { isHeytingCommutativeRing = isHeytingCommutativeRing + ; tight = ≉-tight + } + + heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ + heytingCommutativeRing = record { isHeytingCommutativeRing = isHeytingCommutativeRing } + + heytingField : HeytingField 0ℓ 0ℓ 0ℓ + heytingField = record { isHeytingField = isHeytingField } + + ------------------------------------------------------------------------ -- Properties of _*_ and _≤_ diff --git a/src/Relation/Binary/Properties/DecSetoid.agda b/src/Relation/Binary/Properties/DecSetoid.agda new file mode 100644 index 0000000000..7f9b323d85 --- /dev/null +++ b/src/Relation/Binary/Properties/DecSetoid.agda @@ -0,0 +1,43 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Every decidable setoid induces tight apartness relation. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Relation.Binary.Bundles using (DecSetoid; ApartnessRelation) + +module Relation.Binary.Properties.DecSetoid {c ℓ} (S : DecSetoid c ℓ) where + +open import Data.Product using (_,_) +open import Data.Sum using (inj₁; inj₂) +open import Relation.Binary.Definitions + using (Cotransitive; Tight) +import Relation.Binary.Properties.Setoid as SetoidProperties +open import Relation.Binary.Structures + using (IsApartnessRelation; IsDecEquivalence) +open import Relation.Nullary.Decidable.Core + using (yes; no; decidable-stable) + +open DecSetoid S using (_≈_; _≉_; _≟_; setoid; trans) +open SetoidProperties setoid + +≉-cotrans : Cotransitive _≉_ +≉-cotrans {x} {y} x≉y z with x ≟ z | z ≟ y +... | _ | no z≉y = inj₂ z≉y +... | no x≉z | _ = inj₁ x≉z +... | yes x≈z | yes z≈y = inj₁ λ _ → x≉y (trans x≈z z≈y) + +≉-isApartnessRelation : IsApartnessRelation _≈_ _≉_ +≉-isApartnessRelation = record + { irrefl = ≉-irrefl + ; sym = ≉-sym + ; cotrans = ≉-cotrans + } + +≉-apartnessRelation : ApartnessRelation c ℓ ℓ +≉-apartnessRelation = record { isApartnessRelation = ≉-isApartnessRelation } + +≉-tight : Tight _≈_ _≉_ +≉-tight x y = decidable-stable (x ≟ y) , ≉-irrefl diff --git a/src/Relation/Binary/Properties/Setoid.agda b/src/Relation/Binary/Properties/Setoid.agda index 1b56c32d2a..43dc7e67d0 100644 --- a/src/Relation/Binary/Properties/Setoid.agda +++ b/src/Relation/Binary/Properties/Setoid.agda @@ -8,12 +8,12 @@ open import Data.Product.Base using (_,_) open import Function.Base using (_∘_; id; _$_; flip) -open import Relation.Nullary.Negation.Core using (¬_) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Binary.Core using (_⇒_) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) open import Relation.Binary.Bundles using (Setoid; Preorder; Poset) open import Relation.Binary.Definitions - using (Symmetric; _Respectsˡ_; _Respectsʳ_; _Respects₂_) + using (Symmetric; _Respectsˡ_; _Respectsʳ_; _Respects₂_; Irreflexive) open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder) open import Relation.Binary.Construct.Composition using (_;_; impliesˡ; transitive⇒≈;≈⊆≈) @@ -80,6 +80,9 @@ preorder = record ≉-resp₂ : _≉_ Respects₂ _≈_ ≉-resp₂ = ≉-respʳ , ≉-respˡ +≉-irrefl : Irreflexive _≈_ _≉_ +≉-irrefl x≈y x≉y = contradiction x≈y x≉y + ------------------------------------------------------------------------ -- Equality is closed under composition