From e98f145fac4d79ea0aaae4618a86a3d423b2f326 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Tue, 30 May 2023 17:58:43 -0300 Subject: [PATCH 1/6] added apartness with example --- .../Binary/Reasoning/Base/Apartness.agda | 95 +++++++++++++++++++ 1 file changed, 95 insertions(+) create mode 100644 src/Relation/Binary/Reasoning/Base/Apartness.agda diff --git a/src/Relation/Binary/Reasoning/Base/Apartness.agda b/src/Relation/Binary/Reasoning/Base/Apartness.agda new file mode 100644 index 0000000000..1554302073 --- /dev/null +++ b/src/Relation/Binary/Reasoning/Base/Apartness.agda @@ -0,0 +1,95 @@ +open import Relation.Binary + +module Relation.Binary.Reasoning.Base.Apartness {a ℓ₁ ℓ₂} {A : Set a} + {_≈_ : Rel A ℓ₁} {_#_ : Rel A ℓ₂} + (#-trans : Transitive _#_) + (≈-equiv : IsEquivalence _≈_) + (#-sym : Symmetric _#_) + (#-≈-trans : Trans _#_ _≈_ _#_) (≈-#-trans : Trans _≈_ _#_ _#_) + where + +open import Data.Product using (proj₁; proj₂) +open import Function.Base using (case_of_; id) +open import Level using (Level; _⊔_; Lift; lift) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; sym) +open import Relation.Nullary.Decidable using (Dec; yes; no) +open import Relation.Nullary.Decidable using (True; toWitness) + +infix 4 _IsRelatedTo_ + +open IsEquivalence ≈-equiv + renaming + ( refl to ≈-refl + ; sym to ≈-sym + ; trans to ≈-trans + ) + +data _IsRelatedTo_ (x y : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + nothing : x IsRelatedTo y + apartness : (x#y : x # y) → x IsRelatedTo y + equals : (x≈y : x ≈ y) → x IsRelatedTo y + +data IsApartness {x y} : x IsRelatedTo y → Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + isApartness : ∀ x#y → IsApartness (apartness x#y) + +IsApartness? : ∀ {x y} (x#y : x IsRelatedTo y) → Dec (IsApartness x#y) +IsApartness? nothing = no λ() +IsApartness? (apartness x#y) = yes (isApartness x#y) +IsApartness? (equals x≈y) = no (λ ()) + +extractApartness : ∀ {x y} {x#y : x IsRelatedTo y} → IsApartness x#y → x # y +extractApartness (isApartness x#y) = x#y + +infix 1 begin-apartness_ +infixr 2 step-≈ step-≈˘ step-≡ step-≡˘ step-# step-#˘ _≡⟨⟩_ +infix 3 _∎ + +begin-apartness_ : ∀ {x y} (r : x IsRelatedTo y) → {s : True (IsApartness? r)} → x # y +begin-apartness_ r {s} = extractApartness (toWitness s) + +step-# : ∀ (x : A) {y z} → y IsRelatedTo z → x # y → x IsRelatedTo z +step-# x nothing _ = nothing +step-# x (apartness y#z) x#y = nothing +step-# x (equals y≈z) x#y = apartness (#-≈-trans x#y y≈z) + +step-#˘ : ∀ (x : A) {y z} → y IsRelatedTo z → y # x → x IsRelatedTo z +step-#˘ x y-z y#x = step-# x y-z (#-sym y#x) + +step-≈ : ∀ (x : A) {y z} → y IsRelatedTo z → x ≈ y → x IsRelatedTo z +step-≈ x nothing x≈y = nothing +step-≈ x (apartness y#z) x≈y = apartness (≈-#-trans x≈y y#z) +step-≈ x (equals y≈z) x≈y = equals (≈-trans x≈y y≈z) + +step-≈˘ : ∀ x {y z} → y IsRelatedTo z → y ≈ x → x IsRelatedTo z +step-≈˘ x y∼z x≈y = step-≈ x y∼z (≈-sym x≈y) + +step-≡ : ∀ (x : A) {y z} → y IsRelatedTo z → x ≡ y → x IsRelatedTo z +step-≡ x nothing _ = nothing +step-≡ x (apartness x#y) refl = apartness x#y +step-≡ x (equals x≈y) refl = equals x≈y + +step-≡˘ : ∀ x {y z} → y IsRelatedTo z → y ≡ x → x IsRelatedTo z +step-≡˘ x y∼z x≡y = step-≡ x y∼z (sym x≡y) + +_≡⟨⟩_ : ∀ (x : A) {y} → x IsRelatedTo y → x IsRelatedTo y +x ≡⟨⟩ x≲y = x≲y + +_∎ : ∀ x → x IsRelatedTo x +x ∎ = equals ≈-refl + +syntax step-# x y∼z x Date: Tue, 30 May 2023 17:59:06 -0300 Subject: [PATCH 2/6] removed example --- src/Relation/Binary/Reasoning/Base/Apartness.agda | 9 --------- 1 file changed, 9 deletions(-) diff --git a/src/Relation/Binary/Reasoning/Base/Apartness.agda b/src/Relation/Binary/Reasoning/Base/Apartness.agda index 1554302073..7163b30411 100644 --- a/src/Relation/Binary/Reasoning/Base/Apartness.agda +++ b/src/Relation/Binary/Reasoning/Base/Apartness.agda @@ -84,12 +84,3 @@ syntax step-≈ x y∼z x≈y = x ≈⟨ x≈y ⟩ y∼z syntax step-≈˘ x y∼z y≈x = x ≈˘⟨ y≈x ⟩ y∼z syntax step-≡ x y∼z x≡y = x ≡⟨ x≡y ⟩ y∼z syntax step-≡˘ x y∼z y≡x = x ≡˘⟨ y≡x ⟩ y∼z - -private module _ (a b c d : A) (a≈b : a ≈ b) (b#c : b # c) (c≈d : c ≈ d) where - - _ : a # d - _ = begin-apartness - a ≈⟨ a≈b ⟩ - b #⟨ b#c ⟩ - c ≈⟨ c≈d ⟩ - d ∎ From deb481ecad18a7690f22f2c1de9ef2759757b967 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Tue, 30 May 2023 18:05:38 -0300 Subject: [PATCH 3/6] fixed some mistakes of apartness --- .../Binary/Reasoning/Base/Apartness.agda | 39 +++++++++++-------- 1 file changed, 23 insertions(+), 16 deletions(-) diff --git a/src/Relation/Binary/Reasoning/Base/Apartness.agda b/src/Relation/Binary/Reasoning/Base/Apartness.agda index 7163b30411..e33694b6f6 100644 --- a/src/Relation/Binary/Reasoning/Base/Apartness.agda +++ b/src/Relation/Binary/Reasoning/Base/Apartness.agda @@ -1,3 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The basic code for equational reasoning with three relations: +-- equality and apartness +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + open import Relation.Binary module Relation.Binary.Reasoning.Base.Apartness {a ℓ₁ ℓ₂} {A : Set a} @@ -8,16 +17,12 @@ module Relation.Binary.Reasoning.Base.Apartness {a ℓ₁ ℓ₂} {A : Set a} (#-≈-trans : Trans _#_ _≈_ _#_) (≈-#-trans : Trans _≈_ _#_ _#_) where -open import Data.Product using (proj₁; proj₂) -open import Function.Base using (case_of_; id) -open import Level using (Level; _⊔_; Lift; lift) +open import Level using (Level; _⊔_) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym) open import Relation.Nullary.Decidable using (Dec; yes; no) open import Relation.Nullary.Decidable using (True; toWitness) -infix 4 _IsRelatedTo_ - open IsEquivalence ≈-equiv renaming ( refl to ≈-refl @@ -25,8 +30,10 @@ open IsEquivalence ≈-equiv ; trans to ≈-trans ) +infix 4 _IsRelatedTo_ + data _IsRelatedTo_ (x y : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - nothing : x IsRelatedTo y + nothing : x IsRelatedTo y apartness : (x#y : x # y) → x IsRelatedTo y equals : (x≈y : x ≈ y) → x IsRelatedTo y @@ -34,9 +41,9 @@ data IsApartness {x y} : x IsRelatedTo y → Set (a ⊔ ℓ₁ ⊔ ℓ₂) where isApartness : ∀ x#y → IsApartness (apartness x#y) IsApartness? : ∀ {x y} (x#y : x IsRelatedTo y) → Dec (IsApartness x#y) -IsApartness? nothing = no λ() +IsApartness? nothing = no λ() IsApartness? (apartness x#y) = yes (isApartness x#y) -IsApartness? (equals x≈y) = no (λ ()) +IsApartness? (equals x≈y) = no (λ ()) extractApartness : ∀ {x y} {x#y : x IsRelatedTo y} → IsApartness x#y → x # y extractApartness (isApartness x#y) = x#y @@ -49,17 +56,17 @@ begin-apartness_ : ∀ {x y} (r : x IsRelatedTo y) → {s : True (IsApartness? r begin-apartness_ r {s} = extractApartness (toWitness s) step-# : ∀ (x : A) {y z} → y IsRelatedTo z → x # y → x IsRelatedTo z -step-# x nothing _ = nothing +step-# x nothing _ = nothing step-# x (apartness y#z) x#y = nothing -step-# x (equals y≈z) x#y = apartness (#-≈-trans x#y y≈z) +step-# x (equals y≈z) x#y = apartness (#-≈-trans x#y y≈z) step-#˘ : ∀ (x : A) {y z} → y IsRelatedTo z → y # x → x IsRelatedTo z step-#˘ x y-z y#x = step-# x y-z (#-sym y#x) step-≈ : ∀ (x : A) {y z} → y IsRelatedTo z → x ≈ y → x IsRelatedTo z -step-≈ x nothing x≈y = nothing +step-≈ x nothing x≈y = nothing step-≈ x (apartness y#z) x≈y = apartness (≈-#-trans x≈y y#z) -step-≈ x (equals y≈z) x≈y = equals (≈-trans x≈y y≈z) +step-≈ x (equals y≈z) x≈y = equals (≈-trans x≈y y≈z) step-≈˘ : ∀ x {y z} → y IsRelatedTo z → y ≈ x → x IsRelatedTo z step-≈˘ x y∼z x≈y = step-≈ x y∼z (≈-sym x≈y) @@ -67,19 +74,19 @@ step-≈˘ x y∼z x≈y = step-≈ x y∼z (≈-sym x≈y) step-≡ : ∀ (x : A) {y z} → y IsRelatedTo z → x ≡ y → x IsRelatedTo z step-≡ x nothing _ = nothing step-≡ x (apartness x#y) refl = apartness x#y -step-≡ x (equals x≈y) refl = equals x≈y +step-≡ x (equals x≈y) refl = equals x≈y step-≡˘ : ∀ x {y z} → y IsRelatedTo z → y ≡ x → x IsRelatedTo z step-≡˘ x y∼z x≡y = step-≡ x y∼z (sym x≡y) _≡⟨⟩_ : ∀ (x : A) {y} → x IsRelatedTo y → x IsRelatedTo y -x ≡⟨⟩ x≲y = x≲y +x ≡⟨⟩ x-y = x-y _∎ : ∀ x → x IsRelatedTo x x ∎ = equals ≈-refl -syntax step-# x y∼z x Date: Tue, 30 May 2023 18:07:42 -0300 Subject: [PATCH 4/6] solved one more problem of apartness --- src/Relation/Binary/Reasoning/Base/Apartness.agda | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Relation/Binary/Reasoning/Base/Apartness.agda b/src/Relation/Binary/Reasoning/Base/Apartness.agda index e33694b6f6..0e66c4e54f 100644 --- a/src/Relation/Binary/Reasoning/Base/Apartness.agda +++ b/src/Relation/Binary/Reasoning/Base/Apartness.agda @@ -11,9 +11,8 @@ open import Relation.Binary module Relation.Binary.Reasoning.Base.Apartness {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_#_ : Rel A ℓ₂} - (#-trans : Transitive _#_) (≈-equiv : IsEquivalence _≈_) - (#-sym : Symmetric _#_) + (#-trans : Transitive _#_) (#-sym : Symmetric _#_) (#-≈-trans : Trans _#_ _≈_ _#_) (≈-#-trans : Trans _≈_ _#_ _#_) where @@ -58,7 +57,7 @@ begin-apartness_ r {s} = extractApartness (toWitness s) step-# : ∀ (x : A) {y z} → y IsRelatedTo z → x # y → x IsRelatedTo z step-# x nothing _ = nothing step-# x (apartness y#z) x#y = nothing -step-# x (equals y≈z) x#y = apartness (#-≈-trans x#y y≈z) +step-# x (equals y≈z) x#y = apartness (#-≈-trans x#y y≈z) step-#˘ : ∀ (x : A) {y z} → y IsRelatedTo z → y # x → x IsRelatedTo z step-#˘ x y-z y#x = step-# x y-z (#-sym y#x) From 955485c1028c642356512f44b3b0e6cc3f2f75ce Mon Sep 17 00:00:00 2001 From: Guilherme Date: Tue, 30 May 2023 19:00:21 -0300 Subject: [PATCH 5/6] added isEquality --- .../Binary/Reasoning/Base/Apartness.agda | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/src/Relation/Binary/Reasoning/Base/Apartness.agda b/src/Relation/Binary/Reasoning/Base/Apartness.agda index 0e66c4e54f..7a52568664 100644 --- a/src/Relation/Binary/Reasoning/Base/Apartness.agda +++ b/src/Relation/Binary/Reasoning/Base/Apartness.agda @@ -47,12 +47,26 @@ IsApartness? (equals x≈y) = no (λ ()) extractApartness : ∀ {x y} {x#y : x IsRelatedTo y} → IsApartness x#y → x # y extractApartness (isApartness x#y) = x#y -infix 1 begin-apartness_ +data IsEquality {x y} : x IsRelatedTo y → Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + isEquality : ∀ x≈y → IsEquality (equals x≈y) + +IsEquality? : ∀ {x y} (x≲y : x IsRelatedTo y) → Dec (IsEquality x≲y) +IsEquality? nothing = no λ() +IsEquality? (apartness _) = no λ() +IsEquality? (equals x≈y) = yes (isEquality x≈y) + +extractEquality : ∀ {x y} {x≲y : x IsRelatedTo y} → IsEquality x≲y → x ≈ y +extractEquality (isEquality x≈y) = x≈y + +infix 1 begin-apartness_ begin-equality_ infixr 2 step-≈ step-≈˘ step-≡ step-≡˘ step-# step-#˘ _≡⟨⟩_ infix 3 _∎ begin-apartness_ : ∀ {x y} (r : x IsRelatedTo y) → {s : True (IsApartness? r)} → x # y -begin-apartness_ r {s} = extractApartness (toWitness s) +begin-apartness_ _ {s} = extractApartness (toWitness s) + +begin-equality_ : ∀ {x y} (r : x IsRelatedTo y) → {s : True (IsEquality? r)} → x ≈ y +begin-equality_ _ {s} = extractEquality (toWitness s) step-# : ∀ (x : A) {y z} → y IsRelatedTo z → x # y → x IsRelatedTo z step-# x nothing _ = nothing From 5a75e48586f8933489336537db24ba3db1292a65 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Thu, 1 Jun 2023 00:23:48 -0300 Subject: [PATCH 6/6] add to CHANGELOG --- CHANGELOG.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0e9cd648ab..5091c14691 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3042,3 +3042,15 @@ This is a full list of proofs that have changed form to use irrelevant instance ```agda ↭-reverse : (xs : List A) → reverse xs ↭ xs ``` + +* Added new file `Relation.Binary.Reasoning.Base.Apartness` + +This is how to use it: + ```agda + _ : a # d + _ = begin-apartness + a ≈⟨ a≈b ⟩ + b #⟨ b#c ⟩ + c ≈⟨ c≈d ⟩ + d ∎ + ```