diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-24 11:28:31 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-24 11:28:31 +0100 |
| commit | c56c7e2e2395d65afd8242df3f9ab45216ba5733 (patch) | |
| tree | 0f5769f75738de972093ea4d77f1d3f203d3c4f7 /Precond.agda | |
| parent | d0392d237baa5cb5561ea878fb05ddfb597bba90 (diff) | |
| download | bidiragda-c56c7e2e2395d65afd8242df3f9ab45216ba5733.tar.gz | |
define mapMV via sequenceV
This makes a few proofs easier and eliminates the need for sequence-map
entirely.
Diffstat (limited to 'Precond.agda')
| -rw-r--r-- | Precond.agda | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Precond.agda b/Precond.agda index bc619dc..3e4c219 100644 --- a/Precond.agda +++ b/Precond.agda @@ -25,7 +25,7 @@ open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import Relation.Nullary using (yes ; no) -open import Generic using (mapMV ; sequenceV ; sequence-map) +open import Generic using (mapMV ; sequenceV) open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty ; delete-many ; lemma-tabulate-∘ ; delete ; lemma-lookupM-delete ; lemma-lookupM-fromFunc ; reshape ; lemma-reshape-id) import CheckInsert open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other) @@ -73,7 +73,7 @@ assoc-enough G {i} s v (h , p) = _ , (begin bff G i s v ≡⟨ cong (flip _>>=_ (flip mapMV t ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Get.|gl₁| G i)))) p ⟩ mapMV (flip lookupM (union h (reshape g′ (Get.|gl₁| G i)))) t - ≡⟨ sym (sequence-map (flip lookupM (union h (reshape g′ (Get.|gl₁| G i)))) t) ⟩ + ≡⟨ refl ⟩ sequenceV (map (flip lookupM (union h (reshape g′ (Get.|gl₁| G i)))) t) ≡⟨ cong (sequenceV ∘ flip map t ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩ sequenceV (map (flip lookupM (union h g′)) t) |