From 9646096c75ee8fb169cb107cbc43ced4d774bbbf Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 23 Nov 2023 14:15:40 -0800 Subject: [PATCH] Fix uses of 'absurd' in Fixedpoint.agda --- Fixedpoint.agda | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Fixedpoint.agda b/Fixedpoint.agda index 388fcaf..1ce26cf 100644 --- a/Fixedpoint.agda +++ b/Fixedpoint.agda @@ -13,6 +13,7 @@ module Fixedpoint {a} {A : Set a} open import Data.Nat.Properties using (+-suc; +-comm) open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂) +open import Data.Empty using (⊥-elim) open import Relation.Binary.PropositionalEquality using (_≡_; sym) open import Relation.Nullary using (Dec; ¬_; yes; no) @@ -30,7 +31,7 @@ private ... | 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 ⊥ᴬ))) - ... | no ⊥ᴬ̷≈a⊓⊥ᴬ = absurd (ChainA.Bounded-suc-n (proj₂ fixedHeight) (ChainA.step x≺⊥ᴬ ≈-refl (proj₂ (proj₁ fixedHeight)))) + ... | 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 _ _)) @@ -44,7 +45,7 @@ private -- out, we have exceeded h steps, which shouldn't be possible. doStep : ∀ (g hᶜ : ℕ) (a₁ a₂ : A) (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h) (a₂≼fa₂ : a₂ ≼ f a₂) → Σ A (λ a → a ≈ f a) - doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = absurd (ChainA.Bounded-suc-n (proj₂ fixedHeight) c) + doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) c) doStep (suc g') hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ) with ≈-dec a₂ (f a₂) ... | yes a₂≈fa₂ = (a₂ , a₂≈fa₂) @@ -70,7 +71,7 @@ private (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h) (a₂≼fa₂ : a₂ ≼ f a₂) → proj₁ (doStep g hᶜ a₁ a₂ c g+hᶜ≡h a₂≼fa₂) ≼ a - stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = absurd (ChainA.Bounded-suc-n (proj₂ fixedHeight) c) + stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) c) stepPreservesLess (suc g') hᶜ a₁ a₂ a a≈fa a₂≼a c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ) with ≈-dec a₂ (f a₂) ... | yes _ = a₂≼a