diff options
Diffstat (limited to 'Bidir.agda')
| -rw-r--r-- | Bidir.agda | 6 |
1 files changed, 3 insertions, 3 deletions
@@ -15,7 +15,7 @@ open import Data.List using (List) open import Data.List.All using (All) open import Data.Vec using (Vec ; [] ; _∷_ ; toList ; map ; allFin) renaming (lookup to lookupVec) open import Data.Vec.Equality using () renaming (module Equality to VecEq) -open import Data.Vec.Properties using (lookup∘tabulate ; map-cong ; map-∘ ; map-lookup-allFin) +open import Data.Vec.Properties using (lookup∘tabulate ; lookup∘update ; map-cong ; map-∘ ; map-lookup-allFin) open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂) open import Function using (id ; _∘_ ; flip) open import Relation.Binary.Core using (refl ; _≡_) @@ -56,7 +56,7 @@ lemma-lookupM-checkInserted i x h refl | ._ | same x' x≈x' pl = begin ≈⟨ MaybeEq.just (Setoid.sym A.setoid x≈x') ⟩ just x ∎ where open EqR (MaybeSetoid A.setoid) -lemma-lookupM-checkInserted i x h refl | ._ | new _ = Setoid.reflexive (MaybeSetoid A.setoid) (lemma-lookupM-insert i x h) +lemma-lookupM-checkInserted i x h refl | ._ | new _ = Setoid.reflexive (MaybeSetoid A.setoid) (lookup∘update i h (just x)) lemma-lookupM-checkInserted i x h () | ._ | wrong _ _ _ _in-domain-of_ : {m n : ℕ} {A : Set} → (is : Vec (Fin m) n) → (FinMapMaybe m A) → Set @@ -69,7 +69,7 @@ lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | nothing | [ ph' ] lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ph | just h' | [ ph' ] with checkInsert i' x' h' | inspect (checkInsert i' x') h' | insertionresult i' x' h' lemma-assoc-domain (i' ∷ is') (x' ∷ xs') refl | just h | [ ph' ] | ._ | _ | same x _ pl = All._∷_ (x , pl) (lemma-assoc-domain is' xs' ph') lemma-assoc-domain (i' ∷ is') (x' ∷ xs') refl | just h' | [ ph' ] | ._ | [ cI≡ ] | new _ = All._∷_ - (x' , lemma-lookupM-insert i' x' h') + (x' , lookup∘update i' h' (just x')) (Data.List.All.map (λ {i} p → proj₁ p , lemma-lookupM-checkInsert i i' h' (proj₂ p) x' cI≡) (lemma-assoc-domain is' xs' ph')) |