diff --git a/CHANGELOG.md b/CHANGELOG.md index 26a2fa43fd..f91e67f75f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -88,6 +88,8 @@ Other major changes generalization of the notion of "first element in the list to satisfy a predicate". +* Added new modules `Data.List.Relation.Prefix.Heterogeneous(.Properties)` + * Added new module `Data.Vec.Any.Properties` * Added new module `Relation.Binary.Properties.BoundedLattice` @@ -119,6 +121,17 @@ Other minor additions record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) ``` +* Added new modules `Category.Monad.Monotone(.*)`: + ```agda + record RawMPMonad (M : Pt I ℓ) : Set (suc ℓ) + Identity : Pt I i + record Identity + record ReaderMonad E (M : Pred I ℓ → Pt I ℓ) : Set (suc ℓ) where + record ErrorMonad (M : Pt I ℓ) : Set (suc ℓ) where + record StateMonad (M : Pt I ℓ) : Set (suc ℓ) where + record HeapMonad (M : Pt I ℓ) : Set (suc ℓ) where + ``` + * Added new functions to `Codata.Colist`: ```agda fromCowriter : Cowriter W A i → Colist W i @@ -161,6 +174,13 @@ Other minor additions mapM : (Q ⊆ M ∘′ P) → All Q ⊆ (M ∘′ All P) forA : All Q xs → (Q ⊆ F ∘′ P) → F (All P xs) forM : All Q xs → (Q ⊆ M ∘′ P) → M (All P xs) + + _++_ : ∀ {l m} → All P l → All P m → All P (l List.++ m) + _∷ʳ_ : ∀ {l : List A}{x} → All P l → P x → All P (l List.∷ʳ x) + + updateAt : ∀ {x xs} → x ∈ xs → (P x → P x) → All P xs → All P xs + _[_]%=_ : ∀ {x xs} → All P xs → x ∈ xs → (P x → P x) → All P xs + _[_]≔_ : ∀ {x xs} → All P xs → x ∈ xs → P x → All P xs ``` * Added new operators to `Data.List.Base`: @@ -175,9 +195,10 @@ Other minor additions respects : P Respects _≈_ → (All P) Respects _≋_ ``` -* Added new proof to `Data.List.Membership.Propositional.Properties`: +* Added new proofs to `Data.List.Membership.Propositional.Properties`: ```agda ∈-allFin : (k : Fin n) → k ∈ allFin n + []∈inits : [] ∈ inits as ``` * Added new function to `Data.List.Membership.(Setoid/Propositional)`: @@ -268,6 +289,7 @@ Other minor additions fromList⁻ : Any P (fromList xs) → List.Any P xs toList⁺ : Any P xs → List.Any P (toList xs) toList⁻ : List.Any P (toList xs) → Any P xs + prefix⁺ : ∀ {xs ys} → Prefix R xs ys → Any P xs → Any P ys ``` * Added new functions to `Data.Vec.Membership.Propositional.Properties`: @@ -281,6 +303,11 @@ Other minor additions wlog : Total _R_ → Symmetric Q → (∀ a b → a R b → Q a b) → ∀ a b → Q a b ``` +* Added new definition to `Relation.Binary.Core`: + ```agda + Antisym R S E = ∀ {i j} → R i j → S j i → E i j + ``` + * Added new proofs to `Relation.Binary.Lattice`: ```agda Lattice.setoid : Setoid c ℓ diff --git a/src/Category/Monad/Monotone.agda b/src/Category/Monad/Monotone.agda new file mode 100644 index 0000000000..b2e692913b --- /dev/null +++ b/src/Category/Monad/Monotone.agda @@ -0,0 +1,66 @@ +open import Relation.Binary using (Preorder) + +module Category.Monad.Monotone {ℓ}(pre : Preorder ℓ ℓ ℓ) where + +open Preorder pre renaming (Carrier to I) + +open import Level +open import Function + +open import Data.Product hiding (map) + +open import Relation.Unary +open import Relation.Unary.PredicateTransformer using (Pt) +open import Relation.Unary.Closure.Preorder pre hiding (map) + +open import Category.Monad.Predicate + +open Closed ⦃...⦄ + +record RawMPMonad (M : Pt I ℓ) : Set (suc ℓ) where + + infixl 1 _≥=_ + field + return : ∀ {P} → P ⊆ M P + _≥=_ : ∀ {P Q} → M P ⊆ (□ (P ⇒ M Q) ⇒ M Q) + + {- predicate monad -} + module _ {P : Pred I ℓ} where + + map : ∀ {Q} → M P ⊆ (□ (P ⇒ Q) ⇒ M Q) + map m f = m ≥= (λ w p → return (f w p)) + + _>>=_ : ∀ {Q : Pred I ℓ} → M P ⊆ (λ i → (P ⊆ M Q) → M Q i) + c >>= f = c ≥= λ i≤j pj → f pj + + -- infix monadic strength + infixl 10 _^_ + _^_ : ∀ {Q : Pred I ℓ}⦃ m : Closed Q ⦄ → M P ⊆ (Q ⇒ M (P ∩ Q)) + c ^ qi = c ≥= λ {j} x≤j pj → return (pj , next qi x≤j) + + -- prefix monadic strength; useful when Q cannot be inferred + ts : ∀ Q ⦃ m : Closed Q ⦄ → M P ⊆ (Q ⇒ M (P ∩ Q)) + ts _ c qi = c ^ qi + + pmonad : RawPMonad {ℓ = ℓ} M + pmonad = record + { return? = return + ; _=>= f } + + {- sequencing -} + module _ {A : Set ℓ}{P : A → Pred I ℓ} ⦃ mp : ∀ {a} → Closed (P a) ⦄ where + open import Data.List.All + + instance + _ = ∼-closed + + sequence′ : ∀ {as}{i k} → i ∼ k → + All (λ a → □ (M (P a)) i) as → M (λ j → All (λ a → P a j) as) k + sequence′ _ [] = return [] + sequence′ le (x ∷ xs) = do + px , le ← x le ^ le + pxs , px ← sequence′ le xs ^ px + return (px ∷ pxs) + + sequence : ∀ {as i} → All (λ a → □ (M (P a)) i) as → M (λ j → All (λ a → P a j) as) i + sequence = sequence′ refl diff --git a/src/Category/Monad/Monotone/Error.agda b/src/Category/Monad/Monotone/Error.agda new file mode 100644 index 0000000000..56a2518872 --- /dev/null +++ b/src/Category/Monad/Monotone/Error.agda @@ -0,0 +1,48 @@ +open import Relation.Binary hiding (_⇒_) + +module Category.Monad.Monotone.Error {ℓ}(pre : Preorder ℓ ℓ ℓ)(Exc : Set ℓ) where + +open import Function +open import Level hiding (lift) +open import Data.Sum + +open import Relation.Unary +open import Relation.Unary.Closure.Preorder pre +open import Relation.Unary.PredicateTransformer + +open import Category.Monad.Monotone pre +open import Category.Monad.Monotone.Identity pre + +open Preorder pre renaming (Carrier to I) + +ErrorT : Pt I ℓ → Pt I ℓ +ErrorT M P = M (λ i → Exc ⊎ P i) + +Error = ErrorT Identity + +record ErrorMonad (M : Pt I ℓ) : Set (suc ℓ) where + field + throw : ∀ {P i} → Exc → M P i + try_catch_ : ∀ {P} → M P ⊆ (□ (const Exc ⇒ M P)) ⇒ M P + +module _ {M} (Mon : RawMPMonad M) where + private module M = RawMPMonad Mon + + open RawMPMonad + errorT-monad : RawMPMonad (ErrorT M) + return errorT-monad px = M.return (inj₂ px) + _≥=_ errorT-monad px f = + px M.≥= λ where + v (inj₁ e) → M.return (inj₁ e) + v (inj₂ x) → f v x + + open ErrorMonad + errorT-monad-ops : ErrorMonad (ErrorT M) + throw errorT-monad-ops e = M.return (inj₁ e) + try_catch_ errorT-monad-ops c f = + c M.≥= λ where + v (inj₁ e) → f v e + v (inj₂ x) → M.return (inj₂ x) + + lift-error : ∀ {P} → M P ⊆ ErrorT M P + lift-error x = x M.>>= (λ z → M.return (inj₂ z)) diff --git a/src/Category/Monad/Monotone/Heap.agda b/src/Category/Monad/Monotone/Heap.agda new file mode 100644 index 0000000000..1ef4c5ecea --- /dev/null +++ b/src/Category/Monad/Monotone/Heap.agda @@ -0,0 +1,47 @@ +import Relation.Unary.Closure.Preorder as Closure +open import Relation.Binary using (Preorder) + +module Category.Monad.Monotone.Heap + -- ordered heap types + {ℓ}(pre : Preorder ℓ ℓ ℓ) + -- types + (T : Set ℓ) + -- weakenable values + (V : T → Preorder.Carrier pre → Set ℓ) ⦃ wkV : ∀ {a} → Closure.Closed pre (V a) ⦄ + -- heaps indexed by the heap type + (H : Preorder.Carrier pre → Set ℓ) + -- weakenable heap type membership + (_∈_ : T → Preorder.Carrier pre → Set ℓ) ⦃ wk∈ : ∀ {a} → Closure.Closed pre (_∈_ a) ⦄ where + +open Preorder pre renaming (Carrier to I) + +open import Level +open import Data.Unit using (⊤; tt) +open import Data.Product + +open import Relation.Unary hiding (_∈_) +open import Relation.Unary.PredicateTransformer using (Pt) +open import Relation.Unary.Closure.Preorder pre + +open import Category.Monad.Monotone pre +open import Category.Monad.Monotone.State pre H + +open Closed ⦃...⦄ + +record HeapMonad (M : Pt I ℓ) : Set (suc ℓ) where + field + super : StateMonad M + + open StateMonad super public + + field + store : ∀ {a} → V a ⊆ M (λ W → a ∈ W) + modify : ∀ {a} → _∈_ a ⊆ V a ⇒ M (V a) + deref : ∀ {a} → _∈_ a ⊆ M (V a) + + module HeapMonadOps (m : RawMPMonad M) where + open RawMPMonad m + open import Data.List.All as All + + storeₙ : ∀ {W as} → All (λ a → V a W) as → M (λ W' → All (λ a → a ∈ W') as) W + storeₙ vs = sequence (All.map (λ v {x} ext → store (next v ext)) vs) diff --git a/src/Category/Monad/Monotone/Heap/HList.agda b/src/Category/Monad/Monotone/Heap/HList.agda new file mode 100644 index 0000000000..7daa956194 --- /dev/null +++ b/src/Category/Monad/Monotone/Heap/HList.agda @@ -0,0 +1,75 @@ +-- An example implementation of the monotone HeapMonad +-- using heterogeneous lists as a memory model. + +import Relation.Unary.Closure.Preorder as Closure +import Relation.Binary.PropositionalEquality as P +open import Data.List.Relation.Prefix.Setoid using (preorder) +open import Data.List + +module Category.Monad.Monotone.Heap.HList + (T : Set) + (V : T → List T → Set) + ⦃ wkV : ∀ {a} → Closure.Closed (preorder (P.setoid T)) (V a) ⦄ where + +open import Function +open import Data.Product +open import Data.List.All as All +open import Data.List.All.Properties +open import Data.List.Any +open import Data.List.Any.Properties +open import Data.List.Membership.Propositional using (_∈_) +open import Data.List.Relation.Prefix.Heterogeneous +import Data.List.Relation.Pointwise as PW + +open import Relation.Unary using (Pred) +open import Relation.Binary using (Preorder) + +open import Category.Monad using (RawMonad) + +ord : Preorder _ _ _ +ord = preorder (P.setoid T) + +open Preorder ord renaming (refl to ∼-refl) +open import Relation.Unary.Closure.Preorder ord +open Closed ⦃...⦄ + +instance + _ = ∼-closed + + ∈-closed : ∀ {x} → Closed (x ∈_) + ∈-closed = record + { next = λ x∈xs xs∼ys → prefix⁺ (flip P.trans) xs∼ys x∈xs } + + All-closed : ∀ {ys} → Closed (λ xs → All (λ y → V y xs) ys) + All-closed = record + { next = λ pys xs∼zs → All.map (λ p → next p xs∼zs) pys } + +HeapT : Set +HeapT = List T + +Heap : Pred HeapT _ +Heap = λ W → All (λ a → V a W) W + +open import Category.Monad.Monotone ord +open import Category.Monad.Monotone.State ord Heap +open import Category.Monad.Monotone.Heap ord T V Heap _∈_ + +module _ {M : Set → Set}(mon : RawMonad M) where + private module M = RawMonad mon + + open HeapMonad + hlist-heap-monad : HeapMonad (MST M) + super hlist-heap-monad = mst-monad-ops mon + store hlist-heap-monad {x}{xs} v μ = + let ext = fromView (PW.refl P.refl PrefixView.++ [ x ]) + in M.return ( + xs ∷ʳ x , + ext , + ∷ʳ⁺ (next μ ext) (next v ext) , + ++⁺ʳ xs (here P.refl)) + modify hlist-heap-monad ptr v μ = + M.return (-, ∼-refl , μ [ ptr ]≔ v , All.lookup μ ptr) + deref hlist-heap-monad ptr μ = + M.return (-, ∼-refl , μ , All.lookup μ ptr) + + open HeapMonadOps hlist-heap-monad public diff --git a/src/Category/Monad/Monotone/Identity.agda b/src/Category/Monad/Monotone/Identity.agda new file mode 100644 index 0000000000..830c9b906e --- /dev/null +++ b/src/Category/Monad/Monotone/Identity.agda @@ -0,0 +1,16 @@ +open import Relation.Binary + +module Category.Monad.Monotone.Identity {i}(pre : Preorder i i i) where + +open Preorder pre renaming (Carrier to I) + +open import Relation.Unary.PredicateTransformer using (Pt) +open import Category.Monad.Monotone pre +open RawMPMonad + +Identity : Pt I i +Identity = λ P i → P i + +id-monad : RawMPMonad Identity +return id-monad px = px +_≥=_ id-monad c f = f refl c diff --git a/src/Category/Monad/Monotone/Reader.agda b/src/Category/Monad/Monotone/Reader.agda new file mode 100644 index 0000000000..2605db3173 --- /dev/null +++ b/src/Category/Monad/Monotone/Reader.agda @@ -0,0 +1,54 @@ +open import Relation.Binary using (Preorder) + +module Category.Monad.Monotone.Reader {ℓ}(pre : Preorder ℓ ℓ ℓ) where + +open import Function +open import Level + +open import Data.Product + +open import Relation.Unary.PredicateTransformer using (Pt) +open import Relation.Unary +open import Relation.Unary.Closure.Preorder pre + +open import Category.Monad +open import Category.Monad.Monotone.Identity pre +open import Category.Monad.Monotone pre + +open Preorder pre renaming (Carrier to I) +open Closed ⦃...⦄ + +ReaderT : Pred I ℓ → Pt I ℓ → Pt I ℓ +ReaderT E M P = λ i → E i → M P i + +Reader : (Pred I ℓ) → Pt I ℓ +Reader E = ReaderT E Identity + +record ReaderMonad E (M : Pred I ℓ → Pt I ℓ) : Set (suc ℓ) where + field + ask : ∀ {i} → M E E i + reader : ∀ {P} → (E ⇒ P) ⊆ M E P + local : ∀ {P E'} → (E ⇒ E') ⊆ (M E' P ⇒ M E P) + + asks : ∀ {A} → (E ⇒ A) ⊆ M E A + asks = reader + +module _ {M : Pt I ℓ}(Mon : RawMPMonad M) where + private module M = RawMPMonad Mon + + module _ {E}⦃ _ : Closed E ⦄ where + open RawMPMonad + reader-monad : RawMPMonad (ReaderT E M) + return reader-monad x e = M.return x + _≥=_ reader-monad m f e = + m e M.≥= λ + i≤j px → f i≤j px (next e i≤j) + + open ReaderMonad + reader-monad-ops : ReaderMonad E (λ E → ReaderT E M) + ask reader-monad-ops e = M.return e + reader reader-monad-ops f e = M.return (f e) + local reader-monad-ops f c e = c (f e) + + lift-reader : ∀ {P} E → M P ⊆ ReaderT E M P + lift-reader _ z _ = z diff --git a/src/Category/Monad/Monotone/State.agda b/src/Category/Monad/Monotone/State.agda new file mode 100644 index 0000000000..ab77234bf8 --- /dev/null +++ b/src/Category/Monad/Monotone/State.agda @@ -0,0 +1,48 @@ +open import Relation.Binary using (Preorder) + +module Category.Monad.Monotone.State {ℓ}(pre : Preorder ℓ ℓ ℓ) + (H : Preorder.Carrier pre → Set ℓ) + where + +open Preorder pre renaming (Carrier to I) + +open import Level +open import Function +open import Data.Product + +open import Relation.Unary +open import Relation.Unary.PredicateTransformer using (Pt) +open import Relation.Unary.Closure.Preorder pre + +open import Category.Monad +open import Category.Monad.Monotone pre +open import Category.Monad.Monotone.Identity pre + +MST : (Set ℓ → Set ℓ) → Pt I ℓ +MST M P = H ⇒ (λ i → M (∃ λ j → i ∼ j × H j × P j)) + +MSt : Pt I ℓ +MSt = MST id + +record StateMonad (M : Pt I ℓ) : Set (suc ℓ) where + field + runState : ∀ {P} → □ (H ⇒ (H ∩ P)) ⊆ M P + + get : ∀ {i} → M H i + get = runState λ _ μ → μ , μ + +module _ {M}(Mon : RawMonad {ℓ} M) where + private module M = RawMonad Mon + + open RawMPMonad + mst-monad : RawMPMonad (MST M) + return mst-monad px μ = M.return (_ , refl , μ , px) + _≥=_ mst-monad c f μ = c μ M.>>= λ where + (i₁ , ext₁ , μ₁ , pv) → (f ext₁ pv μ₁) M.>>= λ where + (i₂ , ext₂ , μ₂ , pw) → M.return (i₂ , trans ext₁ ext₂ , μ₂ , pw) + + open StateMonad + mst-monad-ops : StateMonad (MST M) + runState (mst-monad-ops) f μ = + let (μ' , p) = f refl μ + in M.return (_ , refl , μ' , p) diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda index 476edd9b16..18447e7964 100644 --- a/src/Data/Fin/Subset/Properties.agda +++ b/src/Data/Fin/Subset/Properties.agda @@ -133,8 +133,8 @@ x∈⁅y⁆⇔x≡y {_} {x} {y} = equivalence ⊆-trans p⊆q q⊆r x∈p = q⊆r (p⊆q x∈p) ⊆-antisym : ∀ {n} → Antisymmetric _≡_ (_⊆_ {n}) -⊆-antisym {x = []} {[]} p⊆q q⊆p = refl -⊆-antisym {x = x ∷ xs} {y ∷ ys} p⊆q q⊆p with x | y +⊆-antisym {i = []} {[]} p⊆q q⊆p = refl +⊆-antisym {i = x ∷ xs} {y ∷ ys} p⊆q q⊆p with x | y ... | inside | inside = cong₂ _∷_ refl (⊆-antisym (drop-∷-⊆ p⊆q) (drop-∷-⊆ q⊆p)) ... | inside | outside = contradiction (p⊆q here) λ() ... | outside | inside = contradiction (q⊆p here) λ() diff --git a/src/Data/List/All.agda b/src/Data/List/All.agda index c6e1609159..7f3dcd92fe 100644 --- a/src/Data/List/All.agda +++ b/src/Data/List/All.agda @@ -54,6 +54,23 @@ map : ∀ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} → map g [] = [] map g (px ∷ pxs) = g px ∷ map g pxs +------------------------------------------------------------------------ +-- (weak) updateAt + +module _ {a p}{A : Set a}{P : Pred A p} where + infixl 6 _[_]%=_ _[_]≔_ + + updateAt : ∀ {x xs} → x ∈ xs → (P x → P x) → All P xs → All P xs + updateAt () f [] + updateAt (here refl) f (px ∷ pxs) = f px ∷ pxs + updateAt (there i) f (px ∷ pxs) = px ∷ updateAt i f pxs + + _[_]%=_ : ∀ {x xs} → All P xs → x ∈ xs → (P x → P x) → All P xs + pxs [ i ]%= f = updateAt i f pxs + + _[_]≔_ : ∀ {x xs} → All P xs → x ∈ xs → P x → All P xs + pxs [ i ]≔ px = pxs [ i ]%= const px + ------------------------------------------------------------------------ -- (un/)zip(With/) diff --git a/src/Data/List/All/Properties.agda b/src/Data/List/All/Properties.agda index d7719f78b0..1be50b00e5 100644 --- a/src/Data/List/All/Properties.agda +++ b/src/Data/List/All/Properties.agda @@ -20,14 +20,14 @@ open import Data.List.Relation.Subset.Propositional using (_⊆_) open import Data.Maybe as Maybe using (Maybe; just; nothing) open import Data.Maybe.All as MAll using (just; nothing) open import Data.Nat using (zero; suc; z≤n; s≤s; _<_) -open import Data.Product as Prod using (_×_; _,_; uncurry; uncurry′) +open import Data.Product as Prod using (_×_; _,_; uncurry; uncurry′; map₂) open import Function open import Function.Equality using (_⟨$⟩_) open import Function.Equivalence using (_⇔_; equivalence; Equivalence) open import Function.Inverse using (_↔_; inverse) open import Function.Surjection using (_↠_; surjection) open import Relation.Binary using (Setoid; _Respects_) -open import Relation.Binary.PropositionalEquality as P using (_≡_) +open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_) open import Relation.Nullary open import Relation.Unary using (Decidable; Pred; Universal) renaming (_⊆_ to _⋐_) @@ -98,6 +98,32 @@ module _ {a b p} {A : Set a} {B : Set b} {P : B → Set p} {f : A → B} where map⁻ {xs = []} [] = [] map⁻ {xs = _ ∷ _} (p ∷ ps) = p ∷ map⁻ ps +------------------------------------------------------------------------ +-- All.map + +module _ {a p q} {A : Set a} {P : Pred A p}{Q : Pred A q} {f : P ⋐ Q} where + + map-cong : ∀ {xs}{g : P ⋐ Q} → (ps : All P xs) → + (∀ {x} → f {x} ≗ g {x}) → All.map f ps ≡ All.map g ps + map-cong [] _ = P.refl + map-cong (px ∷ ps) feq = P.cong₂ _∷_ (feq px) (map-cong ps feq) + + map-id : ∀ {xs} {f : P ⋐ P} → (ps : All P xs) → + (∀ {x} p → f {x} p ≡ p) → All.map f ps ≡ ps + map-id [] feq = P.refl + map-id (px ∷ ps) feq = P.cong₂ _∷_ (feq px) (map-id ps feq) + + map-compose : ∀ {r}{R : Pred A r}{xs}{f : P ⋐ Q}{g : Q ⋐ R}(ps : All P xs) → + All.map g (All.map f ps) ≡ All.map (g ∘ f) ps + map-compose [] = P.refl + map-compose (px ∷ ps) = P.cong (_ ∷_) (map-compose ps) + + lookup-map : ∀ {xs}{x : A}(ps : All P xs)(i : x ∈ xs) → + All.lookup (All.map f ps) i ≡ f (All.lookup ps i) + lookup-map [] () + lookup-map (px ∷ pxs) (here P.refl) = P.refl + lookup-map (px ∷ pxs) (there i) = lookup-map pxs i + -- A variant of All.map. module _ {a b p q} {A : Set a} {B : Set b} {f : A → B} @@ -254,6 +280,17 @@ module _ {a p} {A : Set a} {P : A → Set p} where singleton⁻ : ∀ {x} → All P [ x ] → P x singleton⁻ (px ∷ []) = px +------------------------------------------------------------------------ +-- snoc + +module _ {a p} {A : Set a} {P : A → Set p} where + + ∷ʳ⁺ : ∀ {xs x} → All P xs → P x → All P (xs ∷ʳ x) + ∷ʳ⁺ pxs px = ++⁺ pxs (px ∷ []) + + ∷ʳ⁻ : ∀ {xs x} → All P (xs ∷ʳ x) → All P xs × P x + ∷ʳ⁻ {xs} pxs = map₂ singleton⁻ $ ++⁻ xs pxs + ------------------------------------------------------------------------ -- fromMaybe diff --git a/src/Data/List/Any/Properties.agda b/src/Data/List/Any/Properties.agda index 8b35779e27..52a1b6cbe4 100644 --- a/src/Data/List/Any/Properties.agda +++ b/src/Data/List/Any/Properties.agda @@ -579,3 +579,15 @@ module _ {ℓ} {A B : Set ℓ} where (Any P xs × Any Q ys) ↔⟨ ×↔ ⟩ Any (λ x → Any (λ y → P x × Q y) ys) xs ↔⟨ ⊗↔ ⟩ Any (P ⟨×⟩ Q) (xs ⊗ ys) ∎ + +------------------------------------------------------------------------ +-- Prefix + +module _ {a r p} {A : Set a} {R : Rel A r} {P : Pred A p} + (resp : P Respects R) where + + open import Data.List.Relation.Prefix.Heterogeneous as Prefix + + prefix⁺ : ∀ {xs ys} → Prefix R xs ys → Any P xs → Any P ys + prefix⁺ rs e with toView rs + prefix⁺ rs e | ss Prefix.++ ts = ++⁺ˡ (lift-resp resp ss e) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index eb75c3c74c..3f87499cb3 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -142,7 +142,7 @@ fromMaybe : ∀ {a} {A : Set a} → Maybe A → List A fromMaybe (just x) = [ x ] fromMaybe nothing = [] -replicate : ∀ {a} {A : Set a} → (n : ℕ) → A → List A +replicate : ∀ {a} {A : Set a} → ℕ → A → List A replicate zero x = [] replicate (suc n) x = x ∷ replicate n x diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda index 2b26248c6e..2182314171 100644 --- a/src/Data/List/Membership/Propositional/Properties.agda +++ b/src/Data/List/Membership/Propositional/Properties.agda @@ -249,6 +249,13 @@ module _ {a} {A : Set a} {_•_ : Op₂ A} where ∈-allFin : ∀ {n} (k : Fin n) → k ∈ allFin n ∈-allFin = ∈-tabulate⁺ +------------------------------------------------------------------------ +-- inits + +[]∈inits : ∀ {a} {A : Set a} (as : List A) → [] ∈ inits as +[]∈inits [] = here refl +[]∈inits (a ∷ as) = here refl + ------------------------------------------------------------------------ -- Other properties diff --git a/src/Data/List/Relation/Prefix/Heterogeneous.agda b/src/Data/List/Relation/Prefix/Heterogeneous.agda new file mode 100644 index 0000000000..dd766d79a7 --- /dev/null +++ b/src/Data/List/Relation/Prefix/Heterogeneous.agda @@ -0,0 +1,50 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- An inductive definition of the heterogeneous prefix relation +------------------------------------------------------------------------ + +module Data.List.Relation.Prefix.Heterogeneous where + +open import Level +open import Data.List.Base as List using (List; []; _∷_) +open import Data.List.Relation.Pointwise using (Pointwise; []; _∷_) +open import Data.Product using (∃; _×_; _,_; uncurry) +open import Relation.Binary using (REL; _⇒_) + +module _ {a b r} {A : Set a} {B : Set b} (R : REL A B r) where + + data Prefix : REL (List A) (List B) r where + [] : ∀ {bs} → Prefix [] bs + _∷_ : ∀ {a b as bs} → R a b → Prefix as bs → Prefix (a ∷ as) (b ∷ bs) + + data PrefixView (as : List A) : List B → Set (b ⊔ r) where + _++_ : ∀ {cs} → Pointwise R as cs → ∀ ds → PrefixView as (cs List.++ ds) + +module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} {a b as bs} where + + head : Prefix R (a ∷ as) (b ∷ bs) → R a b + head (r ∷ rs) = r + + tail : Prefix R (a ∷ as) (b ∷ bs) → Prefix R as bs + tail (r ∷ rs) = rs + + uncons : Prefix R (a ∷ as) (b ∷ bs) → R a b × Prefix R as bs + uncons (r ∷ rs) = r , rs + +module _ {a b r s} {A : Set a} {B : Set b} {R : REL A B r} {S : REL A B s} where + + map : R ⇒ S → Prefix R ⇒ Prefix S + map R⇒S [] = [] + map R⇒S (r ∷ rs) = R⇒S r ∷ map R⇒S rs + +module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where + + toView : ∀ {as bs} → Prefix R as bs → PrefixView R as bs + toView [] = [] ++ _ + toView (r ∷ rs) with toView rs + ... | rs′ ++ ds = (r ∷ rs′) ++ ds + + fromView : ∀ {as bs} → PrefixView R as bs → Prefix R as bs + fromView ([] ++ ds) = [] + fromView ((r ∷ rs) ++ ds) = r ∷ fromView (rs ++ ds) diff --git a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda new file mode 100644 index 0000000000..8cd575cef9 --- /dev/null +++ b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda @@ -0,0 +1,221 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of the heterogeneous prefix relation +------------------------------------------------------------------------ + +module Data.List.Relation.Prefix.Heterogeneous.Properties where + +open import Data.Empty +open import Data.List.All as All using (All; []; _∷_) +import Data.List.All.Properties as All +open import Data.List.Base as List hiding (map; uncons) +open import Data.List.Membership.Propositional.Properties using ([]∈inits) +open import Data.List.Relation.Pointwise using (Pointwise; []; _∷_; isEquivalence) +open import Data.List.Relation.Prefix.Heterogeneous as Prefix hiding (PrefixView; _++_) +open import Data.Nat.Base using (ℕ; zero; suc; _≤_; z≤n; s≤s) +open import Data.Nat.Properties using (suc-injective) +open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂; uncurry) +open import Function + +open import Relation.Nullary using (yes; no; ¬_) +import Relation.Nullary.Decidable as Dec +open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Unary as U using (Pred) +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_) + +------------------------------------------------------------------------ +-- First as a decidable partial order (once made homogeneous) + +module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where + + fromPointwise : Pointwise R ⇒ Prefix R + fromPointwise [] = [] + fromPointwise (r ∷ rs) = r ∷ fromPointwise rs + + toPointwise : ∀ {as bs} → length as ≡ length bs → + Prefix R as bs → Pointwise R as bs + toPointwise {bs = []} eq [] = [] + toPointwise {bs = _ ∷ _} () [] + toPointwise eq (r ∷ rs) = r ∷ toPointwise (suc-injective eq) rs + +module _ {a b c r s t} {A : Set a} {B : Set b} {C : Set c} + {R : REL A B r} {S : REL B C s} {T : REL A C t} where + + trans : Trans R S T → Trans (Prefix R) (Prefix S) (Prefix T) + trans rs⇒t [] ss = [] + trans rs⇒t (r ∷ rs) (s ∷ ss) = rs⇒t r s ∷ trans rs⇒t rs ss + +module _ {a b r s e} {A : Set a} {B : Set b} + {R : REL A B r} {S : REL B A s} {E : REL A B e} where + + antisym : Antisym R S E → Antisym (Prefix R) (Prefix S) (Pointwise E) + antisym rs⇒e [] [] = [] + antisym rs⇒e (r ∷ rs) (s ∷ ss) = rs⇒e r s ∷ antisym rs⇒e rs ss + +------------------------------------------------------------------------ +-- length + +module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where + + length-mono-Prefix-≤ : ∀ {as bs} → Prefix R as bs → length as ≤ length bs + length-mono-Prefix-≤ [] = z≤n + length-mono-Prefix-≤ (r ∷ rs) = s≤s (length-mono-Prefix-≤ rs) + +------------------------------------------------------------------------ +-- _++_ + +module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where + + ++⁺ : ∀ {as bs cs ds} → Pointwise R as bs → + Prefix R cs ds → Prefix R (as ++ cs) (bs ++ ds) + ++⁺ [] cs⊆ds = cs⊆ds + ++⁺ (r ∷ rs) cs⊆ds = r ∷ (++⁺ rs cs⊆ds) + + ++⁻ : ∀ {as bs cs ds} → length as ≡ length bs → + Prefix R (as ++ cs) (bs ++ ds) → Prefix R cs ds + ++⁻ {[]} {[]} eq rs = rs + ++⁻ {_ ∷ _} {_ ∷ _} eq (_ ∷ rs) = ++⁻ (suc-injective eq) rs + ++⁻ {[]} {_ ∷ _} () + ++⁻ {_ ∷ _} {[]} () + +------------------------------------------------------------------------ +-- map + +module _ {a b c d r} {A : Set a} {B : Set b} {C : Set c} {D : Set d} + {R : REL C D r} where + + map⁺ : ∀ {as bs} (f : A → C) (g : B → D) → + Prefix (λ a b → R (f a) (g b)) as bs → + Prefix R (List.map f as) (List.map g bs) + map⁺ f g [] = [] + map⁺ f g (r ∷ rs) = r ∷ map⁺ f g rs + + map⁻ : ∀ {as bs} (f : A → C) (g : B → D) → + Prefix R (List.map f as) (List.map g bs) → + Prefix (λ a b → R (f a) (g b)) as bs + map⁻ {[]} {bs} f g rs = [] + map⁻ {a ∷ as} {[]} f g () + map⁻ {a ∷ as} {b ∷ bs} f g (r ∷ rs) = r ∷ map⁻ f g rs + +------------------------------------------------------------------------ +-- filter + +module _ {a b r p q} {A : Set a} {B : Set b} {R : REL A B r} + {P : Pred A p} {Q : Pred B q} (P? : U.Decidable P) (Q? : U.Decidable Q) + (P⇒Q : ∀ {a b} → R a b → P a → Q b) (Q⇒P : ∀ {a b} → R a b → Q b → P a) + where + + filter⁺ : ∀ {as bs} → Prefix R as bs → Prefix R (filter P? as) (filter Q? bs) + filter⁺ [] = [] + filter⁺ {a ∷ as} {b ∷ bs} (r ∷ rs) with P? a | Q? b + ... | yes pa | yes qb = r ∷ filter⁺ rs + ... | yes pa | no ¬qb = ⊥-elim (¬qb (P⇒Q r pa)) + ... | no ¬pa | yes qb = ⊥-elim (¬pa (Q⇒P r qb)) + ... | no ¬pa | no ¬qb = filter⁺ rs + +------------------------------------------------------------------------ +-- take + +module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where + + take⁺ : ∀ {as bs} n → Prefix R as bs → Prefix R (take n as) (take n bs) + take⁺ zero rs = [] + take⁺ (suc n) [] = [] + take⁺ (suc n) (r ∷ rs) = r ∷ take⁺ n rs + + take⁻ : ∀ {as bs} n → + Prefix R (take n as) (take n bs) → Prefix R (drop n as) (drop n bs) → + Prefix R as bs + take⁻ zero hds tls = tls + take⁻ {[]} (suc n) hds tls = [] + take⁻ {a ∷ as} {[]} (suc n) () tls + take⁻ {a ∷ as} {b ∷ bs} (suc n) (r ∷ hds) tls = r ∷ take⁻ n hds tls + +------------------------------------------------------------------------ +-- drop + + drop⁺ : ∀ {as bs} n → Prefix R as bs → Prefix R (drop n as) (drop n bs) + drop⁺ zero rs = rs + drop⁺ (suc n) [] = [] + drop⁺ (suc n) (r ∷ rs) = drop⁺ n rs + + drop⁻ : ∀ {as bs} n → Pointwise R (take n as) (take n bs) → + Prefix R (drop n as) (drop n bs) → Prefix R as bs + drop⁻ zero hds tls = tls + drop⁻ {[]} (suc n) hds tls = [] + drop⁻ {_ ∷ _} {[]} (suc n) () tls + drop⁻ {_ ∷ _} {_ ∷ _} (suc n) (r ∷ hds) tls = r ∷ (drop⁻ n hds tls) + +------------------------------------------------------------------------ +-- replicate + + replicate⁺ : ∀ {m n a b} → m ≤ n → R a b → Prefix R (replicate m a) (replicate n b) + replicate⁺ z≤n r = [] + replicate⁺ (s≤s m≤n) r = r ∷ replicate⁺ m≤n r + + replicate⁻ : ∀ {m n a b} → m ≢ 0 → Prefix R (replicate m a) (replicate n b) → R a b + replicate⁻ {zero} {n} m≢0 r = ⊥-elim (m≢0 P.refl) + replicate⁻ {suc m} {zero} m≢0 () + replicate⁻ {suc m} {suc n} m≢0 rs = Prefix.head rs + +------------------------------------------------------------------------ +-- inits + +module _ {a r} {A : Set a} {R : Rel A r} where + + inits⁺ : ∀ {as} → Pointwise R as as → All (flip (Prefix R) as) (inits as) + inits⁺ [] = [] ∷ [] + inits⁺ (r ∷ rs) = [] ∷ All.map⁺ (All.map (r ∷_) (inits⁺ rs)) + + inits⁻ : ∀ {as} → All (flip (Prefix R) as) (inits as) → Pointwise R as as + inits⁻ {as = []} rs = [] + inits⁻ {as = a ∷ as} (r ∷ rs) = + let (hd , tls) = All.unzip (All.map uncons (All.map⁻ rs)) in + All.lookup hd ([]∈inits as) ∷ inits⁻ tls + +------------------------------------------------------------------------ +-- zip(With) + +module _ {a b c} {A : Set a} {B : Set b} {C : Set c} + {d e f} {D : Set d} {E : Set e} {F : Set f} + {r s t} {R : REL A D r} {S : REL B E s} {T : REL C F t} where + + zipWith⁺ : ∀ {as bs ds es} {f : A → B → C} {g : D → E → F} → + (∀ {a b c d} → R a c → S b d → T (f a b) (g c d)) → + Prefix R as ds → Prefix S bs es → + Prefix T (zipWith f as bs) (zipWith g ds es) + zipWith⁺ f [] ss = [] + zipWith⁺ f (r ∷ rs) [] = [] + zipWith⁺ f (r ∷ rs) (s ∷ ss) = f r s ∷ zipWith⁺ f rs ss + +module _ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} + {r s} {R : REL A C r} {S : REL B D s} where + + private + R×S : REL (A × B) (C × D) _ + R×S (a , b) (c , d) = R a c × S b d + + zip⁺ : ∀ {as bs cs ds} → Prefix R as cs → Prefix S bs ds → + Prefix R×S (zip as bs) (zip cs ds) + zip⁺ = zipWith⁺ _,_ + +------------------------------------------------------------------------ +-- Irrelevant + +module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where + + irrelevant : Irrelevant R → Irrelevant (Prefix R) + irrelevant R-irr [] [] = P.refl + irrelevant R-irr (r ∷ rs) (r′ ∷ rs′) = + P.cong₂ _∷_ (R-irr r r′) (irrelevant R-irr rs rs′) + +------------------------------------------------------------------------ +-- Decidability + + prefix? : Decidable R → Decidable (Prefix R) + prefix? R? [] bs = yes [] + prefix? R? (a ∷ as) [] = no (λ ()) + prefix? R? (a ∷ as) (b ∷ bs) = Dec.map′ (uncurry _∷_) uncons + $ R? a b ×-dec prefix? R? as bs diff --git a/src/Data/List/Relation/Prefix/Setoid.agda b/src/Data/List/Relation/Prefix/Setoid.agda new file mode 100644 index 0000000000..b56357d2cd --- /dev/null +++ b/src/Data/List/Relation/Prefix/Setoid.agda @@ -0,0 +1,33 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The prefix relation over setoid equality. +------------------------------------------------------------------------ + +open import Relation.Binary using (Setoid; IsPreorder; Preorder; IsEquivalence) + +module Data.List.Relation.Prefix.Setoid + {c ℓ} (S : Setoid c ℓ) where + +open import Data.List using (List) +open import Data.List.Membership.Setoid S using (_∈_) +open import Data.List.Relation.Prefix.Heterogeneous +open import Data.List.Relation.Prefix.Heterogeneous.Properties +open import Data.List.Relation.Pointwise hiding (isPreorder; preorder) +open import Level using (_⊔_) +open import Relation.Nullary using (¬_) + +open Setoid S using () renaming (Carrier to A) +module S = Setoid S + +------------------------------------------------------------------------ +-- Definitions + +isPreorder : IsPreorder {A = List A} (Pointwise S._≈_) (Prefix S._≈_) +isPreorder = record + { isEquivalence = isEquivalence S.isEquivalence + ; reflexive = fromPointwise + ; trans = trans S.trans } + +preorder : Preorder _ _ _ +preorder = record { isPreorder = isPreorder } diff --git a/src/Relation/Binary/Core.agda b/src/Relation/Binary/Core.agda index ac6599c2d4..2a51cd7df8 100644 --- a/src/Relation/Binary/Core.agda +++ b/src/Relation/Binary/Core.agda @@ -97,8 +97,12 @@ TransFlip P Q R = ∀ {i j k} → Q j k → P i j → R i k Transitive : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _ Transitive _∼_ = Trans _∼_ _∼_ _∼_ +Antisym : ∀ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} → + REL A B ℓ₁ → REL B A ℓ₂ → REL A B ℓ₃ → Set _ +Antisym R S E = ∀ {i j} → R i j → S j i → E i j + Antisymmetric : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _ -Antisymmetric _≈_ _≤_ = ∀ {x y} → x ≤ y → y ≤ x → x ≈ y +Antisymmetric _≈_ _≤_ = Antisym _≤_ _≤_ _≈_ Asymmetric : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _ Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x) diff --git a/src/Relation/Unary/Closure/Preorder.agda b/src/Relation/Unary/Closure/Preorder.agda index 2d16751886..339e2224fe 100644 --- a/src/Relation/Unary/Closure/Preorder.agda +++ b/src/Relation/Unary/Closure/Preorder.agda @@ -9,6 +9,7 @@ open import Relation.Binary module Relation.Unary.Closure.Preorder {a r e} (P : Preorder a e r) where open Preorder P + open import Relation.Unary using (Pred) -- Specialising the results proven generically in `Base`. @@ -28,3 +29,6 @@ module _ {t} {T : Pred Carrier t} where □-closed : ∀ {t} {T : Pred Carrier t} → Closed (□ T) □-closed = Base.□-closed trans + +∼-closed : ∀ {x} → Closed (x ∼_) +∼-closed = record { next = λ x∼y y∼z → trans x∼y y∼z }