From ec12f616069cdca041e4d7c6ca9268bb023570c8 Mon Sep 17 00:00:00 2001 From: Jacques Date: Thu, 13 Mar 2025 13:44:00 -0400 Subject: [PATCH 1/4] =?UTF-8?q?[Refractor]=20contradiction=20over=20?= =?UTF-8?q?=E2=8A=A5-elim=20in?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/List/Relation/Binary/Lex/Core.agda | 6 +++--- src/Data/Vec/Relation/Binary/Lex/Strict.agda | 7 ++++--- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/Data/List/Relation/Binary/Lex/Core.agda b/src/Data/List/Relation/Binary/Lex/Core.agda index 0b3e821194..6b1d65b857 100644 --- a/src/Data/List/Relation/Binary/Lex/Core.agda +++ b/src/Data/List/Relation/Binary/Lex/Core.agda @@ -8,13 +8,13 @@ module Data.List.Relation.Binary.Lex.Core where -open import Data.Empty using (⊥; ⊥-elim) -open import Data.Unit.Base using (⊤; tt) +open import Data.Empty using (⊥) +open import Data.Unit.Base using (⊤) open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; uncurry) open import Data.List.Base using (List; []; _∷_) open import Function.Base using (_∘_; flip; id) open import Level using (Level; _⊔_) -open import Relation.Nullary.Negation using (¬_) +open import Relation.Nullary.Negation.Core using (¬_) open import Relation.Binary.Core using (Rel) open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_; head; tail) diff --git a/src/Data/Vec/Relation/Binary/Lex/Strict.agda b/src/Data/Vec/Relation/Binary/Lex/Strict.agda index fa5e125e2a..b48244820c 100644 --- a/src/Data/Vec/Relation/Binary/Lex/Strict.agda +++ b/src/Data/Vec/Relation/Binary/Lex/Strict.agda @@ -23,7 +23,7 @@ open import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise using (Pointwise; []; _∷_; head; tail) open import Function.Base using (id; _on_; _∘_) open import Induction.WellFounded -open import Relation.Nullary using (yes; no; ¬_) +open import Level using (Level; _⊔_) open import Relation.Binary.Core using (REL; Rel; _⇒_) open import Relation.Binary.Bundles using (Poset; StrictPartialOrder; DecPoset; DecStrictPartialOrder @@ -39,7 +39,8 @@ open import Relation.Binary.Definitions open import Relation.Binary.Consequences using (asym⇒irr) open import Relation.Binary.Construct.On as On using (wellFounded) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) -open import Level using (Level; _⊔_) +open import Relation.Nullary.Decidable.Core using (yes; no) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) private variable @@ -139,7 +140,7 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where where <-wellFounded : ∀ {n} → WellFounded (_<_ {n}) - <-wellFounded {0} [] = acc λ ys<[] → ⊥-elim (xs≮[] ys<[]) + <-wellFounded {0} [] = acc λ ys<[] → contradiction ys<[] xs≮[] <-wellFounded {suc n} xs = Subrelation.wellFounded <⇒uncons-Lex uncons-Lex-wellFounded xs where From 34d3fe0ce97d6252b277a547c68b1ad5f3cf2855 Mon Sep 17 00:00:00 2001 From: Jacques Date: Mon, 17 Mar 2025 12:40:50 -0400 Subject: [PATCH 2/4] Modification --- src/Data/Vec/Relation/Binary/Lex/Core.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Data/Vec/Relation/Binary/Lex/Core.agda b/src/Data/Vec/Relation/Binary/Lex/Core.agda index df2c2b7e7c..7d56c4f76d 100644 --- a/src/Data/Vec/Relation/Binary/Lex/Core.agda +++ b/src/Data/Vec/Relation/Binary/Lex/Core.agda @@ -8,7 +8,7 @@ module Data.Vec.Relation.Binary.Lex.Core {a} {A : Set a} where -open import Data.Empty using (⊥; ⊥-elim) +open import Data.Empty using (⊥) open import Data.Nat.Base using (ℕ; suc) import Data.Nat.Properties as ℕ using (_≟_; ≡-irrelevant) open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; uncurry) @@ -27,7 +27,7 @@ open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; cong) import Relation.Nullary as Nullary open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_; _⊎-dec_) -open import Relation.Nullary.Negation +open import Relation.Nullary.Negation.Core using (¬_; contradiction) private variable @@ -114,9 +114,9 @@ module _ {P : Set} {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where antisym : ∀ {n} → Antisymmetric (_≋_ {n}) (_<ₗₑₓ_) antisym (base _) (base _) = [] - antisym (this x≺y m≡n) (this y≺x n≡m) = ⊥-elim (≺-asym x≺y y≺x) - antisym (this x≺y m≡n) (next y≈x ys Date: Mon, 17 Mar 2025 16:15:31 -0400 Subject: [PATCH 3/4] remove of useless import and replacing tt with _ --- src/Data/List/Relation/Binary/Lex/Strict.agda | 8 +++----- src/Data/Vec/Relation/Binary/Lex/Core.agda | 1 - src/Data/Vec/Relation/Binary/Lex/Strict.agda | 2 +- 3 files changed, 4 insertions(+), 7 deletions(-) diff --git a/src/Data/List/Relation/Binary/Lex/Strict.agda b/src/Data/List/Relation/Binary/Lex/Strict.agda index 277996594f..26f05b6878 100644 --- a/src/Data/List/Relation/Binary/Lex/Strict.agda +++ b/src/Data/List/Relation/Binary/Lex/Strict.agda @@ -11,8 +11,6 @@ module Data.List.Relation.Binary.Lex.Strict where -open import Data.Empty using (⊥) -open import Data.Unit.Base using (⊤; tt) open import Function.Base using (_∘_; id) open import Data.Product.Base using (_,_) open import Data.Sum.Base using (inj₁; inj₂) @@ -146,7 +144,7 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where ≤-reflexive : (_≈_ : Rel A ℓ₁) (_≺_ : Rel A ℓ₂) → Pointwise _≈_ ⇒ Lex-≤ _≈_ _≺_ - ≤-reflexive _≈_ _≺_ [] = base tt + ≤-reflexive _≈_ _≺_ [] = base _ ≤-reflexive _≈_ _≺_ (x≈y ∷ xs≈ys) = next x≈y (≤-reflexive _≈_ _≺_ xs≈ys) @@ -168,7 +166,7 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where -- the following lemma. ≤-total : Symmetric _≈_ → Trichotomous _≈_ _≺_ → Total _≤_ - ≤-total _ _ [] [] = inj₁ (base tt) + ≤-total _ _ [] [] = inj₁ (base _) ≤-total _ _ [] (x ∷ xs) = inj₁ halt ≤-total _ _ (x ∷ xs) [] = inj₂ halt ≤-total sym tri (x ∷ xs) (y ∷ ys) with tri x y @@ -179,7 +177,7 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where ... | inj₂ ys≲xs = inj₂ (next (sym x≈y) ys≲xs) ≤-decidable : Decidable _≈_ → Decidable _≺_ → Decidable _≤_ - ≤-decidable = Core.decidable (yes tt) + ≤-decidable = Core.decidable (yes _) ≤-respects₂ : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ → _≤_ Respects₂ _≋_ diff --git a/src/Data/Vec/Relation/Binary/Lex/Core.agda b/src/Data/Vec/Relation/Binary/Lex/Core.agda index 7d56c4f76d..6e892ece02 100644 --- a/src/Data/Vec/Relation/Binary/Lex/Core.agda +++ b/src/Data/Vec/Relation/Binary/Lex/Core.agda @@ -8,7 +8,6 @@ module Data.Vec.Relation.Binary.Lex.Core {a} {A : Set a} where -open import Data.Empty using (⊥) open import Data.Nat.Base using (ℕ; suc) import Data.Nat.Properties as ℕ using (_≟_; ≡-irrelevant) open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; uncurry) diff --git a/src/Data/Vec/Relation/Binary/Lex/Strict.agda b/src/Data/Vec/Relation/Binary/Lex/Strict.agda index b48244820c..29ca6451e0 100644 --- a/src/Data/Vec/Relation/Binary/Lex/Strict.agda +++ b/src/Data/Vec/Relation/Binary/Lex/Strict.agda @@ -11,7 +11,7 @@ module Data.Vec.Relation.Binary.Lex.Strict where -open import Data.Empty using (⊥; ⊥-elim) +open import Data.Empty using (⊥-elim) open import Data.Unit.Base using (⊤; tt) open import Data.Unit.Properties using (⊤-irrelevant) open import Data.Nat.Base using (ℕ; suc) From 008e08ce03abb2a57a7cd76176109804ded9531c Mon Sep 17 00:00:00 2001 From: Jacques Date: Mon, 17 Mar 2025 16:16:45 -0400 Subject: [PATCH 4/4] =?UTF-8?q?=20add=20open=20import=20Data.Empty=20using?= =?UTF-8?q?=20(=E2=8A=A5;=20=E2=8A=A5-elim)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Vec/Relation/Binary/Lex/Strict.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Vec/Relation/Binary/Lex/Strict.agda b/src/Data/Vec/Relation/Binary/Lex/Strict.agda index 29ca6451e0..b48244820c 100644 --- a/src/Data/Vec/Relation/Binary/Lex/Strict.agda +++ b/src/Data/Vec/Relation/Binary/Lex/Strict.agda @@ -11,7 +11,7 @@ module Data.Vec.Relation.Binary.Lex.Strict where -open import Data.Empty using (⊥-elim) +open import Data.Empty using (⊥; ⊥-elim) open import Data.Unit.Base using (⊤; tt) open import Data.Unit.Properties using (⊤-irrelevant) open import Data.Nat.Base using (ℕ; suc)