From 4a90a57388260ce7b96ba45e2cc5db9299c3387d Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 23 Sep 2023 16:39:11 -0700 Subject: [PATCH] Clean up imports a bit Signed-off-by: Danila Fedorin --- Lattice.agda | 13 +++---------- Lattice/Prod.agda | 6 +++--- 2 files changed, 6 insertions(+), 13 deletions(-) diff --git a/Lattice.agda b/Lattice.agda index 14674e0..e4e98d7 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -3,20 +3,13 @@ module Lattice where open import Equivalence import Chain -import Data.Nat.Properties as NatProps -open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; subst) -open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎) open import Relation.Binary.Core using (_Preserves_⟶_ ) -open import Relation.Nullary using (Dec; ¬_; yes; no) -open import Data.Nat as Nat using (ℕ; _≤_; _+_; suc) -open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂) +open import Relation.Nullary using (Dec; ¬_) +open import Data.Nat as Nat using (ℕ) +open import Data.Product using (_×_; Σ; _,_) open import Data.Sum using (_⊎_; inj₁; inj₂) open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_) open import Function.Definitions using (Injective) -open import Data.Empty using (⊥) - -absurd : ∀ {a} {A : Set a} → ⊥ → A -absurd () IsDecidable : ∀ {a} {A : Set a} (R : A → A → Set a) → Set a IsDecidable {a} {A} R = ∀ (a₁ a₂ : A) → Dec (R a₁ a₂) diff --git a/Lattice/Prod.agda b/Lattice/Prod.agda index dbe36e9..ce8948a 100644 --- a/Lattice/Prod.agda +++ b/Lattice/Prod.agda @@ -8,11 +8,11 @@ module Lattice.Prod {a} {A B : Set a} open import Data.Nat using (ℕ; _≤_; _+_; suc) open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂) -open import Equivalence +open import Data.Empty using (⊥-elim) open import Relation.Binary.Core using (_Preserves_⟶_ ) -open import Relation.Binary.Definitions open import Relation.Binary.PropositionalEquality using (sym; subst) open import Relation.Nullary using (¬_; yes; no) +open import Equivalence import Chain open IsLattice lA using () renaming @@ -141,7 +141,7 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl)) unzip {a₁} {a₂} {b₁} {b₂} {n} (step {(a₁ , b₁)} {(a , b)} (((d₁ , d₂) , (a₁⊔d₁≈a , b₁⊔d₂≈b)) , a₁b₁̷≈ab) (a≈a' , b≈b') a'b'a₂b₂) with ≈₁-dec a₁ a | ≈₂-dec b₁ b | unzip a'b'a₂b₂ - ... | yes a₁≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = absurd (a₁b₁̷≈ab (a₁≈a , b₁≈b)) + ... | yes a₁≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ⊥-elim (a₁b₁̷≈ab (a₁≈a , b₁≈b)) ... | no a₁̷≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ((suc n₁ , n₂) , ((step₁ ((d₁ , a₁⊔d₁≈a) , a₁̷≈a) a≈a' c₁ , Chain₂-≈-cong₁ (≈₂-sym (≈₂-trans b₁≈b b≈b')) c₂), +-monoʳ-≤ 1 (n≤n₁+n₂))) ... | yes a₁≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =