Decidable Setoid -> Apartness Relation and Rational Heyting Field

src/Algebra/Properties/Group.agda

@@ -106,3 +106,18 @@ inverseʳ-unique x y eq = begin
   y       ≈⟨ sym (⁻¹-involutive y) ⟩
   y ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong (sym (inverseˡ-unique x y eq)) ⟩
   x ⁻¹    ∎
+
+x∙y⁻¹≈ε→x≈y : (x y : Carrier) → (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 : Carrier) → x ≈ y → (x ∙ y ⁻¹) ≈ ε
+x≈y→x∙y⁻¹≈ε x y x≈y = begin
+  x ∙ y ⁻¹ ≈⟨ ∙-congʳ x≈y ⟩
+  y ∙ y ⁻¹ ≈⟨ inverseʳ y ⟩
+  ε        ∎
+
+x≉y→x∙y⁻¹≉ε : (x y : Carrier) → x ≉ y → (x ∙ y ⁻¹) ≉ ε
+x≉y→x∙y⁻¹≉ε x y x≉y x∙y⁻¹≈ε = x≉y (x∙y⁻¹≈ε→x≈y x y x∙y⁻¹≈ε)

src/Data/Rational/Properties.agda

@@ -21,6 +21,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
+open import Algebra.Apartness
 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)
@@ -95,6 +96,9 @@ mkℚ n₁ d₁ _ ≟ mkℚ n₂ d₂ _ = map′
 ≡-decSetoid : DecSetoid 0ℓ 0ℓ
 ≡-decSetoid = decSetoid _≟_
 
+1≢0 : 1ℚ ≢ 0ℚ
+1≢0 = λ ()
+
 ------------------------------------------------------------------------
 -- mkℚ+
 ------------------------------------------------------------------------
@@ -1238,6 +1242,75 @@ neg-distribʳ-* = +-*-Monomorphism.neg-distribʳ-* ℚᵘ.+-0-isGroup ℚᵘ.*-i
   { isCommutativeRing = +-*-isCommutativeRing
   }
 
+
+------------------------------------------------------------------------
+-- Field-like structures and bundles
+module _ where
+  open CommutativeRing +-*-commutativeRing
+    using (+-group; zeroˡ; *-congʳ; isCommutativeRing)
+
+  open import Algebra.Properties.Group +-group
+  open import Relation.Binary.Reasoning.Setoid ≡-setoid
+  open import Relation.Binary.Properties.DecSetoid ≡-decSetoid
+
+  isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
+  isHeytingCommutativeRing =
+    record
+    { isCommutativeRing = isCommutativeRing
+    ; isApartnessRelation = ≉-isApartnessRelation
+    ; #⇒invertible = #⇒invertible
+    ; invertible⇒# = invertible⇒#
+    }
+    where
+      x*y≡z→x≢0 : ∀ x y z → z ≢ 0ℚ → x * y ≡ z → x ≢ 0ℚ
+      x*y≡z→x≢0 x y z z≉0 x*y≡z x≡0 =
+        z≉0
+        $ begin
+            z
+          ≈⟨ sym x*y≡z ⟩
+            x * y
+          ≈⟨ *-congʳ x≡0 ⟩
+            0ℚ * y
+          ≈⟨ zeroˡ y ⟩
+            0ℚ
+          ∎
+        where
+          open import Function using (_$_)
+
+      #⇒invertible : {x y : ℚ} → x ≢ y → Invertible 1ℚ _*_ (x - y)
+      #⇒invertible {x} {y} x≢y =
+        let instance _ = ≢-nonZero (x≉y→x∙y⁻¹≉ε x y x≢y)
+        in
+          ( 1/_ (x - y)
+          , *-inverseˡ (x - y)
+          , *-inverseʳ (x - y)
+          )
+
+      invertible⇒# : ∀ {i j} → Invertible 1ℚ _*_ (i - j) → i ≢ j
+      invertible⇒# {i} {j} (1/[i-j] , _ , [i-j]/[i-j]≡1) i≡j =
+        x*y≡z→x≢0
+          (i - j)
+          1/[i-j]
+          1ℚ
+          1≢0
+          [i-j]/[i-j]≡1
+          (x≈y→x∙y⁻¹≈ε i j i≡j)
+
+  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,48 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Every decidable setoid induces tight apartness relation.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary using (DecSetoid)
+
+module Relation.Binary.Properties.DecSetoid {c ℓ} (S : DecSetoid c ℓ) where
+
+open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (decidable-stable)
+
+open import Data.Product using (_,_)
+open import Data.Sum using (inj₁; inj₂)
+
+open import Relation.Binary.Definitions
+  using (Cotransitive; Tight)
+
+open import Relation.Binary
+  using (IsApartnessRelation; ApartnessRelation; IsDecEquivalence)
+
+open DecSetoid S using (_≈_; _≉_; isDecEquivalence; Carrier; setoid)
+open IsDecEquivalence isDecEquivalence
+
+open import Relation.Binary.Properties.Setoid setoid
+
+≉-cotrans : Cotransitive _≉_
+≉-cotrans {x} {y} x≉y z with x ≟ z | z ≟ y
+≉-cotrans {x} {y} x≉y z | _ | no z≉y = inj₂ z≉y
+≉-cotrans {x} {y} x≉y z | no x≉z | _ = inj₁ x≉z
+≉-cotrans {x} {y} x≉y 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

@@ -12,7 +12,7 @@ open import Relation.Nullary.Negation.Core using (¬_)
 open import Relation.Binary.PropositionalEquality.Core as P 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)
 
 module Relation.Binary.Properties.Setoid {a ℓ} (S : Setoid a ℓ) where
@@ -77,6 +77,9 @@ preorder = record
 ≉-resp₂ : _≉_ Respects₂ _≈_
 ≉-resp₂ = ≉-respʳ , ≉-respˡ
 
+≉-irrefl : Irreflexive _≈_ _≉_
+≉-irrefl x≈y x≉y = x≉y x≈y
+
 ------------------------------------------------------------------------
 -- Other properties