Decidable Setoid -> Apartness Relation and Rational Heyting Field

src/Data/Rational/Properties/Heyting.agda

@@ -0,0 +1,114 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Proof that the rationals form a HeytingField.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Rational.Properties.Heyting where
+
+open import Level using (0ℓ)
+
+open import Data.Rational using (ℚ; ≢-nonZero; 1/_)
+open import Data.Rational.Properties
+  using (≡-decSetoid; +-*-commutativeRing; *-inverseˡ; *-inverseʳ)
+open import Relation.Binary.Bundles using (DecSetoid)
+
+open import Relation.Binary.Properties.DecSetoid ≡-decSetoid
+
+open import Algebra.Apartness
+  using
+  ( IsHeytingCommutativeRing; IsHeytingField
+  ; HeytingCommutativeRing; HeytingField
+  )
+
+open import Algebra using (CommutativeRing; Invertible)
+
+open CommutativeRing +-*-commutativeRing hiding (_≉_)
+
+-- some useful lemmas -- reproduced elsewhere?
+private
+  x-y≈0→x≈y : (x y : ℚ) → (x - y) ≈ 0# → x ≈ y
+  x-y≈0→x≈y x y x-y≈0 =
+    begin
+      x
+    ≈⟨ inverseˡ-unique x (- y) x-y≈0 ⟩
+      - (- y)
+    ≈⟨ ⁻¹-involutive y ⟩
+      y
+    ∎
+    where
+      open import Relation.Binary.Reasoning.Setoid setoid
+      open import Algebra.Properties.Group +-group
+
+  x≈y→x-y≈0 : (x y : ℚ) → x ≈ y → (x - y) ≈ 0#
+  x≈y→x-y≈0 x y x≈y =
+    begin
+      x - y
+    ≈⟨ +-congʳ x≈y ⟩
+      y - y
+    ≈⟨ -‿inverseʳ y ⟩
+      0#
+    ∎
+    where
+      open import Relation.Binary.Reasoning.Setoid setoid
+      open import Algebra.Properties.Group +-group
+
+  x≉y→x-y≉0 : (x y : ℚ) → x ≉ y → (x - y) ≉ 0#
+  x≉y→x-y≉0 x y x≉y x-y≈0 = x≉y (x-y≈0→x≈y x y x-y≈0)
+
+  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 (_$_)
+      open import Relation.Binary.Reasoning.Setoid setoid
+
+
+  1≉0 : 1# ≉ 0#
+  1≉0 = λ ()
+
+isHeytingCommutativeRing : IsHeytingCommutativeRing _≈_ _≉_ _+_ _*_ -_ 0# 1#
+isHeytingCommutativeRing =
+  record
+  { isCommutativeRing = isCommutativeRing
+  ; isApartnessRelation = ≉-isApartnessRelation
+  ; #⇒invertible =
+    λ {x} {y} x≉y →
+      let nz = ≢-nonZero (x≉y→x-y≉0 x y x≉y)
+      in
+        ( 1/_ (x - y) {{nz}}
+        , *-inverseˡ (x - y) {{nz}} , *-inverseʳ (x - y) {{nz}}
+        )
+  ; invertible⇒# = invert→#
+  }
+  where
+    open import Data.Product using (_,_)
+
+    invert→# : ∀ {x y} → Invertible _≈_ 1# _*_ (x - y) → x ≉ y
+    invert→# {x} {y} (1/[x-y] , _ , [x-y]/[x-y]≈1) x≈y =
+      x*y≈z→x≉0 (x - y) 1/[x-y] 1# 1≉0 [x-y]/[x-y]≈1 (x≈y→x-y≈0 x y x≈y)
+
+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 }

src/Relation/Binary/Properties/DecSetoid.agda

@@ -0,0 +1,57 @@
+------------------------------------------------------------------------
+-- 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 (Irreflexive; Cotransitive; Tight; Symmetric)
+
+open import Relation.Binary
+  using (Rel; IsApartnessRelation; ApartnessRelation; IsDecEquivalence)
+
+open DecSetoid S using (_≈_; isDecEquivalence) renaming (Carrier to A)
+
+open IsDecEquivalence isDecEquivalence
+
+_≉_ : Rel A ℓ
+x ≉ y = ¬ x ≈ y
+
+≉-irrefl : Irreflexive {A = A} _≈_ _≉_
+≉-irrefl x≈y x≉y = x≉y x≈y
+
+≉-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 with trans x≈z z≈y
+≉-cotrans {x} {y} x≉y z | yes x≈z | yes z≈y | x≈y = inj₁ λ _ → x≉y x≈y
+
+≉-sym : Symmetric _≉_
+≉-sym x≉y y≈x = x≉y (sym y≈x)
+
+≉-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