{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Relation.Binary.Prefix.Heterogeneous.Properties where
open import Level
open import Data.Bool.Base using (true; false)
open import Data.Empty
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
import Data.List.Relation.Unary.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.Binary.Pointwise.Base using (Pointwise; []; _∷_)
open import Data.List.Relation.Binary.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.Base as Product using (_×_; _,_; proj₁; proj₂; uncurry)
open import Function.Base
open import Relation.Nullary.Negation using (¬_)
open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no; _because_)
open import Relation.Unary as U using (Pred)
open import Relation.Binary.Core using (Rel; REL; _⇒_)
open import Relation.Binary.Definitions
using (Trans; Antisym; Irrelevant; Decidable)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong₂)
private
variable
a b r s : Level
A : Set a
B : Set b
R : REL A B r
S : REL A B s
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 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-mono : ∀ {as bs} → Prefix R as bs → length as ≤ length bs
length-mono [] = z≤n
length-mono (r ∷ rs) = s≤s (length-mono rs)
++⁺ : ∀ {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
++⁻ {as = []} {[]} eq rs = rs
++⁻ {as = _ ∷ _} {_ ∷ _} eq (_ ∷ rs) = ++⁻ (suc-injective eq) rs
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} {b ∷ bs} f g (r ∷ rs) = r ∷ map⁻ f g rs
module _ {p q} {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
... | true because _ | true because _ = r ∷ filter⁺ rs
... | yes pa | no ¬qb = ⊥-elim (¬qb (P⇒Q r pa))
... | no ¬pa | yes qb = ⊥-elim (¬pa (Q⇒P r qb))
... | false because _ | false because _ = filter⁺ rs
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⁻ {as = []} (suc n) hds tls = []
take⁻ {as = a ∷ as} {b ∷ bs} (suc n) (r ∷ hds) tls = r ∷ take⁻ n hds tls
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⁻ {as = []} (suc n) hds tls = []
drop⁻ {as = _ ∷ _} {_ ∷ _} (suc n) (r ∷ hds) tls = r ∷ (drop⁻ n hds tls)
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⁻ {m = zero} {n} m≢0 r = ⊥-elim (m≢0 refl)
replicate⁻ {m = suc m} {suc n} m≢0 rs = Prefix.head rs
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
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⁺ _,_
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 [] [] = refl
irrelevant R-irr (r ∷ rs) (r′ ∷ rs′) =
cong₂ _∷_ (R-irr r r′) (irrelevant R-irr rs rs′)
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