diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2018-01-02 05:14:32 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2018-01-02 05:14:32 +0100 |
| commit | 1b1c4927937f556d87b6c76c9b64d93a0230f269 (patch) | |
| tree | 6aa516e57b76852b820782548c678d72502b440c /CheckInsert.agda | |
| parent | 3ab245029ac43720a71dfd9c9a15e91f2312f069 (diff) | |
| download | bidiragda-1b1c4927937f556d87b6c76c9b64d93a0230f269.tar.gz | |
remove lemma-lookupM-insert-other in favour of lookup∘update′
Diffstat (limited to 'CheckInsert.agda')
| -rw-r--r-- | CheckInsert.agda | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/CheckInsert.agda b/CheckInsert.agda index e0e35ec..316d8b1 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -9,6 +9,7 @@ open import Data.Fin.Properties using (_≟_) open import Data.Maybe using (Maybe ; nothing ; just) renaming (setoid to MaybeSetoid ; Eq to MaybeEq) open import Data.Vec using (Vec) renaming (_∷_ to _∷V_) open import Data.Vec.Equality using () renaming (module Equality to VecEq) +open import Data.Vec.Properties using (lookup∘update′) open import Relation.Nullary using (Dec ; yes ; no ; ¬_) open import Relation.Nullary.Negation using (contradiction) open import Relation.Binary using (Setoid ; module DecSetoid) @@ -69,7 +70,7 @@ lemma-lookupM-checkInsert i j h pl y ph' | ._ | new _ with i ≟ j lemma-lookupM-checkInsert i .i h pl y ph' | ._ | new pl' | yes refl = contradiction (trans (sym pl) pl') (λ ()) lemma-lookupM-checkInsert i j h {x} pl y refl | ._ | new _ | no i≢j = begin lookupM i (insert j y h) - ≡⟨ lemma-lookupM-insert-other i j y h i≢j ⟩ + ≡⟨ lookup∘update′ i≢j h (just y) ⟩ lookupM i h ≡⟨ pl ⟩ just x ∎ @@ -82,4 +83,4 @@ lemma-lookupM-checkInsert-other i j i≢j x h ph' with lookupM j h lemma-lookupM-checkInsert-other i j i≢j x h ph' | just y with deq x y lemma-lookupM-checkInsert-other i j i≢j x h refl | just y | yes x≈y = refl lemma-lookupM-checkInsert-other i j i≢j x h () | just y | no x≉y -lemma-lookupM-checkInsert-other i j i≢j x h refl | nothing = lemma-lookupM-insert-other i j x h i≢j +lemma-lookupM-checkInsert-other i j i≢j x h refl | nothing = lookup∘update′ i≢j h (just x) |