From 9bc4007c94a94706acbfb02103581b3d94e38001 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Mon, 22 Oct 2012 11:21:10 +0200 Subject: finally parameterize CheckInsert Also adapt depending modules. Long lines generally become shorter. The misleading name "EqInst" (hiding the decidability) got discarded. --- Precond.agda | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'Precond.agda') diff --git a/Precond.agda b/Precond.agda index 5011e41..a6d2d37 100644 --- a/Precond.agda +++ b/Precond.agda @@ -15,7 +15,8 @@ open import Relation.Binary.PropositionalEquality using (refl ; cong) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import FinMap using (FinMap ; FinMapMaybe ; union ; fromFunc ; empty ; insert) -open import CheckInsert using (EqInst ; checkInsert ; lemma-checkInsert-new) +import CheckInsert +open CheckInsert Carrier deq using (checkInsert ; lemma-checkInsert-new) open import BFF using (fmap ; _>>=_) import Bidir open Bidir Carrier deq using (lemma-∉-lookupM-assoc) @@ -67,8 +68,8 @@ different-assoc (u ∷ us) (v ∷ vs) p with different-assoc us vs (λ i j i≢j different-assoc (u ∷ us) (v ∷ vs) p | h , p' = insert u v h , (begin assoc (u ∷ us) (v ∷ vs) ≡⟨ refl ⟩ - assoc us vs >>= checkInsert deq u v - ≡⟨ cong (flip _>>=_ (checkInsert deq u v)) p' ⟩ - checkInsert deq u v h - ≡⟨ lemma-checkInsert-new deq u v h (lemma-∉-lookupM-assoc u us vs h p' (different-∉ u us p)) ⟩ + assoc us vs >>= checkInsert u v + ≡⟨ cong (flip _>>=_ (checkInsert u v)) p' ⟩ + checkInsert u v h + ≡⟨ lemma-checkInsert-new u v h (lemma-∉-lookupM-assoc u us vs h p' (different-∉ u us p)) ⟩ just (insert u v h) ∎) -- cgit v1.2.3