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 ; _≡_)
≈⟨ 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
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'))
open import Data.Fin.Properties using (_≟_)
open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; zip ; toList) renaming (lookup to lookupVec ; map to mapV)
open import Data.Vec.Equality using ()
+open import Data.Vec.Properties using (lookup∘update)
open import Data.Product using (__ ; _,_)
open import Data.List.All as All using (All)
import Data.List.All.Properties as AllP
lemma-lookupM-empty zero = refl
lemma-lookupM-empty (suc i) = lemma-lookupM-empty i
-lemma-lookupM-insert : {A : Set} {n : ℕ} → (i : Fin n) → (a : A) → (m : FinMapMaybe n A) → lookupM i (insert i a m) ≡ just a
-lemma-lookupM-insert zero a (x ∷ xs) = refl
-lemma-lookupM-insert (suc i) a (x ∷ xs) = lemma-lookupM-insert i a xs
-
lemma-lookupM-insert-other : {A : Set} {n : ℕ} → (i j : Fin n) → (a : A) → (m : FinMapMaybe n A) → i ≢ j → lookupM i (insert j a m) ≡ lookupM i m
lemma-lookupM-insert-other zero zero a m p = contradiction refl p
lemma-lookupM-insert-other zero (suc j) a (x ∷ xs) p = refl
lemma-lookupM-restrict i f (i' ∷ is) p with i ≟ i'
lemma-lookupM-restrict i f (.i ∷ is) {a} p | yes refl = just-injective (begin
just (f i)
- ≡⟨ sym (lemma-lookupM-insert i (f i) (restrict f is)) ⟩
+ ≡⟨ sym (lookup∘update i (restrict f is) (just (f i))) ⟩
lookupM i (insert i (f i) (restrict f is))
≡⟨ p ⟩
just a ∎)
lemma-lookupM-restrict-∈ : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (js : Vec (Fin n) m) → i ∈ js → lookupM i (restrict f js) ≡ just (f i)
lemma-lookupM-restrict-∈ i f [] ()
lemma-lookupM-restrict-∈ i f (j ∷ js) p with i ≟ j
-lemma-lookupM-restrict-∈ i f (.i ∷ js) p | yes refl = lemma-lookupM-insert i (f i) (restrict f js)
+lemma-lookupM-restrict-∈ i f (.i ∷ js) p | yes refl = lookup∘update i (restrict f js) (just (f i))
lemma-lookupM-restrict-∈ i f (j ∷ js) (Any.here i≡j) | no i≢j = contradiction i≡j i≢j
lemma-lookupM-restrict-∈ i f (j ∷ js) (Any.there p) | no i≢j =
trans (lemma-lookupM-insert-other i j (f j) (restrict f js) i≢j)