diff options
| -rw-r--r-- | BFF.agda | 5 | ||||
| -rw-r--r-- | BFFPlug.agda | 3 | ||||
| -rw-r--r-- | Bidir.agda | 46 | ||||
| -rw-r--r-- | FinMap.agda | 4 | ||||
| -rw-r--r-- | Generic.agda | 17 | ||||
| -rw-r--r-- | Instances.agda | 15 | ||||
| -rw-r--r-- | Precond.agda | 11 | ||||
| -rw-r--r-- | Structures.agda | 3 |
8 files changed, 56 insertions, 48 deletions
@@ -6,8 +6,9 @@ open import Level using () renaming (zero to ℓ₀) import Category.Monad import Category.Functor open import Data.Maybe using (Maybe ; just ; nothing ; maybe′) -open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_) -open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) +import Data.Maybe.Categorical +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 ; [] ; _∷_ ; map ; length) open import Data.Vec using (Vec ; toList ; fromList ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_) open import Function using (_∘_ ; flip) diff --git a/BFFPlug.agda b/BFFPlug.agda index 4992a3e..48171be 100644 --- a/BFFPlug.agda +++ b/BFFPlug.agda @@ -5,6 +5,7 @@ module BFFPlug (A : DecSetoid ℓ₀ ℓ₀) where open import Data.Nat using (ℕ ; _≟_ ; _+_ ; zero ; suc ; ⌈_/2⌉) open import Data.Maybe using (Maybe ; just ; nothing) +import Data.Maybe.Categorical open import Data.Vec using (Vec) open import Data.Product using (∃ ; _,_) open import Relation.Binary using (module DecSetoid) @@ -13,7 +14,7 @@ open import Relation.Nullary using (yes ; no) open import Function using (flip ; id ; _∘_) open import Function.LeftInverse using (_RightInverseOf_) import Category.Monad -open Category.Monad.RawMonad {ℓ₀} Data.Maybe.monad using (_>>=_) +open Category.Monad.RawMonad {ℓ₀} Data.Maybe.Categorical.monad using (_>>=_) open import Generic using (sequenceV ; ≡-to-Π) import BFF @@ -9,16 +9,18 @@ import Level import Category.Monad import Category.Functor open import Data.Maybe using (Maybe ; nothing ; just ; maybe′ ; drop-just) renaming (setoid to MaybeSetoid ; Eq to MaybeEq) -open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_) -open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) +import Data.Maybe.Categorical +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.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.Relation.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) -open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid) +open import Relation.Binary.Indexed.Heterogeneous using () renaming (IndexedSetoid to ISetoid) +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 @@ -80,19 +82,19 @@ lemma-map-lookupM-assoc i x h ph (j ∷ js) (Data.List.All._∷_ (x' , pl) pj) = (P.trans (lemma-lookupM-checkInsert j i h pl x ph) (P.sym pl)) (lemma-map-lookupM-assoc i x h ph js pj) -lemma-2 : {m n : ℕ} → (is : Vec (Fin n) m) → (v : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc is v ≡ just h → VecISetoid (MaybeSetoid A.setoid) at _ ∋ map (flip lookupM h) is ≈ map just v +lemma-2 : {m n : ℕ} → (is : Vec (Fin n) m) → (v : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc is v ≡ just h → VecISetoid (MaybeSetoid A.setoid) atₛ _ ∋ map (flip lookupM h) is ≈ map just v lemma-2 [] [] h p = ISetoid.refl (VecISetoid (MaybeSetoid A.setoid)) lemma-2 (i ∷ is) (x ∷ xs) h p with assoc is xs | inspect (assoc is) xs lemma-2 (i ∷ is) (x ∷ xs) h () | nothing | _ lemma-2 (i ∷ is) (x ∷ xs) h p | just h' | [ ir ] = begin lookupM i h ∷ map (flip lookupM h) is - ≈⟨ VecEq._∷-cong_ (lemma-lookupM-checkInserted i x h' p) (ISetoid.refl (VecISetoid (MaybeSetoid A.setoid))) ⟩ + ≈⟨ Pointwise._∷_ (lemma-lookupM-checkInserted i x h' p) (ISetoid.refl (VecISetoid (MaybeSetoid A.setoid))) ⟩ just x ∷ map (flip lookupM h) is ≡⟨ P.cong (_∷_ (just x)) (lemma-map-lookupM-assoc i x h' p is (lemma-assoc-domain is xs ir)) ⟩ just x ∷ map (flip lookupM h') is - ≈⟨ VecEq._∷-cong_ (Setoid.refl (MaybeSetoid A.setoid)) (lemma-2 is xs h' ir) ⟩ + ≈⟨ Pointwise._∷_ (Setoid.refl (MaybeSetoid A.setoid)) (lemma-2 is xs h' ir) ⟩ just x ∷ map just xs ∎ - where open EqR (VecISetoid (MaybeSetoid A.setoid) at _) + where open EqR (VecISetoid (MaybeSetoid A.setoid) atₛ _) lemma-fmap-denumerate-enumerate : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {α : Set} {s : S} → (c : C α s) → Shaped.fmap ShapeT (denumerate ShapeT c) (enumerate ShapeT s) ≡ c lemma-fmap-denumerate-enumerate {S} {C} ShapeT {s = s} c = begin @@ -231,16 +233,16 @@ module _ (G : Get) where ≡⟨ P.cong (sequenceView ∘ get) (P.sym (lemma-sequence-successful SourceShapeT v p)) ⟩ sequenceView (get v) ∎ -sequenceV-cong : (S : Setoid ℓ₀ ℓ₀) {n : ℕ} {m₁ m₂ : Setoid.Carrier (VecISetoid (MaybeSetoid S) at n)} → VecISetoid (MaybeSetoid S) at _ ∋ m₁ ≈ m₂ → MaybeSetoid (VecISetoid S at n) ∋ sequenceV m₁ ≈ sequenceV m₂ -sequenceV-cong S VecEq.[]-cong = Setoid.refl (MaybeSetoid (VecISetoid S at _)) -sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) with sequenceV xs | sequenceV ys | sequenceV-cong S xs≈ys -sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | just sys | just p = MaybeEq.just (VecEq._∷-cong_ x≈y p) -sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | just sys | () -sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | nothing | () -sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _)) -sequenceV-cong S (VecEq._∷-cong_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _)) +sequenceV-cong : (S : Setoid ℓ₀ ℓ₀) {n : ℕ} {m₁ m₂ : Setoid.Carrier (VecISetoid (MaybeSetoid S) atₛ n)} → VecISetoid (MaybeSetoid S) atₛ _ ∋ m₁ ≈ m₂ → MaybeSetoid (VecISetoid S atₛ n) ∋ sequenceV m₁ ≈ sequenceV m₂ +sequenceV-cong S Pointwise.[] = Setoid.refl (MaybeSetoid (VecISetoid S atₛ _)) +sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (Pointwise._∷_ (just x≈y) xs≈ys) with sequenceV xs | sequenceV ys | sequenceV-cong S xs≈ys +sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (Pointwise._∷_ (just x≈y) xs≈ys) | just sxs | just sys | just p = MaybeEq.just (Pointwise._∷_ x≈y p) +sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (Pointwise._∷_ (just x≈y) xs≈ys) | nothing | just sys | () +sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (Pointwise._∷_ (just x≈y) xs≈ys) | just sxs | nothing | () +sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (Pointwise._∷_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S atₛ _)) +sequenceV-cong S (Pointwise._∷_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S atₛ _)) -sequence-cong : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Setoid ℓ₀ ℓ₀) → {s : S} {x y : C (Maybe (Setoid.Carrier α)) s} → ShapedISetoid (P.setoid S) ShapeT (MaybeSetoid α) at _ ∋ x ≈ y → MaybeSetoid (ShapedISetoid (P.setoid S) ShapeT α at _) ∋ Shaped.sequence ShapeT x ≈ Shaped.sequence ShapeT y +sequence-cong : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Setoid ℓ₀ ℓ₀) → {s : S} {x y : C (Maybe (Setoid.Carrier α)) s} → ShapedISetoid (P.setoid S) ShapeT (MaybeSetoid α) atₛ _ ∋ x ≈ y → MaybeSetoid (ShapedISetoid (P.setoid S) ShapeT α atₛ _) ∋ Shaped.sequence ShapeT x ≈ Shaped.sequence ShapeT y sequence-cong ShapeT α {x = x} {y = y} (shape≈ , content≈) with sequenceV (Shaped.content ShapeT x) | sequenceV (Shaped.content ShapeT y) | sequenceV-cong α content≈ sequence-cong ShapeT α {s} (shape≈ , content≈) | .(just x) | .(just y) | just {x} {y} x≈y = just (P.refl , (begin content (fill s x) @@ -250,7 +252,7 @@ sequence-cong ShapeT α {s} (shape≈ , content≈) | .(just x) | .(just y) | ju y ≡⟨ P.sym (fill-content s y) ⟩ content (fill s y) ∎)) - where open EqR (VecISetoid α at _) + where open EqR (VecISetoid α atₛ _) open Shaped ShapeT sequence-cong ShapeT α (shape≈ , content≈) | .nothing | .nothing | nothing = nothing @@ -259,7 +261,7 @@ module _ (G : Get) where open Shaped SourceShapeT using () renaming (arity to arityS) open Shaped ViewShapeT using () renaming (content to contentV) - theorem-2 : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer (Maybe Carrier) (gl₁ j)) → bff G j s v ≡ just u → ShapedISetoid (P.setoid _) ViewShapeT (MaybeSetoid A.setoid) at _ ∋ get u ≈ Get.fmapV G just v + theorem-2 : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer (Maybe Carrier) (gl₁ j)) → bff G j s v ≡ just u → ShapedISetoid (P.setoid _) ViewShapeT (MaybeSetoid A.setoid) atₛ _ ∋ get u ≈ Get.fmapV G just v theorem-2 {i} j s v u p with lemma-<$>-just ((flip union (reshape (delete-many (contentV (get (enumerate SourceShapeT (gl₁ i)))) (fromFunc (denumerate SourceShapeT s))) (arityS (gl₁ j)))) <$> assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v)) p theorem-2 {i} j s v u p | h′ , ph′ with lemma-<$>-just (assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v)) ph′ theorem-2 {i} j s v u p | h′ , ph′ | h , ph = P.refl , (begin @@ -279,7 +281,7 @@ module _ (G : Get) where map just (contentV v) ≡⟨ P.sym (Shaped.fmap-content ViewShapeT just v) ⟩ contentV (fmapV just v) ∎) - where open EqR (VecISetoid (MaybeSetoid A.setoid) at _) + where open EqR (VecISetoid (MaybeSetoid A.setoid) atₛ _) s′ = enumerate SourceShapeT (gl₁ i) g = fromFunc (denumerate SourceShapeT s) g′ = delete-many (contentV (get s′)) g @@ -290,7 +292,7 @@ module _ (G : Get) where module _ (G : Get) where open Get G - theorem-2′ : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer Carrier (gl₁ j)) → bff G j s v ≡ just (Get.fmapS G just u) → ShapedISetoid (P.setoid _) ViewShapeT A.setoid at _ ∋ get u ≈ v + theorem-2′ : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer Carrier (gl₁ j)) → bff G j s v ≡ just (Get.fmapS G just u) → ShapedISetoid (P.setoid _) ViewShapeT A.setoid atₛ _ ∋ get u ≈ v theorem-2′ j s v u p = drop-just (begin get <$> just u ≡⟨ P.cong (_<$>_ get) (P.sym (lemma-just-sequence SourceShapeT u)) ⟩ @@ -301,4 +303,4 @@ module _ (G : Get) where Shaped.sequence ViewShapeT (fmapV just v) ≡⟨ lemma-just-sequence ViewShapeT v ⟩ just v ∎) - where open EqR (MaybeSetoid (ShapedISetoid (P.setoid _) ViewShapeT A.setoid at _)) + where open EqR (MaybeSetoid (ShapedISetoid (P.setoid _) ViewShapeT A.setoid atₛ _)) diff --git a/FinMap.agda b/FinMap.agda index 7380b71..df422c3 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -11,7 +11,7 @@ open import Data.Product using (_×_ ; _,_) open import Data.List.All as All using (All) import Data.List.All.Properties as AllP import Data.List.Any as Any -import Data.List.Any.Membership.Propositional +import Data.List.Membership.Setoid open import Function using (id ; _∘_ ; flip ; const) open import Function.Equality using (module Π) open import Function.Surjection using (module Surjection) @@ -24,7 +24,7 @@ open P.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import Generic using (just-injective) _∈_ : {A : Set} {n : ℕ} → A → Vec A n → Set -_∈_ {A} x xs = x Data.List.Any.Membership.Propositional.∈ (toList xs) +_∈_ {A} x xs = Data.List.Membership.Setoid._∈_ (P.setoid A) x (toList xs) _∉_ : {A : Set} {n : ℕ} → A → Vec A n → Set _∉_ {A} x xs = All (_≢_ x) (toList xs) diff --git a/Generic.agda b/Generic.agda index 90f5816..061042f 100644 --- a/Generic.agda +++ b/Generic.agda @@ -4,21 +4,22 @@ import Category.Functor import Category.Monad open import Data.List using (List ; length) renaming ([] to []L ; _∷_ to _∷L_) open import Data.Maybe using (Maybe ; just ; nothing) renaming (setoid to MaybeEq) +import Data.Maybe.Categorical open import Data.Nat using (ℕ ; zero ; suc) open import Data.Product using (_×_ ; _,_) open import Data.Vec using (Vec ; toList ; fromList ; map) renaming ([] to []V ; _∷_ to _∷V_) -open import Data.Vec.Equality using () renaming (module Equality to VecEq) +import Data.Vec.Relation.Pointwise.Inductive as VecEq open import Data.Vec.Properties using (map-cong) open import Function using (_∘_ ; id ; flip) open import Function.Equality using (_⟶_) open import Level using () renaming (zero to ℓ₀) open import Relation.Binary using (Setoid ; module Setoid) -open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid) +open import Relation.Binary.Indexed.Heterogeneous using () renaming (IndexedSetoid to ISetoid) open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_) open Setoid using () renaming (_≈_ to _∋_≈_) -open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) -open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_) +open Category.Functor.RawFunctor {Level.zero} Data.Maybe.Categorical.functor using (_<$>_) +open Category.Monad.RawMonad {Level.zero} Data.Maybe.Categorical.monad using (_>>=_) ≡-to-Π : {A B : Set} → (A → B) → P.setoid A ⟶ P.setoid B ≡-to-Π f = record { _⟨$⟩_ = f; cong = P.cong f } @@ -71,9 +72,9 @@ toList-subst v P.refl = P.refl VecISetoid : Setoid ℓ₀ ℓ₀ → ISetoid ℕ ℓ₀ ℓ₀ VecISetoid S = record { Carrier = Vec (Setoid.Carrier S) - ; _≈_ = λ x → VecEq._≈_ S x + ; _≈_ = VecEq.Pointwise (Setoid._≈_ S) ; isEquivalence = record - { refl = VecEq.refl S _ - ; sym = VecEq.sym S - ; trans = VecEq.trans S } + { refl = VecEq.refl (Setoid.refl S) + ; sym = VecEq.sym (Setoid.sym S) + ; trans = VecEq.trans (Setoid.trans S) } } diff --git a/Instances.agda b/Instances.agda index 3f69627..a09e30d 100644 --- a/Instances.agda +++ b/Instances.agda @@ -3,14 +3,15 @@ module Instances where open import Level using () renaming (zero to ℓ₀) open import Category.Functor using (RawFunctor) open import Data.Maybe as M using (Maybe) +import Data.Maybe.Categorical open import Data.Nat using (ℕ) open import Data.Product using (_×_ ; _,_ ; proj₁ ; proj₂) open import Data.Vec using (Vec) -import Data.Vec.Equality -open Data.Vec.Equality.PropositionalEquality using () renaming (to-≡ to VecEq-to-≡) +open import Data.Vec.Relation.Pointwise.Inductive using (Pointwise-≡⇒≡) open import Function using (_∘_ ; id) open import Relation.Binary using (Setoid ; module Setoid) -open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid) +open import Relation.Binary.Indexed.Heterogeneous using () renaming (IndexedSetoid to ISetoid) +open import Relation.Binary.Indexed.Heterogeneous.Construct.At using (_atₛ_) open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_ ; module ≡-Reasoning) open Setoid using () renaming (_≈_ to _∋_≈_) @@ -20,14 +21,14 @@ open import Structures using (Functor ; Shaped ; module Shaped) MaybeFunctor : Functor Maybe MaybeFunctor = record - { rawfunctor = M.functor + { rawfunctor = Data.Maybe.Categorical.functor ; isFunctor = record { cong = cong ; identity = identity ; composition = composition } } where _<$>_ : {α β : Set} → (α → β) → Maybe α → Maybe β - _<$>_ = RawFunctor._<$>_ M.functor + _<$>_ = RawFunctor._<$>_ Data.Maybe.Categorical.functor cong : {α β : Set} {g h : α → β} → g ≗ h → _<$>_ g ≗ _<$>_ h cong g≗h (M.just x) = P.cong M.just (g≗h x) @@ -61,12 +62,12 @@ ShapedISetoid S {C} ShapeT α = record ; trans = λ p q → Setoid.trans S (proj₁ p) (proj₁ q) , ISetoid.trans (VecISetoid α) (proj₂ p) (proj₂ q) } } where open Shaped ShapeT -Shaped≈-to-≡ : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Set) → {s : S} {x y : C α s} → ShapedISetoid (P.setoid S) ShapeT (P.setoid α) at s ∋ x ≈ y → x ≡ y +Shaped≈-to-≡ : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Set) → {s : S} {x y : C α s} → ShapedISetoid (P.setoid S) ShapeT (P.setoid α) atₛ s ∋ x ≈ y → x ≡ y Shaped≈-to-≡ ShapeT α {s} {x} {y} (shape≈ , content≈) = begin x ≡⟨ P.sym (content-fill x) ⟩ fill s (content x) - ≡⟨ P.cong (fill s) (VecEq-to-≡ content≈) ⟩ + ≡⟨ P.cong (fill s) (Pointwise-≡⇒≡ content≈) ⟩ fill s (content y) ≡⟨ content-fill y ⟩ y ∎ diff --git a/Precond.agda b/Precond.agda index 07775ac..98ba7a6 100644 --- a/Precond.agda +++ b/Precond.agda @@ -11,13 +11,14 @@ open import Level using () renaming (zero to ℓ₀) import Category.Monad import Category.Functor open import Data.Maybe using (Maybe ; nothing ; just ; maybe′) -open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_) -open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) +import Data.Maybe.Categorical +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.Vec using (Vec ; [] ; _∷_ ; map ; lookup ; toList) open import Data.Vec.Properties using (map-cong ; map-∘ ; tabulate-∘) import Data.List.All open import Data.List.Any using (here ; there) -open import Data.List.Any.Membership.Propositional using (_∉_) +open import Data.List.Membership.Setoid using (_∉_) open import Data.Maybe using (just) open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂) open import Function using (flip ; _∘_ ; id) @@ -99,9 +100,9 @@ module _ (G : Get) where data All-different {A : Set} : List A → Set where different-[] : All-different [] - different-∷ : {x : A} {xs : List A} → x ∉ xs → All-different xs → All-different (x ∷ xs) + different-∷ : {x : A} {xs : List A} → _∉_ (P.setoid A) x xs → All-different xs → All-different (x ∷ xs) -lemma-∉-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → {h : FinMapMaybe n Carrier} → assoc is xs ≡ just h → (i ∉ toList is) → lookupM i h ≡ nothing +lemma-∉-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → {h : FinMapMaybe n Carrier} → assoc is xs ≡ just h → _∉_ (P.setoid (Fin n)) i (toList is) → lookupM i h ≡ nothing lemma-∉-lookupM-assoc i [] [] P.refl i∉is = lemma-lookupM-empty i lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') ph i∉is with assoc is' xs' | inspect (assoc is') xs' lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') () i∉is | nothing | [ ph' ] diff --git a/Structures.agda b/Structures.agda index 1a8fd64..fd44534 100644 --- a/Structures.agda +++ b/Structures.agda @@ -2,7 +2,8 @@ module Structures where open import Category.Functor using (RawFunctor ; module RawFunctor) open import Category.Monad using (module RawMonad) -open import Data.Maybe using (Maybe) renaming (monad to MaybeMonad) +open import Data.Maybe using (Maybe) +open import Data.Maybe.Categorical using () renaming (monad to MaybeMonad) open import Data.Nat using (ℕ) open import Data.Vec as V using (Vec) import Data.Vec.Properties as VP |