Update sequential sorting

jonsterling · Oct 4, 2023 · 756631e · 756631e
1 parent c984233
commit 756631e
Show file tree

Hide file tree

Showing 9 changed files with 97 additions and 98 deletions.
diff --git a/src/Examples/Sorting/Comparable.agda b/src/Examples/Sorting/Comparable.agda
@@ -1,14 +1,16 @@
-open import Calf.CostMonoid
+{-# OPTIONS --rewriting #-}
+
+open import Algebra.Cost
 open import Data.Nat using (ℕ)
 
 module Examples.Sorting.Comparable
   (costMonoid : CostMonoid) (fromℕ : ℕ → CostMonoid.ℂ costMonoid) where
 
 open CostMonoid costMonoid using (ℂ)
 
-open import Calf costMonoid
-open import Calf.Types.Bool
-open import Calf.Types.Bounded costMonoid
+open import Calf costMonoid hiding (A)
+open import Calf.Data.Bool using (bool)
+open import Calf.Data.IsBounded costMonoid
 
 open import Relation.Nullary
 open import Relation.Nullary.Negation
@@ -57,24 +59,8 @@ NatComparable = record
   ; ≤-antisym = ≤-antisym
   ; _≤?_ = λ x y → step (F (meta⁺ (Dec (x ≤ y)))) (fromℕ 1) (ret (x ≤? y))
   ; ≤?-total = λ x y u → (x ≤? y) , (step/ext (F _) (ret _) (fromℕ 1) u)
-  ; h-cost = λ _ _ → ≲-refl
+  ; h-cost = λ _ _ → ≤⁻-refl
   }
   where
-    open import Calf.Types.Nat
-
-    open import Data.Nat
+    open import Calf.Data.Nat
     open import Data.Nat.Properties
