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 <[email protected]>
Co-authored-by: James McKinna <[email protected]>

Author: cspollard

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 _≈_ _≉_
   ≈;≈⇒≈ : _≈_ ; _≈_ ⇒ _≈_
   ≈⇒≈;≈ : _≈_ ⇒ _≈_ ; _≈_
   ```

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
 

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 _≤_
 

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

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