From 2713bbdbb464568cd604123719be94f747dfffac Mon Sep 17 00:00:00 2001 From: Runming Li Date: Mon, 6 Nov 2023 22:15:21 -0500 Subject: [PATCH 1/7] partially port rbt to decalf --- src/Examples/Sequence.agda | 219 +++++++ src/Examples/Sequence/ListMSequence.agda | 35 ++ src/Examples/Sequence/MSequence.agda | 25 + src/Examples/Sequence/RedBlackMSequence.agda | 110 ++++ src/Examples/Sequence/RedBlackTree.agda | 625 +++++++++++++++++++ 5 files changed, 1014 insertions(+) create mode 100644 src/Examples/Sequence.agda create mode 100644 src/Examples/Sequence/ListMSequence.agda create mode 100644 src/Examples/Sequence/MSequence.agda create mode 100644 src/Examples/Sequence/RedBlackMSequence.agda create mode 100644 src/Examples/Sequence/RedBlackTree.agda diff --git a/src/Examples/Sequence.agda b/src/Examples/Sequence.agda new file mode 100644 index 00000000..43c09024 --- /dev/null +++ b/src/Examples/Sequence.agda @@ -0,0 +1,219 @@ +{-# OPTIONS --prop --rewriting #-} + +module Examples.Sequence where + +open import Algebra.Cost + +parCostMonoid = ℕ²-ParCostMonoid +open ParCostMonoid parCostMonoid + +open import Calf costMonoid +open import Calf.Parallel parCostMonoid + +open import Calf.Data.Product +open import Calf.Data.Sum +open import Calf.Data.Bool +open import Calf.Data.Maybe +open import Calf.Data.Nat hiding (compare) +open import Calf.Data.List hiding (filter) + +open import Level using (0ℓ) +open import Relation.Binary +open import Data.Nat as Nat using (_<_; _+_) +import Data.Nat.Properties as Nat +open import Data.String using (String) +open import Relation.Binary.PropositionalEquality as Eq using (_≡_) + +open import Function using (case_of_; _$_) + +open import Examples.Sequence.MSequence +open import Examples.Sequence.ListMSequence +open import Examples.Sequence.RedBlackMSequence + + +module Ex/FromList where + open MSequence RedBlackMSequence + + fromList : cmp (Π (list nat) λ _ → F (seq nat)) + fromList [] = empty + fromList (x ∷ l) = + bind (F (seq nat)) empty λ s₁ → + bind (F (seq nat)) (fromList l) λ s₂ → + join s₁ x s₂ + + example : cmp (F (seq nat)) + example = fromList (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []) + + +module BinarySearchTree + (MSeq : MSequence) + (Key : StrictTotalOrder 0ℓ 0ℓ 0ℓ) + where + + open StrictTotalOrder Key + + 𝕂 : tp⁺ + 𝕂 = meta⁺ (StrictTotalOrder.Carrier Key) + + open MSequence MSeq public + + singleton : cmp (Π 𝕂 λ _ → F (seq 𝕂)) + singleton a = + bind (F (seq 𝕂)) empty λ t → + join t a t + + Split : tp⁻ + Split = F ((seq 𝕂) ×⁺ ((maybe 𝕂) ×⁺ (seq 𝕂))) + + split : cmp (Π (seq 𝕂) λ _ → Π 𝕂 λ _ → Split) + split t a = + rec + {X = Split} + (bind Split empty λ t → + ret (t , nothing , t)) + (λ t₁ ih₁ a' t₂ ih₂ → + case compare a a' of λ + { (tri< aa') → + bind Split ih₁ λ ( t₁₁ , a? , t₁₂ ) → + bind Split (join t₁₂ a' t₂) λ t → + ret (t₁₁ , a? , t) + ; (tri≈ ¬aa') → ret (t₁ , just a' , t₂) + ; (tri> ¬aa') → + bind Split ih₂ λ ( t₂₁ , a? , t₂₂ ) → + bind Split (join t₁ a' t₂₁) λ t → + ret (t , a? , t₂₂) + }) + t + + find : cmp (Π (seq 𝕂) λ _ → Π 𝕂 λ _ → F (maybe 𝕂)) + find t a = bind (F (maybe 𝕂)) (split t a) λ { (_ , a? , _) → ret a? } + + insert : cmp (Π (seq 𝕂) λ _ → Π 𝕂 λ _ → F (seq 𝕂)) + insert t a = bind (F (seq 𝕂)) (split t a) λ { (t₁ , _ , t₂) → join t₁ a t₂ } + + append : cmp (Π (seq 𝕂) λ _ → Π (seq 𝕂) λ _ → F (seq 𝕂)) + append t₁ t₂ = + rec + {X = F (seq 𝕂)} + (ret t₂) + (λ t'₁ ih₁ a' t'₂ ih₂ → + bind (F (seq 𝕂)) ih₂ λ t' → + join t'₁ a' t') + t₁ + + delete : cmp (Π (seq 𝕂) λ _ → Π 𝕂 λ _ → F (seq 𝕂)) + delete t a = bind (F (seq 𝕂)) (split t a) λ { (t₁ , _ , t₂) → append t₁ t₂ } + + union : cmp (Π (seq 𝕂) λ _ → Π (seq 𝕂) λ _ → F (seq 𝕂)) + union = + rec + {X = Π (seq 𝕂) λ _ → F (seq 𝕂)} + ret + λ t'₁ ih₁ a' t'₂ ih₂ t₂ → + bind (F (seq 𝕂)) (split t₂ a') λ { (t₂₁ , a? , t₂₂) → + bind (F (seq 𝕂)) ((ih₁ t₂₁) ∥ (ih₂ t₂₂)) λ (s₁ , s₂) → + join s₁ a' s₂ } + + intersection : cmp (Π (seq 𝕂) λ _ → Π (seq 𝕂) λ _ → F (seq 𝕂)) + intersection = + rec + {X = Π (seq 𝕂) λ _ → F (seq 𝕂)} + (λ t₂ → empty) + λ t'₁ ih₁ a' t'₂ ih₂ t₂ → + bind (F (seq 𝕂)) (split t₂ a') λ { (t₂₁ , a? , t₂₂) → + bind (F (seq 𝕂)) ((ih₁ t₂₁) ∥ (ih₂ t₂₂)) λ (s₁ , s₂) → + case a? of + λ { (just a) → join s₁ a s₂ + ; nothing → append s₁ s₂ } + } + + difference : cmp (Π (seq 𝕂) λ _ → Π (seq 𝕂) λ _ → F (seq 𝕂)) + difference t₁ t₂ = helper t₁ + where + helper : cmp (Π (seq 𝕂) λ _ → F (seq 𝕂)) + helper = + rec + {X = Π (seq 𝕂) λ _ → F (seq 𝕂)} + ret + (λ t'₁ ih₁ a' t'₂ ih₂ t₁ → + bind (F (seq 𝕂)) (split t₁ a') λ { (t₁₁ , a? , t₁₂) → + bind (F (seq 𝕂)) ((ih₁ t₁₁) ∥ (ih₂ t₁₂)) λ (s₁ , s₂) → + append s₁ s₂ + }) + t₂ + + filter : cmp (Π (seq 𝕂) λ _ → Π (U (Π 𝕂 λ _ → F bool)) λ _ → F (seq 𝕂)) + filter t f = + rec + {X = F (seq 𝕂)} + (bind (F (seq 𝕂)) empty ret) + (λ t'₁ ih₁ a' t'₂ ih₂ → + bind (F (seq 𝕂)) (ih₁ ∥ ih₂) (λ (s₁ , s₂) → + bind (F (seq 𝕂)) (f a') λ b → + if b then (join s₁ a' s₂) else (append s₁ s₂))) + t + + mapreduce : {X : tp⁻} → + cmp ( + Π (seq 𝕂) λ _ → + Π (U (Π 𝕂 λ _ → X)) λ _ → + Π (U (Π (U X) λ _ → Π (U X) λ _ → X)) λ _ → + Π (U X) λ _ → + X + ) + mapreduce {X} t g f l = + rec {X = X} l (λ t'₁ ih₁ a' t'₂ ih₂ → f ih₁ (f (g a') ih₂)) t + + +module Ex/NatSet where + open BinarySearchTree RedBlackMSequence Nat.<-strictTotalOrder + + example : cmp Split + example = + bind Split (singleton 1) λ t₁ → + bind Split (insert t₁ 2) λ t₁ → + bind Split (singleton 4) λ t₂ → + bind Split (join t₁ 3 t₂) λ t → + split t 2 + + sum/seq : cmp (Π (seq nat) λ _ → F (nat)) + sum/seq = + rec + {X = F (nat)} + (ret 0) + λ t'₁ ih₁ a' t'₂ ih₂ → + step (F nat) (1 , 1) $ + bind (F (nat)) (ih₁ ∥ ih₂) + (λ (s₁ , s₂) → ret (s₁ + a' + s₂)) + + + +module Ex/NatStringDict where + strictTotalOrder : StrictTotalOrder 0ℓ 0ℓ 0ℓ + strictTotalOrder = + record + { Carrier = ℕ × String + ; _≈_ = λ (n₁ , _) (n₂ , _) → n₁ ≡ n₂ + ; _<_ = λ (n₁ , _) (n₂ , _) → n₁ Nat.< n₂ + ; isStrictTotalOrder = + record + { isEquivalence = + record + { refl = Eq.refl + ; sym = Eq.sym + ; trans = Eq.trans + } + ; trans = Nat.<-trans + ; compare = λ (n₁ , _) (n₂ , _) → Nat.<-cmp n₁ n₂ + } + } + + open BinarySearchTree RedBlackMSequence strictTotalOrder + + example : cmp Split + example = + bind Split (singleton (1 , "red")) λ t₁ → + bind Split (insert t₁ (2 , "orange")) λ t₁ → + bind Split (singleton (4 , "green")) λ t₂ → + bind Split (join t₁ (3 , "yellow") t₂) λ t → + split t (2 , "") diff --git a/src/Examples/Sequence/ListMSequence.agda b/src/Examples/Sequence/ListMSequence.agda new file mode 100644 index 00000000..768f7f6a --- /dev/null +++ b/src/Examples/Sequence/ListMSequence.agda @@ -0,0 +1,35 @@ +{-# OPTIONS --prop --rewriting #-} + +module Examples.Sequence.ListMSequence where + +open import Algebra.Cost + +parCostMonoid = ℕ²-ParCostMonoid +open ParCostMonoid parCostMonoid + +open import Calf costMonoid +open import Calf.Data.List +open import Data.Nat as Nat using (_+_) + +open import Examples.Sequence.MSequence + +ListMSequence : MSequence +ListMSequence = + record + { seq = list + ; empty = ret [] + ; join = + λ {A} l₁ a l₂ → + let n = length l₁ + 1 + length l₂ in + step (F (list A)) (n , n) (ret (l₁ ++ [ a ] ++ l₂)) + ; rec = λ {A} {X} → rec {A} {X} + } + where + rec : {X : tp⁻} → + cmp + ( Π (U X) λ _ → + Π (U (Π (list A) λ _ → Π (U X) λ _ → Π A λ _ → Π (list A) λ _ → Π (U X) λ _ → X)) λ _ → + Π (list A) λ _ → X + ) + rec {A} {X} z f [] = z + rec {A} {X} z f (x ∷ l) = step X (1 , 1) (f [] z x l (rec {A} {X} z f l)) diff --git a/src/Examples/Sequence/MSequence.agda b/src/Examples/Sequence/MSequence.agda new file mode 100644 index 00000000..bed07a64 --- /dev/null +++ b/src/Examples/Sequence/MSequence.agda @@ -0,0 +1,25 @@ +{-# OPTIONS --prop --rewriting #-} + +module Examples.Sequence.MSequence where + +open import Algebra.Cost + +parCostMonoid = ℕ²-ParCostMonoid +open ParCostMonoid parCostMonoid + +open import Calf costMonoid + +-- Middle Sequence +record MSequence : Set where + field + seq : tp⁺ → tp⁺ + + empty : cmp (F (seq A)) + join : cmp (Π (seq A) λ s₁ → Π A λ a → Π (seq A) λ s₂ → F (seq A)) + + rec : {X : tp⁻} → + cmp + ( Π (U X) λ _ → + Π (U (Π (seq A) λ _ → Π (U X) λ _ → Π A λ _ → Π (seq A) λ _ → Π (U X) λ _ → X)) λ _ → + Π (seq A) λ _ → X + ) diff --git a/src/Examples/Sequence/RedBlackMSequence.agda b/src/Examples/Sequence/RedBlackMSequence.agda new file mode 100644 index 00000000..371ce1af --- /dev/null +++ b/src/Examples/Sequence/RedBlackMSequence.agda @@ -0,0 +1,110 @@ +{-# OPTIONS --prop --rewriting #-} + +module Examples.Sequence.RedBlackMSequence where + +open import Algebra.Cost + +parCostMonoid = ℕ²-ParCostMonoid +open ParCostMonoid parCostMonoid + +open import Calf costMonoid + +open import Calf.Data.Nat +open import Calf.Data.List +open import Calf.Data.Product +open import Calf.Data.Sum +open import Calf.Data.IsBounded costMonoid + +open import Data.Nat as Nat using (_+_; _*_; ⌊_/2⌋; _≥_; _∸_) +import Data.Nat.Properties as Nat +open import Data.Nat.Logarithm + +open import Examples.Sequence.MSequence +open import Examples.Sequence.RedBlackTree + + +RedBlackMSequence : MSequence +RedBlackMSequence = + record + { seq = rbt + ; empty = ret ⟪ leaf ⟫ + ; join = join + ; rec = λ {A} {X} → rec {A} {X} + } + where + record RBT (A : tp⁺) : Set where + pattern + constructor ⟪_⟫ + field + {y} : val color + {n} : val nat + {l} : val (list A) + t : val (irbt A y n l) + rbt : (A : tp⁺) → tp⁺ + rbt A = meta⁺ (RBT A) + + join : cmp (Π (rbt A) λ _ → Π A λ _ → Π (rbt A) λ _ → F (rbt A)) + join {A} t₁ a t₂ = bind (F (rbt A)) (i-join _ _ _ (RBT.t t₁) a _ _ _ (RBT.t t₂)) λ { (_ , _ , _ , inj₁ t) → ret ⟪ t ⟫ + ; (_ , _ , _ , inj₂ t) → ret ⟪ t ⟫ } + + -- join/is-bounded : ∀ {A} t₁ a t₂ → IsBounded (rbt A) (join t₁ a t₂) + -- (1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)) , 1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂))) + -- join/is-bounded {A} t₁ a t₂ = + -- Eq.subst + -- (IsBounded _ _) {x = 1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)) + 0 , 1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)) + 0} + -- (Eq.cong₂ _,_ (Eq.cong suc (Nat.+-identityʳ (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)))) + -- ((Eq.cong suc (Nat.+-identityʳ (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)))))) + -- (bound/bind/const (1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)) , 1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂))) (0 , 0) + -- (i-join/is-bounded _ _ _ (RBT.t t₁) a _ _ _ (RBT.t t₂)) + -- (λ { (_ , _ , _ , inj₁ t) → bound/ret + -- ; (_ , _ , _ , inj₂ t) → bound/ret})) + + nodes : RBT A → val nat + nodes ⟪ t ⟫ = i-nodes t + + nodes/upper-bound : (t : RBT A) → RBT.n t Nat.≤ ⌈log₂ (1 + (nodes t)) ⌉ + nodes/upper-bound ⟪ t ⟫ = i-nodes/bound/log-node-black-height t + + nodes/lower-bound : (t : RBT A) → RBT.n t Nat.≥ ⌊ (⌈log₂ (1 + (nodes t)) ⌉ ∸ 1) /2⌋ + nodes/lower-bound ⟪ t ⟫ = i-nodes/lower-bound/log-node-black-height t  + + join/cost : ∀ {A} (t₁ : RBT A) (t₂ : RBT A) → ℂ + join/cost {A} t₁ t₂ = + let max = ⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ in + let min = ⌊ (⌈log₂ (1 + (nodes t₁)) ⌉ ∸ 1) /2⌋ Nat.⊓ ⌊ (⌈log₂ (1 + (nodes t₂)) ⌉ ∸ 1) /2⌋ in + (1 + 2 * (max ∸ min)) , (1 + 2 * (max ∸ min)) + + -- join/is-bounded/nodes : ∀ {A} t₁ a t₂ → IsBounded (rbt A) (join t₁ a t₂) (join/cost t₁ t₂) + -- join/is-bounded/nodes {A} t₁ a t₂ = + -- bound/relax + -- (λ u → + -- (let open Nat.≤-Reasoning in + -- begin + -- 1 + 2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂) + -- ≤⟨ Nat.+-monoʳ-≤ 1 (Nat.*-monoʳ-≤ 2 (Nat.∸-monoˡ-≤ (RBT.n t₁ Nat.⊓ RBT.n t₂) (Nat.⊔-mono-≤ (nodes/upper-bound t₁) (nodes/upper-bound t₂)))) ⟩ + -- 1 + 2 * (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂) + -- ≤⟨ Nat.+-monoʳ-≤ 1 (Nat.*-monoʳ-≤ 2 (Nat.∸-monoʳ-≤ (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉) (Nat.⊓-mono-≤ (nodes/lower-bound t₁) (nodes/lower-bound t₂)))) ⟩ + -- 1 + 2 * (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ ∸ ⌊ (⌈log₂ (1 + (nodes t₁)) ⌉ ∸ 1) /2⌋ Nat.⊓ ⌊ (⌈log₂ (1 + (nodes t₂)) ⌉ ∸ 1) /2⌋) + -- ∎) , + -- (let open Nat.≤-Reasoning in + -- begin + -- 1 + 2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂) + -- ≤⟨ Nat.+-monoʳ-≤ 1 (Nat.*-monoʳ-≤ 2 (Nat.∸-monoˡ-≤ (RBT.n t₁ Nat.⊓ RBT.n t₂) (Nat.⊔-mono-≤ (nodes/upper-bound t₁) (nodes/upper-bound t₂)))) ⟩ + -- 1 + 2 * (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂) + -- ≤⟨ Nat.+-monoʳ-≤ 1 (Nat.*-monoʳ-≤ 2 (Nat.∸-monoʳ-≤ (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉) (Nat.⊓-mono-≤ (nodes/lower-bound t₁) (nodes/lower-bound t₂)))) ⟩ + -- 1 + 2 * (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ ∸ ⌊ (⌈log₂ (1 + (nodes t₁)) ⌉ ∸ 1) /2⌋ Nat.⊓ ⌊ (⌈log₂ (1 + (nodes t₂)) ⌉ ∸ 1) /2⌋) + -- ∎) + -- ) + -- (join/is-bounded t₁ a t₂) + + rec : {A : tp⁺} {X : tp⁻} → + cmp + ( Π (U X) λ _ → + Π (U (Π (rbt A) λ _ → Π (U X) λ _ → Π A λ _ → Π (rbt A) λ _ → Π (U X) λ _ → X)) λ _ → + Π (rbt A) λ _ → X + ) + rec {A} {X} z f ⟪ t ⟫ = + i-rec {A} {X} + z + (λ _ _ _ t₁ ih₁ a _ _ _ t₂ ih₂ → f ⟪ t₁ ⟫ ih₁ a ⟪ t₂ ⟫ ih₂) + _ _ _ t diff --git a/src/Examples/Sequence/RedBlackTree.agda b/src/Examples/Sequence/RedBlackTree.agda new file mode 100644 index 00000000..745ce6ba --- /dev/null +++ b/src/Examples/Sequence/RedBlackTree.agda @@ -0,0 +1,625 @@ +{-# OPTIONS --prop --rewriting #-} +{-# OPTIONS --allow-unsolved-metas #-} + +module Examples.Sequence.RedBlackTree where + +open import Algebra.Cost + +parCostMonoid = ℕ²-ParCostMonoid +open ParCostMonoid parCostMonoid + +open import Calf costMonoid + +open import Calf.Data.Product +open import Calf.Data.Sum +open import Calf.Data.Nat +open import Calf.Data.List +open import Calf.Data.IsBounded costMonoid +open import Calf.Data.IsBoundedG costMonoid +open import Data.Nat as Nat using (_+_; _*_; _<_; _>_; _≤ᵇ_; _<ᵇ_; ⌊_/2⌋; _≡ᵇ_; _≥_; _∸_) +open import Data.Nat.Logarithm +import Data.Nat.Properties as Nat +import Data.List.Properties as List + +open import Function using (_$_; case_of_) + +open import Relation.Nullary +open import Relation.Nullary.Negation using (contradiction) +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≢_; module ≡-Reasoning; ≢-sym) + + +data Color : Set where + red : Color + black : Color +color : tp⁺ +color = meta⁺ Color + +-- Indexed Red Black Tree +data IRBT (A : tp⁺) : val color → val nat → val (list A) → Set where + leaf : IRBT A black zero [] + red : {n : val nat} {l₁ l₂ : val (list A)} + (t₁ : IRBT A black n l₁) (a : val A) (t₂ : IRBT A black n l₂) + → IRBT A red n (l₁ ++ [ a ] ++ l₂) + black : {n : val nat} {y₁ y₂ : val color} {l₁ l₂ : val (list A)} + (t₁ : IRBT A y₁ n l₁) (a : val A) (t₂ : IRBT A y₂ n l₂) + → IRBT A black (suc n) (l₁ ++ [ a ] ++ l₂) +irbt : (A : tp⁺) → val color → val nat → val (list A) → tp⁺ +irbt A y n l = meta⁺ (IRBT A y n l) + + +data AlmostLeftRBT (A : tp⁺) : (right-color : val color) → val nat → val (list A) → Set where + violation : + {n : val nat} {l₁ l₂ : val (list A)} + → IRBT A red n l₁ → (a : val A) → IRBT A black n l₂ + → AlmostLeftRBT A red n (l₁ ++ [ a ] ++ l₂) + valid : + {right-color : val color} {n : val nat} {y : val color} {l : val (list A)} → IRBT A y n l + → AlmostLeftRBT A right-color n l +alrbt : (A : tp⁺) → val color → val nat → val (list A) → tp⁺ +alrbt A y n l = meta⁺ (AlmostLeftRBT A y n l) + +joinLeft : + cmp + ( Π color λ y₁ → Π nat λ n₁ → Π (list A) λ l₁ → Π (irbt A y₁ n₁ l₁) λ _ → + Π A λ a → + Π color λ y₂ → Π nat λ n₂ → Π (list A) λ l₂ → Π (irbt A y₂ n₂ l₂) λ _ → + Π (meta⁺ (n₁ < n₂)) λ _ → + F (Σ⁺ (list A) λ l → (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ (alrbt A y₂ n₂ l)) + ) +joinLeft {A} y₁ n₁ l₁ t₁ a .red n₂ l₂ (red {l₁ = l₂₁} {l₂ = l₂₂} t₂₁ a₁ t₂₂) n₁ n₂)) λ _ → + F (Σ⁺ (list A) λ l → (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ (arrbt A y₁ n₁ l)) + ) +joinRight {A} .red n₁ l₁ (red {l₁ = l₁₁} {l₂ = l₁₂} t₁₁ a₁ t₁₂) a y₂ n₂ l₂ t₂ n₁>n₂ = + step (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂)) ×⁺ (arrbt A red n₁ l)))) (1 , 1) $ + bind (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂)) ×⁺ (arrbt A red n₁ l)))) + (joinRight _ _ _ t₁₂ a _ _ _ t₂ n₁>n₂) + (λ { (l , l≡l₁₂++a₁∷l₂ , valid {y = red} t') → + ret (l₁₁ ++ [ a₁ ] ++ (l₁₂ ++ [ a ] ++ l₂) , + Eq.sym (List.++-assoc l₁₁ (a₁ ∷ l₁₂) (a ∷ l₂)) , + Eq.subst (λ l' → AlmostRightRBT A red n₁ l') (Eq.cong₂ _++_ refl (Eq.cong₂ _∷_ refl l≡l₁₂++a₁∷l₂)) (violation t₁₁ a₁ t')) + ; (l , l≡l₁₂++a₁∷l₂ , valid {y = black} t') → + ret (l₁₁ ++ [ a₁ ] ++ (l₁₂ ++ [ a ] ++ l₂) , + Eq.sym (List.++-assoc l₁₁ (a₁ ∷ l₁₂) (a ∷ l₂)) , + Eq.subst (λ l' → AlmostRightRBT A red n₁ l') (Eq.cong₂ _++_ refl (Eq.cong₂ _∷_ refl l≡l₁₂++a₁∷l₂)) (valid (red t₁₁ a₁ t'))) + }) +joinRight {A} .black (suc n₁) l₁ (black {l₁ = l₁₁} {l₂ = l₁₂} t₁₁ a₁ t₁₂) a y₂ n₂ l₂ t₂ n₁>n₂ with n₁ Nat.≟ n₂ +joinRight {A} .black (suc n₁) l₁ (black {l₁ = l₁₁} {l₂ = l₁₂} t₁₁ a₁ t₁₂) a red n₁ l₂ (red {l₁ = l₂₁} {l₂ = l₂₂} t₂₁ a₂ t₂₂) n₁>n₂ | yes refl = + ret ((l₁₁ ++ [ a₁ ] ++ l₁₂) ++ [ a ] ++ (l₂₁ ++ [ a₂ ] ++ l₂₂) , + refl , + valid (red (black t₁₁ a₁ t₁₂) a (black t₂₁ a₂ t₂₂))) +joinRight {A} .black (suc n₁) l₁ (black {y₂ = red} {l₁ = l₁₁} t₁₁ a₁ (red {l₁ = l₁₂₁} {l₂ = l₁₂₂} t₁₂₁ a₁₂ t₁₂₂)) a black n₁ l₂ t₂ n₁>n₂ | yes refl = + ret ((l₁₁ ++ [ a₁ ] ++ l₁₂₁) ++ [ a₁₂ ] ++ (l₁₂₂ ++ [ a ] ++ l₂) , + (begin + (l₁₁ ++ a₁ ∷ l₁₂₁) ++ a₁₂ ∷ l₁₂₂ ++ a ∷ l₂ + ≡⟨ List.++-assoc l₁₁ (a₁ ∷ l₁₂₁) (a₁₂ ∷ l₁₂₂ ++ a ∷ l₂) ⟩ + l₁₁ ++ a₁ ∷ l₁₂₁ ++ a₁₂ ∷ l₁₂₂ ++ a ∷ l₂ + ≡⟨ Eq.cong₂ _++_ refl (Eq.sym (List.++-assoc (a₁ ∷ l₁₂₁) (a₁₂ ∷ l₁₂₂) (a ∷ l₂))) ⟩ + l₁₁ ++ (a₁ ∷ l₁₂₁ ++ a₁₂ ∷ l₁₂₂) ++ a ∷ l₂ + ≡˘⟨ List.++-assoc l₁₁ (a₁ ∷ l₁₂₁ ++ a₁₂ ∷ l₁₂₂) (a ∷ l₂) ⟩ + (l₁₁ ++ a₁ ∷ l₁₂₁ ++ a₁₂ ∷ l₁₂₂) ++ a ∷ l₂ + ∎) , + valid (red (black t₁₁ a₁ t₁₂₁) a₁₂ (black t₁₂₂ a t₂))) + where open ≡-Reasoning +joinRight {A} .black (suc n₁) l₁ (black {y₂ = black} {l₁ = l₁₁} {l₂ = l₁₂} t₁₁ a₁ t₁₂) a black n₁ l₂ t₂ n₁>n₂ | yes refl = + ret (l₁₁ ++ [ a₁ ] ++ (l₁₂ ++ [ a ] ++ l₂) , + Eq.sym (List.++-assoc l₁₁ (a₁ ∷ l₁₂) (a ∷ l₂)) , + valid (black t₁₁ a₁ (red t₁₂ a t₂))) +... | no n₁≢n₂ = + step (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂)) ×⁺ (arrbt A black (suc n₁) l)))) (1 , 1) $ + bind (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂)) ×⁺ (arrbt A black (suc n₁) l)))) + (joinRight _ _ _ t₁₂ a _ _ _ t₂ (Nat.≤∧≢⇒< (Nat.≤-pred n₁>n₂) (≢-sym n₁≢n₂))) + λ { (l , l≡l₁₂++a∷l₂ , violation {l₁ = l'₁} t'₁ a' (red {l₁ = l'₂₁} {l₂ = l'₂₂} t'₂₁ a'₂ t'₂₂)) → + ret ((l₁₁ ++ [ a₁ ] ++ l'₁) ++ [ a' ] ++ (l'₂₁ ++ [ a'₂ ] ++ l'₂₂) , + (begin + (l₁₁ ++ a₁ ∷ l'₁) ++ a' ∷ l'₂₁ ++ a'₂ ∷ l'₂₂ + ≡⟨ List.++-assoc l₁₁ (a₁ ∷ l'₁) (a' ∷ l'₂₁ ++ a'₂ ∷ l'₂₂) ⟩ + l₁₁ ++ a₁ ∷ l'₁ ++ a' ∷ l'₂₁ ++ a'₂ ∷ l'₂₂ + ≡⟨ Eq.cong₂ _++_ refl (Eq.cong₂ _∷_ refl l≡l₁₂++a∷l₂) ⟩ + l₁₁ ++ a₁ ∷ l₁₂ ++ a ∷ l₂ + ≡˘⟨ List.++-assoc l₁₁ (a₁ ∷ l₁₂) (a ∷ l₂) ⟩ + (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂ + ∎) , + (valid (red (black t₁₁ a₁ t'₁) a' (black t'₂₁ a'₂ t'₂₂)))) + ; (l , l≡l₁₂++a∷l₂ , valid t') → + ret (l₁₁ ++ [ a₁ ] ++ (l₁₂ ++ [ a ] ++ l₂) , + Eq.sym (List.++-assoc l₁₁ (a₁ ∷ l₁₂) (a ∷ l₂)) , + Eq.subst (λ l' → AlmostRightRBT A black (suc n₁) l') (Eq.cong₂ _++_ refl (Eq.cong₂ _∷_ refl l≡l₁₂++a∷l₂)) (valid (black t₁₁ a₁ t'))) + } + where open ≡-Reasoning + +-- joinRight/cost : (y : val color) (n₁ n₂ : val nat) → ℂ +-- joinRight/cost red n₁ n₂ = 1 + (2 * (n₁ ∸ n₂)) , 1 + (2 * (n₁ ∸ n₂)) +-- joinRight/cost black n₁ n₂ = (2 * (n₁ ∸ n₂)) , (2 * (n₁ ∸ n₂)) + +-- joinRight/is-bounded' : ∀ y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ +-- → IsBounded (Σ++ (list A) λ l → prod⁺ (U (meta (l ≡ l₁ ++ [ a ] ++ l₂))) (arrbt A y₁ n₁ l)) (joinRight y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂) (joinRight/cost y₁ n₁ n₂) + +-- joinRight/is-bounded : ∀ {A} y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ +-- → IsBounded (Σ++ (list A) λ l → prod⁺ (U (meta (l ≡ l₁ ++ [ a ] ++ l₂))) (arrbt A y₁ n₁ l)) (joinRight y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂) (1 + (2 * (n₁ ∸ n₂)) , 1 + (2 * (n₁ ∸ n₂))) + +-- joinRight/is-bounded' red n₁ l₁ (red t₁₁ a₁ t₁₂) a y₂ n₂ l₂ t₂ n₁>n₂ = +-- bound/step (1 , 1) (2 * (n₁ ∸ n₂) , 2 * (n₁ ∸ n₂)) +-- (Eq.subst +-- (IsBounded _ _) +-- (Eq.cong₂ _,_ (Nat.+-identityʳ (2 * (n₁ ∸ n₂))) (Nat.+-identityʳ (2 * (n₁ ∸ n₂)))) +-- (bound/bind/const (2 * (n₁ ∸ n₂) , 2 * (n₁ ∸ n₂)) (0 , 0) +-- (joinRight/is-bounded' _ _ _ t₁₂ a _ _ _ t₂ n₁>n₂) +-- λ {(_ , _ , valid (red _ _ _)) → bound/ret +-- ; (_ , _ , valid (black _ _ _)) → bound/ret} +-- )) +-- joinRight/is-bounded' black (suc n₁) l₁ (black t₁₁ a₁ t₁₂) a y₂ n₂ l₂ t₂ n₁>n₂ with n₁ Nat.≟ n₂ +-- joinRight/is-bounded' black _ _ (black _ _ _) _ red _ _ (red _ _ _) _ | yes refl = +-- bound/relax (λ u → Nat.z≤n , Nat.z≤n) bound/ret +-- joinRight/is-bounded' black _ _ (black {y₂ = red} _ _ (red _ _ _)) _ black _ _ _ _ | yes refl = +-- bound/relax (λ u → Nat.z≤n , Nat.z≤n) bound/ret +-- joinRight/is-bounded' black _ _ (black {y₂ = black} _ _ _) _ black _ _ _ _ | yes refl = +-- bound/relax (λ u → Nat.z≤n , Nat.z≤n) bound/ret +-- ... | no n₁≢n₂ = +-- Eq.subst +-- (IsBounded _ _) {x = 2 + 2 * (n₁ ∸ n₂) , 2 + 2 * (n₁ ∸ n₂)} +-- (Eq.cong₂ _,_ (Eq.trans (Eq.sym (Nat.*-suc 2 (n₁ ∸ n₂))) (Eq.cong (2 *_) (Eq.sym (Nat.+-∸-assoc 1 n₁>n₂)))) +-- (Eq.trans (Eq.sym (Nat.*-suc 2 (n₁ ∸ n₂))) (Eq.cong (2 *_) (Eq.sym (Nat.+-∸-assoc 1 n₁>n₂))))) +-- (bound/step (1 , 1) (1 + 2 * (n₁ ∸ n₂) , 1 + 2 * (n₁ ∸ n₂)) +-- (Eq.subst +-- (IsBounded _ _) {x = 1 + 2 * (n₁ ∸ n₂) + 0 , 1 + 2 * (n₁ ∸ n₂) + 0} +-- (Eq.cong₂ _,_ (Nat.+-identityʳ (1 + 2 * (n₁ ∸ n₂))) (Nat.+-identityʳ (1 + 2 * (n₁ ∸ n₂)))) +-- (bound/bind/const (1 + 2 * (n₁ ∸ n₂) , 1 + 2 * (n₁ ∸ n₂)) (0 , 0) +-- (joinRight/is-bounded _ _ _ t₁₂ a _ _ _ t₂ _) +-- (λ { (_ , _ , (violation _ _ (red _ _ _))) → bound/ret +-- ; (_ , _ , (valid _)) → bound/ret })))) + +-- joinRight/is-bounded red n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ = +-- joinRight/is-bounded' red n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ +-- joinRight/is-bounded black n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ = +-- bound/relax (λ u → Nat.n≤1+n _ , Nat.n≤1+n _) (joinRight/is-bounded' black n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂) + +i-join : + cmp + ( Π color λ y₁ → Π nat λ n₁ → Π (list A) λ l₁ → Π (irbt A y₁ n₁ l₁) λ _ → + Π A λ a → + Π color λ y₂ → Π nat λ n₂ → Π (list A) λ l₂ → Π (irbt A y₂ n₂ l₂) λ _ → + F (Σ⁺ color λ y → Σ⁺ (list A) λ l → + (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ ((irbt A y (1 + (n₁ Nat.⊔ n₂)) l) ⊎⁺ (irbt A y (n₁ Nat.⊔ n₂) l))) + ) +i-join {A} y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ with Nat.<-cmp n₁ n₂ +i-join {A} red n₁ l₁ t₁ a y₂ n₂ l₂ t₂ | tri≈ ¬n₁n₂ = + ret (black , l₁ ++ [ a ] ++ l₂ , refl , + inj₁ (Eq.subst (λ n → IRBT A black (suc n) (l₁ ++ a ∷ l₂)) (Eq.sym (Nat.⊔-idem n₁)) (black t₁ a t₂))) +i-join {A} black n₁ l₁ t₁ a red n₂ l₂ t₂ | tri≈ ¬n₁n₂ = + ret (black , l₁ ++ [ a ] ++ l₂ , refl , + inj₁ (Eq.subst (λ n → IRBT A black (suc n) (l₁ ++ a ∷ l₂)) (Eq.sym (Nat.⊔-idem n₁)) (black t₁ a t₂))) +i-join {A} black n₁ l₁ t₁ a black n₂ l₂ t₂ | tri≈ ¬n₁n₂ = + ret (red , l₁ ++ [ a ] ++ l₂ , refl , + inj₂ (Eq.subst (λ n → IRBT A red n (l₁ ++ a ∷ l₂)) (Eq.sym (Nat.⊔-idem n₁)) (red t₁ a t₂))) +... | tri< n₁n₂ = + bind (F (Σ⁺ color λ y → Σ⁺ (list A) λ l → + (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ ((irbt A y (1 + (n₁ Nat.⊔ n₂)) l) ⊎⁺ (irbt A y (n₁ Nat.⊔ n₂) l)))) + (joinLeft _ _ _ t₁ a _ _ _ t₂ n₁ ¬n₁n₂ = + bind (F (Σ⁺ color λ y → Σ⁺ (list A) λ l → + (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ ((irbt A y (1 + (n₁ Nat.⊔ n₂)) l) ⊎⁺ (irbt A y (n₁ Nat.⊔ n₂) l)))) + (joinRight _ _ _ t₁ a _ _ _ t₂ n₁>n₂) + (λ { (l , l≡l₁++a∷l₂ , violation {l₁ = l'₁} {l₂ = l'₂} t'₁ a' t'₂) → + ret (black , l'₁ ++ [ a' ] ++ l'₂ , l≡l₁++a∷l₂ , + inj₁ (Eq.subst (λ n → IRBT A black (suc n) (l'₁ ++ a' ∷ l'₂)) (Eq.sym (Nat.m≥n⇒m⊔n≡m (Nat.<⇒≤ n₁>n₂))) + (black t'₁ a' t'₂))) + ; (l , l≡l₁++a∷l₂ , valid {n = n} {y = y} {l = l} t') → + ret (y , l , l≡l₁++a∷l₂ , inj₂ (Eq.subst (λ n → IRBT A y n l) (Eq.sym (Nat.m≥n⇒m⊔n≡m (Nat.<⇒≤ n₁>n₂))) t')) + } + ) + +-- i-join/is-bounded : ∀ {A} y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ +-- → IsBounded (Σ++ color λ y → Σ++ (list A) λ l → +-- prod⁺ (U (meta (l ≡ l₁ ++ [ a ] ++ l₂))) (sum (irbt A y (1 + (n₁ Nat.⊔ n₂)) l) (irbt A y (n₁ Nat.⊔ n₂) l))) (i-join y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂) +-- (1 + (2 * (n₁ Nat.⊔ n₂ ∸ n₁ Nat.⊓ n₂)) , 1 + (2 * (n₁ Nat.⊔ n₂ ∸ n₁ Nat.⊓ n₂))) +-- i-join/is-bounded {A} y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ with Nat.<-cmp n₁ n₂ +-- i-join/is-bounded {A} red n₁ l₁ t₁ a y₂ .n₁ l₂ t₂ | tri≈ ¬n₁n₂ = +-- bound/relax (λ u → Nat.z≤n , Nat.z≤n) bound/ret +-- i-join/is-bounded {A} black n₁ l₁ t₁ a red n₁ l₂ t₂ | tri≈ ¬n₁n₂ = +-- bound/relax (λ u → Nat.z≤n , Nat.z≤n) bound/ret +-- i-join/is-bounded {A} black n₁ l₁ t₁ a black n₁ l₂ t₂ | tri≈ ¬n₁n₂ = +-- bound/relax (λ u → Nat.z≤n , Nat.z≤n) bound/ret +-- ... | tri< n₁n₂ = +-- Eq.subst +-- (IsBounded _ _) {x = 1 + 2 * (n₂ ∸ n₁) + 0 , 1 + 2 * (n₂ ∸ n₁) + 0} +-- (Eq.cong₂ _,_ (Eq.cong suc (Eq.trans (Nat.+-identityʳ (2 * (n₂ ∸ n₁))) (Eq.cong (2 *_) (Eq.cong₂ _∸_ (Eq.sym (Nat.m≤n⇒m⊔n≡n (Nat.<⇒≤ n₁ ¬n₁n₂ = +-- Eq.subst +-- (IsBounded _ _) {x = 1 + 2 * (n₁ ∸ n₂) + 0 , 1 + 2 * (n₁ ∸ n₂) + 0} +-- (Eq.cong₂ _,_ (Eq.cong suc (Eq.trans (Nat.+-identityʳ (2 * (n₁ ∸ n₂))) (Eq.cong (2 *_) (Eq.cong₂ _∸_ (Eq.sym (Nat.m≥n⇒m⊔n≡m (Nat.<⇒≤ n₁>n₂))) (Eq.sym (Nat.m≥n⇒m⊓n≡n (Nat.<⇒≤ n₁>n₂))))))) +-- ((Eq.cong suc (Eq.trans (Nat.+-identityʳ (2 * (n₁ ∸ n₂))) (Eq.cong (2 *_) (Eq.cong₂ _∸_ (Eq.sym (Nat.m≥n⇒m⊔n≡m (Nat.<⇒≤ n₁>n₂))) (Eq.sym (Nat.m≥n⇒m⊓n≡n (Nat.<⇒≤ n₁>n₂))))))))) +-- (bound/bind/const (1 + 2 * (n₁ ∸ n₂) , 1 + 2 * (n₁ ∸ n₂)) (0 , 0) +-- (joinRight/is-bounded _ _ _ t₁ a _ _ _ t₂ n₁>n₂) +-- λ { (_ , _ , violation _ _ _) → bound/ret +-- ; (_ , _ , valid _) → bound/ret}) + +i-nodes : {y : val color} {n : val nat} {l : val (list A)} → IRBT A y n l → val nat +i-nodes leaf = 0 +i-nodes (red t₁ _ t₂) = 1 + (i-nodes t₁) + (i-nodes t₂) +i-nodes (black t₁ _ t₂) = 1 + (i-nodes t₁) + (i-nodes t₂) + +i-nodes≡lengthl : ∀ {y} {n} {l} → (t : IRBT A y n l) → i-nodes t ≡ length l +i-nodes≡lengthl leaf = refl +i-nodes≡lengthl (red {l₁ = l₁} {l₂ = l₂} t₁ a t₂) = + begin + 1 + (i-nodes t₁) + (i-nodes t₂) + ≡⟨ Eq.cong₂ _+_ (Eq.cong₂ _+_ refl (i-nodes≡lengthl t₁)) (i-nodes≡lengthl t₂) ⟩ + 1 + length l₁ + length l₂ + ≡⟨ Eq.cong₂ _+_ (Nat.+-comm 1 (length l₁)) refl ⟩ + (length l₁ + 1) + length l₂ + ≡⟨ Nat.+-assoc (length l₁) 1 (length l₂) ⟩ + length l₁ + (1 + length l₂) + ≡⟨⟩ + length l₁ + length ([ a ] ++ l₂) + ≡˘⟨ List.length-++ l₁ ⟩ + length (l₁ ++ [ a ] ++ l₂) + ∎ + where open ≡-Reasoning +i-nodes≡lengthl (black {l₁ = l₁} {l₂ = l₂} t₁ a t₂) = + begin + 1 + (i-nodes t₁) + (i-nodes t₂) + ≡⟨ Eq.cong₂ _+_ (Eq.cong₂ _+_ refl (i-nodes≡lengthl t₁)) (i-nodes≡lengthl t₂) ⟩ + 1 + length l₁ + length l₂ + ≡⟨ Eq.cong₂ _+_ (Nat.+-comm 1 (length l₁)) refl ⟩ + (length l₁ + 1) + length l₂ + ≡⟨ Nat.+-assoc (length l₁) 1 (length l₂) ⟩ + length l₁ + (1 + length l₂) + ≡⟨⟩ + length l₁ + length ([ a ] ++ l₂) + ≡˘⟨ List.length-++ l₁ ⟩ + length (l₁ ++ [ a ] ++ l₂) + ∎ + where open ≡-Reasoning + +i-total-height : {y : val color} {n : val nat} {l : val (list A)} → IRBT A y n l → val nat +i-total-height leaf = 0 +i-total-height (red t₁ _ t₂) = 1 + (i-total-height t₁ Nat.⊔ i-total-height t₂) +i-total-height (black t₁ _ t₂) = 1 + (i-total-height t₁ Nat.⊔ i-total-height t₂) + +i-nodes/bound/node-black-height : {y : val color} {n : val nat} {l : val (list A)} → (t : IRBT A y n l) → 1 + (i-nodes t) Nat.≥ (2 Nat.^ n) +i-nodes/bound/node-black-height leaf = Nat.s≤s Nat.z≤n +i-nodes/bound/node-black-height (red {n} t₁ _ t₂) = + let open Nat.≤-Reasoning in + begin + 2 Nat.^ n + ≤⟨ i-nodes/bound/node-black-height t₁ ⟩ + suc (i-nodes t₁) + ≤⟨ Nat.m≤m+n (suc (i-nodes t₁)) (suc (i-nodes t₂)) ⟩ + (suc (i-nodes t₁)) + (suc (i-nodes t₂)) + ≡⟨ Eq.cong suc (Nat.+-suc (i-nodes t₁) (i-nodes t₂)) ⟩ + suc (suc (i-nodes t₁ + i-nodes t₂)) + ∎ +i-nodes/bound/node-black-height (black {n} t₁ _ t₂) = + let open Nat.≤-Reasoning in + begin + (2 Nat.^ n) + ((2 Nat.^ n) + zero) + ≡⟨ Eq.sym (Eq.trans (Eq.sym (Nat.+-identityʳ ((2 Nat.^ n) + (2 Nat.^ n)))) (Nat.+-assoc ((2 Nat.^ n)) ((2 Nat.^ n)) 0)) ⟩ + (2 Nat.^ n) + (2 Nat.^ n) + ≤⟨ Nat.+-monoʳ-≤ (2 Nat.^ n) (i-nodes/bound/node-black-height t₂) ⟩ + (2 Nat.^ n) + (suc (i-nodes t₂)) + ≤⟨ Nat.+-monoˡ-≤ ((suc (i-nodes t₂))) (i-nodes/bound/node-black-height t₁) ⟩ + (suc (i-nodes t₁)) + (suc (i-nodes t₂)) + ≡⟨ Eq.cong suc (Nat.+-suc (i-nodes t₁) (i-nodes t₂)) ⟩ + suc (suc (i-nodes t₁ + i-nodes t₂)) + ∎ + +i-nodes/bound/log-node-black-height : {y : val color} {n : val nat} {l : val (list A)} → (t : IRBT A y n l) → n Nat.≤ ⌈log₂ (1 + (i-nodes t)) ⌉ +i-nodes/bound/log-node-black-height {A} {y} {n} t = + let open Nat.≤-Reasoning in + begin + n + ≡⟨ Eq.sym (⌈log₂2^n⌉≡n n) ⟩ + ⌈log₂ (2 Nat.^ n) ⌉ + ≤⟨ ⌈log₂⌉-mono-≤ (i-nodes/bound/node-black-height t) ⟩ + ⌈log₂ (1 + (i-nodes t)) ⌉ + ∎ + +total-height/black-height : {y : val color} {n : val nat} {l : val (list A)} → (t : IRBT A y n l) → (i-total-height t) Nat.≤ (2 * n + 1) +total-height/black-height leaf = Nat.z≤n +total-height/black-height (red leaf _ leaf) = Nat.s≤s Nat.z≤n +total-height/black-height (red (black {n} t₁₁ _ t₁₂) _ (black t₂₁ _ t₂₂)) = + let open Nat.≤-Reasoning in + begin + suc (suc ((i-total-height t₁₁ Nat.⊔ i-total-height t₁₂) Nat.⊔ (i-total-height t₂₁ Nat.⊔ i-total-height t₂₂))) + ≤⟨ Nat.s≤s (Nat.s≤s (Nat.⊔-mono-≤ (Nat.⊔-mono-≤ (total-height/black-height t₁₁) (total-height/black-height t₁₂)) (Nat.⊔-mono-≤ (total-height/black-height t₂₁) (total-height/black-height t₂₂)))) ⟩ + suc (suc (((2 * n + 1) Nat.⊔ (2 * n + 1)) Nat.⊔ ((2 * n + 1) Nat.⊔ (2 * n + 1)))) + ≡⟨ Eq.cong suc (Eq.cong suc (Nat.m≤n⇒m⊔n≡n Nat.≤-refl)) ⟩ + suc (suc ((2 * n + 1) Nat.⊔ (2 * n + 1))) + ≡⟨ Eq.cong suc (Eq.cong suc (Nat.m≤n⇒m⊔n≡n Nat.≤-refl)) ⟩ + suc (suc (2 * n + 1)) + ≡⟨ Eq.cong suc (Eq.trans (Eq.cong suc (Nat.+-assoc n (n + zero) 1)) (Eq.sym (Nat.+-suc n ((n + zero) + 1)))) ⟩ + suc (n + suc ((n + zero) + 1)) + ≡⟨ Eq.cong suc (Eq.sym (Nat.+-assoc n (suc (n + zero)) 1)) ⟩ + 2 * (suc n) + 1 + ∎ +total-height/black-height (black {n} t₁ _ t₂) = + let open Nat.≤-Reasoning in + begin + suc (i-total-height t₁ Nat.⊔ i-total-height t₂) + ≤⟨ Nat.s≤s (Nat.⊔-mono-≤ (total-height/black-height t₁) (total-height/black-height t₂)) ⟩ + suc ((2 * n + 1) Nat.⊔ (2 * n + 1)) + ≡⟨ Eq.cong suc (Nat.m≤n⇒m⊔n≡n Nat.≤-refl) ⟩ + suc (2 * n + 1) + ≤⟨ Nat.s≤s (Nat.+-monoˡ-≤ 1 (Nat.+-monoʳ-≤ n (Nat.n≤1+n (n + zero)))) ⟩ + 2 * (suc n) + 1 + ∎ + +i-nodes/bound/total-height : {y : val color} {n : val nat} {l : val (list A)} → (t : IRBT A y n l) → (1 + (i-nodes t)) Nat.≤ (2 Nat.^ (i-total-height t)) +i-nodes/bound/total-height leaf = Nat.s≤s Nat.z≤n +i-nodes/bound/total-height (red t₁ _ t₂) = + let open Nat.≤-Reasoning in + begin + suc (suc (i-nodes t₁ + i-nodes t₂)) + ≡⟨ Eq.cong suc (Eq.sym (Nat.+-suc (i-nodes t₁) (i-nodes t₂))) ⟩ + (suc (i-nodes t₁) + (suc (i-nodes t₂))) + ≤⟨ Nat.+-monoˡ-≤ (suc (i-nodes t₂)) (i-nodes/bound/total-height t₁) ⟩ + (2 Nat.^ (i-total-height t₁)) + (suc (i-nodes t₂)) + ≤⟨ Nat.+-monoʳ-≤ (2 Nat.^ (i-total-height t₁)) (i-nodes/bound/total-height t₂) ⟩ + (2 Nat.^ (i-total-height t₁)) + (2 Nat.^ (i-total-height t₂)) + ≤⟨ Nat.+-monoˡ-≤ ((2 Nat.^ (i-total-height t₂))) (Nat.^-monoʳ-≤ 2 {x = i-total-height t₁} (Nat.m≤n⇒m≤n⊔o (i-total-height t₂) (Nat.≤-refl))) ⟩ + (2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + (2 Nat.^ (i-total-height t₂)) + ≤⟨ Nat.+-monoʳ-≤ ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂))) ((Nat.^-monoʳ-≤ 2 {x = i-total-height t₂} (Nat.m≤n⇒m≤o⊔n (i-total-height t₁) (Nat.≤-refl)))) ⟩ + (2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + (2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + ≡⟨ Eq.trans (Eq.sym (Nat.+-identityʳ ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + (2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂))))) (Nat.+-assoc ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂))) ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂))) 0) ⟩ + ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + zero)) + ∎ +i-nodes/bound/total-height (black t₁ _ t₂) = + let open Nat.≤-Reasoning in + begin + suc (suc (i-nodes t₁ + i-nodes t₂)) + ≡⟨ Eq.cong suc (Eq.sym (Nat.+-suc (i-nodes t₁) (i-nodes t₂))) ⟩ + (suc (i-nodes t₁) + (suc (i-nodes t₂))) + ≤⟨ Nat.+-monoˡ-≤ (suc (i-nodes t₂)) (i-nodes/bound/total-height t₁) ⟩ + (2 Nat.^ (i-total-height t₁)) + (suc (i-nodes t₂)) + ≤⟨ Nat.+-monoʳ-≤ (2 Nat.^ (i-total-height t₁)) (i-nodes/bound/total-height t₂) ⟩ + (2 Nat.^ (i-total-height t₁)) + (2 Nat.^ (i-total-height t₂)) + ≤⟨ Nat.+-monoˡ-≤ ((2 Nat.^ (i-total-height t₂))) (Nat.^-monoʳ-≤ 2 {x = i-total-height t₁} (Nat.m≤n⇒m≤n⊔o (i-total-height t₂) (Nat.≤-refl))) ⟩ + (2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + (2 Nat.^ (i-total-height t₂)) + ≤⟨ Nat.+-monoʳ-≤ ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂))) ((Nat.^-monoʳ-≤ 2 {x = i-total-height t₂} (Nat.m≤n⇒m≤o⊔n (i-total-height t₁) (Nat.≤-refl)))) ⟩ + (2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + (2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + ≡⟨ Eq.trans (Eq.sym (Nat.+-identityʳ ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + (2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂))))) (Nat.+-assoc ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂))) ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂))) 0) ⟩ + ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + zero)) + ∎ + +i-nodes/lower-bound/node-black-height : {y : val color} {n : val nat} {l : val (list A)} → (t : IRBT A y n l) → (1 + (i-nodes t)) Nat.≤ (2 Nat.^ (2 * n + 1)) +i-nodes/lower-bound/node-black-height {A} {y} {n} t = + let open Nat.≤-Reasoning in + begin + 1 + (i-nodes t) + ≤⟨ i-nodes/bound/total-height t ⟩ + 2 Nat.^ (i-total-height t) + ≤⟨ Nat.^-monoʳ-≤ 2 (total-height/black-height t) ⟩ + 2 Nat.^ (2 * n + 1) + ∎ + +i-nodes/lower-bound/log-node-black-height : {y : val color} {n : val nat} {l : val (list A)} → (t : IRBT A y n l) → n Nat.≥ ⌊ (⌈log₂ (1 + (i-nodes t)) ⌉ ∸ 1) /2⌋ +i-nodes/lower-bound/log-node-black-height {A} {y} {n} t = + let open Nat.≤-Reasoning in + begin + ⌊ (⌈log₂ (1 + (i-nodes t)) ⌉ ∸ 1) /2⌋ + ≤⟨ Nat.⌊n/2⌋-mono (h t) ⟩ + ⌊ (2 * n) /2⌋ + ≡⟨ Eq.sym (Eq.trans (Nat.n≡⌊n+n/2⌋ n) (Eq.cong ⌊_/2⌋ (Eq.cong₂ _+_ refl (Eq.sym (Nat.+-identityʳ n))))) ⟩ + n + ∎ + where + m≤o+n⇒m∸n≤o : (m n o : val nat) → (m Nat.≤ (o + n)) → ((m ∸ n) Nat.≤ o) + m≤o+n⇒m∸n≤o m n o m≤o+n = + let open Nat.≤-Reasoning in + begin + m ∸ n + ≤⟨ Nat.∸-monoˡ-≤ n m≤o+n ⟩ + (o + n) ∸ n + ≡⟨ Nat.m+n∸n≡m o n ⟩ + o + ∎ + + h : {y : val color} {n : val nat} {l : val (list A)} → (t : IRBT A y n l) → (⌈log₂ (1 + (i-nodes t)) ⌉ ∸ 1) Nat.≤ (2 * n) + h {y} {n} t = m≤o+n⇒m∸n≤o ⌈log₂ (1 + (i-nodes t)) ⌉ 1 (2 * n) ( + let open Nat.≤-Reasoning in + begin + ⌈log₂ (1 + (i-nodes t)) ⌉ + ≤⟨ ⌈log₂⌉-mono-≤ (i-nodes/lower-bound/node-black-height t) ⟩ + ⌈log₂ (2 Nat.^ (2 * n + 1)) ⌉ + ≡⟨ ⌈log₂2^n⌉≡n (2 * n + 1) ⟩ + 2 * n + 1 + ∎) + + +i-rec : {A : tp⁺} {X : tp⁻} → + cmp + ( Π (U X) λ _ → + Π + ( U + ( Π color λ y₁ → Π nat λ n₁ → Π (list A) λ l₁ → Π (irbt A y₁ n₁ l₁) λ _ → Π (U X) λ _ → + Π A λ _ → + Π color λ y₂ → Π nat λ n₂ → Π (list A) λ l₂ → Π (irbt A y₂ n₂ l₂) λ _ → Π (U X) λ _ → + X + ) + ) λ _ → + Π color λ y → Π nat λ n → Π (list A) λ l → Π (irbt A y n l) λ _ → + X + ) +i-rec {A} {X} z f .black .zero .[] leaf = z +i-rec {A} {X} z f .red n .(_ ++ [ a ] ++ _) (red t₁ a t₂) = + f + _ _ _ t₁ (i-rec {A} {X} z f _ _ _ t₁) + a + _ _ _ t₂ (i-rec {A} {X} z f _ _ _ t₂) +i-rec {A} {X} z f .black .(suc _) .(_ ++ [ a ] ++ _) (black t₁ a t₂) = + f + _ _ _ t₁ (i-rec {A} {X} z f _ _ _ t₁) + a + _ _ _ t₂ (i-rec {A} {X} z f _ _ _ t₂) From 67f9958d531d4962571c9de85fce06bc0a9236fc Mon Sep 17 00:00:00 2001 From: Runming Li Date: Fri, 10 Nov 2023 19:11:46 -0500 Subject: [PATCH 2/7] cost analysis of rbt in decalf --- src/Examples.agda | 3 + src/Examples/Sequence/RedBlackMSequence.agda | 84 +-- src/Examples/Sequence/RedBlackTree.agda | 528 +++++++++++-------- 3 files changed, 353 insertions(+), 262 deletions(-) diff --git a/src/Examples.agda b/src/Examples.agda index 0a7a63e1..62e0c835 100644 --- a/src/Examples.agda +++ b/src/Examples.agda @@ -16,5 +16,8 @@ import Examples.Exp2 -- Amortized Analysis via Coinduction import Examples.Amortized +-- Sequence +import Examples.Sequence + -- Effectful import Examples.Decalf diff --git a/src/Examples/Sequence/RedBlackMSequence.agda b/src/Examples/Sequence/RedBlackMSequence.agda index 371ce1af..3357fa8e 100644 --- a/src/Examples/Sequence/RedBlackMSequence.agda +++ b/src/Examples/Sequence/RedBlackMSequence.agda @@ -14,11 +14,15 @@ open import Calf.Data.List open import Calf.Data.Product open import Calf.Data.Sum open import Calf.Data.IsBounded costMonoid +open import Calf.Data.IsBoundedG costMonoid open import Data.Nat as Nat using (_+_; _*_; ⌊_/2⌋; _≥_; _∸_) import Data.Nat.Properties as Nat open import Data.Nat.Logarithm +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) + open import Examples.Sequence.MSequence open import Examples.Sequence.RedBlackTree @@ -43,21 +47,30 @@ RedBlackMSequence = rbt : (A : tp⁺) → tp⁺ rbt A = meta⁺ (RBT A) + joinCont : ∀ (t₁ : RBT A) (t₂ : RBT A) a → Σ Color (λ c → Σ (List (val A)) (λ l → Σ (l ≡ (RBT.l t₁ ++ [ a ] ++ RBT.l t₂)) (λ x → + IRBT A c (suc (RBT.n t₁ ⊔ RBT.n t₂)) l ⊎ IRBT A c (RBT.n t₁ ⊔ RBT.n t₂) l))) → cmp (F (rbt A)) + joinCont _ _ _ (_ , _ , _ , inj₁ t) = ret ⟪ t ⟫ + joinCont _ _ _ (_ , _ , _ , inj₂ t) = ret ⟪ t ⟫ + join : cmp (Π (rbt A) λ _ → Π A λ _ → Π (rbt A) λ _ → F (rbt A)) - join {A} t₁ a t₂ = bind (F (rbt A)) (i-join _ _ _ (RBT.t t₁) a _ _ _ (RBT.t t₂)) λ { (_ , _ , _ , inj₁ t) → ret ⟪ t ⟫ - ; (_ , _ , _ , inj₂ t) → ret ⟪ t ⟫ } - - -- join/is-bounded : ∀ {A} t₁ a t₂ → IsBounded (rbt A) (join t₁ a t₂) - -- (1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)) , 1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂))) - -- join/is-bounded {A} t₁ a t₂ = - -- Eq.subst - -- (IsBounded _ _) {x = 1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)) + 0 , 1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)) + 0} - -- (Eq.cong₂ _,_ (Eq.cong suc (Nat.+-identityʳ (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)))) - -- ((Eq.cong suc (Nat.+-identityʳ (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)))))) - -- (bound/bind/const (1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)) , 1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂))) (0 , 0) - -- (i-join/is-bounded _ _ _ (RBT.t t₁) a _ _ _ (RBT.t t₂)) - -- (λ { (_ , _ , _ , inj₁ t) → bound/ret - -- ; (_ , _ , _ , inj₂ t) → bound/ret})) + join {A} t₁ a t₂ = bind (F (rbt A)) (i-join _ _ _ (RBT.t t₁) a _ _ _ (RBT.t t₂)) (joinCont t₁ t₂ a) + + join/is-bounded : ∀ {A} t₁ a t₂ → IsBounded (rbt A) (join t₁ a t₂) + (1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)) , 1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂))) + join/is-bounded {A} t₁ a t₂ = + let open ≤⁻-Reasoning cost in + begin + bind cost ( + bind (F (rbt A)) (i-join _ _ _ (RBT.t t₁) a _ _ _ (RBT.t t₂)) (joinCont t₁ t₂ a)) + (λ _ → ret triv) + ≡⟨ Eq.cong + (λ f → bind cost (i-join _ _ _ (RBT.t t₁) a _ _ _ (RBT.t t₂)) f) + (funext (λ { (_ , _ , _ , inj₁ _) → refl + ; (_ , _ , _ , inj₂ _) → refl })) ⟩ + bind cost (i-join _ _ _ (RBT.t t₁) a _ _ _ (RBT.t t₂)) (λ _ → ret triv) + ≤⟨ i-join/is-bounded _ _ _ (RBT.t t₁) a _ _ _ (RBT.t t₂) ⟩ + step⋆ (1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)) , 1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂))) + ∎ nodes : RBT A → val nat nodes ⟪ t ⟫ = i-nodes t @@ -74,28 +87,27 @@ RedBlackMSequence = let min = ⌊ (⌈log₂ (1 + (nodes t₁)) ⌉ ∸ 1) /2⌋ Nat.⊓ ⌊ (⌈log₂ (1 + (nodes t₂)) ⌉ ∸ 1) /2⌋ in (1 + 2 * (max ∸ min)) , (1 + 2 * (max ∸ min)) - -- join/is-bounded/nodes : ∀ {A} t₁ a t₂ → IsBounded (rbt A) (join t₁ a t₂) (join/cost t₁ t₂) - -- join/is-bounded/nodes {A} t₁ a t₂ = - -- bound/relax - -- (λ u → - -- (let open Nat.≤-Reasoning in - -- begin - -- 1 + 2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂) - -- ≤⟨ Nat.+-monoʳ-≤ 1 (Nat.*-monoʳ-≤ 2 (Nat.∸-monoˡ-≤ (RBT.n t₁ Nat.⊓ RBT.n t₂) (Nat.⊔-mono-≤ (nodes/upper-bound t₁) (nodes/upper-bound t₂)))) ⟩ - -- 1 + 2 * (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂) - -- ≤⟨ Nat.+-monoʳ-≤ 1 (Nat.*-monoʳ-≤ 2 (Nat.∸-monoʳ-≤ (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉) (Nat.⊓-mono-≤ (nodes/lower-bound t₁) (nodes/lower-bound t₂)))) ⟩ - -- 1 + 2 * (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ ∸ ⌊ (⌈log₂ (1 + (nodes t₁)) ⌉ ∸ 1) /2⌋ Nat.⊓ ⌊ (⌈log₂ (1 + (nodes t₂)) ⌉ ∸ 1) /2⌋) - -- ∎) , - -- (let open Nat.≤-Reasoning in - -- begin - -- 1 + 2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂) - -- ≤⟨ Nat.+-monoʳ-≤ 1 (Nat.*-monoʳ-≤ 2 (Nat.∸-monoˡ-≤ (RBT.n t₁ Nat.⊓ RBT.n t₂) (Nat.⊔-mono-≤ (nodes/upper-bound t₁) (nodes/upper-bound t₂)))) ⟩ - -- 1 + 2 * (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂) - -- ≤⟨ Nat.+-monoʳ-≤ 1 (Nat.*-monoʳ-≤ 2 (Nat.∸-monoʳ-≤ (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉) (Nat.⊓-mono-≤ (nodes/lower-bound t₁) (nodes/lower-bound t₂)))) ⟩ - -- 1 + 2 * (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ ∸ ⌊ (⌈log₂ (1 + (nodes t₁)) ⌉ ∸ 1) /2⌋ Nat.⊓ ⌊ (⌈log₂ (1 + (nodes t₂)) ⌉ ∸ 1) /2⌋) - -- ∎) - -- ) - -- (join/is-bounded t₁ a t₂) + join/is-bounded/nodes : ∀ {A} t₁ a t₂ → IsBounded (rbt A) (join t₁ a t₂) (join/cost t₁ t₂) + join/is-bounded/nodes {A} t₁ a t₂ = + let open ≤⁻-Reasoning cost in + begin + bind cost (join t₁ a t₂) (λ _ → ret triv) + ≤⟨ join/is-bounded t₁ a t₂ ⟩ + step⋆ (1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)) , 1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂))) + ≤⟨ step⋆-mono-≤⁻ (black-height-cost/to/node-cost , black-height-cost/to/node-cost) ⟩ + step⋆ (join/cost t₁ t₂) + ∎ + where + black-height-cost/to/node-cost : 1 + 2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂) Nat.≤ 1 + 2 * (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ ∸ ⌊ (⌈log₂ (1 + (nodes t₁)) ⌉ ∸ 1) /2⌋ Nat.⊓ ⌊ (⌈log₂ (1 + (nodes t₂)) ⌉ ∸ 1) /2⌋) + black-height-cost/to/node-cost = + let open Nat.≤-Reasoning in + begin + 1 + 2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂) + ≤⟨ Nat.+-monoʳ-≤ 1 (Nat.*-monoʳ-≤ 2 (Nat.∸-monoˡ-≤ (RBT.n t₁ Nat.⊓ RBT.n t₂) (Nat.⊔-mono-≤ (nodes/upper-bound t₁) (nodes/upper-bound t₂)))) ⟩ + 1 + 2 * (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂) + ≤⟨ Nat.+-monoʳ-≤ 1 (Nat.*-monoʳ-≤ 2 (Nat.∸-monoʳ-≤ (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉) (Nat.⊓-mono-≤ (nodes/lower-bound t₁) (nodes/lower-bound t₂)))) ⟩ + 1 + 2 * (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ ∸ ⌊ (⌈log₂ (1 + (nodes t₁)) ⌉ ∸ 1) /2⌋ Nat.⊓ ⌊ (⌈log₂ (1 + (nodes t₂)) ⌉ ∸ 1) /2⌋) + ∎ rec : {A : tp⁺} {X : tp⁻} → cmp diff --git a/src/Examples/Sequence/RedBlackTree.agda b/src/Examples/Sequence/RedBlackTree.agda index 745ce6ba..625c915b 100644 --- a/src/Examples/Sequence/RedBlackTree.agda +++ b/src/Examples/Sequence/RedBlackTree.agda @@ -1,5 +1,4 @@ {-# OPTIONS --prop --rewriting #-} -{-# OPTIONS --allow-unsolved-metas #-} module Examples.Sequence.RedBlackTree where @@ -16,15 +15,14 @@ open import Calf.Data.Nat open import Calf.Data.List open import Calf.Data.IsBounded costMonoid open import Calf.Data.IsBoundedG costMonoid -open import Data.Nat as Nat using (_+_; _*_; _<_; _>_; _≤ᵇ_; _<ᵇ_; ⌊_/2⌋; _≡ᵇ_; _≥_; _∸_) +open import Data.Nat as Nat using (_+_; _*_; _∸_) open import Data.Nat.Logarithm import Data.Nat.Properties as Nat import Data.List.Properties as List -open import Function using (_$_; case_of_) +open import Function using (_$_) open import Relation.Nullary -open import Relation.Nullary.Negation using (contradiction) open import Relation.Binary open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≢_; module ≡-Reasoning; ≢-sym) @@ -59,6 +57,39 @@ data AlmostLeftRBT (A : tp⁺) : (right-color : val color) → val nat → val ( alrbt : (A : tp⁺) → val color → val nat → val (list A) → tp⁺ alrbt A y n l = meta⁺ (AlmostLeftRBT A y n l) +joinLeftContCase₁ : ∀ l₁ l₂₁ l₂₂ a a₁ n₂ t₂₂ → + (Σ (List (val A)) λ l → Σ ((l ≡ l₁ ++ [ a ] ++ l₂₁)) (λ _ → (AlmostLeftRBT A black n₂ l))) → + cmp (F (Σ⁺ (list A) λ l → (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂₁ ++ [ a₁ ] ++ l₂₂)) ×⁺ (alrbt A red n₂ l))) +joinLeftContCase₁ {A} l₁ l₂₁ l₂₂ a a₁ n₂ t₂₂ (l , l≡l₂₁++a₁∷l₂₂ , valid {y = red} t') = + ret (((l₁ ++ [ a ] ++ l₂₁) ++ [ a₁ ] ++ l₂₂) , + (List.++-assoc l₁ (a ∷ l₂₁) (a₁ ∷ l₂₂) , + (Eq.subst (λ l' → AlmostLeftRBT A red n₂ l') (Eq.cong₂ _++_ l≡l₂₁++a₁∷l₂₂ refl) (violation t' a₁ t₂₂)))) +joinLeftContCase₁ {A} l₁ l₂₁ l₂₂ a a₁ n₂ t₂₂ (l , l≡l₂₁++a₁∷l₂₂ , valid {y = black} t') = + ret (((l₁ ++ [ a ] ++ l₂₁) ++ [ a₁ ] ++ l₂₂) , + (List.++-assoc l₁ (a ∷ l₂₁) (a₁ ∷ l₂₂) , + Eq.subst (λ l' → AlmostLeftRBT A red n₂ l') (Eq.cong₂ _++_ l≡l₂₁++a₁∷l₂₂ refl) (valid (red t' a₁ t₂₂)))) + +joinLeftContCase₂ : ∀ l₁ l₂₁ l₂₂ a a₁ y₂₁ y₂₂ n₂ (t₂₂ : IRBT A y₂₂ n₂ l₂₂) → + (Σ (List (val A))(λ a₂ → Σ (a₂ ≡ l₁ ++ a ∷ l₂₁) (λ x → AlmostLeftRBT A y₂₁ n₂ a₂))) → + cmp (F (Σ⁺ (list A) (λ l → meta⁺ (l ≡ l₁ ++ a ∷ l₂₁ ++ a₁ ∷ l₂₂) ×⁺ alrbt A black (suc n₂) l))) +joinLeftContCase₂ {A} l₁ l₂₁ l₂₂ a a₁ y₂₁ y₂₂ n₂ t₂₂ (l , l≡l₁++a∷l₂₁ , violation {l₂ = l'₂} (red {l₁ = l'₁₁} {l₂ = l'₁₂} t'₁₁ a'₁ t'₁₂) a' t'₂) = + ret ((l'₁₁ ++ [ a'₁ ] ++ l'₁₂) ++ [ a' ] ++ (l'₂ ++ [ a₁ ] ++ l₂₂) , + ((begin + (l'₁₁ ++ a'₁ ∷ l'₁₂) ++ a' ∷ l'₂ ++ a₁ ∷ l₂₂ + ≡˘⟨ List.++-assoc (l'₁₁ ++ a'₁ ∷ l'₁₂) (a' ∷ l'₂) (a₁ ∷ l₂₂) ⟩ + ((l'₁₁ ++ a'₁ ∷ l'₁₂) ++ a' ∷ l'₂) ++ a₁ ∷ l₂₂ + ≡⟨ Eq.cong₂ _++_ l≡l₁++a∷l₂₁ refl ⟩ + (l₁ ++ a ∷ l₂₁) ++ a₁ ∷ l₂₂ + ≡⟨ List.++-assoc l₁ (a ∷ l₂₁) (a₁ ∷ l₂₂) ⟩ + l₁ ++ a ∷ l₂₁ ++ a₁ ∷ l₂₂ + ∎) , + (valid (red (black t'₁₁ a'₁ t'₁₂) a' (black t'₂ a₁ t₂₂))))) + where open ≡-Reasoning +joinLeftContCase₂ {A} l₁ l₂₁ l₂₂ a a₁ y₂₁ y₂₂ n₂ t₂₂ (l , l≡l₁++a∷l₂₁ , valid t') = + ret (((l₁ ++ [ a ] ++ l₂₁) ++ [ a₁ ] ++ l₂₂) , + (List.++-assoc l₁ (a ∷ l₂₁) (a₁ ∷ l₂₂) , + Eq.subst (λ l' → AlmostLeftRBT A black (suc n₂) l') (Eq.cong₂ _++_ l≡l₁++a∷l₂₁ refl) (valid (black t' a₁ t₂₂)))) + joinLeft : cmp ( Π color λ y₁ → Π nat λ n₁ → Π (list A) λ l₁ → Π (irbt A y₁ n₁ l₁) λ _ → @@ -71,16 +102,8 @@ joinLeft {A} y₁ n₁ l₁ t₁ a .red n₂ l₂ (red {l₁ = l₂₁} {l₂ = step (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ l₁ ++ a ∷ l₂₁ ++ a₁ ∷ l₂₂)) ×⁺ (alrbt A red n₂ l)))) (1 , 1) $ bind (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ l₁ ++ a ∷ l₂₁ ++ a₁ ∷ l₂₂)) ×⁺ (alrbt A red n₂ l)))) (joinLeft _ _ _ t₁ a _ _ _ t₂₁ n₁n₂) - (λ { (l , l≡l₁₂++a₁∷l₂ , valid {y = red} t') → - ret (l₁₁ ++ [ a₁ ] ++ (l₁₂ ++ [ a ] ++ l₂) , - Eq.sym (List.++-assoc l₁₁ (a₁ ∷ l₁₂) (a ∷ l₂)) , - Eq.subst (λ l' → AlmostRightRBT A red n₁ l') (Eq.cong₂ _++_ refl (Eq.cong₂ _∷_ refl l≡l₁₂++a₁∷l₂)) (violation t₁₁ a₁ t')) - ; (l , l≡l₁₂++a₁∷l₂ , valid {y = black} t') → - ret (l₁₁ ++ [ a₁ ] ++ (l₁₂ ++ [ a ] ++ l₂) , - Eq.sym (List.++-assoc l₁₁ (a₁ ∷ l₁₂) (a ∷ l₂)) , - Eq.subst (λ l' → AlmostRightRBT A red n₁ l') (Eq.cong₂ _++_ refl (Eq.cong₂ _∷_ refl l≡l₁₂++a₁∷l₂)) (valid (red t₁₁ a₁ t'))) - }) -joinRight {A} .black (suc n₁) l₁ (black {l₁ = l₁₁} {l₂ = l₁₂} t₁₁ a₁ t₁₂) a y₂ n₂ l₂ t₂ n₁>n₂ with n₁ Nat.≟ n₂ + (joinRightContCase₁ l₁₁ l₁₂ l₂ a a₁ n₁ t₁₁) +joinRight {A} .black (suc n₁) l₁ (black {y₁ = y₁₁} {y₂ = y₁₂} {l₁ = l₁₁} {l₂ = l₁₂} t₁₁ a₁ t₁₂) a y₂ n₂ l₂ t₂ n₁>n₂ with n₁ Nat.≟ n₂ joinRight {A} .black (suc n₁) l₁ (black {l₁ = l₁₁} {l₂ = l₁₂} t₁₁ a₁ t₁₂) a red n₁ l₂ (red {l₁ = l₂₁} {l₂ = l₂₂} t₂₁ a₂ t₂₂) n₁>n₂ | yes refl = ret ((l₁₁ ++ [ a₁ ] ++ l₁₂) ++ [ a ] ++ (l₂₁ ++ [ a₂ ] ++ l₂₂) , refl , @@ -267,70 +293,108 @@ joinRight {A} .black (suc n₁) l₁ (black {y₂ = black} {l₁ = l₁₁} {l step (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂)) ×⁺ (arrbt A black (suc n₁) l)))) (1 , 1) $ bind (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂)) ×⁺ (arrbt A black (suc n₁) l)))) (joinRight _ _ _ t₁₂ a _ _ _ t₂ (Nat.≤∧≢⇒< (Nat.≤-pred n₁>n₂) (≢-sym n₁≢n₂))) - λ { (l , l≡l₁₂++a∷l₂ , violation {l₁ = l'₁} t'₁ a' (red {l₁ = l'₂₁} {l₂ = l'₂₂} t'₂₁ a'₂ t'₂₂)) → - ret ((l₁₁ ++ [ a₁ ] ++ l'₁) ++ [ a' ] ++ (l'₂₁ ++ [ a'₂ ] ++ l'₂₂) , - (begin - (l₁₁ ++ a₁ ∷ l'₁) ++ a' ∷ l'₂₁ ++ a'₂ ∷ l'₂₂ - ≡⟨ List.++-assoc l₁₁ (a₁ ∷ l'₁) (a' ∷ l'₂₁ ++ a'₂ ∷ l'₂₂) ⟩ - l₁₁ ++ a₁ ∷ l'₁ ++ a' ∷ l'₂₁ ++ a'₂ ∷ l'₂₂ - ≡⟨ Eq.cong₂ _++_ refl (Eq.cong₂ _∷_ refl l≡l₁₂++a∷l₂) ⟩ - l₁₁ ++ a₁ ∷ l₁₂ ++ a ∷ l₂ - ≡˘⟨ List.++-assoc l₁₁ (a₁ ∷ l₁₂) (a ∷ l₂) ⟩ - (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂ - ∎) , - (valid (red (black t₁₁ a₁ t'₁) a' (black t'₂₁ a'₂ t'₂₂)))) - ; (l , l≡l₁₂++a∷l₂ , valid t') → - ret (l₁₁ ++ [ a₁ ] ++ (l₁₂ ++ [ a ] ++ l₂) , - Eq.sym (List.++-assoc l₁₁ (a₁ ∷ l₁₂) (a ∷ l₂)) , - Eq.subst (λ l' → AlmostRightRBT A black (suc n₁) l') (Eq.cong₂ _++_ refl (Eq.cong₂ _∷_ refl l≡l₁₂++a∷l₂)) (valid (black t₁₁ a₁ t'))) - } - where open ≡-Reasoning + (joinRightContCase₂ l₁₁ l₁₂ l₂ a a₁ y₁₁ y₁₂ n₁ t₁₁) + +joinRight/cost : (y : val color) (n₁ n₂ : val nat) → ℂ +joinRight/cost red n₁ n₂ = 1 + (2 * (n₁ ∸ n₂)) , 1 + (2 * (n₁ ∸ n₂)) +joinRight/cost black n₁ n₂ = (2 * (n₁ ∸ n₂)) , (2 * (n₁ ∸ n₂)) --- joinRight/cost : (y : val color) (n₁ n₂ : val nat) → ℂ --- joinRight/cost red n₁ n₂ = 1 + (2 * (n₁ ∸ n₂)) , 1 + (2 * (n₁ ∸ n₂)) --- joinRight/cost black n₁ n₂ = (2 * (n₁ ∸ n₂)) , (2 * (n₁ ∸ n₂)) - --- joinRight/is-bounded' : ∀ y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ --- → IsBounded (Σ++ (list A) λ l → prod⁺ (U (meta (l ≡ l₁ ++ [ a ] ++ l₂))) (arrbt A y₁ n₁ l)) (joinRight y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂) (joinRight/cost y₁ n₁ n₂) - --- joinRight/is-bounded : ∀ {A} y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ --- → IsBounded (Σ++ (list A) λ l → prod⁺ (U (meta (l ≡ l₁ ++ [ a ] ++ l₂))) (arrbt A y₁ n₁ l)) (joinRight y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂) (1 + (2 * (n₁ ∸ n₂)) , 1 + (2 * (n₁ ∸ n₂))) - --- joinRight/is-bounded' red n₁ l₁ (red t₁₁ a₁ t₁₂) a y₂ n₂ l₂ t₂ n₁>n₂ = --- bound/step (1 , 1) (2 * (n₁ ∸ n₂) , 2 * (n₁ ∸ n₂)) --- (Eq.subst --- (IsBounded _ _) --- (Eq.cong₂ _,_ (Nat.+-identityʳ (2 * (n₁ ∸ n₂))) (Nat.+-identityʳ (2 * (n₁ ∸ n₂)))) --- (bound/bind/const (2 * (n₁ ∸ n₂) , 2 * (n₁ ∸ n₂)) (0 , 0) --- (joinRight/is-bounded' _ _ _ t₁₂ a _ _ _ t₂ n₁>n₂) --- λ {(_ , _ , valid (red _ _ _)) → bound/ret --- ; (_ , _ , valid (black _ _ _)) → bound/ret} --- )) --- joinRight/is-bounded' black (suc n₁) l₁ (black t₁₁ a₁ t₁₂) a y₂ n₂ l₂ t₂ n₁>n₂ with n₁ Nat.≟ n₂ --- joinRight/is-bounded' black _ _ (black _ _ _) _ red _ _ (red _ _ _) _ | yes refl = --- bound/relax (λ u → Nat.z≤n , Nat.z≤n) bound/ret --- joinRight/is-bounded' black _ _ (black {y₂ = red} _ _ (red _ _ _)) _ black _ _ _ _ | yes refl = --- bound/relax (λ u → Nat.z≤n , Nat.z≤n) bound/ret --- joinRight/is-bounded' black _ _ (black {y₂ = black} _ _ _) _ black _ _ _ _ | yes refl = --- bound/relax (λ u → Nat.z≤n , Nat.z≤n) bound/ret --- ... | no n₁≢n₂ = --- Eq.subst --- (IsBounded _ _) {x = 2 + 2 * (n₁ ∸ n₂) , 2 + 2 * (n₁ ∸ n₂)} --- (Eq.cong₂ _,_ (Eq.trans (Eq.sym (Nat.*-suc 2 (n₁ ∸ n₂))) (Eq.cong (2 *_) (Eq.sym (Nat.+-∸-assoc 1 n₁>n₂)))) --- (Eq.trans (Eq.sym (Nat.*-suc 2 (n₁ ∸ n₂))) (Eq.cong (2 *_) (Eq.sym (Nat.+-∸-assoc 1 n₁>n₂))))) --- (bound/step (1 , 1) (1 + 2 * (n₁ ∸ n₂) , 1 + 2 * (n₁ ∸ n₂)) --- (Eq.subst --- (IsBounded _ _) {x = 1 + 2 * (n₁ ∸ n₂) + 0 , 1 + 2 * (n₁ ∸ n₂) + 0} --- (Eq.cong₂ _,_ (Nat.+-identityʳ (1 + 2 * (n₁ ∸ n₂))) (Nat.+-identityʳ (1 + 2 * (n₁ ∸ n₂)))) --- (bound/bind/const (1 + 2 * (n₁ ∸ n₂) , 1 + 2 * (n₁ ∸ n₂)) (0 , 0) --- (joinRight/is-bounded _ _ _ t₁₂ a _ _ _ t₂ _) --- (λ { (_ , _ , (violation _ _ (red _ _ _))) → bound/ret --- ; (_ , _ , (valid _)) → bound/ret })))) - --- joinRight/is-bounded red n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ = --- joinRight/is-bounded' red n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ --- joinRight/is-bounded black n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ = --- bound/relax (λ u → Nat.n≤1+n _ , Nat.n≤1+n _) (joinRight/is-bounded' black n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂) +joinRight/is-bounded' : ∀ y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ + → IsBounded (Σ⁺ (list A) λ l → (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ (arrbt A y₁ n₁ l)) (joinRight y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂) (joinRight/cost y₁ n₁ n₂) + +joinRight/is-bounded : ∀ {A} y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ + → IsBounded (Σ⁺ (list A) λ l → (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ (arrbt A y₁ n₁ l)) (joinRight y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂) (1 + (2 * (n₁ ∸ n₂)) , 1 + (2 * (n₁ ∸ n₂))) + +joinRight/is-bounded' {A} red n₁ l₁ (red {l₁ = l₁₁} {l₂ = l₁₂} t₁₁ a₁ t₁₂) a y₂ n₂ l₂ t₂ n₁>n₂ = + let open ≤⁻-Reasoning cost in + begin + step cost (1 , 1) ( + bind cost ( + bind (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂)) ×⁺ (arrbt A red n₁ l)))) + (joinRight _ _ _ t₁₂ a _ _ _ t₂ n₁>n₂) + (joinRightContCase₁ l₁₁ l₁₂ l₂ a a₁ n₁ t₁₁)) + (λ _ → ret triv)) + ≡⟨ Eq.cong + (λ e → step cost (1 , 1) e) + (Eq.cong + (λ f → bind cost (joinRight _ _ _ t₁₂ a _ _ _ t₂ n₁>n₂) f) + (funext ((λ { (_ , _ , valid {y = red} _) → refl + ; (_ , _ , valid {y = black} _) → refl })))) ⟩ + step cost (1 , 1) ( + bind cost (joinRight _ _ _ t₁₂ a _ _ _ t₂ n₁>n₂) + (λ _ → ret triv)) + ≤⟨ ≤⁻-mono (λ e → step cost (1 , 1) e) (joinRight/is-bounded' _ _ _ t₁₂ a _ _ _ t₂ n₁>n₂) ⟩ + step cost (1 , 1) ( + bind cost (step⋆ (2 * (n₁ ∸ n₂) , 2 * (n₁ ∸ n₂))) λ _ → ret triv) + ≤⟨ ≤⁻-refl ⟩ + step⋆ (1 + 2 * (n₁ ∸ n₂) , 1 + 2 * (n₁ ∸ n₂)) + ∎ +joinRight/is-bounded' {A} black (suc n₁) l₁ (black {y₁ = y₁₁} {y₂ = y₁₂} {l₁ = l₁₁} {l₂ = l₁₂} t₁₁ a₁ t₁₂) a y₂ n₂ l₂ t₂ n₁>n₂ with n₁ Nat.≟ n₂ +joinRight/is-bounded' black n₁ _ (black _ _ _) _ red _ _ (red _ _ _) _ | yes refl = + step⋆-mono-≤⁻ (Nat.z≤n {2 * (suc n₁ ∸ n₁)} , Nat.z≤n {2 * (suc n₁ ∸ n₁)}) +joinRight/is-bounded' black n₁ _ (black {y₂ = red} _ _ (red _ _ _)) _ black _ _ _ _ | yes refl = + step⋆-mono-≤⁻ (Nat.z≤n {2 * (suc n₁ ∸ n₁)} , Nat.z≤n {2 * (suc n₁ ∸ n₁)}) +joinRight/is-bounded' black n₁ _ (black {y₂ = black} _ _ _) _ black _ _ _ _ | yes refl = + step⋆-mono-≤⁻ (Nat.z≤n {2 * (suc n₁ ∸ n₁)} , Nat.z≤n {2 * (suc n₁ ∸ n₁)}) +... | no n₁≢n₂ = + let open ≤⁻-Reasoning cost in + begin + step cost (1 , 1) ( + bind cost ( + bind (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂)) ×⁺ (arrbt A black (suc n₁) l)))) + (joinRight _ _ _ t₁₂ a _ _ _ t₂ (Nat.≤∧≢⇒< (Nat.≤-pred n₁>n₂) (≢-sym n₁≢n₂))) + (joinRightContCase₂ l₁₁ l₁₂ l₂ a a₁ y₁₁ y₁₂ n₁ t₁₁)) + (λ _ → ret triv)) + ≡⟨ Eq.cong + (λ e → step cost (1 , 1) e) + (Eq.cong + (λ f → bind cost (joinRight _ _ _ t₁₂ a _ _ _ t₂ (Nat.≤∧≢⇒< (Nat.≤-pred n₁>n₂) (≢-sym n₁≢n₂))) f) + (funext (λ { (_ , _ , violation _ _ (red _ _ _)) → refl + ; (_ , _ , valid _) → refl }))) ⟩ + step cost (1 , 1) ( + bind cost (joinRight _ _ _ t₁₂ a _ _ _ t₂ (Nat.≤∧≢⇒< (Nat.≤-pred n₁>n₂) (≢-sym n₁≢n₂))) + (λ _ → ret triv)) + ≤⟨ ≤⁻-mono (λ e → step cost (1 , 1) e) (joinRight/is-bounded _ _ _ t₁₂ a _ _ _ t₂ _) ⟩ + step cost (1 , 1) ( + bind cost (step⋆ (1 + 2 * (n₁ ∸ n₂) , 1 + 2 * (n₁ ∸ n₂))) λ _ → ret triv) + ≡⟨ Eq.cong (λ c → step⋆ c) + (Eq.cong₂ _,_ + (Eq.trans (Eq.sym (Nat.*-suc 2 (n₁ ∸ n₂))) (Eq.cong (2 *_) (Eq.sym (Nat.+-∸-assoc 1 n₁>n₂)))) + (Eq.trans (Eq.sym (Nat.*-suc 2 (n₁ ∸ n₂))) (Eq.cong (2 *_) (Eq.sym (Nat.+-∸-assoc 1 n₁>n₂))))) ⟩ + step⋆ (2 * (suc n₁ ∸ n₂) , 2 * (suc n₁ ∸ n₂)) + ∎ + +joinRight/is-bounded red n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ = + joinRight/is-bounded' red n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ +joinRight/is-bounded black n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ = + let open ≤⁻-Reasoning cost in + begin + bind cost (joinRight black n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂) (λ _ → ret triv) + ≤⟨ joinRight/is-bounded' black n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ ⟩ + step⋆ (2 * (n₁ ∸ n₂) , 2 * (n₁ ∸ n₂)) + ≤⟨ step⋆-mono-≤⁻ (Nat.n≤1+n _ , Nat.n≤1+n _) ⟩ + step⋆ (1 + 2 * (n₁ ∸ n₂) , 1 + 2 * (n₁ ∸ n₂)) + ∎ + +i-joinContCaseLeft : ∀ l₁ l₂ a y₂ n₁ n₂ n₁n₂ → + (Σ (List (val A)) (λ a₁ → Σ (a₁ ≡ l₁ ++ a ∷ l₂) (λ x → AlmostRightRBT A y₁ n₁ a₁))) → + cmp (F (Σ⁺ color (λ y → Σ⁺ (list A) (λ l → meta⁺ (l ≡ l₁ ++ a ∷ l₂) ×⁺ (irbt A y (suc (n₁ ⊔ n₂)) l ⊎⁺ irbt A y (n₁ ⊔ n₂) l))))) +i-joinContCaseRight {A} l₁ l₂ a y₁ n₁ n₂ n₁>n₂ (l , l≡l₁++a∷l₂ , violation {l₁ = l'₁} {l₂ = l'₂} t'₁ a' t'₂) = + ret (black , l'₁ ++ [ a' ] ++ l'₂ , l≡l₁++a∷l₂ , + inj₁ (Eq.subst (λ n → IRBT A black (suc n) (l'₁ ++ a' ∷ l'₂)) (Eq.sym (Nat.m≥n⇒m⊔n≡m (Nat.<⇒≤ n₁>n₂))) + (black t'₁ a' t'₂))) +i-joinContCaseRight {A} l₁ l₂ a y₁ n₁ n₂ n₁>n₂ (l , l≡l₁++a∷l₂ , valid {n = n} {y = y} {l = l} t') = + ret (y , l , l≡l₁++a∷l₂ , inj₂ (Eq.subst (λ n → IRBT A y n l) (Eq.sym (Nat.m≥n⇒m⊔n≡m (Nat.<⇒≤ n₁>n₂))) t')) i-join : cmp @@ -354,56 +418,68 @@ i-join {A} black n₁ l₁ t₁ a black n₂ l₂ t₂ | tri≈ ¬n₁ ¬n₁n₂ = bind (F (Σ⁺ color λ y → Σ⁺ (list A) λ l → (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ ((irbt A y (1 + (n₁ Nat.⊔ n₂)) l) ⊎⁺ (irbt A y (n₁ Nat.⊔ n₂) l)))) (joinRight _ _ _ t₁ a _ _ _ t₂ n₁>n₂) - (λ { (l , l≡l₁++a∷l₂ , violation {l₁ = l'₁} {l₂ = l'₂} t'₁ a' t'₂) → - ret (black , l'₁ ++ [ a' ] ++ l'₂ , l≡l₁++a∷l₂ , - inj₁ (Eq.subst (λ n → IRBT A black (suc n) (l'₁ ++ a' ∷ l'₂)) (Eq.sym (Nat.m≥n⇒m⊔n≡m (Nat.<⇒≤ n₁>n₂))) - (black t'₁ a' t'₂))) - ; (l , l≡l₁++a∷l₂ , valid {n = n} {y = y} {l = l} t') → - ret (y , l , l≡l₁++a∷l₂ , inj₂ (Eq.subst (λ n → IRBT A y n l) (Eq.sym (Nat.m≥n⇒m⊔n≡m (Nat.<⇒≤ n₁>n₂))) t')) - } - ) - --- i-join/is-bounded : ∀ {A} y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ --- → IsBounded (Σ++ color λ y → Σ++ (list A) λ l → --- prod⁺ (U (meta (l ≡ l₁ ++ [ a ] ++ l₂))) (sum (irbt A y (1 + (n₁ Nat.⊔ n₂)) l) (irbt A y (n₁ Nat.⊔ n₂) l))) (i-join y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂) --- (1 + (2 * (n₁ Nat.⊔ n₂ ∸ n₁ Nat.⊓ n₂)) , 1 + (2 * (n₁ Nat.⊔ n₂ ∸ n₁ Nat.⊓ n₂))) --- i-join/is-bounded {A} y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ with Nat.<-cmp n₁ n₂ --- i-join/is-bounded {A} red n₁ l₁ t₁ a y₂ .n₁ l₂ t₂ | tri≈ ¬n₁n₂ = --- bound/relax (λ u → Nat.z≤n , Nat.z≤n) bound/ret --- i-join/is-bounded {A} black n₁ l₁ t₁ a red n₁ l₂ t₂ | tri≈ ¬n₁n₂ = --- bound/relax (λ u → Nat.z≤n , Nat.z≤n) bound/ret --- i-join/is-bounded {A} black n₁ l₁ t₁ a black n₁ l₂ t₂ | tri≈ ¬n₁n₂ = --- bound/relax (λ u → Nat.z≤n , Nat.z≤n) bound/ret --- ... | tri< n₁n₂ = --- Eq.subst --- (IsBounded _ _) {x = 1 + 2 * (n₂ ∸ n₁) + 0 , 1 + 2 * (n₂ ∸ n₁) + 0} --- (Eq.cong₂ _,_ (Eq.cong suc (Eq.trans (Nat.+-identityʳ (2 * (n₂ ∸ n₁))) (Eq.cong (2 *_) (Eq.cong₂ _∸_ (Eq.sym (Nat.m≤n⇒m⊔n≡n (Nat.<⇒≤ n₁ ¬n₁n₂ = --- Eq.subst --- (IsBounded _ _) {x = 1 + 2 * (n₁ ∸ n₂) + 0 , 1 + 2 * (n₁ ∸ n₂) + 0} --- (Eq.cong₂ _,_ (Eq.cong suc (Eq.trans (Nat.+-identityʳ (2 * (n₁ ∸ n₂))) (Eq.cong (2 *_) (Eq.cong₂ _∸_ (Eq.sym (Nat.m≥n⇒m⊔n≡m (Nat.<⇒≤ n₁>n₂))) (Eq.sym (Nat.m≥n⇒m⊓n≡n (Nat.<⇒≤ n₁>n₂))))))) --- ((Eq.cong suc (Eq.trans (Nat.+-identityʳ (2 * (n₁ ∸ n₂))) (Eq.cong (2 *_) (Eq.cong₂ _∸_ (Eq.sym (Nat.m≥n⇒m⊔n≡m (Nat.<⇒≤ n₁>n₂))) (Eq.sym (Nat.m≥n⇒m⊓n≡n (Nat.<⇒≤ n₁>n₂))))))))) --- (bound/bind/const (1 + 2 * (n₁ ∸ n₂) , 1 + 2 * (n₁ ∸ n₂)) (0 , 0) --- (joinRight/is-bounded _ _ _ t₁ a _ _ _ t₂ n₁>n₂) --- λ { (_ , _ , violation _ _ _) → bound/ret --- ; (_ , _ , valid _) → bound/ret}) + (i-joinContCaseRight l₁ l₂ a y₁ n₁ n₂ n₁>n₂) + +i-join/is-bounded : ∀ {A} y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ + → IsBounded (Σ⁺ color λ y → Σ⁺ (list A) λ l → + (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ ((irbt A y (1 + (n₁ Nat.⊔ n₂)) l) ⊎⁺ (irbt A y (n₁ Nat.⊔ n₂) l))) (i-join y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂) + (1 + (2 * (n₁ Nat.⊔ n₂ ∸ n₁ Nat.⊓ n₂)) , 1 + (2 * (n₁ Nat.⊔ n₂ ∸ n₁ Nat.⊓ n₂))) +i-join/is-bounded {A} y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ with Nat.<-cmp n₁ n₂ +i-join/is-bounded {A} red n₁ l₁ t₁ a y₂ .n₁ l₂ t₂ | tri≈ ¬n₁n₂ = + step⋆-mono-≤⁻ (Nat.z≤n {1 + (2 * (n₁ Nat.⊔ n₁ ∸ n₁ Nat.⊓ n₁))}, Nat.z≤n {1 + (2 * (n₁ Nat.⊔ n₁ ∸ n₁ Nat.⊓ n₁))}) +i-join/is-bounded {A} black n₁ l₁ t₁ a red n₁ l₂ t₂ | tri≈ ¬n₁n₂ = + step⋆-mono-≤⁻ (Nat.z≤n {1 + (2 * (n₁ Nat.⊔ n₁ ∸ n₁ Nat.⊓ n₁))}, Nat.z≤n {1 + (2 * (n₁ Nat.⊔ n₁ ∸ n₁ Nat.⊓ n₁))}) +i-join/is-bounded {A} black n₁ l₁ t₁ a black n₁ l₂ t₂ | tri≈ ¬n₁n₂ = + step⋆-mono-≤⁻ (Nat.z≤n {1 + (2 * (n₁ Nat.⊔ n₁ ∸ n₁ Nat.⊓ n₁))}, Nat.z≤n {1 + (2 * (n₁ Nat.⊔ n₁ ∸ n₁ Nat.⊓ n₁))}) +... | tri< n₁n₂ = + let open ≤⁻-Reasoning cost in + begin + bind cost ( + bind (F (Σ⁺ color λ y → Σ⁺ (list A) λ l → + (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ ((irbt A y (1 + (n₁ Nat.⊔ n₂)) l) ⊎⁺ (irbt A y (n₁ Nat.⊔ n₂) l)))) + (joinLeft _ _ _ t₁ a _ _ _ t₂ n₁ ¬n₁n₂ = + let open ≤⁻-Reasoning cost in + begin + bind cost ( + bind (F (Σ⁺ color λ y → Σ⁺ (list A) λ l → + (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ ((irbt A y (1 + (n₁ Nat.⊔ n₂)) l) ⊎⁺ (irbt A y (n₁ Nat.⊔ n₂) l)))) + (joinRight _ _ _ t₁ a _ _ _ t₂ n₁>n₂) + (i-joinContCaseRight l₁ l₂ a y₁ n₁ n₂ n₁>n₂)) + (λ _ → ret triv) + ≡⟨ Eq.cong + (λ f → bind cost (joinRight _ _ _ t₁ a _ _ _ t₂ n₁>n₂) f) + (funext (λ { (_ , _ , violation _ _ _) → refl + ; (_ , _ , valid _) → refl })) ⟩ + bind cost (joinRight _ _ _ t₁ a _ _ _ t₂ n₁>n₂) (λ _ → ret triv) + ≤⟨ joinRight/is-bounded _ _ _ t₁ a _ _ _ t₂ n₁>n₂ ⟩ + step⋆ (1 + 2 * (n₁ ∸ n₂) , 1 + 2 * (n₁ ∸ n₂)) + ≡⟨ Eq.cong (λ c → step⋆ c) + (Eq.cong₂ _,_ + (Eq.cong (1 +_) (Eq.cong (2 *_) (Eq.cong₂ _∸_ (Eq.sym (Nat.m≥n⇒m⊔n≡m (Nat.<⇒≤ n₁>n₂))) (Eq.sym (Nat.m≥n⇒m⊓n≡n (Nat.<⇒≤ n₁>n₂)))))) + (Eq.cong (1 +_) (Eq.cong (2 *_) (Eq.cong₂ _∸_ (Eq.sym (Nat.m≥n⇒m⊔n≡m (Nat.<⇒≤ n₁>n₂))) (Eq.sym (Nat.m≥n⇒m⊓n≡n (Nat.<⇒≤ n₁>n₂))))))) ⟩ + step⋆ (1 + (2 * (n₁ Nat.⊔ n₂ ∸ n₁ Nat.⊓ n₂)) , 1 + (2 * (n₁ Nat.⊔ n₂ ∸ n₁ Nat.⊓ n₂))) + ∎ i-nodes : {y : val color} {n : val nat} {l : val (list A)} → IRBT A y n l → val nat i-nodes leaf = 0 From 19c17bef6c6e31a85c234d4da922113494f5418d Mon Sep 17 00:00:00 2001 From: Runming Li Date: Sat, 18 Nov 2023 15:26:55 -0500 Subject: [PATCH 3/7] mapreduce draft --- src/Examples/Sequence/DerivedFormsRBT.agda | 150 +++++++++++++++++++++ 1 file changed, 150 insertions(+) create mode 100644 src/Examples/Sequence/DerivedFormsRBT.agda diff --git a/src/Examples/Sequence/DerivedFormsRBT.agda b/src/Examples/Sequence/DerivedFormsRBT.agda new file mode 100644 index 00000000..ae8aa3b2 --- /dev/null +++ b/src/Examples/Sequence/DerivedFormsRBT.agda @@ -0,0 +1,150 @@ +{-# OPTIONS --prop --rewriting #-} + +module Examples.Sequence.DerivedFormsRBT where + +open import Algebra.Cost + +parCostMonoid = ℕ²-ParCostMonoid +open ParCostMonoid parCostMonoid + +open import Calf costMonoid +open import Calf.Parallel parCostMonoid + +open import Calf.Data.Nat +open import Calf.Data.List +open import Calf.Data.Product +-- open import Calf.Data.Sum +open import Calf.Data.IsBounded costMonoid +open import Calf.Data.IsBoundedG costMonoid +-- open import Data.Product hiding (map) +-- open import Data.List as List hiding (sum; map) +-- import Data.List.Properties as List +open import Data.Nat as Nat using (_+_; _*_; _<_; _>_; _≤ᵇ_; _<ᵇ_; ⌊_/2⌋; _≡ᵇ_; _∸_) +import Data.Nat.Properties as Nat +-- open import Data.Nat.Logarithm + +open import Level using (0ℓ) +open import Function using (_$_) +open import Relation.Nullary +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≢_; module ≡-Reasoning; ≢-sym) + +open import Examples.Sequence.RedBlackTree + + +module MapReduce {A B : tp⁺} where + mapreduce : cmp $ + Π color λ y → Π nat λ n → Π (list A) λ l → Π (irbt A y n l) λ _ → + Π (U (Π A λ _ → F B)) λ _ → + Π (U (Π B λ _ → Π B λ _ → F B)) λ _ → + Π B λ _ → + F B + mapreduce .black .zero .[] leaf f g z = ret z + mapreduce .red n l (red t₁ a t₂) f g z = + bind (F B) + ((mapreduce _ _ _ t₁ f g z) ∥ (mapreduce _ _ _ t₂ f g z)) λ s → + bind (F B) (f a) (λ b → + bind (F B) (g b (proj₂ s)) (λ s₃ → + bind (F B) (g (proj₁ s) s₃) ret)) + mapreduce .black n@(suc n') l (black t₁ a t₂) f g z = + bind (F B) + ((mapreduce _ _ _ t₁ f g z) ∥ (mapreduce _ _ _ t₂ f g z)) λ s → + bind (F B) (f a) (λ b → + bind (F B) (g b (proj₂ s)) (λ s₃ → + bind (F B) (g (proj₁ s) s₃) ret)) + + mapreduce/cost/work : val color → val nat → val nat + mapreduce/cost/work red n = 12 * (4 ^ (n ∸ 1)) ∸ 3 + mapreduce/cost/work black n = 6 * (4 ^ (n ∸ 1)) ∸ 3 + + mapreduce/cost/work' : val nat → val nat + mapreduce/cost/work' n = 12 * (4 ^ (n ∸ 1)) ∸ 3 + + mapreduce/cost/work≤mapreduce/cost/work' : (y : val color) → (n : val nat) → mapreduce/cost/work y n Nat.≤ mapreduce/cost/work' n + mapreduce/cost/work≤mapreduce/cost/work' red n = Nat.≤-refl + mapreduce/cost/work≤mapreduce/cost/work' black n = + Nat.∸-monoˡ-≤ {n = 12 * (4 ^ (n ∸ 1))} 3 + (Nat.*-monoˡ-≤ (4 ^ (n ∸ 1)) {y = 12} (Nat.s≤s (Nat.s≤s (Nat.s≤s (Nat.s≤s (Nat.s≤s (Nat.s≤s Nat.z≤n))))))) + + mapreduce/cost/span : val color → val nat → val nat + mapreduce/cost/span red n = 6 * n + mapreduce/cost/span black n = 6 * n ∸ 3 + + mapreduce/cost/span' : val nat → val nat + mapreduce/cost/span' n = 6 * n + + mapreduce/cost/span≤mapreduce/cost/span' : (y : val color) → (n : val nat) → mapreduce/cost/span y n Nat.≤ mapreduce/cost/span' n + mapreduce/cost/span≤mapreduce/cost/span' red n = Nat.≤-refl + mapreduce/cost/span≤mapreduce/cost/span' black n = Nat.m∸n≤m (6 * n) 3 + + mapreduce/is-bounded : + (f : cmp (Π A λ _ → F B)) → + ({x : val A} → IsBounded B (f x) (1 , 1)) → + (g : cmp (Π B λ _ → Π B λ _ → F B)) → + ({x y : val B} → IsBounded B (g x y) (1 , 1)) → + (z : val B) → + (y : val color) → (n : val nat) → (l : val (list A)) → (t : val (irbt A y n l)) → + IsBounded B (mapreduce y n l t f g z) (mapreduce/cost/work y n , mapreduce/cost/span y n) + mapreduce/is-bounded f f-bound g g-bound z .black .zero .[] leaf = + step⋆-mono-≤⁻ {c' = 3 , 0} (Nat.z≤n , Nat.z≤n) + mapreduce/is-bounded f f-bound g g-bound z .red n l (red t₁ a t₂) = + let open ≤⁻-Reasoning cost in + begin + bind cost ( + bind (F B) + ((mapreduce _ _ _ t₁ f g z) ∥ (mapreduce _ _ _ t₂ f g z)) λ _ → + bind (F B) (f a) (λ _ → + bind (F B) (g _ _) (λ _ → + bind (F B) (g _ _) ret))) + (λ _ → ret triv) + ≡⟨⟩ + ( + bind cost + ((mapreduce _ _ _ t₁ f g z) ∥ (mapreduce _ _ _ t₂ f g z)) λ (s₁ , s₂) → + bind cost (f a) λ b → + bind cost (g b s₂) λ s₃ → + bind cost (g s₁ s₃) λ _ → + ret triv + ) + ≤⟨ ≤⁻-mono (λ e → + bind cost + ((mapreduce _ _ _ t₁ f g z) ∥ (mapreduce _ _ _ t₂ f g z)) λ (s₁ , s₂) → + bind cost (f a) λ b → + bind cost (g b s₂) λ s₃ → + bind cost e λ _ → + ret triv) {! g-bound !} ⟩ + ( + bind cost + ((mapreduce _ _ _ t₁ f g z) ∥ (mapreduce _ _ _ t₂ f g z)) λ (s₁ , s₂) → + bind cost (f a) λ b → + bind cost (g b s₂) λ s₃ → + step⋆ (1 , 1) + ) + ≤⟨ {! !} ⟩ + {! !} + ∎ + mapreduce/is-bounded f f-bound g g-bound z .black n@(suc n') l (black t₁ a t₂) = + let open ≤⁻-Reasoning cost in + begin + {! !} + ≤⟨ {! !} ⟩ + {! !} + ∎ + + mapreduce/is-bounded' : + (f : cmp (Π A λ _ → F B)) → + ({x : val A} → IsBounded B (f x) (1 , 1)) → + (g : cmp (Π B λ _ → Π B λ _ → F B)) → + ({x y : val B} → IsBounded B (g x y) (1 , 1)) → + (z : val B) → + (y : val color) → (n : val nat) → (l : val (list A)) → (t : val (irbt A y n l)) → + IsBounded B (mapreduce y n l t f g z) (mapreduce/cost/work' n , mapreduce/cost/span' n) + mapreduce/is-bounded' f f-bound g g-bound z y n l t = + let open ≤⁻-Reasoning cost in + begin + bind cost (mapreduce y n l t f g z) (λ _ → ret triv) + ≤⟨ mapreduce/is-bounded f f-bound g g-bound z y n l t ⟩ + step⋆ (mapreduce/cost/work y n , mapreduce/cost/span y n) + ≤⟨ step⋆-mono-≤⁻ (mapreduce/cost/work≤mapreduce/cost/work' y n , mapreduce/cost/span≤mapreduce/cost/span' y n) ⟩ + step⋆ (mapreduce/cost/work' n , mapreduce/cost/span' n) + ∎ From 810ead85fe9de94945b8df787848ad3a1d5dad1b Mon Sep 17 00:00:00 2001 From: Runming Li Date: Sun, 19 Nov 2023 20:59:58 -0500 Subject: [PATCH 4/7] sum --- src/Examples/Sequence/DerivedFormsRBT.agda | 179 +++++++++++++++++++-- 1 file changed, 167 insertions(+), 12 deletions(-) diff --git a/src/Examples/Sequence/DerivedFormsRBT.agda b/src/Examples/Sequence/DerivedFormsRBT.agda index ae8aa3b2..d1d70939 100644 --- a/src/Examples/Sequence/DerivedFormsRBT.agda +++ b/src/Examples/Sequence/DerivedFormsRBT.agda @@ -13,21 +13,16 @@ open import Calf.Parallel parCostMonoid open import Calf.Data.Nat open import Calf.Data.List open import Calf.Data.Product --- open import Calf.Data.Sum open import Calf.Data.IsBounded costMonoid open import Calf.Data.IsBoundedG costMonoid --- open import Data.Product hiding (map) --- open import Data.List as List hiding (sum; map) --- import Data.List.Properties as List -open import Data.Nat as Nat using (_+_; _*_; _<_; _>_; _≤ᵇ_; _<ᵇ_; ⌊_/2⌋; _≡ᵇ_; _∸_) +open import Data.List as List hiding (sum; map) +import Data.List.Properties as List +open import Data.Nat as Nat using (_+_; _*_) import Data.Nat.Properties as Nat --- open import Data.Nat.Logarithm +open import Data.Nat.Logarithm -open import Level using (0ℓ) open import Function using (_$_) -open import Relation.Nullary -open import Relation.Binary -open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≢_; module ≡-Reasoning; ≢-sym) +open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; module ≡-Reasoning) open import Examples.Sequence.RedBlackTree @@ -106,13 +101,13 @@ module MapReduce {A B : tp⁺} where bind cost (g s₁ s₃) λ _ → ret triv ) - ≤⟨ ≤⁻-mono (λ e → + ≤⟨ {! ≤⁻-mono (λ e → bind cost ((mapreduce _ _ _ t₁ f g z) ∥ (mapreduce _ _ _ t₂ f g z)) λ (s₁ , s₂) → bind cost (f a) λ b → bind cost (g b s₂) λ s₃ → bind cost e λ _ → - ret triv) {! g-bound !} ⟩ + ret triv) ? !} ⟩ ( bind cost ((mapreduce _ _ _ t₁ f g z) ∥ (mapreduce _ _ _ t₂ f g z)) λ (s₁ , s₂) → @@ -148,3 +143,163 @@ module MapReduce {A B : tp⁺} where ≤⟨ step⋆-mono-≤⁻ (mapreduce/cost/work≤mapreduce/cost/work' y n , mapreduce/cost/span≤mapreduce/cost/span' y n) ⟩ step⋆ (mapreduce/cost/work' n , mapreduce/cost/span' n) ∎ + + +module Sum where + sum/seq : cmp $ + Π color λ y → Π nat λ n → Π (list nat) λ l → Π (irbt nat y n l) λ _ → F nat + sum/seq .black .zero .[] leaf = ret 0 + sum/seq .red n l (red t₁ a t₂) = + step (F nat) (1 , 1) $ + bind (F (nat)) ((sum/seq _ _ _ t₁) ∥ (sum/seq _ _ _ t₂)) + (λ (s₁ , s₂) → ret (s₁ + a + s₂)) + sum/seq .black n l (black t₁ a t₂) = + step (F nat) (1 , 1) $ + bind (F (nat)) ((sum/seq _ _ _ t₁) ∥ (sum/seq _ _ _ t₂)) + (λ (s₁ , s₂) → ret (s₁ + a + s₂)) + + span/sum : val color → val nat → val nat + span/sum red n = 1 + 2 * n + span/sum black n = 2 * n + + span/bounded : ∀ y n → (span/sum y n) Nat.≤ (1 + 2 * n) + span/bounded red n = Nat.≤-refl + span/bounded black n = Nat.n≤1+n (2 * n) + + list/preserves/length : ∀ (l₁ : List ℕ) a (l₂ : List ℕ) → 1 + (length l₁ + length l₂) ≡ length (l₁ ++ a ∷ l₂) + list/preserves/length l₁ a l₂ = + let open ≡-Reasoning in + begin + 1 + (length l₁ + length l₂) + ≡˘⟨ Nat.+-assoc 1 (length l₁) (length l₂) ⟩ + 1 + length l₁ + length l₂ + ≡⟨ Eq.cong₂ _+_ (Nat.+-comm 1 (length l₁)) refl ⟩ + length l₁ + 1 + length l₂ + ≡⟨ Nat.+-assoc (length l₁) 1 (length l₂) ⟩ + length l₁ + (1 + length l₂) + ≡⟨⟩ + length l₁ + length (a ∷ l₂) + ≡˘⟨ List.length-++ l₁ ⟩ + length (l₁ ++ a ∷ l₂) + ∎ + + sum/bounded' : ∀ y n l t → IsBounded nat (sum/seq y n l t) (length l , span/sum y n) + sum/bounded' .black .zero .[] leaf = ≤⁻-refl + sum/bounded' .red n l (red {l₁ = l₁} {l₂ = l₂} t₁ a t₂) = + let open ≤⁻-Reasoning cost in + begin + step cost (1 , 1) ( + bind cost ( + bind (F (nat)) ((sum/seq _ _ _ t₁) ∥ (sum/seq _ _ _ t₂)) + (λ (s₁ , s₂) → ret (s₁ + a + s₂))) + (λ _ → ret triv)) + ≡⟨⟩ + step cost (1 , 1) ( + bind cost ((sum/seq _ _ _ t₁) ∥ (sum/seq _ _ _ t₂)) + (λ _ → ret triv)) + ≤⟨ {! !} ⟩ + step cost (1 , 1) ( + bind cost (bind cost (sum/seq _ _ _ t₁) (λ _ → ret triv) ∥ bind cost (sum/seq _ _ _ t₂) (λ _ → ret triv)) + (λ _ → ret triv)) + ≤⟨ ≤⁻-mono + (λ e → step cost (1 , 1) (bind cost e (λ _ → ret triv))) + (∥-mono-≤⁻ (sum/bounded' black n l₁ t₁) (sum/bounded' black n l₂ t₂)) ⟩ + step cost (1 , 1) ( + bind cost ((step⋆ (length l₁ , span/sum black n)) ∥ (step⋆ (length l₂ , span/sum black n))) + (λ _ → ret triv)) + ≡⟨ Eq.cong (λ e → step cost (1 , 1) e) + {x = bind cost + ((step⋆ (length l₁ , span/sum black n)) ∥ (step⋆ (length l₂ , span/sum black n))) + (λ _ → ret triv)} + refl ⟩ + step cost (1 , 1) ( + step⋆ ((length l₁ , span/sum black n) ⊗ (length l₂ , span/sum black n))) + ≡⟨ Eq.cong (λ c → step cost (1 , 1) (step⋆ c)) (Eq.cong₂ _,_ refl (Nat.⊔-idem (span/sum black n))) ⟩ + step cost (1 , 1) ( + step⋆ (length l₁ + length l₂ , span/sum black n)) + ≡⟨⟩ + step⋆ (1 + (length l₁ + length l₂) , 1 + 2 * n) + ≡⟨ Eq.cong₂ (λ c₁ c₂ → step⋆ (c₁ , c₂)) (list/preserves/length l₁ a l₂) refl ⟩ + step⋆ (length l , span/sum red n) + ∎ + sum/bounded' .black n@(suc n') l (black {y₁ = y₁} {y₂ = y₂} {l₁ = l₁} {l₂ = l₂} t₁ a t₂) = + let open ≤⁻-Reasoning cost in + begin + step cost (1 , 1) ( + bind cost ( + bind (F (nat)) ((sum/seq _ _ _ t₁) ∥ (sum/seq _ _ _ t₂)) + (λ (s₁ , s₂) → ret (s₁ + a + s₂))) + (λ _ → ret triv)) + ≡⟨⟩ + step cost (1 , 1) ( + bind cost ((sum/seq _ _ _ t₁) ∥ (sum/seq _ _ _ t₂)) + (λ _ → ret triv)) + ≤⟨ {! !} ⟩ + step cost (1 , 1) ( + bind cost (bind cost (sum/seq _ _ _ t₁) (λ _ → ret triv) ∥ bind cost (sum/seq _ _ _ t₂) (λ _ → ret triv)) + (λ _ → ret triv)) + ≤⟨ ≤⁻-mono + (λ e → step cost (1 , 1) (bind cost e (λ _ → ret triv))) + (∥-mono-≤⁻ (sum/bounded' y₁ n' l₁ t₁) (sum/bounded' y₂ n' l₂ t₂)) ⟩ + step cost (1 , 1) ( + bind cost ((step⋆ (length l₁ , span/sum y₁ n')) ∥ (step⋆ (length l₂ , span/sum y₂ n'))) + (λ _ → ret triv)) + ≤⟨ ≤⁻-mono₂ + (λ e₁ e₂ → step cost (1 , 1) (bind cost (e₁ ∥ e₂) (λ _ → ret triv))) + (step⋆-mono-≤⁻ (Nat.≤-refl {length l₁} , span/bounded y₁ n')) + (step⋆-mono-≤⁻ (Nat.≤-refl {length l₂} , span/bounded y₂ n')) ⟩ + step cost (1 , 1) ( + bind cost ((step⋆ (length l₁ , 1 + 2 * n')) ∥ (step⋆ (length l₂ , 1 + 2 * n'))) + (λ _ → ret triv)) + ≡⟨ Eq.cong (λ e → step cost (1 , 1) e) + {x = bind cost + ((step⋆ (length l₁ , 1 + 2 * n')) ∥ (step⋆ (length l₂ , 1 + 2 * n'))) + (λ _ → ret triv)} + refl ⟩ + step cost (1 , 1) ( + step⋆ ((length l₁ , 1 + 2 * n') ⊗ (length l₂ , 1 + 2 * n'))) + ≡⟨ Eq.cong (λ c → step cost (1 , 1) (step⋆ c)) (Eq.cong₂ _,_ refl (Nat.⊔-idem (1 + 2 * n'))) ⟩ + step cost (1 , 1) ( + step⋆ (length l₁ + length l₂ , 1 + 2 * n')) + ≡⟨⟩ + step⋆ (1 + (length l₁ + length l₂) , 1 + (1 + 2 * n')) + ≡⟨ Eq.cong₂ (λ c₁ c₂ → step⋆ (c₁ , c₂)) (list/preserves/length l₁ a l₂) (arithemtic n') ⟩ + step⋆ (length l , span/sum black n) + ∎ + where + arithemtic : ∀ n → 1 + (1 + 2 * n) ≡ 2 * (suc n) + arithemtic n = + let open ≡-Reasoning in + begin + 1 + (1 + 2 * n) + ≡⟨ Nat.+-assoc 1 1 (2 * n) ⟩ + (1 + 1) + 2 * n + ≡⟨⟩ + 2 + 2 * n + ≡˘⟨ Nat.*-suc 2 n ⟩ + 2 * (suc n) + ∎ + + sum/bounded : ∀ y n l t → IsBounded nat (sum/seq y n l t) (length l , 1 + 2 * ⌈log₂ (1 + length l) ⌉) + sum/bounded y n l t = + let open ≤⁻-Reasoning cost in + begin + bind cost (sum/seq y n l t) (λ _ → ret triv) + ≤⟨ sum/bounded' y n l t ⟩ + step⋆ (length l , span/sum y n) + ≤⟨ step⋆-mono-≤⁻ (Nat.≤-refl {length l} , lemma) ⟩ + step⋆ (length l , 1 + 2 * ⌈log₂ (1 + length l) ⌉) + ∎ + where + lemma : span/sum y n Nat.≤ 1 + (2 * ⌈log₂ (1 + length l) ⌉) + lemma = + let open Nat.≤-Reasoning in + begin + span/sum y n + ≤⟨ span/bounded y n ⟩ + 1 + (2 * n) + ≤⟨ Nat.s≤s (Nat.*-monoʳ-≤ 2 (i-nodes/bound/log-node-black-height t)) ⟩ + 1 + (2 * ⌈log₂ (1 + i-nodes t) ⌉) + ≡⟨ Eq.cong (λ x → 1 + (2 * ⌈log₂ (1 + x) ⌉)) (i-nodes≡lengthl t) ⟩ + 1 + (2 * ⌈log₂ (1 + length l) ⌉) + ∎ From 787ed54aec8d7613b8220adea9a10f1ef624a867 Mon Sep 17 00:00:00 2001 From: Harrison Grodin Date: Mon, 20 Nov 2023 11:41:14 -0500 Subject: [PATCH 5/7] Cleanup --- src/Examples/Sequence/DerivedFormsRBT.agda | 44 +++++++++++----------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/src/Examples/Sequence/DerivedFormsRBT.agda b/src/Examples/Sequence/DerivedFormsRBT.agda index d1d70939..e4c70f47 100644 --- a/src/Examples/Sequence/DerivedFormsRBT.agda +++ b/src/Examples/Sequence/DerivedFormsRBT.agda @@ -101,13 +101,18 @@ module MapReduce {A B : tp⁺} where bind cost (g s₁ s₃) λ _ → ret triv ) - ≤⟨ {! ≤⁻-mono (λ e → - bind cost - ((mapreduce _ _ _ t₁ f g z) ∥ (mapreduce _ _ _ t₂ f g z)) λ (s₁ , s₂) → - bind cost (f a) λ b → - bind cost (g b s₂) λ s₃ → - bind cost e λ _ → - ret triv) ? !} ⟩ + ≤⟨ ( + {! !} + -- ≤⁻-mono {Π _ λ _ → cost} {cost} (bind cost (mapreduce _ _ _ t₁ f g z ∥ mapreduce _ _ _ t₂ f g z)) + -- {λ (s₁ , s₂) → + -- bind cost (f a) λ b → + -- bind cost (g b s₂) λ s₃ → + -- funext + -- $ λ-mono-≤⁻ λ (s₁ , s₂) → + -- ≤⁻-mono (bind cost (f a)) $ λ-mono-≤⁻ λ b → + -- ≤⁻-mono (bind cost (g b s₂)) $ λ-mono-≤⁻ λ s₃ → + -- g-bound {s₁} {s₃} + ) ⟩ ( bind cost ((mapreduce _ _ _ t₁ f g z) ∥ (mapreduce _ _ _ t₂ f g z)) λ (s₁ , s₂) → @@ -197,21 +202,16 @@ module Sum where step cost (1 , 1) ( bind cost ((sum/seq _ _ _ t₁) ∥ (sum/seq _ _ _ t₂)) (λ _ → ret triv)) - ≤⟨ {! !} ⟩ - step cost (1 , 1) ( - bind cost (bind cost (sum/seq _ _ _ t₁) (λ _ → ret triv) ∥ bind cost (sum/seq _ _ _ t₂) (λ _ → ret triv)) - (λ _ → ret triv)) - ≤⟨ ≤⁻-mono - (λ e → step cost (1 , 1) (bind cost e (λ _ → ret triv))) - (∥-mono-≤⁻ (sum/bounded' black n l₁ t₁) (sum/bounded' black n l₂ t₂)) ⟩ - step cost (1 , 1) ( - bind cost ((step⋆ (length l₁ , span/sum black n)) ∥ (step⋆ (length l₂ , span/sum black n))) - (λ _ → ret triv)) - ≡⟨ Eq.cong (λ e → step cost (1 , 1) e) - {x = bind cost - ((step⋆ (length l₁ , span/sum black n)) ∥ (step⋆ (length l₂ , span/sum black n))) - (λ _ → ret triv)} - refl ⟩ + ≤⟨ + ≤⁻-mono + (step cost (1 , 1)) + (bound/par + {e₁ = sum/seq _ _ _ t₁} + {e₂ = sum/seq _ _ _ t₂} + {c₁ = (length l₁ , span/sum black n)} + (sum/bounded' black n l₁ t₁) + (sum/bounded' black n l₂ t₂)) + ⟩ step cost (1 , 1) ( step⋆ ((length l₁ , span/sum black n) ⊗ (length l₂ , span/sum black n))) ≡⟨ Eq.cong (λ c → step cost (1 , 1) (step⋆ c)) (Eq.cong₂ _,_ refl (Nat.⊔-idem (span/sum black n))) ⟩ From 78bdb84dbb286ba0d257b4a977e09162bc23d4ed Mon Sep 17 00:00:00 2001 From: Runming Li Date: Tue, 21 Nov 2023 00:30:40 -0500 Subject: [PATCH 6/7] sum --- src/Examples/Sequence/DerivedFormsRBT.agda | 95 +++++++++------------- 1 file changed, 37 insertions(+), 58 deletions(-) diff --git a/src/Examples/Sequence/DerivedFormsRBT.agda b/src/Examples/Sequence/DerivedFormsRBT.agda index e4c70f47..d7e62431 100644 --- a/src/Examples/Sequence/DerivedFormsRBT.agda +++ b/src/Examples/Sequence/DerivedFormsRBT.agda @@ -28,49 +28,39 @@ open import Examples.Sequence.RedBlackTree module MapReduce {A B : tp⁺} where - mapreduce : cmp $ + mapreduce/seq : cmp $ Π color λ y → Π nat λ n → Π (list A) λ l → Π (irbt A y n l) λ _ → Π (U (Π A λ _ → F B)) λ _ → Π (U (Π B λ _ → Π B λ _ → F B)) λ _ → Π B λ _ → F B - mapreduce .black .zero .[] leaf f g z = ret z - mapreduce .red n l (red t₁ a t₂) f g z = + mapreduce/seq .black .zero .[] leaf f g z = ret z + mapreduce/seq .red n l (red t₁ a t₂) f g z = bind (F B) - ((mapreduce _ _ _ t₁ f g z) ∥ (mapreduce _ _ _ t₂ f g z)) λ s → + ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ s → bind (F B) (f a) (λ b → bind (F B) (g b (proj₂ s)) (λ s₃ → bind (F B) (g (proj₁ s) s₃) ret)) - mapreduce .black n@(suc n') l (black t₁ a t₂) f g z = + mapreduce/seq .black n@(suc n') l (black t₁ a t₂) f g z = bind (F B) - ((mapreduce _ _ _ t₁ f g z) ∥ (mapreduce _ _ _ t₂ f g z)) λ s → + ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ s → bind (F B) (f a) (λ b → bind (F B) (g b (proj₂ s)) (λ s₃ → bind (F B) (g (proj₁ s) s₃) ret)) - mapreduce/cost/work : val color → val nat → val nat - mapreduce/cost/work red n = 12 * (4 ^ (n ∸ 1)) ∸ 3 - mapreduce/cost/work black n = 6 * (4 ^ (n ∸ 1)) ∸ 3 + mapreduce/work : val (list A) → val nat + mapreduce/work l = 3 * length l - mapreduce/cost/work' : val nat → val nat - mapreduce/cost/work' n = 12 * (4 ^ (n ∸ 1)) ∸ 3 + mapreduce/span : val color → val nat → val nat + mapreduce/span red n = 6 * n + mapreduce/span black n = 6 * n ∸ 3 - mapreduce/cost/work≤mapreduce/cost/work' : (y : val color) → (n : val nat) → mapreduce/cost/work y n Nat.≤ mapreduce/cost/work' n - mapreduce/cost/work≤mapreduce/cost/work' red n = Nat.≤-refl - mapreduce/cost/work≤mapreduce/cost/work' black n = - Nat.∸-monoˡ-≤ {n = 12 * (4 ^ (n ∸ 1))} 3 - (Nat.*-monoˡ-≤ (4 ^ (n ∸ 1)) {y = 12} (Nat.s≤s (Nat.s≤s (Nat.s≤s (Nat.s≤s (Nat.s≤s (Nat.s≤s Nat.z≤n))))))) + mapreduce/span' : val nat → val nat + mapreduce/span' n = 6 * n - mapreduce/cost/span : val color → val nat → val nat - mapreduce/cost/span red n = 6 * n - mapreduce/cost/span black n = 6 * n ∸ 3 - - mapreduce/cost/span' : val nat → val nat - mapreduce/cost/span' n = 6 * n - - mapreduce/cost/span≤mapreduce/cost/span' : (y : val color) → (n : val nat) → mapreduce/cost/span y n Nat.≤ mapreduce/cost/span' n - mapreduce/cost/span≤mapreduce/cost/span' red n = Nat.≤-refl - mapreduce/cost/span≤mapreduce/cost/span' black n = Nat.m∸n≤m (6 * n) 3 + span/bounded : (y : val color) → (n : val nat) → mapreduce/span y n Nat.≤ mapreduce/span' n + span/bounded red n = Nat.≤-refl + span/bounded black n = Nat.m∸n≤m (6 * n) 3 mapreduce/is-bounded : (f : cmp (Π A λ _ → F B)) → @@ -79,15 +69,14 @@ module MapReduce {A B : tp⁺} where ({x y : val B} → IsBounded B (g x y) (1 , 1)) → (z : val B) → (y : val color) → (n : val nat) → (l : val (list A)) → (t : val (irbt A y n l)) → - IsBounded B (mapreduce y n l t f g z) (mapreduce/cost/work y n , mapreduce/cost/span y n) - mapreduce/is-bounded f f-bound g g-bound z .black .zero .[] leaf = - step⋆-mono-≤⁻ {c' = 3 , 0} (Nat.z≤n , Nat.z≤n) + IsBounded B (mapreduce/seq y n l t f g z) (mapreduce/work l , mapreduce/span y n) + mapreduce/is-bounded f f-bound g g-bound z .black .zero .[] leaf = ≤⁻-refl mapreduce/is-bounded f f-bound g g-bound z .red n l (red t₁ a t₂) = let open ≤⁻-Reasoning cost in begin bind cost ( bind (F B) - ((mapreduce _ _ _ t₁ f g z) ∥ (mapreduce _ _ _ t₂ f g z)) λ _ → + ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ _ → bind (F B) (f a) (λ _ → bind (F B) (g _ _) (λ _ → bind (F B) (g _ _) ret))) @@ -95,7 +84,7 @@ module MapReduce {A B : tp⁺} where ≡⟨⟩ ( bind cost - ((mapreduce _ _ _ t₁ f g z) ∥ (mapreduce _ _ _ t₂ f g z)) λ (s₁ , s₂) → + ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ (s₁ , s₂) → bind cost (f a) λ b → bind cost (g b s₂) λ s₃ → bind cost (g s₁ s₃) λ _ → @@ -115,7 +104,7 @@ module MapReduce {A B : tp⁺} where ) ⟩ ( bind cost - ((mapreduce _ _ _ t₁ f g z) ∥ (mapreduce _ _ _ t₂ f g z)) λ (s₁ , s₂) → + ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ (s₁ , s₂) → bind cost (f a) λ b → bind cost (g b s₂) λ s₃ → step⋆ (1 , 1) @@ -138,15 +127,15 @@ module MapReduce {A B : tp⁺} where ({x y : val B} → IsBounded B (g x y) (1 , 1)) → (z : val B) → (y : val color) → (n : val nat) → (l : val (list A)) → (t : val (irbt A y n l)) → - IsBounded B (mapreduce y n l t f g z) (mapreduce/cost/work' n , mapreduce/cost/span' n) + IsBounded B (mapreduce/seq y n l t f g z) (mapreduce/work l , mapreduce/span' n) mapreduce/is-bounded' f f-bound g g-bound z y n l t = let open ≤⁻-Reasoning cost in begin - bind cost (mapreduce y n l t f g z) (λ _ → ret triv) + bind cost (mapreduce/seq y n l t f g z) (λ _ → ret triv) ≤⟨ mapreduce/is-bounded f f-bound g g-bound z y n l t ⟩ - step⋆ (mapreduce/cost/work y n , mapreduce/cost/span y n) - ≤⟨ step⋆-mono-≤⁻ (mapreduce/cost/work≤mapreduce/cost/work' y n , mapreduce/cost/span≤mapreduce/cost/span' y n) ⟩ - step⋆ (mapreduce/cost/work' n , mapreduce/cost/span' n) + step⋆ (mapreduce/work l , mapreduce/span y n) + ≤⟨ step⋆-mono-≤⁻ (Nat.≤-refl {mapreduce/work l}, span/bounded y n) ⟩ + step⋆ (mapreduce/work l , mapreduce/span' n) ∎ @@ -207,7 +196,6 @@ module Sum where (step cost (1 , 1)) (bound/par {e₁ = sum/seq _ _ _ t₁} - {e₂ = sum/seq _ _ _ t₂} {c₁ = (length l₁ , span/sum black n)} (sum/bounded' black n l₁ t₁) (sum/bounded' black n l₂ t₂)) @@ -234,28 +222,19 @@ module Sum where step cost (1 , 1) ( bind cost ((sum/seq _ _ _ t₁) ∥ (sum/seq _ _ _ t₂)) (λ _ → ret triv)) - ≤⟨ {! !} ⟩ - step cost (1 , 1) ( - bind cost (bind cost (sum/seq _ _ _ t₁) (λ _ → ret triv) ∥ bind cost (sum/seq _ _ _ t₂) (λ _ → ret triv)) - (λ _ → ret triv)) ≤⟨ ≤⁻-mono - (λ e → step cost (1 , 1) (bind cost e (λ _ → ret triv))) - (∥-mono-≤⁻ (sum/bounded' y₁ n' l₁ t₁) (sum/bounded' y₂ n' l₂ t₂)) ⟩ - step cost (1 , 1) ( - bind cost ((step⋆ (length l₁ , span/sum y₁ n')) ∥ (step⋆ (length l₂ , span/sum y₂ n'))) - (λ _ → ret triv)) - ≤⟨ ≤⁻-mono₂ - (λ e₁ e₂ → step cost (1 , 1) (bind cost (e₁ ∥ e₂) (λ _ → ret triv))) - (step⋆-mono-≤⁻ (Nat.≤-refl {length l₁} , span/bounded y₁ n')) - (step⋆-mono-≤⁻ (Nat.≤-refl {length l₂} , span/bounded y₂ n')) ⟩ + (step cost (1 , 1)) + (bound/par + {e₁ = sum/seq _ _ _ t₁} + {c₁ = (length l₁ , span/sum y₁ n')} + (sum/bounded' y₁ n' l₁ t₁) + (sum/bounded' y₂ n' l₂ t₂)) ⟩ step cost (1 , 1) ( - bind cost ((step⋆ (length l₁ , 1 + 2 * n')) ∥ (step⋆ (length l₂ , 1 + 2 * n'))) - (λ _ → ret triv)) - ≡⟨ Eq.cong (λ e → step cost (1 , 1) e) - {x = bind cost - ((step⋆ (length l₁ , 1 + 2 * n')) ∥ (step⋆ (length l₂ , 1 + 2 * n'))) - (λ _ → ret triv)} - refl ⟩ + step⋆ ((length l₁ , span/sum y₁ n') ⊗ (length l₂ , span/sum y₂ n'))) + ≤⟨ ≤⁻-mono + (λ e → step cost (1 , 1) e) + (step⋆-mono-≤⁻ + (Nat.≤-refl , Nat.⊔-mono-≤ (span/bounded y₁ n') (span/bounded y₂ n'))) ⟩ step cost (1 , 1) ( step⋆ ((length l₁ , 1 + 2 * n') ⊗ (length l₂ , 1 + 2 * n'))) ≡⟨ Eq.cong (λ c → step cost (1 , 1) (step⋆ c)) (Eq.cong₂ _,_ refl (Nat.⊔-idem (1 + 2 * n'))) ⟩ From f43b08641ed401043105478c7b1f24d67039eab4 Mon Sep 17 00:00:00 2001 From: Runming Li Date: Sat, 25 Nov 2023 23:35:39 -0500 Subject: [PATCH 7/7] mapreduce --- src/Examples/Sequence/DerivedFormsRBT.agda | 355 +++++++++++++++++---- 1 file changed, 293 insertions(+), 62 deletions(-) diff --git a/src/Examples/Sequence/DerivedFormsRBT.agda b/src/Examples/Sequence/DerivedFormsRBT.agda index d7e62431..ff1197a2 100644 --- a/src/Examples/Sequence/DerivedFormsRBT.agda +++ b/src/Examples/Sequence/DerivedFormsRBT.agda @@ -26,6 +26,35 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; modu open import Examples.Sequence.RedBlackTree +module _ {A : Set} where + list/preserves/length : ∀ (l₁ : List A) a (l₂ : List A) → 1 + (length l₁ + length l₂) ≡ length (l₁ ++ a ∷ l₂) + list/preserves/length l₁ a l₂ = + let open ≡-Reasoning in + begin + 1 + (length l₁ + length l₂) + ≡˘⟨ Nat.+-assoc 1 (length l₁) (length l₂) ⟩ + 1 + length l₁ + length l₂ + ≡⟨ Eq.cong₂ _+_ (Nat.+-comm 1 (length l₁)) refl ⟩ + length l₁ + 1 + length l₂ + ≡⟨ Nat.+-assoc (length l₁) 1 (length l₂) ⟩ + length l₁ + (1 + length l₂) + ≡⟨⟩ + length l₁ + length (a ∷ l₂) + ≡˘⟨ List.length-++ l₁ ⟩ + length (l₁ ++ a ∷ l₂) + ∎ + + list/preserves/length' : ∀ (l₁ : List A) a (l₂ : List A) → (length l₁ + length l₂) + 1 ≡ length (l₁ ++ a ∷ l₂) + list/preserves/length' l₁ a l₂ = + let open ≡-Reasoning in + begin + (length l₁ + length l₂) + 1 + ≡⟨ Nat.+-comm (length l₁ + length l₂) 1 ⟩ + 1 + (length l₁ + length l₂) + ≡⟨ list/preserves/length l₁ a l₂ ⟩ + length (l₁ ++ a ∷ l₂) + ∎ + module MapReduce {A B : tp⁺} where mapreduce/seq : cmp $ @@ -48,30 +77,36 @@ module MapReduce {A B : tp⁺} where bind (F B) (g b (proj₂ s)) (λ s₃ → bind (F B) (g (proj₁ s) s₃) ret)) - mapreduce/work : val (list A) → val nat - mapreduce/work l = 3 * length l + mapreduce/work : val nat → val nat → val (list A) → val nat + mapreduce/work c₁ c₂ l = (c₁ + 2 * c₂) * length l - mapreduce/span : val color → val nat → val nat - mapreduce/span red n = 6 * n - mapreduce/span black n = 6 * n ∸ 3 + mapreduce/span : val nat → val nat → val color → val nat → val nat + mapreduce/span c₁ c₂ red n = (2 * c₁ + 4 * c₂) * n + (c₁ + 2 * c₂) + mapreduce/span c₁ c₂ black n = (2 * c₁ + 4 * c₂) * n - mapreduce/span' : val nat → val nat - mapreduce/span' n = 6 * n + mapreduce/span' : val nat → val nat → val nat → val nat + mapreduce/span' c₁ c₂ n = (2 * c₁ + 4 * c₂) * n + (c₁ + 2 * c₂) - span/bounded : (y : val color) → (n : val nat) → mapreduce/span y n Nat.≤ mapreduce/span' n - span/bounded red n = Nat.≤-refl - span/bounded black n = Nat.m∸n≤m (6 * n) 3 + span/bounded : (c₁ c₂ : val nat) → (y : val color) → (n : val nat) → mapreduce/span c₁ c₂ y n Nat.≤ mapreduce/span' c₁ c₂ n + span/bounded c₁ c₂ red n = Nat.≤-refl + span/bounded c₁ c₂ black n = Nat.m≤m+n ((2 * c₁ + 4 * c₂) * n) (c₁ + 2 * c₂) - mapreduce/is-bounded : + mapreduce/is-bounded' : + {c₁ c₁' c₂ c₂' : val nat} → (f : cmp (Π A λ _ → F B)) → - ({x : val A} → IsBounded B (f x) (1 , 1)) → + ({x : val A} → IsBounded B (f x) (c₁ , c₁')) → (g : cmp (Π B λ _ → Π B λ _ → F B)) → - ({x y : val B} → IsBounded B (g x y) (1 , 1)) → + ({x y : val B} → IsBounded B (g x y) (c₂ , c₂')) → (z : val B) → (y : val color) → (n : val nat) → (l : val (list A)) → (t : val (irbt A y n l)) → - IsBounded B (mapreduce/seq y n l t f g z) (mapreduce/work l , mapreduce/span y n) - mapreduce/is-bounded f f-bound g g-bound z .black .zero .[] leaf = ≤⁻-refl - mapreduce/is-bounded f f-bound g g-bound z .red n l (red t₁ a t₂) = + IsBounded B (mapreduce/seq y n l t f g z) (mapreduce/work c₁ c₂ l , mapreduce/span c₁' c₂' y n) + mapreduce/is-bounded' {c₁} {c₁'} {c₂} {c₂'} f f-bound g g-bound z .black .zero .[] leaf = + Eq.subst₂ + (λ c c' → IsBounded B (mapreduce/seq black 0 [] leaf f g z) (c , c')) + (Eq.sym (Nat.*-zeroʳ (c₁ + 2 * c₂))) + (Eq.sym (Nat.*-zeroʳ (2 * c₁' + 4 * c₂'))) + ≤⁻-refl + mapreduce/is-bounded' {c₁} {c₁'} {c₂} {c₂'} f f-bound g g-bound z .red n l (red {l₁ = l₁} {l₂ = l₂} t₁ a t₂) = let open ≤⁻-Reasoning cost in begin bind cost ( @@ -90,53 +125,266 @@ module MapReduce {A B : tp⁺} where bind cost (g s₁ s₃) λ _ → ret triv ) - ≤⟨ ( - {! !} - -- ≤⁻-mono {Π _ λ _ → cost} {cost} (bind cost (mapreduce _ _ _ t₁ f g z ∥ mapreduce _ _ _ t₂ f g z)) - -- {λ (s₁ , s₂) → - -- bind cost (f a) λ b → - -- bind cost (g b s₂) λ s₃ → - -- funext - -- $ λ-mono-≤⁻ λ (s₁ , s₂) → - -- ≤⁻-mono (bind cost (f a)) $ λ-mono-≤⁻ λ b → - -- ≤⁻-mono (bind cost (g b s₂)) $ λ-mono-≤⁻ λ s₃ → - -- g-bound {s₁} {s₃} - ) ⟩ + ≤⟨ bind-monoʳ-≤⁻ ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) (λ (s₁ , s₂) → + bind-monoʳ-≤⁻ (f a) (λ b → + bind-monoʳ-≤⁻ (g b s₂) (λ s₃ → g-bound))) ⟩ ( bind cost ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ (s₁ , s₂) → bind cost (f a) λ b → - bind cost (g b s₂) λ s₃ → - step⋆ (1 , 1) + bind cost (g b s₂) λ _ → + step⋆ (c₂ , c₂') ) - ≤⟨ {! !} ⟩ - {! !} + ≤⟨ bind-monoʳ-≤⁻ ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) (λ (s₁ , s₂) → + bind-monoʳ-≤⁻ (f a) (λ b → + bind-monoˡ-≤⁻ (λ _ → step⋆ (c₂ , c₂')) g-bound)) ⟩ + ( + bind cost + ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ (s₁ , s₂) → + bind cost (f a) λ b → + bind cost (step⋆ (c₂ , c₂')) λ _ → + step⋆ (c₂ , c₂') + ) + ≤⟨ bind-monoʳ-≤⁻ ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) (λ (s₁ , s₂) → + bind-monoˡ-≤⁻ (λ _ → bind cost (step⋆ (c₂ , c₂')) λ _ → step⋆ (c₂ , c₂')) f-bound) ⟩ + ( + bind cost + ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ (s₁ , s₂) → + bind cost (step⋆ (c₁ , c₁')) λ _ → + bind cost (step⋆ (c₂ , c₂')) λ _ → + step⋆ (c₂ , c₂') + ) + ≤⟨ bind-monoˡ-≤⁻ (λ _ → bind cost (step⋆ (c₁ , c₁')) λ _ → bind cost (step⋆ (c₂ , c₂')) λ _ → step⋆ (c₂ , c₂')) + (bound/par + {e₁ = mapreduce/seq _ _ _ t₁ f g z} + {c₁ = mapreduce/work c₁ c₂ l₁ , mapreduce/span c₁' c₂' black n} + (mapreduce/is-bounded' {c₁} {c₁'} {c₂} {c₂'} f f-bound g g-bound z black n l₁ t₁) + (mapreduce/is-bounded' {c₁} {c₁'} {c₂} {c₂'} f f-bound g g-bound z black n l₂ t₂)) ⟩ + ( + bind cost (step⋆ ((mapreduce/work c₁ c₂ l₁ , mapreduce/span c₁' c₂' black n) ⊗ (mapreduce/work c₁ c₂ l₂ , mapreduce/span c₁' c₂' black n))) λ _ → + bind cost (step⋆ (c₁ , c₁')) λ _ → + bind cost (step⋆ (c₂ , c₂')) λ _ → + step⋆ (c₂ , c₂') + ) + ≡⟨ Eq.cong + (λ c → bind cost (step⋆ c) (λ _ → + bind cost (step⋆ (c₁ , c₁')) λ _ → + bind cost (step⋆ (c₂ , c₂')) λ _ → + step⋆ (c₂ , c₂'))) + {x = (mapreduce/work c₁ c₂ l₁ , mapreduce/span c₁' c₂' black n) ⊗ (mapreduce/work c₁ c₂ l₂ , mapreduce/span c₁' c₂' black n)} + (Eq.cong₂ _,_ refl (Nat.⊔-idem (mapreduce/span c₁' c₂' black n))) ⟩ + ( + bind cost (step⋆ (((c₁ + 2 * c₂) * length l₁) + ((c₁ + 2 * c₂) * length l₂) , (2 * c₁' + 4 * c₂') * n)) λ _ → + bind cost (step⋆ (c₁ , c₁')) λ _ → + bind cost (step⋆ (c₂ , c₂')) λ _ → + step⋆ (c₂ , c₂') + ) + ≡⟨⟩ + step⋆ ((((c₁ + 2 * c₂) * length l₁) + ((c₁ + 2 * c₂) * length l₂)) + (c₁ + (c₂ + c₂)) , + ((2 * c₁' + 4 * c₂') * n) + (c₁' + (c₂' + c₂'))) + ≡⟨ Eq.cong₂ (λ c c' → step⋆ (c , c')) arithemtic₁ arithemtic₂ ⟩ + step⋆ (mapreduce/work c₁ c₂ l , mapreduce/span c₁' c₂' red n) ∎ - mapreduce/is-bounded f f-bound g g-bound z .black n@(suc n') l (black t₁ a t₂) = + where + arithemtic₁ : (((c₁ + 2 * c₂) * length l₁) + ((c₁ + 2 * c₂) * length l₂)) + (c₁ + (c₂ + c₂)) ≡ (c₁ + 2 * c₂) * length l + arithemtic₁ = + let open ≡-Reasoning in + begin + (((c₁ + 2 * c₂) * length l₁) + ((c₁ + 2 * c₂) * length l₂)) + (c₁ + (c₂ + c₂)) + ≡˘⟨ Eq.cong₂ _+_ + (Nat.*-distribˡ-+ (c₁ + 2 * c₂) (length l₁) (length l₂)) + (Eq.cong₂ _+_ {x = c₁} refl (Eq.trans (Nat.*-distribʳ-+ c₂ 1 1) (Eq.cong₂ _+_ (Nat.*-identityˡ c₂) (Nat.*-identityˡ c₂)))) ⟩ + ((c₁ + 2 * c₂) * (length l₁ + length l₂)) + (c₁ + 2 * c₂) + ≡˘⟨ Eq.cong₂ _+_ refl (Nat.*-identityʳ (c₁ + 2 * c₂)) ⟩ + ((c₁ + 2 * c₂) * (length l₁ + length l₂)) + (c₁ + 2 * c₂) * 1 + ≡˘⟨ Nat.*-distribˡ-+ (c₁ + 2 * c₂) (length l₁ + length l₂) 1 ⟩ + (c₁ + 2 * c₂) * (length l₁ + length l₂ + 1) + ≡⟨ Eq.cong₂ _*_ {x = c₁ + 2 * c₂} refl (list/preserves/length' l₁ a l₂) ⟩ + (c₁ + 2 * c₂) * length l + ∎ + + arithemtic₂ : (2 * c₁' + 4 * c₂') * n + (c₁' + (c₂' + c₂')) ≡ (2 * c₁' + 4 * c₂') * n + (c₁' + 2 * c₂') + arithemtic₂ = + let open ≡-Reasoning in + begin + (2 * c₁' + 4 * c₂') * n + (c₁' + (c₂' + c₂')) + ≡˘⟨ Eq.cong₂ _+_ + {x = (2 * c₁' + 4 * c₂') * n} + refl + (Eq.cong₂ _+_ {x = c₁'} refl (Eq.trans (Nat.*-distribʳ-+ c₂' 1 1) (Eq.cong₂ _+_ (Nat.*-identityˡ c₂') (Nat.*-identityˡ c₂')))) ⟩ + (2 * c₁' + 4 * c₂') * n + (c₁' + 2 * c₂') + ∎ + mapreduce/is-bounded' {c₁} {c₁'} {c₂} {c₂'} f f-bound g g-bound z .black n@(suc n') l (black {y₁ = y₁} {y₂ = y₂} {l₁ = l₁} {l₂ = l₂} t₁ a t₂) = let open ≤⁻-Reasoning cost in begin - {! !} - ≤⟨ {! !} ⟩ - {! !} + bind cost ( + bind (F B) + ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ _ → + bind (F B) (f a) (λ _ → + bind (F B) (g _ _) (λ _ → + bind (F B) (g _ _) ret))) + (λ _ → ret triv) + ≡⟨⟩ + ( + bind cost + ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ (s₁ , s₂) → + bind cost (f a) λ b → + bind cost (g b s₂) λ s₃ → + bind cost (g s₁ s₃) λ _ → + ret triv + ) + ≤⟨ bind-monoʳ-≤⁻ ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) (λ (s₁ , s₂) → + bind-monoʳ-≤⁻ (f a) (λ b → + bind-monoʳ-≤⁻ (g b s₂) (λ s₃ → g-bound))) ⟩ + ( + bind cost + ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ (s₁ , s₂) → + bind cost (f a) λ b → + bind cost (g b s₂) λ _ → + step⋆ (c₂ , c₂') + ) + ≤⟨ bind-monoʳ-≤⁻ ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) (λ (s₁ , s₂) → + bind-monoʳ-≤⁻ (f a) (λ b → + bind-monoˡ-≤⁻ (λ _ → step⋆ (c₂ , c₂')) g-bound)) ⟩ + ( + bind cost + ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ (s₁ , s₂) → + bind cost (f a) λ b → + bind cost (step⋆ (c₂ , c₂')) λ _ → + step⋆ (c₂ , c₂') + ) + ≤⟨ bind-monoʳ-≤⁻ ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) (λ (s₁ , s₂) → + bind-monoˡ-≤⁻ (λ _ → bind cost (step⋆ (c₂ , c₂')) λ _ → step⋆ (c₂ , c₂')) f-bound) ⟩ + ( + bind cost + ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ (s₁ , s₂) → + bind cost (step⋆ (c₁ , c₁')) λ _ → + bind cost (step⋆ (c₂ , c₂')) λ _ → + step⋆ (c₂ , c₂') + ) + ≤⟨ bind-monoˡ-≤⁻ (λ _ → bind cost (step⋆ (c₁ , c₁')) λ _ → bind cost (step⋆ (c₂ , c₂')) λ _ → step⋆ (c₂ , c₂')) + (bound/par + {e₁ = mapreduce/seq _ _ _ t₁ f g z} + {c₁ = mapreduce/work c₁ c₂ l₁ , mapreduce/span c₁' c₂' y₁ n'} + (mapreduce/is-bounded' {c₁} {c₁'} {c₂} {c₂'} f f-bound g g-bound z y₁ n' l₁ t₁) + (mapreduce/is-bounded' {c₁} {c₁'} {c₂} {c₂'} f f-bound g g-bound z y₂ n' l₂ t₂)) ⟩ + ( + bind cost (step⋆ ((mapreduce/work c₁ c₂ l₁ , mapreduce/span c₁' c₂' y₁ n') ⊗ (mapreduce/work c₁ c₂ l₂ , mapreduce/span c₁' c₂' y₂ n'))) λ _ → + bind cost (step⋆ (c₁ , c₁')) λ _ → + bind cost (step⋆ (c₂ , c₂')) λ _ → + step⋆ (c₂ , c₂') + ) + ≤⟨ bind-monoˡ-≤⁻ + (λ _ → + bind cost (step⋆ (c₁ , c₁')) λ _ → + bind cost (step⋆ (c₂ , c₂')) λ _ → + step⋆ (c₂ , c₂')) + (step⋆-mono-≤⁻ {c = mapreduce/work c₁ c₂ l₁ + mapreduce/work c₁ c₂ l₂ , mapreduce/span c₁' c₂' y₁ n' Nat.⊔ mapreduce/span c₁' c₂' y₂ n'} + (Nat.≤-refl , Nat.⊔-mono-≤ (span/bounded c₁' c₂' y₁ n') (span/bounded c₁' c₂' y₂ n'))) ⟩ + ( + bind cost (step⋆ ((mapreduce/work c₁ c₂ l₁ , mapreduce/span' c₁' c₂' n') ⊗ (mapreduce/work c₁ c₂ l₂ , mapreduce/span' c₁' c₂' n'))) λ _ → + bind cost (step⋆ (c₁ , c₁')) λ _ → + bind cost (step⋆ (c₂ , c₂')) λ _ → + step⋆ (c₂ , c₂') + ) + ≡⟨ Eq.cong + (λ c → bind cost (step⋆ c) λ _ → + bind cost (step⋆ (c₁ , c₁')) λ _ → + bind cost (step⋆ (c₂ , c₂')) λ _ → + step⋆ (c₂ , c₂')) + {x = mapreduce/work c₁ c₂ l₁ + mapreduce/work c₁ c₂ l₂ , mapreduce/span' c₁' c₂' n' Nat.⊔ mapreduce/span' c₁' c₂' n'} + (Eq.cong₂ _,_ refl (Nat.⊔-idem ((2 * c₁' + 4 * c₂') * n' + (c₁' + 2 * c₂')))) ⟩ + ( + bind cost (step⋆ (((c₁ + 2 * c₂) * length l₁) + ((c₁ + 2 * c₂) * length l₂) , (2 * c₁' + 4 * c₂') * n' + (c₁' + 2 * c₂'))) λ _ → + bind cost (step⋆ (c₁ , c₁')) λ _ → + bind cost (step⋆ (c₂ , c₂')) λ _ → + step⋆ (c₂ , c₂') + ) + ≡⟨⟩ + step⋆ (((c₁ + 2 * c₂) * length l₁) + ((c₁ + 2 * c₂) * length l₂) + (c₁ + (c₂ + c₂)) , + ((2 * c₁' + 4 * c₂') * n' + (c₁' + 2 * c₂')) + (c₁' + (c₂' + c₂')) ) + ≡⟨ Eq.cong₂ (λ c c' → step⋆ (c , c')) arithemtic₁ arithemtic₂ ⟩ + step⋆ (mapreduce/work c₁ c₂ l , mapreduce/span c₁' c₂' black n) ∎ + where + arithemtic₁ : ((c₁ + 2 * c₂) * length l₁) + ((c₁ + 2 * c₂) * length l₂) + (c₁ + (c₂ + c₂)) ≡ (c₁ + 2 * c₂) * length l + arithemtic₁ = + let open ≡-Reasoning in + begin + (((c₁ + 2 * c₂) * length l₁) + ((c₁ + 2 * c₂) * length l₂)) + (c₁ + (c₂ + c₂)) + ≡˘⟨ Eq.cong₂ _+_ + (Nat.*-distribˡ-+ (c₁ + 2 * c₂) (length l₁) (length l₂)) + (Eq.cong₂ _+_ {x = c₁} refl (Eq.trans (Nat.*-distribʳ-+ c₂ 1 1) (Eq.cong₂ _+_ (Nat.*-identityˡ c₂) (Nat.*-identityˡ c₂)))) ⟩ + ((c₁ + 2 * c₂) * (length l₁ + length l₂)) + (c₁ + 2 * c₂) + ≡˘⟨ Eq.cong₂ _+_ refl (Nat.*-identityʳ (c₁ + 2 * c₂)) ⟩ + ((c₁ + 2 * c₂) * (length l₁ + length l₂)) + (c₁ + 2 * c₂) * 1 + ≡˘⟨ Nat.*-distribˡ-+ (c₁ + 2 * c₂) (length l₁ + length l₂) 1 ⟩ + (c₁ + 2 * c₂) * (length l₁ + length l₂ + 1) + ≡⟨ Eq.cong₂ _*_ {x = c₁ + 2 * c₂} refl (list/preserves/length' l₁ a l₂) ⟩ + (c₁ + 2 * c₂) * length l + ∎ - mapreduce/is-bounded' : + arithemtic₂ : ((2 * c₁' + 4 * c₂') * n' + (c₁' + 2 * c₂')) + (c₁' + (c₂' + c₂')) ≡ (2 * c₁' + 4 * c₂') * n + arithemtic₂ = + let open ≡-Reasoning in + begin + ((2 * c₁' + 4 * c₂') * n' + (c₁' + 2 * c₂')) + (c₁' + (c₂' + c₂')) + ≡˘⟨ Eq.cong₂ _+_ + {x = (2 * c₁' + 4 * c₂') * n' + (c₁' + 2 * c₂')} + refl + (Eq.cong₂ _+_ {x = c₁'} refl (Eq.trans (Nat.*-distribʳ-+ c₂' 1 1) (Eq.cong₂ _+_ (Nat.*-identityˡ c₂') (Nat.*-identityˡ c₂')))) ⟩ + ((2 * c₁' + 4 * c₂') * n' + (c₁' + 2 * c₂')) + (c₁' + 2 * c₂') + ≡⟨ Nat.+-assoc ((2 * c₁' + 4 * c₂') * n') (c₁' + 2 * c₂') (c₁' + 2 * c₂') ⟩ + (2 * c₁' + 4 * c₂') * n' + ((c₁' + 2 * c₂') + (c₁' + 2 * c₂')) + ≡˘⟨ Eq.cong₂ _+_ + {x = (2 * c₁' + 4 * c₂') * n'} + refl + (Eq.trans (Nat.*-distribʳ-+ (c₁' + 2 * c₂') 1 1) (Eq.cong₂ _+_ (Nat.*-identityˡ (c₁' + 2 * c₂')) (Nat.*-identityˡ (c₁' + 2 * c₂')))) ⟩ + (2 * c₁' + 4 * c₂') * n' + 2 * (c₁' + 2 * c₂') + ≡⟨ Eq.cong₂ _+_ + {x = (2 * c₁' + 4 * c₂') * n'} + refl + (Nat.*-distribˡ-+ 2 c₁' (2 * c₂')) ⟩ + (2 * c₁' + 4 * c₂') * n' + (2 * c₁' + 2 * (2 * c₂')) + ≡⟨ Eq.cong (λ x → (2 * c₁' + 4 * c₂') * n' + (2 * c₁' + x)) (Eq.sym (Nat.*-assoc 2 2 c₂')) ⟩ + (2 * c₁' + 4 * c₂') * n' + (2 * c₁' + 4 * c₂') + ≡⟨ Nat.+-comm ((2 * c₁' + 4 * c₂') * n') (2 * c₁' + 4 * c₂') ⟩ + (2 * c₁' + 4 * c₂') + (2 * c₁' + 4 * c₂') * n' + ≡˘⟨ Nat.*-suc (2 * c₁' + 4 * c₂') n' ⟩ + (2 * c₁' + 4 * c₂') * n + ∎ + + mapreduce/is-bounded : + {c₁ c₁' c₂ c₂' : val nat} → (f : cmp (Π A λ _ → F B)) → - ({x : val A} → IsBounded B (f x) (1 , 1)) → + ({x : val A} → IsBounded B (f x) (c₁ , c₁')) → (g : cmp (Π B λ _ → Π B λ _ → F B)) → - ({x y : val B} → IsBounded B (g x y) (1 , 1)) → + ({x y : val B} → IsBounded B (g x y) (c₂ , c₂')) → (z : val B) → (y : val color) → (n : val nat) → (l : val (list A)) → (t : val (irbt A y n l)) → - IsBounded B (mapreduce/seq y n l t f g z) (mapreduce/work l , mapreduce/span' n) - mapreduce/is-bounded' f f-bound g g-bound z y n l t = + IsBounded B (mapreduce/seq y n l t f g z) ((c₁ + 2 * c₂) * length l , (2 * c₁' + 4 * c₂') * ⌈log₂ (1 + length l) ⌉ + (c₁' + 2 * c₂')) + mapreduce/is-bounded {c₁} {c₁'} {c₂} {c₂'} f f-bound g g-bound z y n l t = let open ≤⁻-Reasoning cost in begin bind cost (mapreduce/seq y n l t f g z) (λ _ → ret triv) - ≤⟨ mapreduce/is-bounded f f-bound g g-bound z y n l t ⟩ - step⋆ (mapreduce/work l , mapreduce/span y n) - ≤⟨ step⋆-mono-≤⁻ (Nat.≤-refl {mapreduce/work l}, span/bounded y n) ⟩ - step⋆ (mapreduce/work l , mapreduce/span' n) + ≤⟨ mapreduce/is-bounded' {c₁} {c₁'} {c₂} {c₂'} f f-bound g g-bound z y n l t ⟩ + step⋆ (mapreduce/work c₁ c₂ l , mapreduce/span c₁' c₂' y n) + ≤⟨ step⋆-mono-≤⁻ (Nat.≤-refl {mapreduce/work c₁ c₂ l}, span/bounded c₁' c₂' y n) ⟩ + step⋆ (mapreduce/work c₁ c₂ l , mapreduce/span' c₁' c₂' n) + ≤⟨ step⋆-mono-≤⁻ (Nat.≤-refl {mapreduce/work c₁ c₂ l} , lemma) ⟩ + step⋆ ((c₁ + 2 * c₂) * length l , (2 * c₁' + 4 * c₂') * ⌈log₂ (1 + length l) ⌉ + (c₁' + 2 * c₂')) ∎ + where + lemma : mapreduce/span' c₁' c₂' n Nat.≤ (2 * c₁' + 4 * c₂') * ⌈log₂ (1 + length l) ⌉ + (c₁' + 2 * c₂') + lemma = + let open Nat.≤-Reasoning in + begin + (2 * c₁' + 4 * c₂') * n + (c₁' + 2 * c₂') + ≤⟨ Nat.+-monoˡ-≤ (c₁' + 2 * c₂') (Nat.*-monoʳ-≤ (2 * c₁' + 4 * c₂') (i-nodes/bound/log-node-black-height t)) ⟩ + (2 * c₁' + 4 * c₂') * ⌈log₂ (1 + i-nodes t) ⌉ + (c₁' + 2 * c₂') + ≡⟨ Eq.cong (λ x → (2 * c₁' + 4 * c₂') * ⌈log₂ (1 + x) ⌉ + (c₁' + 2 * c₂')) (i-nodes≡lengthl t) ⟩ + (2 * c₁' + 4 * c₂') * ⌈log₂ (1 + length l) ⌉ + (c₁' + 2 * c₂') + ∎ module Sum where @@ -160,23 +408,6 @@ module Sum where span/bounded red n = Nat.≤-refl span/bounded black n = Nat.n≤1+n (2 * n) - list/preserves/length : ∀ (l₁ : List ℕ) a (l₂ : List ℕ) → 1 + (length l₁ + length l₂) ≡ length (l₁ ++ a ∷ l₂) - list/preserves/length l₁ a l₂ = - let open ≡-Reasoning in - begin - 1 + (length l₁ + length l₂) - ≡˘⟨ Nat.+-assoc 1 (length l₁) (length l₂) ⟩ - 1 + length l₁ + length l₂ - ≡⟨ Eq.cong₂ _+_ (Nat.+-comm 1 (length l₁)) refl ⟩ - length l₁ + 1 + length l₂ - ≡⟨ Nat.+-assoc (length l₁) 1 (length l₂) ⟩ - length l₁ + (1 + length l₂) - ≡⟨⟩ - length l₁ + length (a ∷ l₂) - ≡˘⟨ List.length-++ l₁ ⟩ - length (l₁ ++ a ∷ l₂) - ∎ - sum/bounded' : ∀ y n l t → IsBounded nat (sum/seq y n l t) (length l , span/sum y n) sum/bounded' .black .zero .[] leaf = ≤⁻-refl sum/bounded' .red n l (red {l₁ = l₁} {l₂ = l₂} t₁ a t₂) =