-
-    ret-injective : ∀ {𝕊 v₁ v₂} → ret {U (meta 𝕊)} v₁ ≡ ret {U (meta 𝕊)} v₂ → v₁ ≡ v₂
-    ret-injective {𝕊} = Eq.cong (λ e → bind {U (meta 𝕊)} (meta 𝕊) e id)
-
-    reflects : ∀ {x y b} → ◯ (step (F bool) (fromℕ 1) (ret (x ≤ᵇ y)) ≡ ret {bool} b → Reflects (x ≤ y) b)
-    reflects {x} {y} {b} u h with ret-injective (Eq.subst (_≡ ret b) (step/ext (F bool) (ret (x ≤ᵇ y)) (fromℕ 1) u) h)
-    ... | refl = ≤ᵇ-reflects-≤ x y
-
-    reflects⁻¹ : ∀ {x y b} → ◯ (Reflects (x ≤ y) b → step (F (U (meta Bool))) (fromℕ 1) (ret (x ≤ᵇ y)) ≡ ret b)
-    reflects⁻¹ {x} {y} u h with x ≤ᵇ y | invert (≤ᵇ-reflects-≤ x y)
-    reflects⁻¹ {x} {y} u (ofʸ x≤y)  | false | ¬x≤y = contradiction x≤y ¬x≤y
-    reflects⁻¹ {x} {y} u (ofⁿ ¬x≤y) | false | _    = step/ext (F bool) (ret false) (fromℕ 1) u
-    reflects⁻¹ {x} {y} u (ofʸ x≤y)  | true  | _    = step/ext (F bool) (ret true) (fromℕ 1) u
-    reflects⁻¹ {x} {y} u (ofⁿ ¬x≤y) | true  | x≤y  = contradiction x≤y ¬x≤y
diff --git a/src/Examples/Sorting/Core.agda b/src/Examples/Sorting/Core.agda
@@ -1,4 +1,6 @@
-open import Calf.CostMonoid
+{-# OPTIONS --rewriting #-}
+
+open import Algebra.Cost
 open import Data.Nat using (ℕ)
 open import Examples.Sorting.Comparable
 
@@ -9,9 +11,9 @@ module Examples.Sorting.Core
 
 open Comparable M
 
-open import Calf costMonoid
-open import Calf.Types.Product
-open import Calf.Types.List
+open import Calf costMonoid hiding (A)
+open import Calf.Data.Product using (_×⁺_; _,_; proj₁; proj₂)
+open import Calf.Data.List using (list; []; _∷_; _∷ʳ_; [_]; length; _++_; reverse)
 
 open import Relation.Nullary
 open import Relation.Nullary.Negation
@@ -86,10 +88,10 @@ uncons₂ : ∀ {x xs} → Sorted (x ∷ xs) → Sorted xs
 uncons₂ (h ∷ sorted) = sorted
 
 sorted-of : val (list A) → val (list A) → tp pos
-sorted-of l l' = prod⁺ (meta⁺ (l ↭ l')) (sorted l')
+sorted-of l l' = meta⁺ (l ↭ l') ×⁺ (sorted l')
 
 sort-result : val (list A) → tp pos
-sort-result l = Σ++ (list A) (sorted-of l)
+sort-result l = Σ⁺ (list A) (sorted-of l)
 
 sorting : tp neg
 sorting = Π (list A) λ l → F (sort-result l)

diff --git a/src/Examples/Sorting/Sequential.agda b/src/Examples/Sorting/Sequential.agda
@@ -1,10 +1,12 @@
+{-# OPTIONS --rewriting #-}
+
 module Examples.Sorting.Sequential where
 
 open import Examples.Sorting.Sequential.Comparable
 
 open import Calf costMonoid
-open import Calf.Types.Nat
-open import Calf.Types.List
+open import Calf.Data.Nat
+open import Calf.Data.List
 
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
 open import Data.Product using (_,_)

diff --git a/src/Examples/Sorting/Sequential/Comparable.agda b/src/Examples/Sorting/Sequential/Comparable.agda
@@ -1,7 +1,9 @@
+{-# OPTIONS --rewriting #-}
+
 module Examples.Sorting.Sequential.Comparable where
 
-open import Calf.CostMonoid public
-open import Calf.CostMonoids
+open import Algebra.Cost public
+
 
 costMonoid = ℕ-CostMonoid
 

diff --git a/src/Examples/Sorting/Sequential/Core.agda b/src/Examples/Sorting/Sequential/Core.agda
@@ -1,8 +1,10 @@
+{-# OPTIONS --rewriting #-}
+
 open import Examples.Sorting.Sequential.Comparable
 
 module Examples.Sorting.Sequential.Core (M : Comparable) where
 
-open import Calf.CostMonoid
+open import Algebra.Cost
 open CostMonoid costMonoid
   hiding (zero; _+_; _≤_; ≤-refl; ≤-trans) public
 

diff --git a/src/Examples/Sorting/Sequential/InsertionSort.agda b/src/Examples/Sorting/Sequential/InsertionSort.agda
@@ -1,17 +1,19 @@
+{-# OPTIONS --rewriting #-}
+
 open import Examples.Sorting.Sequential.Comparable
 
 module Examples.Sorting.Sequential.InsertionSort (M : Comparable) where
 
 open Comparable M
 open import Examples.Sorting.Sequential.Core M
 
-open import Calf costMonoid
-open import Calf.Types.Bool
-open import Calf.Types.List
-open import Calf.Types.Eq
-open import Calf.Types.BoundedG costMonoid
-open import Calf.Types.Bounded costMonoid
-open import Calf.Types.BigO costMonoid
+open import Calf costMonoid hiding (A)
+open import Calf.Data.Bool using (bool)
+open import Calf.Data.List
+open import Calf.Data.Equality using (_≡_; refl)
+open import Calf.Data.IsBoundedG costMonoid
+open import Calf.Data.IsBounded costMonoid
+open import Calf.Data.BigO costMonoid
 
 open import Relation.Nullary
 open import Relation.Nullary.Negation
@@ -24,7 +26,7 @@ import Data.Nat.Properties as N
 open import Data.Nat.Square
 
 
-insert : cmp (Π A λ x → Π (list A) λ l → Π (sorted l) λ _ → F (Σ++ (list A) λ l' → sorted-of (x ∷ l) l'))
+insert : cmp (Π A λ x → Π (list A) λ l → Π (sorted l) λ _ → F (Σ⁺ (list A) λ l' → sorted-of (x ∷ l) l'))
 insert x []       []       = ret ([ x ] , refl , [] ∷ [])
 insert x (y ∷ ys) (h ∷ hs) =
   bind (F _) (x ≤? y) $ case-≤
@@ -54,25 +56,25 @@ insert/total x (y ∷ ys) (h ∷ hs) u with ≤?-total x y u
 insert/cost : cmp (Π A λ _ → Π (list A) λ _ → cost)
 insert/cost x l = step⋆ (length l)
 
-insert/is-bounded : ∀ x l h → IsBoundedG (Σ++ (list A) λ l' → sorted-of (x ∷ l) l') (insert x l h) (insert/cost x l)
-insert/is-bounded x []       []       = ≲-refl
+insert/is-bounded : ∀ x l h → IsBoundedG (Σ⁺ (list A) λ l' → sorted-of (x ∷ l) l') (insert x l h) (insert/cost x l)
+insert/is-bounded x []       []       = ≤⁻-refl
 insert/is-bounded x (y ∷ ys) (h ∷ hs) =
-  bound/bind/const {_} {Σ++ (list A) λ l' → sorted-of (x ∷ (y ∷ ys)) l'}
+  bound/bind/const {_} {Σ⁺ (list A) λ l' → sorted-of (x ∷ (y ∷ ys)) l'}
     {x ≤? y}
     {case-≤ _ _}
     1
     (length ys)
     (h-cost x y)
-    λ { (yes x≤y) → step-monoˡ-≲ (ret _) (z≤n {length ys})
+    λ { (yes x≤y) → step-monoˡ-≤⁻ (ret _) (z≤n {length ys})
       ; (no ¬x≤y) → insert/is-bounded x ys hs
       }
 
 
 sort : cmp sorting
 sort []       = ret ([] , refl , [])
 sort (x ∷ xs) =
-  bind (F (Σ++ (list A) (sorted-of (x ∷ xs)))) (sort xs) λ (xs' , xs↭xs' , sorted-xs') →
-  bind (F (Σ++ (list A) (sorted-of (x ∷ xs)))) (insert x xs' sorted-xs') λ (x∷xs' , x∷xs↭x∷xs' , sorted-x∷xs') →
+  bind (F (Σ⁺ (list A) (sorted-of (x ∷ xs)))) (sort xs) λ (xs' , xs↭xs' , sorted-xs') →
+  bind (F (Σ⁺ (list A) (sorted-of (x ∷ xs)))) (insert x xs' sorted-xs') λ (x∷xs' , x∷xs↭x∷xs' , sorted-x∷xs') →
   ret (x∷xs' , trans (prep x xs↭xs') x∷xs↭x∷xs' , sorted-x∷xs')
 
 sort/total : IsTotal sort
@@ -86,18 +88,18 @@ sort/total (x ∷ xs) u = ↓
   ≡⟨
     Eq.cong
       (λ e →
-        bind (F (Σ++ (list A) (sorted-of (x ∷ xs)))) e λ (xs' , xs↭xs' , sorted-xs') →
-        bind (F (Σ++ (list A) (sorted-of (x ∷ xs)))) (insert x xs' sorted-xs') λ (x∷xs' , x∷xs↭x∷xs' , sorted-x∷xs') →
+        bind (F (Σ⁺ (list A) (sorted-of (x ∷ xs)))) e λ (xs' , xs↭xs' , sorted-xs') →
+        bind (F (Σ⁺ (list A) (sorted-of (x ∷ xs)))) (insert x xs' sorted-xs') λ (x∷xs' , x∷xs↭x∷xs' , sorted-x∷xs') →
         ret (x∷xs' , trans (prep x xs↭xs') x∷xs↭x∷xs' , sorted-x∷xs'))
       (Valuable.proof (sort/total xs u))
   ⟩
-    ( bind (F (Σ++ (list A) (sorted-of (x ∷ xs)))) (insert x xs' sorted-xs') λ (x∷xs' , x∷xs↭x∷xs' , sorted-x∷xs') →
+    ( bind (F (Σ⁺ (list A) (sorted-of (x ∷ xs)))) (insert x xs' sorted-xs') λ (x∷xs' , x∷xs↭x∷xs' , sorted-x∷xs') →
       ret (x∷xs' , _ , sorted-x∷xs')
     )
   ≡⟨
     Eq.cong
       (λ e →
-        bind (F (Σ++ (list A) (sorted-of (x ∷ xs)))) e λ (x∷xs' , x∷xs↭x∷xs' , sorted-x∷xs') →
+        bind (F (Σ⁺ (list A) (sorted-of (x ∷ xs)))) e λ (x∷xs' , x∷xs↭x∷xs' , sorted-x∷xs') →
         ret (x∷xs' , trans (prep x xs↭xs') x∷xs↭x∷xs' , sorted-x∷xs'))
       (Valuable.proof (insert/total x xs' sorted-xs' u))
   ⟩
@@ -107,16 +109,16 @@ sort/total (x ∷ xs) u = ↓
 sort/cost : cmp (Π (list A) λ _ → cost)
 sort/cost l = step⋆ (length l ²)
 
-sort/is-bounded : ∀ l → IsBoundedG (Σ++ (list A) (sorted-of l)) (sort l) (sort/cost l)
-sort/is-bounded []       = ≲-refl
+sort/is-bounded : ∀ l → IsBoundedG (Σ⁺ (list A) (sorted-of l)) (sort l) (sort/cost l)
+sort/is-bounded []       = ≤⁻-refl
 sort/is-bounded (x ∷ xs) =
-  let open ≲-Reasoning cost in
+  let open ≤⁻-Reasoning cost in
   begin
     ( bind cost (sort xs) λ (xs' , xs↭xs' , sorted-xs') →
       bind cost (insert x xs' sorted-xs') λ _ →
       step⋆ zero
     )
-  ≤⟨ bind-monoʳ-≲ (sort xs) (λ (xs' , xs↭xs' , sorted-xs') → insert/is-bounded x xs' sorted-xs') ⟩
+  ≤⟨ bind-monoʳ-≤⁻ (sort xs) (λ (xs' , xs↭xs' , sorted-xs') → insert/is-bounded x xs' sorted-xs') ⟩
     ( bind cost (sort xs) λ (xs' , xs↭xs' , sorted-xs') →
       step⋆ (length xs')
     )
@@ -128,9 +130,9 @@ sort/is-bounded (x ∷ xs) =
     ( bind cost (sort xs) λ _ →
       step⋆ (length xs)
     )
-  ≤⟨ bind-monoˡ-≲ (λ _ → step⋆ (length xs)) (sort/is-bounded xs) ⟩
+  ≤⟨ bind-monoˡ-≤⁻ (λ _ → step⋆ (length xs)) (sort/is-bounded xs) ⟩
     step⋆ ((length xs ²) + length xs)
-  ≤⟨ step⋆-mono-≲ (N.+-mono-≤ (N.*-monoʳ-≤ (length xs) (N.n≤1+n (length xs))) (N.n≤1+n (length xs))) ⟩
+  ≤⟨ step⋆-mono-≤⁻ (N.+-mono-≤ (N.*-monoʳ-≤ (length xs) (N.n≤1+n (length xs))) (N.n≤1+n (length xs))) ⟩
     step⋆ (length xs * length (x ∷ xs) + length (x ∷ xs))
   ≡⟨ Eq.cong step⋆ (N.+-comm (length xs * length (x ∷ xs)) (length (x ∷ xs))) ⟩
     step⋆ (length (x ∷ xs) ²)

diff --git a/src/Examples/Sorting/Sequential/MergeSort.agda b/src/Examples/Sorting/Sequential/MergeSort.agda
@@ -1,20 +1,21 @@
+{-# OPTIONS --rewriting #-}
+
 open import Examples.Sorting.Sequential.Comparable
 
 module Examples.Sorting.Sequential.MergeSort (M : Comparable) where
 
 open Comparable M
 open import Examples.Sorting.Sequential.Core M
 
-open import Calf costMonoid
-open import Calf.Types.Unit
-open import Calf.Types.Product
-open import Calf.Types.Bool
-open import Calf.Types.Nat
-open import Calf.Types.List
-open import Calf.Types.Eq
-open import Calf.Types.BoundedG costMonoid
-open import Calf.Types.Bounded costMonoid
-open import Calf.Types.BigO costMonoid
+open import Calf costMonoid hiding (A)
+open import Calf.Data.Product
+open import Calf.Data.Bool
+open import Calf.Data.Nat
+open import Calf.Data.List using (list; []; _∷_; _∷ʳ_; [_]; length; _++_; reverse)
+open import Calf.Data.Equality using (_≡_; refl)
+open import Calf.Data.IsBoundedG costMonoid
+open import Calf.Data.IsBounded costMonoid
+open import Calf.Data.BigO costMonoid
 
 open import Relation.Nullary
 open import Relation.Nullary.Negation
@@ -134,7 +135,7 @@ sort/clocked/cost : cmp $ Π nat λ k → Π (list A) λ l → Π (meta⁺ (⌈l
 sort/clocked/cost k l _ = step⋆ (k * length l)
 
 sort/clocked/is-bounded : ∀ k l h → IsBoundedG (sort-result l) (sort/clocked k l h) (sort/clocked/cost k l h)
-sort/clocked/is-bounded zero    l h = ≲-refl
+sort/clocked/is-bounded zero    l h = ≤⁻-refl
 sort/clocked/is-bounded (suc k) l h =
   bound/bind/const
     {e = split l}
@@ -211,7 +212,7 @@ sort/clocked/is-bounded (suc k) l h =
     0
     (merge/is-bounded (l₁' , l₂') _)
     λ _ →
-  ≲-refl
+  ≤⁻-refl
 
 
 sort : cmp (Π (list A) λ l → F (sort-result l))

diff --git a/src/Examples/Sorting/Sequential/MergeSort/Merge.agda b/src/Examples/Sorting/Sequential/MergeSort/Merge.agda
@@ -1,19 +1,20 @@
+{-# OPTIONS --rewriting #-}
+
 open import Examples.Sorting.Sequential.Comparable
 
 module Examples.Sorting.Sequential.MergeSort.Merge (M : Comparable) where
 
 open Comparable M
 open import Examples.Sorting.Sequential.Core M
 
-open import Calf costMonoid
-open import Calf.Types.Unit
-open import Calf.Types.Product
-open import Calf.Types.Bool
-open import Calf.Types.Nat
-open import Calf.Types.List
-open import Calf.Types.Eq
-open import Calf.Types.BoundedG costMonoid
-open import Calf.Types.Bounded costMonoid
+open import Calf costMonoid hiding (A)
+open import Calf.Data.Product
+open import Calf.Data.Bool using (bool)
+open import Calf.Data.Nat using (nat)
+open import Calf.Data.List using (list; []; _∷_; _∷ʳ_; [_]; length; _++_; reverse)
+open import Calf.Data.Equality
+open import Calf.Data.IsBoundedG costMonoid
+open import Calf.Data.IsBounded costMonoid
 
 open import Relation.Nullary
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; module ≡-Reasoning)
@@ -42,11 +43,11 @@ prep' {x} {xs} y {ys} {l} h =
   ∎
 
 merge/type : val pair → tp pos
-merge/type (l₁ , l₂) = Σ++ (list A) λ l → sorted-of (l₁ ++ l₂) l
+merge/type (l₁ , l₂) = Σ⁺ (list A) λ l → sorted-of (l₁ ++ l₂) l
 
 merge/clocked : cmp $
   Π nat λ k → Π pair λ (l₁ , l₂) →
-  Π (prod⁺ (sorted l₁) (sorted l₂)) λ _ →
+  Π (sorted l₁ ×⁺ sorted l₂) λ _ →
   Π (meta⁺ (length l₁ + length l₂ ≡ k)) λ _ →
   F (merge/type (l₁ , l₂))
 merge/clocked zero    ([]     , []    ) (sorted₁      , sorted₂     ) h = ret ([] , refl , [])
@@ -84,30 +85,30 @@ merge/clocked/total (suc k) (x ∷ xs , y ∷ ys) (h₁ ∷ sorted₁ , h₂ ∷
 
 merge/clocked/cost : cmp $
   Π nat λ k → Π pair λ (l₁ , l₂) →
-  Π (prod⁺ (sorted l₁) (sorted l₂)) λ _ →
+  Π (sorted l₁ ×⁺ sorted l₂) λ _ →
   Π (meta⁺ (length l₁ + length l₂ ≡ k)) λ _ →
   F unit
 merge/clocked/cost k _ _ _ = step⋆ k
 
 merge/clocked/is-bounded : ∀ k p s h → IsBoundedG (merge/type p) (merge/clocked k p s h) (merge/clocked/cost k p s h)
-merge/clocked/is-bounded zero    ([]     , []    ) (sorted₁      , sorted₂     ) h = ≲-refl
-merge/clocked/is-bounded (suc k) ([]     , l₂    ) ([]           , sorted₂     ) h = step⋆-mono-≲ (z≤n {suc k})
-merge/clocked/is-bounded (suc k) (x ∷ xs , []    ) (sorted₁      , []          ) h = step⋆-mono-≲ (z≤n {suc k})
+merge/clocked/is-bounded zero    ([]     , []    ) (sorted₁      , sorted₂     ) h = ≤⁻-refl
+merge/clocked/is-bounded (suc k) ([]     , l₂    ) ([]           , sorted₂     ) h = step⋆-mono-≤⁻ (z≤n {suc k})
+merge/clocked/is-bounded (suc k) (x ∷ xs , []    ) (sorted₁      , []          ) h = step⋆-mono-≤⁻ (z≤n {suc k})
 merge/clocked/is-bounded (suc k) (x ∷ xs , y ∷ ys) (h₁ ∷ sorted₁ , h₂ ∷ sorted₂) h =
   bound/bind/const
     {e = x ≤? y}
     {f = case-≤ (λ _ → bind (F (merge/type (x ∷ xs , y ∷ ys))) (merge/clocked k (xs , y ∷ ys) _ _) _) _}
     1
     k
     (h-cost x y)
-    λ { (yes p) → bind-mono-≲ (merge/clocked/is-bounded k (xs , y ∷ ys) _ _) (λ _ → ≲-refl)
-      ; (no ¬p) → bind-mono-≲ (merge/clocked/is-bounded k (x ∷ xs , ys) _ _) (λ _ → ≲-refl)
+    λ { (yes p) → bind-monoˡ-≤⁻ (λ _ → step⋆ zero) (merge/clocked/is-bounded k (xs , y ∷ ys) _ _)
+      ; (no ¬p) → bind-monoˡ-≤⁻ (λ _ → step⋆ zero) (merge/clocked/is-bounded k (x ∷ xs , ys) _ _)
       }
 
 
 merge : cmp $
   Π pair λ (l₁ , l₂) →
-  Π (prod⁺ (sorted l₁) (sorted l₂)) λ _ →
+  Π (sorted l₁ ×⁺ sorted l₂) λ _ →
   F (merge/type (l₁ , l₂))
 merge (l₁ , l₂) s = merge/clocked (length l₁ + length l₂) (l₁ , l₂) s refl
 
@@ -116,7 +117,7 @@ merge/total (l₁ , l₂) s = merge/clocked/total (length l₁ + length l₂) (l
 
 merge/cost : cmp $
   Π pair λ (l₁ , l₂) →
-  Π (prod⁺ (sorted l₁) (sorted l₂)) λ _ →
+  Π (sorted l₁ ×⁺ sorted l₂) λ _ →
   cost
 merge/cost (l₁ , l₂) s = merge/clocked/cost (length l₁ + length l₂) (l₁ , l₂) s refl