diff options
Diffstat (limited to 'Bidir.agda')
| -rw-r--r-- | Bidir.agda | 12 |
1 files changed, 6 insertions, 6 deletions
@@ -15,9 +15,9 @@ open import Data.Maybe.Relation.Binary.Pointwise using (just ; nothing ; drop-ju open Category.Monad.RawMonad {Level.zero} Data.Maybe.Categorical.monad using (_>>=_) open Category.Functor.RawFunctor {Level.zero} Data.Maybe.Categorical.functor using (_<$>_) open import Data.List using (List) -open import Data.List.All using (All) +open import Data.List.Relation.Unary.All using (All) open import Data.Vec using (Vec ; [] ; _∷_ ; toList ; map ; allFin) renaming (lookup to lookupVec) -open import Data.Vec.Relation.Pointwise.Inductive using (Pointwise) +open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise) 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) @@ -25,7 +25,7 @@ open import Relation.Binary.Indexed.Heterogeneous using () renaming (IndexedSeto open import Relation.Binary.Indexed.Heterogeneous.Construct.At using (_atₛ_) open import Relation.Binary.PropositionalEquality as P using (_≡_ ; inspect ; [_] ; module ≡-Reasoning) open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid) -import Relation.Binary.EqReasoning as EqR +import Relation.Binary.Reasoning.Setoid as EqR open import Structures using (Functor ; IsFunctor ; Shaped ; module Shaped) open import Instances using (MaybeFunctor ; ShapedISetoid) @@ -66,21 +66,21 @@ _in-domain-of_ : {m n : ℕ} {A : Set} → (is : Vec (Fin m) n) → (FinMapMaybe _in-domain-of_ is h = All (λ i → ∃ λ x → lookupM i h ≡ just x) (toList is) lemma-assoc-domain : {m n : ℕ} → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → {h : FinMapMaybe n Carrier} → assoc is xs ≡ just h → is in-domain-of h -lemma-assoc-domain [] [] ph = Data.List.All.[] +lemma-assoc-domain [] [] ph = Data.List.Relation.Unary.All.[] lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ph with assoc is' xs' | inspect (assoc is') xs' 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') P.refl | just h | [ ph' ] | ._ | _ | same x _ pl = All._∷_ (x , pl) (lemma-assoc-domain is' xs' ph') lemma-assoc-domain (i' ∷ is') (x' ∷ xs') P.refl | just h' | [ ph' ] | ._ | [ cI≡ ] | new _ = All._∷_ (x' , lookup∘update i' h' (just x')) - (Data.List.All.map + (Data.List.Relation.Unary.All.map (λ {i} p → proj₁ p , lemma-lookupM-checkInsert i i' h' (proj₂ p) x' cI≡) (lemma-assoc-domain is' xs' ph')) lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | just h' | [ ph' ] | ._ | _ | wrong _ _ _ lemma-map-lookupM-assoc : {m : ℕ} → (i : Fin m) → (x : Carrier) → (h : FinMapMaybe m Carrier) → {h' : FinMapMaybe m Carrier} → checkInsert i x h ≡ just h' → {n : ℕ} → (js : Vec (Fin m) n) → js in-domain-of h → map (flip lookupM h') js ≡ map (flip lookupM h) js lemma-map-lookupM-assoc i x h ph [] pj = P.refl -lemma-map-lookupM-assoc i x h ph (j ∷ js) (Data.List.All._∷_ (x' , pl) pj) = P.cong₂ _∷_ +lemma-map-lookupM-assoc i x h ph (j ∷ js) (Data.List.Relation.Unary.All._∷_ (x' , pl) pj) = P.cong₂ _∷_ (P.trans (lemma-lookupM-checkInsert j i h pl x ph) (P.sym pl)) (lemma-map-lookupM-assoc i x h ph js pj) |