Some work on formalizing Suffix (re: #517)

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)
+  ```

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
 

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))

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<cs)
+    where
+    open ℕₚ.≤-Reasoning
+    ds<cs : length ds < length cs
+    ds<cs = begin suc (length ds)             ≤⟨ N.s≤s (ℕₚ.n≤m+n (length bs) (length ds)) ⟩
+                  suc (length bs + length ds) ≡⟨ sym $ Listₚ.length-++ (b ∷ bs) ⟩
+                  length (b ∷ bs ++ ds)       ≡⟨ sym $ Pointwise-length rs ⟩
+                  length cs                    ∎
+
+------------------------------------------------------------------------
+-- 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) →
+         Suffix (λ a b → R (f a) (g b)) as bs →
+         Suffix R (List.map f as) (List.map g bs)
+  map⁺ f g (here rs)   = here (Pw.map⁺ f g rs)
+  map⁺ f g (there suf) = there (map⁺ f g suf)
+
+  map⁻ : ∀ {as bs} (f : A → C) (g : B → D) →
+         Suffix R (List.map f as) (List.map g bs) →
+         Suffix (λ a b → R (f a) (g b)) as bs
+  map⁻ {as} {b ∷ bs} f g (here rs) = here (Pw.map⁻ f g rs)
+  map⁻ {as} {b ∷ bs} f g (there suf) = there (map⁻ f g suf)
+  map⁻ {x ∷ as} {[]} f g suf with length-mono-Suffix-≤ suf
+  ... | ()
+  map⁻ {[]} {[]} f g suf = here []
+
+------------------------------------------------------------------------
+-- 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} → Suffix R as bs → Suffix R (filter P? as) (filter Q? bs)
+  filter⁺ (here rs) = here (Pw.filter⁺ P? Q? P⇒Q Q⇒P rs)
+  filter⁺ (there {a} suf) with Q? a
+  ... | yes q = there (filter⁺ suf)
+  ... | no ¬q = filter⁺ suf
+
+------------------------------------------------------------------------
+-- replicate
+
+module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
+
+  replicate⁺ : ∀ {m n a b} → m ≤ n → R a b → Suffix R (replicate m a) (replicate n b)
+  replicate⁺ {a = a} {b = b} m≤n r = repl (ℕₚ.≤⇒≤′ m≤n)
+    where
+    repl : ∀ {m n} → m N.≤′ n → Suffix R (replicate m a) (replicate n b)
+    repl N.≤′-refl       = here (Pw.replicate⁺ r _)
+    repl (N.≤′-step m≤n) = there (repl m≤n)
+
+------------------------------------------------------------------------
+-- Irrelevant
+
+module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
+
+  irrelevant : Irrelevant R → Irrelevant (Suffix R)
+  irrelevant R-irr (here rs)    (here rs₁)    = P.cong here $ Pw.irrelevant R-irr rs rs₁
+  irrelevant R-irr (here rs)    (there rsuf)  = contradiction (length-mono-Suffix-≤ rsuf)
+                                                              (ℕₚ.<⇒≱ (ℕₚ.≤-reflexive (sym (Pointwise-length rs))))
+  irrelevant R-irr (there rsuf) (here rs)     = contradiction (length-mono-Suffix-≤ rsuf)
+                                                              (ℕₚ.<⇒≱ (ℕₚ.≤-reflexive (sym (Pointwise-length rs))))
+  irrelevant R-irr (there rsuf) (there rsuf₁) = P.cong there $ irrelevant R-irr rsuf rsuf₁
+
+------------------------------------------------------------------------
+-- Decidability
+
+  suffix? : B.Decidable R → B.Decidable (Suffix R)
+  suffix? R? as bs = Dec.map′ fromPrefix⁻ toPrefix⁺
+                   $ Prefixₚ.prefix? R? (reverse as) (reverse bs)