diff --git a/Fixedpoint.agda b/Fixedpoint.agda index 1ce26cf..3e6ca39 100644 --- a/Fixedpoint.agda +++ b/Fixedpoint.agda @@ -30,14 +30,14 @@ private ⊥ᴬ≼ a with ≈-dec a ⊥ᴬ ... | yes a≈⊥ᴬ = ≼-cong a≈⊥ᴬ ≈-refl (≼-refl a) ... | no a̷≈⊥ᴬ with ≈-dec ⊥ᴬ (a ⊓ ⊥ᴬ) - ... | yes ⊥ᴬ≈a⊓⊥ᴬ = (a , ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ))) + ... | yes ⊥ᴬ≈a⊓⊥ᴬ = ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ)) ... | no ⊥ᴬ̷≈a⊓⊥ᴬ = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) (ChainA.step x≺⊥ᴬ ≈-refl (proj₂ (proj₁ fixedHeight)))) where ⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ ⊓ a) ≈ ⊥ᴬ ⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ → ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _)) x≺⊥ᴬ : (⊥ᴬ ⊓ a) ≺ ⊥ᴬ - x≺⊥ᴬ = ((⊥ᴬ , ≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ᴬ ⊔ (⊥ᴬ ⊓ a)}) (absorb-⊔-⊓ ⊥ᴬ a))) , ⊥ᴬ⊓a̷≈⊥ᴬ) + x≺⊥ᴬ = (≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ᴬ ⊔ (⊥ᴬ ⊓ a)}) (absorb-⊔-⊓ ⊥ᴬ a)) , ⊥ᴬ⊓a̷≈⊥ᴬ) -- using 'g', for gas, here helps make sure the function terminates. -- since A forms a fixed-height lattice, we must find a solution after diff --git a/Lattice.agda b/Lattice.agda index e4e98d7..c06b2bc 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -19,7 +19,7 @@ record IsSemilattice {a} (A : Set a) (_⊔_ : A → A → A) : Set a where _≼_ : A → A → Set a - a ≼ b = Σ A (λ c → (a ⊔ c) ≈ b) + a ≼ b = (a ⊔ b) ≈ b _≺_ : A → A → Set a a ≺ b = (a ≼ b) × (¬ a ≈ b) @@ -34,11 +34,22 @@ record IsSemilattice {a} (A : Set a) open IsEquivalence ≈-equiv public + open import Relation.Binary.Reasoning.Base.Single _≈_ ≈-refl ≈-trans + ≼-refl : ∀ (a : A) → a ≼ a - ≼-refl a = (a , ⊔-idemp a) + ≼-refl a = ⊔-idemp a ≼-cong : ∀ {a₁ a₂ a₃ a₄ : A} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≼ a₃ → a₂ ≼ a₄ - ≼-cong a₁≈a₂ a₃≈a₄ (c₁ , a₁⊔c₁≈a₃) = (c₁ , ≈-trans (≈-⊔-cong (≈-sym a₁≈a₂) ≈-refl) (≈-trans a₁⊔c₁≈a₃ a₃≈a₄)) + ≼-cong {a₁} {a₂} {a₃} {a₄} a₁≈a₂ a₃≈a₄ a₁⊔a₃≈a₃ = + begin + a₂ ⊔ a₄ + ∼⟨ ≈-⊔-cong (≈-sym a₁≈a₂) (≈-sym a₃≈a₄) ⟩ + a₁ ⊔ a₃ + ∼⟨ a₁⊔a₃≈a₃ ⟩ + a₃ + ∼⟨ a₃≈a₄ ⟩ + a₄ + ∎ ≺-cong : ∀ {a₁ a₂ a₃ a₄ : A} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≺ a₃ → a₂ ≺ a₄ ≺-cong a₁≈a₂ a₃≈a₄ (a₁≼a₃ , a₁̷≈a₃) = diff --git a/Lattice/AboveBelow.agda b/Lattice/AboveBelow.agda index 3abef25..30e1ea3 100644 --- a/Lattice/AboveBelow.agda +++ b/Lattice/AboveBelow.agda @@ -282,29 +282,26 @@ module Plain where open IsLattice isLattice using (_≼_; _≺_) ⊥≺[x] : ∀ (x : A) → ⊥ ≺ [ x ] - ⊥≺[x] x = (([ x ] , ≈-refl) , λ ()) + ⊥≺[x] x = (≈-refl , λ ()) - x≺[y]⇒y≡⊥ : ∀ (x : AboveBelow) (y : A) → x ≺ [ y ] → x ≡ ⊥ - x≺[y]⇒y≡⊥ x y ((d , x⊔d≈[y]) , x̷≈[y]) with d - ... | ⊥ rewrite x⊔⊥≡x x with ≈-lift a≈y ← x⊔d≈[y] = ⊥-elim (x̷≈[y] (≈-lift a≈y)) - ... | ⊤ rewrite x⊔⊤≡⊤ x with () <- x⊔d≈[y] - ... | [ a ] with x - ... | ⊥ = refl - ... | ⊤ with () <- x⊔d≈[y] - ... | [ b ] with ≈₁-dec b a - ... | yes _ with ≈-lift b≈y ← x⊔d≈[y] = ⊥-elim (x̷≈[y] (≈-lift b≈y)) - ... | no _ with () <- x⊔d≈[y] + x≺[y]⇒x≡⊥ : ∀ (x : AboveBelow) (y : A) → x ≺ [ y ] → x ≡ ⊥ + x≺[y]⇒x≡⊥ x y ((x⊔[y]≈[y]) , x̷≈[y]) with x + ... | ⊥ = refl + ... | ⊤ with () ← x⊔[y]≈[y] + ... | [ b ] with ≈₁-dec b y + ... | yes b≈y = ⊥-elim (x̷≈[y] (≈-lift b≈y)) + ... | no _ with () ← x⊔[y]≈[y] [x]≺⊤ : ∀ (x : A) → [ x ] ≺ ⊤ - [x]≺⊤ x rewrite x⊔⊤≡⊤ [ x ] = ((⊤ , ≈-⊤-⊤) , λ ()) + [x]≺⊤ x rewrite x⊔⊤≡⊤ [ x ] = (≈-⊤-⊤ , λ ()) [x]≺y⇒y≡⊤ : ∀ (x : A) (y : AboveBelow) → [ x ] ≺ y → y ≡ ⊤ - [x]≺y⇒y≡⊤ x y ((d , [x]⊔d≈y) , [x]̷≈y) with d - ... | ⊥ rewrite x⊔⊥≡x [ x ] with ≈-lift x≈a ← [x]⊔d≈y = ⊥-elim ([x]̷≈y (≈-lift x≈a)) - ... | ⊤ rewrite x⊔⊤≡⊤ [ x ] with ≈-⊤-⊤ ← [x]⊔d≈y = refl + [x]≺y⇒y≡⊤ x y ([x]⊔y≈y , [x]̷≈y) with y + ... | ⊥ with () ← [x]⊔y≈y + ... | ⊤ = refl ... | [ a ] with ≈₁-dec x a - ... | yes _ with ≈-lift x≈a ← [x]⊔d≈y = ⊥-elim ([x]̷≈y (≈-lift x≈a)) - ... | no _ with ≈-⊤-⊤ ← [x]⊔d≈y = refl + ... | yes x≈a = ⊥-elim ([x]̷≈y (≈-lift x≈a)) + ... | no _ with () ← [x]⊔y≈y open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice) @@ -313,7 +310,7 @@ module Plain where longestChain = step (⊥≺[x] x) ≈-refl (step ([x]≺⊤ x) ≈-⊤-⊤ (done ≈-⊤-⊤)) ¬-Chain-⊤ : ∀ {ab : AboveBelow} {n : ℕ} → ¬ Chain ⊤ ab (suc n) - ¬-Chain-⊤ (step ((d , ⊤⊔d≈x) , ⊤̷≈x) _ _) rewrite ⊤⊔x≡⊤ d = ⊥-elim (⊤̷≈x ⊤⊔d≈x) + ¬-Chain-⊤ {x} (step (⊤⊔x≈x , ⊤̷≈x) _ _) rewrite ⊤⊔x≡⊤ x = ⊥-elim (⊤̷≈x ⊤⊔x≈x) isLongest : ∀ {ab₁ ab₂ : AboveBelow} {n : ℕ} → Chain ab₁ ab₂ n → n ≤ 2 isLongest (done _) = z≤n diff --git a/Lattice/Prod.agda b/Lattice/Prod.agda index ce8948a..7dc79d7 100644 --- a/Lattice/Prod.agda +++ b/Lattice/Prod.agda @@ -114,13 +114,13 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) private a,∙-Monotonic : ∀ (a : A) → Monotonic _≼₂_ _≼_ (λ b → (a , b)) - a,∙-Monotonic a {b₁} {b₂} (b , b₁⊔b≈b₂) = ((a , b) , (⊔₁-idemp a , b₁⊔b≈b₂)) + a,∙-Monotonic a {b₁} {b₂} b₁⊔b₂≈b₂ = (⊔₁-idemp a , b₁⊔b₂≈b₂) a,∙-Preserves-≈₂ : ∀ (a : A) → (λ b → (a , b)) Preserves _≈₂_ ⟶ _≈_ a,∙-Preserves-≈₂ a {b₁} {b₂} b₁≈b₂ = (≈₁-refl , b₁≈b₂) ∙,b-Monotonic : ∀ (b : B) → Monotonic _≼₁_ _≼_ (λ a → (a , b)) - ∙,b-Monotonic b {a₁} {a₂} (a , a₁⊔a≈a₂) = ((a , b) , (a₁⊔a≈a₂ , ⊔₂-idemp b)) + ∙,b-Monotonic b {a₁} {a₂} a₁⊔a₂≈a₂ = (a₁⊔a₂≈a₂ , ⊔₂-idemp b) ∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶ _≈_ ∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl) @@ -139,17 +139,17 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) unzip : ∀ {a₁ a₂ : A} {b₁ b₂ : B} {n : ℕ} → Chain (a₁ , b₁) (a₂ , b₂) n → Σ (ℕ × ℕ) (λ (n₁ , n₂) → ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n ≤ n₁ + n₂))) 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₂) + unzip {a₁} {a₂} {b₁} {b₂} {n} (step {(a₁ , b₁)} {(a , b)} ((a₁≼a , b₁≼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₂)) = ⊥-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₂))) + ((suc n₁ , n₂) , ((step₁ (a₁≼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₂)) = - ((n₁ , suc n₂) , ( (Chain₁-≈-cong₁ (≈₁-sym (≈₁-trans a₁≈a a≈a')) c₁ , step₂ ((d₂ , b₁⊔d₂≈b) , b₁̷≈b) b≈b' c₂) + ((n₁ , suc n₂) , ( (Chain₁-≈-cong₁ (≈₁-sym (≈₁-trans a₁≈a a≈a')) c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂) , subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂) )) ... | no a₁̷≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = - ((suc n₁ , suc n₂) , ( (step₁ ((d₁ , a₁⊔d₁≈a) , a₁̷≈a) a≈a' c₁ , step₂ ((d₂ , b₁⊔d₂≈b) , b₁̷≈b) b≈b' c₂) + ((suc n₁ , suc n₂) , ( (step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂) , ≤-stepsˡ 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂)) )) diff --git a/Lattice/Unit.agda b/Lattice/Unit.agda index 5fb4809..d736dbe 100644 --- a/Lattice/Unit.agda +++ b/Lattice/Unit.agda @@ -96,7 +96,7 @@ private longestChain = done refl isLongest : ∀ {t₁ t₂ : ⊤} {n : ℕ} → Chain t₁ t₂ n → n ≤ 0 - isLongest {tt} {tt} (step ((tt , tt⊔tt≈tt) , tt≈tt) _ _) = ⊥-elim (tt≈tt refl) + isLongest {tt} {tt} (step (tt⊔tt≈tt , tt̷≈tt) _ _) = ⊥-elim (tt̷≈tt refl) isLongest (done _) = z≤n isFiniteHeightLattice : IsFiniteHeightLattice ⊤ 0 _≈_ _⊔_ _⊓_