diff --git a/CHANGELOG.md b/CHANGELOG.md index c19b04188e..5a4c6db3f2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -266,6 +266,9 @@ Splitting up `Data.Maybe` into the standard hierarchy. * The proofs `toList⁺` and `toList⁻` in `Data.Vec.All.Properties` have been swapped as they were the opposite way round to similar properties in the rest of the library. +* The type of `antisymmetric` in `Data.List.Relation.Pointwise` has been modified to work + on heterogeneous relations. + Other major changes ------------------- @@ -822,3 +825,14 @@ Other minor additions _Respectsʳ_ : REL A B ℓ₁ → Rel B ℓ₂ → Set _ _Respectsˡ_ : REL A B ℓ₁ → Rel A ℓ₂ → Set _ ``` + +* Added new proofs to `Data.List.Relation.Pointwise`: + ```agda + reverseAcc⁺ : Pointwise R a x → Pointwise R b y → Pointwise R (reverseAcc a b) (reverseAcc x y) + reverse⁺ : Pointwise R as bs → Pointwise R (reverse as) (reverse bs) + map⁺ : ∀ f g → Pointwise (λ a b → R (f a) (g b)) as bs → Pointwise R (map f as) (map g bs) + map⁻ : ∀ f g → Pointwise R (map f as) (map g bs) → Pointwise (λ a b → R (f a) (g b)) as bs + filter⁺ : Pointwise R as bs → Pointwise R (filter P? as) (filter Q? bs) + replicate⁺ : R a b → (n : ℕ) → Pointwise R (replicate n a) (replicate n b) + irrelevant : Irrelevant R → Irrelevant (Pointwise R) + ``` diff --git a/src/Data/List/Relation/Pointwise.agda b/src/Data/List/Relation/Pointwise.agda index ef64fa9bad..3bab5008b9 100644 --- a/src/Data/List/Relation/Pointwise.agda +++ b/src/Data/List/Relation/Pointwise.agda @@ -11,12 +11,14 @@ module Data.List.Relation.Pointwise where open import Function open import Function.Inverse using (Inverse) open import Data.Product hiding (map) -open import Data.List.Base hiding (map ; head ; tail) +open import Data.List.Base as List hiding (map; head; tail) open import Data.Fin using (Fin) renaming (zero to fzero; suc to fsuc) open import Data.Nat using (ℕ; zero; suc) open import Level open import Relation.Nullary +open import Relation.Nullary.Negation using (contradiction) import Relation.Nullary.Decidable as Dec using (map′) +open import Relation.Unary as U using (Pred) open import Relation.Binary renaming (Rel to Rel₂) open import Relation.Binary.PropositionalEquality as P using (_≡_) @@ -82,10 +84,10 @@ transitive trans [] [] = [] transitive trans (x∼y ∷ xs∼ys) (y∼z ∷ ys∼zs) = trans x∼y y∼z ∷ transitive trans xs∼ys ys∼zs -antisymmetric : ∀ {a ℓ₁ ℓ₂} {A : Set a} - {_≈_ : Rel₂ A ℓ₁} {_≤_ : Rel₂ A ℓ₂} → - Antisymmetric _≈_ _≤_ → - Antisymmetric (Pointwise _≈_) (Pointwise _≤_) +antisymmetric : ∀ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} + {_≤_ : REL A B ℓ₁} {_≤′_ : REL B A ℓ₂} {_≈_ : REL A B ℓ₃} → + Antisym _≤_ _≤′_ _≈_ → + Antisym (Pointwise _≤_) (Pointwise _≤′_) (Pointwise _≈_) antisymmetric antisym [] [] = [] antisymmetric antisym (x∼y ∷ xs∼ys) (y∼x ∷ ys∼xs) = antisym x∼y y∼x ∷ antisymmetric antisym xs∼ys ys∼xs @@ -217,6 +219,76 @@ module _ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} where Pointwise-length [] = P.refl Pointwise-length (x∼y ∷ xs∼ys) = P.cong ℕ.suc (Pointwise-length xs∼ys) +------------------------------------------------------------------------ +-- reverse + +module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where + + reverseAcc⁺ : ∀ {as bs as′ bs′} → Pointwise R as′ bs′ → Pointwise R as bs → + Pointwise R (reverseAcc as′ as) (reverseAcc bs′ bs) + reverseAcc⁺ rs′ [] = rs′ + reverseAcc⁺ rs′ (r ∷ rs) = reverseAcc⁺ (r ∷ rs′) rs + + reverse⁺ : ∀ {as bs} → Pointwise R as bs → Pointwise R (reverse as) (reverse bs) + reverse⁺ = reverseAcc⁺ [] + +------------------------------------------------------------------------ +-- 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) → + Pointwise (λ a b → R (f a) (g b)) as bs → + Pointwise 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) → + Pointwise R (List.map f as) (List.map g bs) → + Pointwise (λ a b → R (f a) (g b)) as bs + map⁻ {[]} {[]} f g [] = [] + map⁻ {[]} {b ∷ bs} f g rs with Pointwise-length rs + ... | () + map⁻ {a ∷ as} {[]} f g rs with Pointwise-length rs + ... | () + 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} → Pointwise R as bs → Pointwise R (filter P? as) (filter Q? bs) + filter⁺ [] = [] + filter⁺ {a ∷ _} {b ∷ _} (r ∷ rs) with P? a | Q? b + ... | yes p | yes q = r ∷ filter⁺ rs + ... | yes p | no ¬q = contradiction (P⇒Q r p) ¬q + ... | no ¬p | yes q = contradiction (Q⇒P r q) ¬p + ... | no ¬p | no ¬q = filter⁺ rs + +------------------------------------------------------------------------ +-- replicate + +module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where + + replicate⁺ : ∀ {a b} → R a b → ∀ n → Pointwise R (replicate n a) (replicate n b) + replicate⁺ r 0 = [] + replicate⁺ r (suc n) = r ∷ replicate⁺ r n + +------------------------------------------------------------------------ +-- Irrelevance + +module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where + + irrelevant : Irrelevant R → Irrelevant (Pointwise R) + irrelevant R-irr [] [] = P.refl + irrelevant R-irr (r ∷ rs) (r₁ ∷ rs₁) = + P.cong₂ _∷_ (R-irr r r₁) (irrelevant R-irr rs rs₁) + ------------------------------------------------------------------------ -- Properties of propositional pointwise diff --git a/src/Data/List/Relation/Suffix/Heterogeneous.agda b/src/Data/List/Relation/Suffix/Heterogeneous.agda new file mode 100644 index 0000000000..32e607b043 --- /dev/null +++ b/src/Data/List/Relation/Suffix/Heterogeneous.agda @@ -0,0 +1,44 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- An inductive definition of the heterogeneous suffix relation +------------------------------------------------------------------------ + +module Data.List.Relation.Suffix.Heterogeneous where + +open import Level +open import Relation.Binary using (REL; _⇒_) +open import Data.List.Base as List using (List; []; _∷_) +open import Data.List.Relation.Pointwise as Pointwise using (Pointwise; []; _∷_) + +module _ {a b r} {A : Set a} {B : Set b} (R : REL A B r) where + + data Suffix : REL (List A) (List B) (a ⊔ b ⊔ r) where + here : ∀ {as bs} → Pointwise R as bs → Suffix as bs + there : ∀ {b as bs} → Suffix as bs → Suffix as (b ∷ bs) + + data SuffixView (as : List A) : List B → Set (a ⊔ b ⊔ r) where + _++_ : ∀ cs {ds} → Pointwise R as ds → SuffixView as (cs List.++ ds) + +module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where + + tail : ∀ {a as bs} → Suffix R (a ∷ as) bs → Suffix R as bs + tail (here (_ ∷ rs)) = there (here rs) + tail (there x) = there (tail x) + +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 → Suffix R ⇒ Suffix S + map R⇒S (here rs) = here (Pointwise.map R⇒S rs) + map R⇒S (there suf) = there (map R⇒S suf) + +module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where + + toView : ∀ {as bs} → Suffix R as bs → SuffixView R as bs + toView (here rs) = [] ++ rs + toView (there {c} suf) with toView suf + ... | cs ++ rs = (c ∷ cs) ++ rs + + fromView : ∀ {as bs} → SuffixView R as bs → Suffix R as bs + fromView ([] ++ rs) = here rs + fromView ((c ∷ cs) ++ rs) = there (fromView (cs ++ rs)) diff --git a/src/Data/List/Relation/Suffix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Suffix/Heterogeneous/Properties.agda new file mode 100644 index 0000000000..a365f2523b --- /dev/null +++ b/src/Data/List/Relation/Suffix/Heterogeneous/Properties.agda @@ -0,0 +1,185 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of the heterogeneous suffix relation +------------------------------------------------------------------------ + +module Data.List.Relation.Suffix.Heterogeneous.Properties where + +open import Function using (_$_; flip) +open import Relation.Nullary using (Dec; yes; no) +import Relation.Nullary.Decidable as Dec +open import Relation.Unary as U using (Pred) +open import Relation.Nullary.Negation using (contradiction) +open import Relation.Binary as B using (REL; Rel; Trans; Antisym; Irrelevant; _⇒_) +open import Relation.Binary.PropositionalEquality as P using (_≡_; refl; sym; subst) +open import Data.Nat as N using (suc; _+_; _≤_; _<_) +open import Data.List as List + using (List; []; _∷_; _++_; length; filter; replicate; reverse; reverseAcc) +open import Data.List.Relation.Pointwise as Pw using (Pointwise; []; _∷_; Pointwise-length) +open import Data.List.Relation.Suffix.Heterogeneous as Suffix using (Suffix; here; there; tail) +open import Data.List.Relation.Prefix.Heterogeneous as Prefix using (Prefix) +import Data.Nat.Properties as ℕₚ +import Data.List.Properties as Listₚ +import Data.List.Relation.Prefix.Heterogeneous.Properties as Prefixₚ + +------------------------------------------------------------------------ +-- reverse (convert to and from Prefix) + +module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where + + fromPrefix⁺ : ∀ {as bs} → Prefix R as bs → Suffix R (reverse as) (reverse bs) + fromPrefix⁺ {as} {bs} p with Prefix.toView p + ... | Prefix._++_ {cs} rs ds = subst (Suffix R (reverse as)) + (sym (Listₚ.reverse-++-commute cs ds)) + $ Suffix.fromView (reverse ds Suffix.++ Pw.reverse⁺ rs) + + fromPrefix⁻ : ∀ {as bs} → Prefix R (reverse as) (reverse bs) → Suffix R as bs + fromPrefix⁻ pre = P.subst₂ (Suffix R) (Listₚ.reverse-involutive _) (Listₚ.reverse-involutive _) + $ fromPrefix⁺ pre + + toPrefix⁺ : ∀ {as bs} → Suffix R as bs → Prefix R (reverse as) (reverse bs) + toPrefix⁺ {as} {bs} s with Suffix.toView s + ... | Suffix._++_ cs {ds} rs = subst (Prefix R (reverse as)) + (sym (Listₚ.reverse-++-commute cs ds)) + $ Prefix.fromView (Pw.reverse⁺ rs Prefix.++ reverse cs) + + toPrefix⁻ : ∀ {as bs} → Suffix R (reverse as) (reverse bs) → Prefix R as bs + toPrefix⁻ suf = P.subst₂ (Prefix R) (Listₚ.reverse-involutive _) (Listₚ.reverse-involutive _) + $ toPrefix⁺ suf + +------------------------------------------------------------------------ +-- length + +module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} {as} where + + length-mono-Suffix-≤ : ∀ {bs} → Suffix R as bs → length as ≤ length bs + length-mono-Suffix-≤ (here rs) = ℕₚ.≤-reflexive (Pointwise-length rs) + length-mono-Suffix-≤ (there suf) = ℕₚ.≤-step (length-mono-Suffix-≤ suf) + +------------------------------------------------------------------------ +-- Pointwise conversion + +module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where + + fromPointwise : Pointwise R ⇒ Suffix R + fromPointwise = here + + toPointwise : ∀ {as bs} → length as ≡ length bs → Suffix R as bs → Pointwise R as bs + toPointwise eq (here rs) = rs + toPointwise eq (there suf) = + let as≤bs = length-mono-Suffix-≤ suf + as>bs = ℕₚ.≤-reflexive (sym eq) + in contradiction as≤bs (ℕₚ.<⇒≱ as>bs) + +------------------------------------------------------------------------ +-- Suffix as a partial order + +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 (Suffix R) (Suffix S) (Suffix T) + trans rs⇒t (here rs) (here ss) = here (Pw.transitive rs⇒t rs ss) + trans rs⇒t (here rs) (there ssuf) = there (trans rs⇒t (here rs) ssuf) + trans rs⇒t (there rsuf) ssuf = trans rs⇒t rsuf (tail ssuf) + +module _ {a b e r s} {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 (Suffix R) (Suffix S) (Pointwise E) + antisym rs⇒e rsuf ssuf = Pw.antisymmetric + rs⇒e + (toPointwise eq rsuf) + (toPointwise (sym eq) ssuf) + where eq = ℕₚ.≤-antisym (length-mono-Suffix-≤ rsuf) (length-mono-Suffix-≤ ssuf) + +------------------------------------------------------------------------ +-- _++_ + +module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where + + ++⁺ : ∀ {as bs cs ds} → Suffix R as bs → Pointwise R cs ds → + Suffix R (as ++ cs) (bs ++ ds) + ++⁺ (here rs) rs′ = here (Pw.++⁺ rs rs′) + ++⁺ (there suf) rs′ = there (++⁺ suf rs′) + + ++⁻ : ∀ {as bs cs ds} → length cs ≡ length ds → + Suffix R (as ++ cs) (bs ++ ds) → Pointwise R cs ds + ++⁻ {_ ∷ _} {_} eq suf = ++⁻ eq (tail suf) + ++⁻ {[]} {[]} eq suf = toPointwise eq suf + ++⁻ {[]} {b ∷ bs} eq (there suf) = ++⁻ eq suf + ++⁻ {[]} {b ∷ bs} {cs} {ds} eq (here rs) = contradiction (sym eq) (ℕₚ.<⇒≢ ds