From dfd3d5e6ec6d63ca0279756816b1622376fb2b30 Mon Sep 17 00:00:00 2001 From: Github Actions Date: Mon, 9 Dec 2024 11:06:15 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20agda/agd?= =?UTF-8?q?a-stdlib@8d5403a48b831a3dde784bd610ddd0c850952e56=20?= =?UTF-8?q?=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...sitional.Example.UniqueBoundVariables.html | 38 +- ...nary.Sublist.Propositional.Properties.html | 449 +++++++++--------- 2 files changed, 242 insertions(+), 245 deletions(-) diff --git a/master/Data.List.Relation.Binary.Sublist.Propositional.Example.UniqueBoundVariables.html b/master/Data.List.Relation.Binary.Sublist.Propositional.Example.UniqueBoundVariables.html index 9bb33c4270..0a8432e072 100644 --- a/master/Data.List.Relation.Binary.Sublist.Propositional.Example.UniqueBoundVariables.html +++ b/master/Data.List.Relation.Binary.Sublist.Propositional.Example.UniqueBoundVariables.html @@ -30,14 +30,14 @@ ) open import Data.List.Relation.Binary.Sublist.Propositional.Properties using ( ∷ˡ⁻ - ; ⊆-trans-assoc - ; from∈∘to∈; from∈∘lookup; lookup-⊆-trans - ; ⊆-pushoutˡ-is-wpo + ; ⊆-trans-assoc + ; from∈∘to∈; from∈∘lookup; lookup-⊆-trans + ; ⊆-pushoutˡ-is-wpo ; Disjoint→DisjointUnion; DisjointUnion→Disjoint - ; Disjoint-sym; DisjointUnion-inj₁; DisjointUnion-inj₂; DisjointUnion-[]ʳ + ; Disjoint-sym; DisjointUnion-inj₁; DisjointUnion-inj₂; DisjointUnion-[]ʳ ; weakenDisjoint; weakenDisjointUnion; shrinkDisjointˡ ; disjoint⇒disjoint-to-union; DisjointUnion-fromAny∘toAny-∷ˡ⁻ - ; equalize-separators + ; equalize-separators ) open import Data.Product.Base using (_,_; proj₁; proj₂) @@ -132,7 +132,7 @@ where y′ = lookup γ y -- Typing: y′# : DisjointUnion (from∈ y′) (⊆-trans β\y γ) (⊆-trans β γ) - y′# = subst (λ □ → DisjointUnion □ _ _) (sym (from∈∘lookup _ _)) (weakenDisjointUnion γ y#) + y′# = subst (λ □ → DisjointUnion □ _ _) (sym (from∈∘lookup _ _)) (weakenDisjointUnion γ y#) -- We bring de Bruijn terms into scope as Exp. @@ -202,11 +202,11 @@ (let t′ = weakenBV γ t) → δ ⊢ e ~ β ▷ t → δ′ ⊢ e ~ β′ ▷ t′ -weaken~ γ (var refl δ#β) = var (lookup-⊆-trans γ _) (weakenDisjoint γ δ#β) +weaken~ γ (var refl δ#β) = var (lookup-⊆-trans γ _) (weakenDisjoint γ δ#β) weaken~ γ (abs y#δ y#β d) = abs y′#δ′ y′#β′ (weaken~ γ d) where - y′#δ′ = subst (λ □ → DisjointUnion □ _ _) (sym (from∈∘lookup _ _)) (weakenDisjointUnion γ y#δ) - y′#β′ = subst (λ □ → DisjointUnion □ _ _) (sym (from∈∘lookup _ _)) (weakenDisjointUnion γ y#β) + y′#δ′ = subst (λ □ → DisjointUnion □ _ _) (sym (from∈∘lookup _ _)) (weakenDisjointUnion γ y#δ) + y′#β′ = subst (λ □ → DisjointUnion □ _ _) (sym (from∈∘lookup _ _)) (weakenDisjointUnion γ y#β) weaken~ γ (app dₜ dᵤ t#u) = app (weaken~ γ dₜ) (weaken~ γ dᵤ) (weakenDisjointUnion γ t#u) -- Lemma: If δ ⊢ e ~ β ▷ t, then @@ -220,7 +220,7 @@ where δ#y = Disjoint-sym (DisjointUnion→Disjoint y⊎δ) yδ#β = disjoint-fv-bv d - δ⊆yδ,eq = DisjointUnion-inj₂ y⊎δ + δ⊆yδ,eq = DisjointUnion-inj₂ y⊎δ δ⊆yδ = proj₁ δ⊆yδ,eq eq = proj₂ δ⊆yδ,eq δ#β = subst (λ □ → Disjoint □ _) eq (shrinkDisjointˡ δ⊆yδ yδ#β) @@ -294,7 +294,7 @@ [a]⊆aΔ : [ a ] ⊆ (a ∷ Δ) [a]⊆aΔ = refl ∷ minimum _ eq : ⊆-trans [a]⊆aΔ zδ ≡ [a]⊆Γ - eq = sym (from∈∘to∈ _) + eq = sym (from∈∘to∈ _) z#β : Disjoint [a]⊆Γ β z#β = subst (λ □ → Disjoint □ β) eq (shrinkDisjointˡ [a]⊆aΔ zδ#β) z⊎β = Disjoint→DisjointUnion z#β @@ -355,7 +355,7 @@ δ₂′#β₂′ : Disjoint δ₂′ β₂′ δ₂′#β₂′ = weakenDisjoint ϕ₂ δ₂#β₂ δ₁′≡δ₂′ : δ₁′ ≡ δ₂′ - δ₁′≡δ₂′ = ⊆-pushoutˡ-is-wpo δ₁ δ₂ + δ₁′≡δ₂′ = ⊆-pushoutˡ-is-wpo δ₁ δ₂ δ₂′#β₁′ : Disjoint δ₂′ β₁′ δ₂′#β₁′ = subst (λ □ → Disjoint □ β₁′) δ₁′≡δ₂′ δ₁′#β₁′ @@ -372,14 +372,14 @@ β̇ = proj₁ (proj₂ uni) β₁″⊎β₂″ : DisjointUnion β₁″ β₂″ β̇ β₁″⊎β₂″ = proj₂ (proj₂ uni) - ι₁ = DisjointUnion-inj₁ β₁″⊎β₂″ - ι₂ = DisjointUnion-inj₂ β₁″⊎β₂″ + ι₁ = DisjointUnion-inj₁ β₁″⊎β₂″ + ι₂ = DisjointUnion-inj₂ β₁″⊎β₂″ -- after separation, the FVs are still disjoint from the BVs. δ₁″ = ⊆-trans δ₂′ γ₁ δ₂″ = ⊆-trans δ₂′ γ₂ δ₁″≡δ₂″ : δ₁″ ≡ δ₂″ - δ₁″≡δ₂″ = equalize-separators δ₂′#β₁′ δ₂′#β₂′ + δ₁″≡δ₂″ = equalize-separators δ₂′#β₁′ δ₂′#β₂′ δ₁″#β₁″ : Disjoint δ₁″ β₁″ δ₁″#β₁″ = weakenDisjoint γ₁ δ₂′#β₁′ δ₂″#β₂″ : Disjoint δ₂″ β₂″ @@ -399,14 +399,14 @@ d₁′ = weaken~ γ₁′ d₁ δ₁≤δ̇ : ⊆-trans δ₁ γ₁′ ≡ ⊆-trans δ₂′ γ₂ δ₁≤δ̇ = begin - ⊆-trans δ₁ γ₁′ ≡⟨ ⊆-trans-assoc ⟩ + ⊆-trans δ₁ γ₁′ ≡⟨ ⊆-trans-assoc ⟩ ⊆-trans δ₁′ γ₁ ≡⟨ cong (λ □ → ⊆-trans □ γ₁) δ₁′≡δ₂′ ⟩ ⊆-trans δ₂′ γ₁ ≡⟨⟩ δ₁″ ≡⟨ δ₁″≡δ₂″ ⟩ δ₂″ ≡⟨⟩ δ̇ ∎ β₁≤β₁″ : ⊆-trans β₁ γ₁′ ≡ β₁″ - β₁≤β₁″ = ⊆-trans-assoc + β₁≤β₁″ = ⊆-trans-assoc d₁″ : δ̇ ⊢ f ~ β₁″ ▷ subst (λ □ → Tm □ _) β₁≤β₁″ (weakenBV γ₁′ t) d₁″ = subst~ δ₁≤δ̇ β₁≤β₁″ refl d₁′ @@ -414,9 +414,9 @@ d₂′ : ⊆-trans δ₂ γ₂′ ⊢ e ~ ⊆-trans β₂ γ₂′ ▷ weakenBV γ₂′ u d₂′ = weaken~ γ₂′ d₂ β₂≤β₂″ : ⊆-trans β₂ γ₂′ ≡ β₂″ - β₂≤β₂″ = ⊆-trans-assoc + β₂≤β₂″ = ⊆-trans-assoc δ₂≤δ̇ : ⊆-trans δ₂ γ₂′ ≡ δ̇ - δ₂≤δ̇ = ⊆-trans-assoc + δ₂≤δ̇ = ⊆-trans-assoc d₂″ : δ̇ ⊢ e ~ β₂″ ▷ subst (λ □ → Tm □ _) β₂≤β₂″ (weakenBV γ₂′ u) d₂″ = subst~ δ₂≤δ̇ β₂≤β₂″ refl d₂′ \ No newline at end of file diff --git a/master/Data.List.Relation.Binary.Sublist.Propositional.Properties.html b/master/Data.List.Relation.Binary.Sublist.Propositional.Properties.html index f6eee86903..700eec7d57 100644 --- a/master/Data.List.Relation.Binary.Sublist.Propositional.Properties.html +++ b/master/Data.List.Relation.Binary.Sublist.Propositional.Properties.html @@ -7,230 +7,227 @@ {-# OPTIONS --cubical-compatible --safe #-} -module Data.List.Relation.Binary.Sublist.Propositional.Properties - {a} {A : Set a} where - -open import Data.List.Base using (List; []; _∷_; map) -open import Data.List.Membership.Propositional using (_∈_) -open import Data.List.Relation.Unary.All using (All; []; _∷_) -open import Data.List.Relation.Unary.Any using (Any; here; there) -open import Data.List.Relation.Unary.Any.Properties - using (here-injective; there-injective) -open import Data.List.Relation.Binary.Sublist.Propositional - hiding (map) -import Data.List.Relation.Binary.Sublist.Setoid.Properties - as SetoidProperties -open import Data.Product.Base using (∃; _,_; proj₂) -open import Function.Base using (id; _∘_; _∘′_) -open import Level using (Level) -open import Relation.Binary.Definitions using (_Respects_) -open import Relation.Binary.PropositionalEquality.Core as ≡ - using (_≡_; refl; cong; _≗_; trans) -open import Relation.Binary.PropositionalEquality.Properties - using (setoid; subst-injective; trans-reflʳ; trans-assoc) -open import Relation.Unary using (Pred) - -private - variable - b ℓ : Level - B : Set b - ------------------------------------------------------------------------- --- Re-exporting setoid properties - -open SetoidProperties (setoid A) public - hiding (map⁺; ⊆-trans-idˡ; ⊆-trans-idʳ; ⊆-trans-assoc) - -map⁺ : ∀ {as bs} (f : A → B) → as ⊆ bs → map f as ⊆ map f bs -map⁺ {B = B} f = SetoidProperties.map⁺ (setoid A) (setoid B) (cong f) - ------------------------------------------------------------------------- --- Category laws for _⊆_ - -⊆-trans-idˡ : ∀ {xs ys : List A} {τ : xs ⊆ ys} → - ⊆-trans ⊆-refl τ ≡ τ -⊆-trans-idˡ {τ = τ} = SetoidProperties.⊆-trans-idˡ (setoid A) (λ _ → refl) τ - -⊆-trans-idʳ : ∀ {xs ys : List A} {τ : xs ⊆ ys} → - ⊆-trans τ ⊆-refl ≡ τ -⊆-trans-idʳ {τ = τ} = SetoidProperties.⊆-trans-idʳ (setoid A) trans-reflʳ τ - --- Note: The associativity law is oriented such that rewriting with it --- may trigger reductions of ⊆-trans, which matches first on its --- second argument and then on its first argument. - -⊆-trans-assoc : ∀ {ws xs ys zs : List A} - {τ₁ : ws ⊆ xs} {τ₂ : xs ⊆ ys} {τ₃ : ys ⊆ zs} → - ⊆-trans τ₁ (⊆-trans τ₂ τ₃) ≡ ⊆-trans (⊆-trans τ₁ τ₂) τ₃ -⊆-trans-assoc {τ₁ = τ₁} {τ₂ = τ₂} {τ₃ = τ₃} = - SetoidProperties.⊆-trans-assoc (setoid A) (λ p _ _ → ≡.sym (trans-assoc p)) τ₁ τ₂ τ₃ - ------------------------------------------------------------------------- --- Laws concerning ⊆-trans and ∷ˡ⁻ - -⊆-trans-∷ˡ⁻ᵣ : ∀ {y} {xs ys zs : List A} {τ : xs ⊆ ys} {σ : (y ∷ ys) ⊆ zs} → - ⊆-trans τ (∷ˡ⁻ σ) ≡ ⊆-trans (y ∷ʳ τ) σ -⊆-trans-∷ˡ⁻ᵣ {σ = x ∷ σ} = refl -⊆-trans-∷ˡ⁻ᵣ {σ = y ∷ʳ σ} = cong (y ∷ʳ_) ⊆-trans-∷ˡ⁻ᵣ - -⊆-trans-∷ˡ⁻ₗ : ∀ {x} {xs ys zs : List A} {τ : (x ∷ xs) ⊆ ys} {σ : ys ⊆ zs} → - ⊆-trans (∷ˡ⁻ τ) σ ≡ ∷ˡ⁻ (⊆-trans τ σ) -⊆-trans-∷ˡ⁻ₗ {σ = y ∷ʳ σ} = cong (y ∷ʳ_) ⊆-trans-∷ˡ⁻ₗ -⊆-trans-∷ˡ⁻ₗ {τ = y ∷ʳ τ} {σ = refl ∷ σ} = cong (y ∷ʳ_) ⊆-trans-∷ˡ⁻ₗ -⊆-trans-∷ˡ⁻ₗ {τ = refl ∷ τ} {σ = refl ∷ σ} = refl - -⊆-∷ˡ⁻trans-∷ : ∀ {y} {xs ys zs : List A} {τ : xs ⊆ ys} {σ : (y ∷ ys) ⊆ zs} → - ∷ˡ⁻ (⊆-trans (refl ∷ τ) σ) ≡ ⊆-trans (y ∷ʳ τ) σ -⊆-∷ˡ⁻trans-∷ {σ = y ∷ʳ σ} = cong (y ∷ʳ_) ⊆-∷ˡ⁻trans-∷ -⊆-∷ˡ⁻trans-∷ {σ = refl ∷ σ} = refl - ------------------------------------------------------------------------- --- Relationships to other predicates - --- All P is a contravariant functor from _⊆_ to Set. - -All-resp-⊆ : {P : Pred A ℓ} → (All P) Respects _⊇_ -All-resp-⊆ [] [] = [] -All-resp-⊆ (_ ∷ʳ p) (_ ∷ xs) = All-resp-⊆ p xs -All-resp-⊆ (refl ∷ p) (x ∷ xs) = x ∷ All-resp-⊆ p xs - --- Any P is a covariant functor from _⊆_ to Set. - -Any-resp-⊆ : {P : Pred A ℓ} → (Any P) Respects _⊆_ -Any-resp-⊆ = lookup - ------------------------------------------------------------------------- --- Functor laws for All-resp-⊆ - --- First functor law: identity. - -All-resp-⊆-refl : ∀ {P : Pred A ℓ} {xs : List A} → - All-resp-⊆ ⊆-refl ≗ id {A = All P xs} -All-resp-⊆-refl [] = refl -All-resp-⊆-refl (p ∷ ps) = cong (p ∷_) (All-resp-⊆-refl ps) - --- Second functor law: composition. - -All-resp-⊆-trans : ∀ {P : Pred A ℓ} {xs ys zs} {τ : xs ⊆ ys} (τ′ : ys ⊆ zs) → - All-resp-⊆ {P = P} (⊆-trans τ τ′) ≗ All-resp-⊆ τ ∘ All-resp-⊆ τ′ -All-resp-⊆-trans (_ ∷ʳ τ′) (p ∷ ps) = All-resp-⊆-trans τ′ ps -All-resp-⊆-trans {τ = _ ∷ʳ _ } (refl ∷ τ′) (p ∷ ps) = All-resp-⊆-trans τ′ ps -All-resp-⊆-trans {τ = refl ∷ _} (refl ∷ τ′) (p ∷ ps) = cong (p ∷_) (All-resp-⊆-trans τ′ ps) -All-resp-⊆-trans {τ = [] } ([] ) [] = refl - ------------------------------------------------------------------------- --- Functor laws for Any-resp-⊆ / lookup - --- First functor law: identity. - -Any-resp-⊆-refl : ∀ {P : Pred A ℓ} {xs} → - Any-resp-⊆ ⊆-refl ≗ id {A = Any P xs} -Any-resp-⊆-refl (here p) = refl -Any-resp-⊆-refl (there i) = cong there (Any-resp-⊆-refl i) - -lookup-⊆-refl = Any-resp-⊆-refl - --- Second functor law: composition. - -Any-resp-⊆-trans : ∀ {P : Pred A ℓ} {xs ys zs} {τ : xs ⊆ ys} (τ′ : ys ⊆ zs) → - Any-resp-⊆ {P = P} (⊆-trans τ τ′) ≗ Any-resp-⊆ τ′ ∘ Any-resp-⊆ τ -Any-resp-⊆-trans (_ ∷ʳ τ′) i = cong there (Any-resp-⊆-trans τ′ i) -Any-resp-⊆-trans {τ = _ ∷ʳ _} (_ ∷ τ′) i = cong there (Any-resp-⊆-trans τ′ i) -Any-resp-⊆-trans {τ = _ ∷ _} (_ ∷ τ′) (there i) = cong there (Any-resp-⊆-trans τ′ i) -Any-resp-⊆-trans {τ = refl ∷ _} (_ ∷ τ′) (here _) = refl -Any-resp-⊆-trans {τ = [] } [] () - -lookup-⊆-trans = Any-resp-⊆-trans - ------------------------------------------------------------------------- --- The `lookup` function for `xs ⊆ ys` is injective. --- --- Note: `lookup` can be seen as a strictly increasing reindexing --- function for indices into `xs`, producing indices into `ys`. - -lookup-injective : ∀ {P : Pred A ℓ} {xs ys} {τ : xs ⊆ ys} {i j : Any P xs} → - lookup τ i ≡ lookup τ j → i ≡ j -lookup-injective {τ = _ ∷ʳ _} = lookup-injective ∘′ there-injective -lookup-injective {τ = x≡y ∷ _} {here _} {here _} = cong here ∘′ subst-injective x≡y ∘′ here-injective - -- Note: instead of using subst-injective, we could match x≡y against refl on the lhs. - -- However, this turns the following clause into a non-strict match. -lookup-injective {τ = _ ∷ _} {there _} {there _} = cong there ∘′ lookup-injective ∘′ there-injective - ------------------------------------------------------------------------- --- from∈ ∘ to∈ turns a sublist morphism τ : x∷xs ⊆ ys into a morphism --- [x] ⊆ ys. The same morphism is obtained by pre-composing τ with --- the canonial morphism [x] ⊆ x∷xs. --- --- Note: This lemma does not hold for Sublist.Setoid, but could hold for --- a hypothetical Sublist.Groupoid where trans refl = id. - -from∈∘to∈ : ∀ {x : A} {xs ys} (τ : x ∷ xs ⊆ ys) → - from∈ (to∈ τ) ≡ ⊆-trans (refl ∷ minimum xs) τ -from∈∘to∈ (x≡y ∷ τ) = cong (x≡y ∷_) ([]⊆-irrelevant _ _) -from∈∘to∈ (y ∷ʳ τ) = cong (y ∷ʳ_) (from∈∘to∈ τ) - -from∈∘lookup : ∀{x : A} {xs ys} (τ : xs ⊆ ys) (i : x ∈ xs) → - from∈ (lookup τ i) ≡ ⊆-trans (from∈ i) τ -from∈∘lookup (y ∷ʳ τ) i = cong (y ∷ʳ_) (from∈∘lookup τ i) -from∈∘lookup (_ ∷ τ) (there i) = cong (_ ∷ʳ_) (from∈∘lookup τ i) -from∈∘lookup (refl ∷ τ) (here refl) = cong (refl ∷_) ([]⊆-irrelevant _ _) - ------------------------------------------------------------------------- --- Weak pushout (wpo) - --- A raw pushout is a weak pushout if the pushout square commutes. - -IsWeakPushout : ∀{xs ys zs : List A} {τ : xs ⊆ ys} {σ : xs ⊆ zs} → - RawPushout τ σ → Set a -IsWeakPushout {τ = τ} {σ = σ} rpo = - ⊆-trans τ (RawPushout.leg₁ rpo) ≡ - ⊆-trans σ (RawPushout.leg₂ rpo) - --- Joining two list extensions with ⊆-pushout produces a weak pushout. - -⊆-pushoutˡ-is-wpo : ∀{xs ys zs : List A} (τ : xs ⊆ ys) (σ : xs ⊆ zs) → - IsWeakPushout (⊆-pushoutˡ τ σ) -⊆-pushoutˡ-is-wpo [] σ - rewrite ⊆-trans-idʳ {τ = σ} - = ⊆-trans-idˡ {xs = []} -⊆-pushoutˡ-is-wpo (y ∷ʳ τ) σ = cong (y ∷ʳ_) (⊆-pushoutˡ-is-wpo τ σ) -⊆-pushoutˡ-is-wpo (x≡y ∷ τ) (z ∷ʳ σ) = cong (z ∷ʳ_) (⊆-pushoutˡ-is-wpo (x≡y ∷ τ) σ) -⊆-pushoutˡ-is-wpo (refl ∷ τ) (refl ∷ σ) = cong (refl ∷_) (⊆-pushoutˡ-is-wpo τ σ) - ------------------------------------------------------------------------- --- Properties of disjointness - --- From τ₁ ⊎ τ₂ = τ, compute the injection ι₁ such that τ₁ = ⊆-trans ι₁ τ. - -DisjointUnion-inj₁ : ∀ {xs ys zs xys : List A} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : xys ⊆ zs} → - DisjointUnion τ₁ τ₂ τ → ∃ λ (ι₁ : xs ⊆ xys) → ⊆-trans ι₁ τ ≡ τ₁ -DisjointUnion-inj₁ [] = [] , refl -DisjointUnion-inj₁ (y ∷ₙ d) = _ , cong (y ∷ʳ_) (proj₂ (DisjointUnion-inj₁ d)) -DisjointUnion-inj₁ (x≈y ∷ₗ d) = refl ∷ _ , cong (x≈y ∷_) (proj₂ (DisjointUnion-inj₁ d)) -DisjointUnion-inj₁ (x≈y ∷ᵣ d) = _ ∷ʳ _ , cong (_ ∷ʳ_) (proj₂ (DisjointUnion-inj₁ d)) - --- From τ₁ ⊎ τ₂ = τ, compute the injection ι₂ such that τ₂ = ⊆-trans ι₂ τ. - -DisjointUnion-inj₂ : ∀ {xs ys zs xys : List A} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : xys ⊆ zs} → - DisjointUnion τ₁ τ₂ τ → ∃ λ (ι₂ : ys ⊆ xys) → ⊆-trans ι₂ τ ≡ τ₂ -DisjointUnion-inj₂ [] = [] , refl -DisjointUnion-inj₂ (y ∷ₙ d) = _ , cong (y ∷ʳ_) (proj₂ (DisjointUnion-inj₂ d)) -DisjointUnion-inj₂ (x≈y ∷ᵣ d) = refl ∷ _ , cong (x≈y ∷_) (proj₂ (DisjointUnion-inj₂ d)) -DisjointUnion-inj₂ (x≈y ∷ₗ d) = _ ∷ʳ _ , cong (_ ∷ʳ_) (proj₂ (DisjointUnion-inj₂ d)) - --- A sublist σ disjoint to both τ₁ and τ₂ is an equalizer --- for the separators of τ₁ and τ₂. - -equalize-separators : ∀ {us xs ys zs : List A} - {σ : us ⊆ zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} (let s = separateˡ τ₁ τ₂) → - Disjoint σ τ₁ → Disjoint σ τ₂ → - ⊆-trans σ (Separation.separator₁ s) ≡ - ⊆-trans σ (Separation.separator₂ s) -equalize-separators [] [] = refl -equalize-separators (y ∷ₙ d₁) (.y ∷ₙ d₂) = cong (y ∷ʳ_) (equalize-separators d₁ d₂) -equalize-separators (y ∷ₙ d₁) (refl ∷ᵣ d₂) = cong (y ∷ʳ_) (equalize-separators d₁ d₂) -equalize-separators (refl ∷ᵣ d₁) (y ∷ₙ d₂) = cong (y ∷ʳ_) (equalize-separators d₁ d₂) -equalize-separators {τ₁ = refl ∷ _} {τ₂ = refl ∷ _} -- match here to work around deficiency of Agda's forcing translation - (_ ∷ᵣ d₁) (_ ∷ᵣ d₂) = cong (_ ∷ʳ_) (cong (_ ∷ʳ_) (equalize-separators d₁ d₂)) -equalize-separators (x≈y ∷ₗ d₁) (.x≈y ∷ₗ d₂) = cong (trans x≈y refl ∷_) (equalize-separators d₁ d₂) +module Data.List.Relation.Binary.Sublist.Propositional.Properties where + +open import Data.List.Base using (List; []; _∷_; map) +open import Data.List.Membership.Propositional using (_∈_) +open import Data.List.Relation.Unary.All using (All; []; _∷_) +open import Data.List.Relation.Unary.Any using (Any; here; there) +open import Data.List.Relation.Unary.Any.Properties + using (here-injective; there-injective) +open import Data.List.Relation.Binary.Sublist.Propositional + hiding (map) +import Data.List.Relation.Binary.Sublist.Setoid.Properties + as SetoidProperties +open import Data.Product.Base using (∃; _,_; proj₂) +open import Function.Base using (id; _∘_; _∘′_) +open import Level using (Level) +open import Relation.Binary.Definitions using (_Respects_) +open import Relation.Binary.PropositionalEquality.Core as ≡ + using (_≡_; refl; cong; _≗_; trans) +open import Relation.Binary.PropositionalEquality.Properties + using (setoid; subst-injective; trans-reflʳ; trans-assoc) +open import Relation.Unary using (Pred) + +private + variable + a ℓ : Level + A B : Set a + x y : A + ws xs ys zs : List A + +------------------------------------------------------------------------ +-- Re-exporting setoid properties + +module _ {A : Set a} where + open SetoidProperties (setoid A) public + hiding (map⁺; ⊆-trans-idˡ; ⊆-trans-idʳ; ⊆-trans-assoc) + +map⁺ : (f : A → B) → xs ⊆ ys → map f xs ⊆ map f ys +map⁺ f = SetoidProperties.map⁺ (setoid _) (setoid _) (cong f) + +------------------------------------------------------------------------ +-- Category laws for _⊆_ + +⊆-trans-idˡ : ∀ {τ : xs ⊆ ys} → ⊆-trans ⊆-refl τ ≡ τ +⊆-trans-idˡ {τ = τ} = SetoidProperties.⊆-trans-idˡ (setoid _) (λ _ → refl) τ + +⊆-trans-idʳ : ∀ {τ : xs ⊆ ys} → ⊆-trans τ ⊆-refl ≡ τ +⊆-trans-idʳ {τ = τ} = SetoidProperties.⊆-trans-idʳ (setoid _) trans-reflʳ τ + +-- Note: The associativity law is oriented such that rewriting with it +-- may trigger reductions of ⊆-trans, which matches first on its +-- second argument and then on its first argument. + +⊆-trans-assoc : ∀ {τ₁ : ws ⊆ xs} {τ₂ : xs ⊆ ys} {τ₃ : ys ⊆ zs} → + ⊆-trans τ₁ (⊆-trans τ₂ τ₃) ≡ ⊆-trans (⊆-trans τ₁ τ₂) τ₃ +⊆-trans-assoc {τ₁ = τ₁} {τ₂ = τ₂} {τ₃ = τ₃} = + SetoidProperties.⊆-trans-assoc (setoid _) (λ p _ _ → ≡.sym (trans-assoc p)) τ₁ τ₂ τ₃ + +------------------------------------------------------------------------ +-- Laws concerning ⊆-trans and ∷ˡ⁻ + +⊆-trans-∷ˡ⁻ᵣ : ∀ {τ : xs ⊆ ys} {σ : (y ∷ ys) ⊆ zs} → + ⊆-trans τ (∷ˡ⁻ σ) ≡ ⊆-trans (y ∷ʳ τ) σ +⊆-trans-∷ˡ⁻ᵣ {σ = x ∷ σ} = refl +⊆-trans-∷ˡ⁻ᵣ {σ = y ∷ʳ σ} = cong (y ∷ʳ_) ⊆-trans-∷ˡ⁻ᵣ + +⊆-trans-∷ˡ⁻ₗ : ∀ {τ : (x ∷ xs) ⊆ ys} {σ : ys ⊆ zs} → + ⊆-trans (∷ˡ⁻ τ) σ ≡ ∷ˡ⁻ (⊆-trans τ σ) +⊆-trans-∷ˡ⁻ₗ {σ = y ∷ʳ σ} = cong (y ∷ʳ_) ⊆-trans-∷ˡ⁻ₗ +⊆-trans-∷ˡ⁻ₗ {τ = y ∷ʳ τ} {σ = refl ∷ σ} = cong (y ∷ʳ_) ⊆-trans-∷ˡ⁻ₗ +⊆-trans-∷ˡ⁻ₗ {τ = refl ∷ τ} {σ = refl ∷ σ} = refl + +⊆-∷ˡ⁻trans-∷ : ∀ {τ : xs ⊆ ys} {σ : (y ∷ ys) ⊆ zs} → + ∷ˡ⁻ (⊆-trans (refl ∷ τ) σ) ≡ ⊆-trans (y ∷ʳ τ) σ +⊆-∷ˡ⁻trans-∷ {σ = y ∷ʳ σ} = cong (y ∷ʳ_) ⊆-∷ˡ⁻trans-∷ +⊆-∷ˡ⁻trans-∷ {σ = refl ∷ σ} = refl + +------------------------------------------------------------------------ +-- Relationships to other predicates + +-- All P is a contravariant functor from _⊆_ to Set. + +All-resp-⊆ : {P : Pred A ℓ} → (All P) Respects _⊇_ +All-resp-⊆ [] [] = [] +All-resp-⊆ (_ ∷ʳ p) (_ ∷ xs) = All-resp-⊆ p xs +All-resp-⊆ (refl ∷ p) (x ∷ xs) = x ∷ All-resp-⊆ p xs + +-- Any P is a covariant functor from _⊆_ to Set. + +Any-resp-⊆ : {P : Pred A ℓ} → (Any P) Respects _⊆_ +Any-resp-⊆ = lookup + +------------------------------------------------------------------------ +-- Functor laws for All-resp-⊆ + +-- First functor law: identity. + +All-resp-⊆-refl : ∀ {P : Pred A ℓ} → + All-resp-⊆ ⊆-refl ≗ id {A = All P xs} +All-resp-⊆-refl [] = refl +All-resp-⊆-refl (p ∷ ps) = cong (p ∷_) (All-resp-⊆-refl ps) + +-- Second functor law: composition. + +All-resp-⊆-trans : ∀ {P : Pred A ℓ} {τ : xs ⊆ ys} (τ′ : ys ⊆ zs) → + All-resp-⊆ {P = P} (⊆-trans τ τ′) ≗ All-resp-⊆ τ ∘ All-resp-⊆ τ′ +All-resp-⊆-trans (_ ∷ʳ τ′) (p ∷ ps) = All-resp-⊆-trans τ′ ps +All-resp-⊆-trans {τ = _ ∷ʳ _ } (refl ∷ τ′) (p ∷ ps) = All-resp-⊆-trans τ′ ps +All-resp-⊆-trans {τ = refl ∷ _} (refl ∷ τ′) (p ∷ ps) = cong (p ∷_) (All-resp-⊆-trans τ′ ps) +All-resp-⊆-trans {τ = [] } ([] ) [] = refl + +------------------------------------------------------------------------ +-- Functor laws for Any-resp-⊆ / lookup + +-- First functor law: identity. + +Any-resp-⊆-refl : ∀ {P : Pred A ℓ} → + Any-resp-⊆ ⊆-refl ≗ id {A = Any P xs} +Any-resp-⊆-refl (here p) = refl +Any-resp-⊆-refl (there i) = cong there (Any-resp-⊆-refl i) + +lookup-⊆-refl = Any-resp-⊆-refl + +-- Second functor law: composition. + +Any-resp-⊆-trans : ∀ {P : Pred A ℓ} {τ : xs ⊆ ys} (τ′ : ys ⊆ zs) → + Any-resp-⊆ {P = P} (⊆-trans τ τ′) ≗ Any-resp-⊆ τ′ ∘ Any-resp-⊆ τ +Any-resp-⊆-trans (_ ∷ʳ τ′) i = cong there (Any-resp-⊆-trans τ′ i) +Any-resp-⊆-trans {τ = _ ∷ʳ _} (_ ∷ τ′) i = cong there (Any-resp-⊆-trans τ′ i) +Any-resp-⊆-trans {τ = _ ∷ _} (_ ∷ τ′) (there i) = cong there (Any-resp-⊆-trans τ′ i) +Any-resp-⊆-trans {τ = refl ∷ _} (_ ∷ τ′) (here _) = refl +Any-resp-⊆-trans {τ = [] } [] () + +lookup-⊆-trans = Any-resp-⊆-trans + +------------------------------------------------------------------------ +-- The `lookup` function for `xs ⊆ ys` is injective. +-- +-- Note: `lookup` can be seen as a strictly increasing reindexing +-- function for indices into `xs`, producing indices into `ys`. + +lookup-injective : ∀ {P : Pred A ℓ} {τ : xs ⊆ ys} {i j : Any P xs} → + lookup τ i ≡ lookup τ j → i ≡ j +lookup-injective {τ = _ ∷ʳ _} = lookup-injective ∘′ there-injective +lookup-injective {τ = x≡y ∷ _} {here _} {here _} = cong here ∘′ subst-injective x≡y ∘′ here-injective + -- Note: instead of using subst-injective, we could match x≡y against refl on the lhs. + -- However, this turns the following clause into a non-strict match. +lookup-injective {τ = _ ∷ _} {there _} {there _} = cong there ∘′ lookup-injective ∘′ there-injective + +------------------------------------------------------------------------ +-- from∈ ∘ to∈ turns a sublist morphism τ : x∷xs ⊆ ys into a morphism +-- [x] ⊆ ys. The same morphism is obtained by pre-composing τ with +-- the canonial morphism [x] ⊆ x∷xs. +-- +-- Note: This lemma does not hold for Sublist.Setoid, but could hold for +-- a hypothetical Sublist.Groupoid where trans refl = id. + +from∈∘to∈ : ∀ (τ : x ∷ xs ⊆ ys) → + from∈ (to∈ τ) ≡ ⊆-trans (refl ∷ minimum xs) τ +from∈∘to∈ (x≡y ∷ τ) = cong (x≡y ∷_) ([]⊆-irrelevant _ _) +from∈∘to∈ (y ∷ʳ τ) = cong (y ∷ʳ_) (from∈∘to∈ τ) + +from∈∘lookup : ∀ (τ : xs ⊆ ys) (i : x ∈ xs) → + from∈ (lookup τ i) ≡ ⊆-trans (from∈ i) τ +from∈∘lookup (y ∷ʳ τ) i = cong (y ∷ʳ_) (from∈∘lookup τ i) +from∈∘lookup (_ ∷ τ) (there i) = cong (_ ∷ʳ_) (from∈∘lookup τ i) +from∈∘lookup (refl ∷ τ) (here refl) = cong (refl ∷_) ([]⊆-irrelevant _ _) + +------------------------------------------------------------------------ +-- Weak pushout (wpo) + +-- A raw pushout is a weak pushout if the pushout square commutes. + +IsWeakPushout : ∀ {τ : xs ⊆ ys} {σ : xs ⊆ zs} → RawPushout τ σ → Set _ +IsWeakPushout {τ = τ} {σ = σ} rpo = + ⊆-trans τ (RawPushout.leg₁ rpo) ≡ + ⊆-trans σ (RawPushout.leg₂ rpo) + +-- Joining two list extensions with ⊆-pushout produces a weak pushout. + +⊆-pushoutˡ-is-wpo : ∀ (τ : xs ⊆ ys) (σ : xs ⊆ zs) → + IsWeakPushout (⊆-pushoutˡ τ σ) +⊆-pushoutˡ-is-wpo [] σ + rewrite ⊆-trans-idʳ {τ = σ} + = ⊆-trans-idˡ {xs = []} +⊆-pushoutˡ-is-wpo (y ∷ʳ τ) σ = cong (y ∷ʳ_) (⊆-pushoutˡ-is-wpo τ σ) +⊆-pushoutˡ-is-wpo (x≡y ∷ τ) (z ∷ʳ σ) = cong (z ∷ʳ_) (⊆-pushoutˡ-is-wpo (x≡y ∷ τ) σ) +⊆-pushoutˡ-is-wpo (refl ∷ τ) (refl ∷ σ) = cong (refl ∷_) (⊆-pushoutˡ-is-wpo τ σ) + +------------------------------------------------------------------------ +-- Properties of disjointness + +-- From τ₁ ⊎ τ₂ = τ, compute the injection ι₁ such that τ₁ = ⊆-trans ι₁ τ. + +DisjointUnion-inj₁ : ∀ {xys : List A} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : xys ⊆ zs} → + DisjointUnion τ₁ τ₂ τ → ∃ λ (ι₁ : xs ⊆ xys) → ⊆-trans ι₁ τ ≡ τ₁ +DisjointUnion-inj₁ [] = [] , refl +DisjointUnion-inj₁ (y ∷ₙ d) = _ , cong (y ∷ʳ_) (proj₂ (DisjointUnion-inj₁ d)) +DisjointUnion-inj₁ (x≈y ∷ₗ d) = refl ∷ _ , cong (x≈y ∷_) (proj₂ (DisjointUnion-inj₁ d)) +DisjointUnion-inj₁ (x≈y ∷ᵣ d) = _ ∷ʳ _ , cong (_ ∷ʳ_) (proj₂ (DisjointUnion-inj₁ d)) + +-- From τ₁ ⊎ τ₂ = τ, compute the injection ι₂ such that τ₂ = ⊆-trans ι₂ τ. + +DisjointUnion-inj₂ : ∀ {xys : List A} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : xys ⊆ zs} → + DisjointUnion τ₁ τ₂ τ → ∃ λ (ι₂ : ys ⊆ xys) → ⊆-trans ι₂ τ ≡ τ₂ +DisjointUnion-inj₂ [] = [] , refl +DisjointUnion-inj₂ (y ∷ₙ d) = _ , cong (y ∷ʳ_) (proj₂ (DisjointUnion-inj₂ d)) +DisjointUnion-inj₂ (x≈y ∷ᵣ d) = refl ∷ _ , cong (x≈y ∷_) (proj₂ (DisjointUnion-inj₂ d)) +DisjointUnion-inj₂ (x≈y ∷ₗ d) = _ ∷ʳ _ , cong (_ ∷ʳ_) (proj₂ (DisjointUnion-inj₂ d)) + +-- A sublist σ disjoint to both τ₁ and τ₂ is an equalizer +-- for the separators of τ₁ and τ₂. + +equalize-separators : ∀ {σ : ws ⊆ zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} (let s = separateˡ τ₁ τ₂) → + Disjoint σ τ₁ → Disjoint σ τ₂ → + ⊆-trans σ (Separation.separator₁ s) ≡ + ⊆-trans σ (Separation.separator₂ s) +equalize-separators [] [] = refl +equalize-separators (y ∷ₙ d₁) (.y ∷ₙ d₂) = cong (y ∷ʳ_) (equalize-separators d₁ d₂) +equalize-separators (y ∷ₙ d₁) (refl ∷ᵣ d₂) = cong (y ∷ʳ_) (equalize-separators d₁ d₂) +equalize-separators (refl ∷ᵣ d₁) (y ∷ₙ d₂) = cong (y ∷ʳ_) (equalize-separators d₁ d₂) +equalize-separators {τ₁ = refl ∷ _} {τ₂ = refl ∷ _} -- match here to work around deficiency of Agda's forcing translation + (_ ∷ᵣ d₁) (_ ∷ᵣ d₂) = cong (_ ∷ʳ_) (cong (_ ∷ʳ_) (equalize-separators d₁ d₂)) +equalize-separators (x≈y ∷ₗ d₁) (.x≈y ∷ₗ d₂) = cong (trans x≈y refl ∷_) (equalize-separators d₁ d₂) \ No newline at end of file