diff --git a/calf.agda-lib b/calf.agda-lib index 0af7642e..1fe6b3c0 100644 --- a/calf.agda-lib +++ b/calf.agda-lib @@ -1,4 +1,4 @@ name: calf -depend: standard-library +depend: standard-library-2.0 include: src flags: --prop --guardedness diff --git a/src/Algebra/Cost/Bundles.agda b/src/Algebra/Cost/Bundles.agda index 38d86b9e..7a07d8b6 100644 --- a/src/Algebra/Cost/Bundles.agda +++ b/src/Algebra/Cost/Bundles.agda @@ -27,7 +27,8 @@ record CostMonoid : Set₁ where Preorder._≲_ ≤-preorder = _≤_ Preorder.isPreorder ≤-preorder = isPreorder - open import Relation.Binary.Reasoning.Preorder ≤-preorder public + module ≤-Reasoning where + open import Relation.Binary.Reasoning.Preorder ≤-preorder public record ParCostMonoid : Set₁ where @@ -63,4 +64,5 @@ record ParCostMonoid : Set₁ where Preorder._≲_ ≤-preorder = _≤_ Preorder.isPreorder ≤-preorder = isPreorder - open import Relation.Binary.Reasoning.Preorder ≤-preorder public + module ≤-Reasoning where + open import Relation.Binary.Reasoning.Preorder ≤-preorder public diff --git a/src/Calf/Data/IsBounded.agda b/src/Calf/Data/IsBounded.agda index 84874f36..aca9223b 100644 --- a/src/Calf/Data/IsBounded.agda +++ b/src/Calf/Data/IsBounded.agda @@ -40,11 +40,11 @@ bound/bind/const {e = e} {f} c d he hf = let open ≤⁻-Reasoning cost in begin bind cost e (λ v → bind cost (f v) (λ _ → ret triv)) - ≤⁻⟨ bind-monoʳ-≤⁻ e hf ⟩ + ≲⟨ bind-monoʳ-≤⁻ e hf ⟩ bind cost e (λ _ → step⋆ d) ≡⟨⟩ bind cost (bind cost e λ _ → ret triv) (λ _ → step⋆ d) - ≤⁻⟨ bind-monoˡ-≤⁻ (λ _ → step⋆ d) he ⟩ + ≲⟨ bind-monoˡ-≤⁻ (λ _ → step⋆ d) he ⟩ bind cost (step⋆ c) (λ _ → step⋆ d) ≡⟨⟩ step⋆ (c + d) @@ -66,6 +66,6 @@ module Legacy where bind cost (step (F A) c' (ret a)) (λ _ → ret triv) ≡⟨⟩ step⋆ c' - ≤⁻⟨ step-monoˡ-≤⁻ (ret triv) c'≤c ⟩ + ≲⟨ step-monoˡ-≤⁻ (ret triv) c'≤c ⟩ step⋆ c ∎ diff --git a/src/Calf/Data/IsBoundedG.agda b/src/Calf/Data/IsBoundedG.agda index 1c69cff2..7648d26c 100644 --- a/src/Calf/Data/IsBoundedG.agda +++ b/src/Calf/Data/IsBoundedG.agda @@ -38,9 +38,9 @@ boundg/relax {b = b} {b'} h {e = e} ib-b = let open ≤⁻-Reasoning cost in begin bind cost e (λ _ → ret triv) - ≤⁻⟨ ib-b ⟩ + ≲⟨ ib-b ⟩ b - ≤⁻⟨ h ⟩ + ≲⟨ h ⟩ b' ∎ @@ -53,7 +53,7 @@ boundg/step c {b} e h = bind cost (step (F _) c e) (λ _ → ret triv) ≡⟨⟩ step cost c (bind cost e (λ _ → ret triv)) - ≤⁻⟨ step-monoʳ-≤⁻ c h ⟩ + ≲⟨ step-monoʳ-≤⁻ c h ⟩ step cost c b ∎ @@ -67,6 +67,6 @@ boundg/bind {e = e} {f} b hf = bind cost (bind (F _) e f) (λ _ → ret triv) ≡⟨⟩ bind cost e (λ a → bind cost (f a) λ _ → ret triv) - ≤⁻⟨ bind-monoʳ-≤⁻ e hf ⟩ + ≲⟨ bind-monoʳ-≤⁻ e hf ⟩ bind cost e b ∎ diff --git a/src/Calf/Parallel.agda b/src/Calf/Parallel.agda index 3fdb0951..93155de9 100644 --- a/src/Calf/Parallel.agda +++ b/src/Calf/Parallel.agda @@ -58,11 +58,11 @@ boundg/par {A₁} {A₂} {e₁} {e₂} {b₁} {b₂} ib₁ ib₂ = let open ≤⁻-Reasoning cost in begin bind cost (e₁ ∥ e₂) (λ _ → ret triv) - ≤⁻⟨ {! !} ⟩ + ≲⟨ {! !} ⟩ bind cost ((bind cost e₁ λ _ → ret triv) ∥ (bind cost e₂ λ _ → ret triv)) (λ _ → ret triv) - ≤⁻⟨ ≤⁻-mono (λ e → bind cost (e ∥ (bind cost e₂ λ _ → ret triv)) (λ _ → ret triv)) ib₁ ⟩ + ≲⟨ ≤⁻-mono (λ e → bind cost (e ∥ (bind cost e₂ λ _ → ret triv)) (λ _ → ret triv)) ib₁ ⟩ bind cost (b₁ ∥ (bind cost e₂ λ _ → ret triv)) (λ _ → ret triv) - ≤⁻⟨ ≤⁻-mono (λ e → bind cost (b₁ ∥ e) (λ _ → ret triv)) ib₂ ⟩ + ≲⟨ ≤⁻-mono (λ e → bind cost (b₁ ∥ e) (λ _ → ret triv)) ib₂ ⟩ bind cost (b₁ ∥ b₂) (λ _ → ret triv) ∎ diff --git a/src/Calf/Step.agda b/src/Calf/Step.agda index 14ffbc14..ee8897e3 100644 --- a/src/Calf/Step.agda +++ b/src/Calf/Step.agda @@ -80,8 +80,8 @@ step-mono-≤⁻ {X} {c} {c'} {e} {e'} c≤c' e≤e' = let open ≤⁻-Reasoning X in begin step X c e - ≤⁻⟨ step-monoˡ-≤⁻ e c≤c' ⟩ + ≲⟨ step-monoˡ-≤⁻ e c≤c' ⟩ step X c' e - ≤⁻⟨ step-monoʳ-≤⁻ c' e≤e' ⟩ + ≲⟨ step-monoʳ-≤⁻ c' e≤e' ⟩ step X c' e' ∎ diff --git a/src/Data/Nat/PredExp2.agda b/src/Data/Nat/PredExp2.agda index 4c335b07..c2f88809 100644 --- a/src/Data/Nat/PredExp2.agda +++ b/src/Data/Nat/PredExp2.agda @@ -50,7 +50,7 @@ private ... | zero | () pred[2^]-mono : pred[2^_] Preserves _≤_ ⟶ _≤_ -pred[2^]-mono m≤n = pred-mono (2^-mono m≤n) +pred[2^]-mono m≤n = pred-mono-≤ (2^-mono m≤n) where 2^-mono : (2 ^_) Preserves _≤_ ⟶ _≤_ 2^-mono {y = y} z≤n = lemma/1≤2^n y diff --git a/src/Examples/Decalf/HigherOrderFunction.agda b/src/Examples/Decalf/HigherOrderFunction.agda index 3f413fff..57316fd7 100644 --- a/src/Examples/Decalf/HigherOrderFunction.agda +++ b/src/Examples/Decalf/HigherOrderFunction.agda @@ -42,7 +42,7 @@ module Twice where bind cost e λ _ → ret triv ) - ≤⁻⟨ ≤⁻-mono₂ (λ e₁ e₂ → bind (F _) e₁ λ _ → bind (F _) e₂ λ _ → ret triv) e≤step⋆1 e≤step⋆1 ⟩ + ≲⟨ ≤⁻-mono₂ (λ e₁ e₂ → bind (F _) e₁ λ _ → bind (F _) e₂ λ _ → ret triv) e≤step⋆1 e≤step⋆1 ⟩ ( bind cost (step⋆ 1) λ _ → bind cost (step⋆ 1) λ _ → ret triv @@ -79,7 +79,7 @@ module Map where bind cost (map f xs) λ _ → ret triv ) - ≤⁻⟨ + ≲⟨ ≤⁻-mono₂ (λ e₁ e₂ → bind cost e₁ λ _ → bind cost e₂ λ _ → ret triv) (f-bound x) (map/is-bounded f f-bound xs) @@ -114,11 +114,11 @@ module Map where bind cost (map f xs) λ _ → ret triv ) - ≤⁻⟨ ≤⁻-mono (λ e → bind cost (f x) λ _ → e) (map/is-bounded' f f-bound xs) ⟩ + ≲⟨ ≤⁻-mono (λ e → bind cost (f x) λ _ → e) (map/is-bounded' f f-bound xs) ⟩ ( bind cost (f x) λ _ → binomial (length xs * n) ) - ≤⁻⟨ ≤⁻-mono (λ e → bind cost e λ _ → binomial (length xs * n)) (f-bound x) ⟩ + ≲⟨ ≤⁻-mono (λ e → bind cost e λ _ → binomial (length xs * n)) (f-bound x) ⟩ ( bind cost (binomial n) λ _ → binomial (length xs * n) ) diff --git a/src/Examples/Decalf/Nondeterminism.agda b/src/Examples/Decalf/Nondeterminism.agda index a4b8dad2..c127703c 100644 --- a/src/Examples/Decalf/Nondeterminism.agda +++ b/src/Examples/Decalf/Nondeterminism.agda @@ -70,7 +70,7 @@ module QuickSort (M : Comparable) where let open ≤⁻-Reasoning cost in begin branch (F unit) (bind (F unit) (choose (x' ∷ xs)) λ _ → ret triv) (ret triv) - ≤⁻⟨ ≤⁻-mono (λ e → branch (F unit) (bind (F unit) e λ _ → ret triv) (ret triv)) (choose/is-bounded x' xs) ⟩ + ≲⟨ ≤⁻-mono (λ e → branch (F unit) (bind (F unit) e λ _ → ret triv) (ret triv)) (choose/is-bounded x' xs) ⟩ branch (F unit) (ret triv) (ret triv) ≡⟨ branch/idem ⟩ ret triv @@ -128,7 +128,7 @@ module QuickSort (M : Comparable) where bind (F unit) (x ≤? pivot) λ _ → ret triv ) - ≤⁻⟨ + ≲⟨ ( ≤⁻-mono {Π (Σ⁺ (list A) λ l₁ → Σ⁺ (list A) λ l₂ → meta⁺ (All (_≤ pivot) l₁) ×⁺ meta⁺ (All (pivot ≤_) l₂) ×⁺ meta⁺ (l₁ ++ l₂ ↭ xs)) λ _ → F unit} (bind (F unit) (partition pivot xs)) $ @@ -143,7 +143,7 @@ module QuickSort (M : Comparable) where ( bind (F unit) (bind (F unit) (partition pivot xs) λ _ → ret triv) λ _ → step⋆ 1 ) - ≤⁻⟨ ≤⁻-mono (λ e → bind (F unit) (bind (F unit) e λ _ → ret triv) λ _ → step (F unit) 1 (ret triv)) (partition/is-bounded pivot xs) ⟩ + ≲⟨ ≤⁻-mono (λ e → bind (F unit) (bind (F unit) e λ _ → ret triv) λ _ → step (F unit) 1 (ret triv)) (partition/is-bounded pivot xs) ⟩ ( bind (F unit) (step (F unit) (length xs) (ret triv)) λ _ → step⋆ 1 ) @@ -171,7 +171,7 @@ module QuickSort (M : Comparable) where let open Nat.≤-Reasoning in begin m ² + n ² - ≤⁻⟨ Nat.+-mono-≤ (Nat.m≤m+n (m * m) (n * m)) (Nat.m≤n+m (n * n) (m * n)) ⟩ + ≤⟨ Nat.+-mono-≤ (Nat.m≤m+n (m * m) (n * m)) (Nat.m≤n+m (n * n) (m * n)) ⟩ (m * m + n * m) + (m * n + n * n) ≡˘⟨ Eq.cong₂ _+_ (Nat.*-distribʳ-+ m m n) (Nat.*-distribʳ-+ n m n) ⟩ (m + n) * m + (m + n) * n @@ -191,7 +191,7 @@ module QuickSort (M : Comparable) where bind (F _) (sort l₂) λ _ → ret triv ) - ≤⁻⟨ + ≲⟨ ( ≤⁻-mono {Π (Σ⁺ A λ pivot → Σ⁺ (list A) λ l' → meta⁺ (x ∷ xs ↭ pivot ∷ l')) λ _ → F unit} {F unit} @@ -220,7 +220,7 @@ module QuickSort (M : Comparable) where bind (F _) (sort l₁) λ _ → step⋆ (length l₂ ²) ) - ≤⁻⟨ + ≲⟨ ( ≤⁻-mono {Π (Σ⁺ A λ pivot → Σ⁺ (list A) λ l' → meta⁺ (x ∷ xs ↭ pivot ∷ l')) λ _ → F unit} {F unit} @@ -245,7 +245,7 @@ module QuickSort (M : Comparable) where bind (F _) (partition pivot l) λ (l₁ , l₂ , h₁ , h₂ , l₁++l₂↭l) → step⋆ (length l₁ ² + length l₂ ²) ) - ≤⁻⟨ + ≲⟨ ( ≤⁻-mono {Π (Σ⁺ A λ pivot → Σ⁺ (list A) λ l' → meta⁺ (x ∷ xs ↭ pivot ∷ l')) λ _ → F unit} {F unit} @@ -270,7 +270,7 @@ module QuickSort (M : Comparable) where bind (F _) (partition pivot l) λ _ → step⋆ (length l ²) ) - ≤⁻⟨ + ≲⟨ ( ≤⁻-mono {Π (Σ⁺ A λ pivot → Σ⁺ (list A) λ l' → meta⁺ (x ∷ xs ↭ pivot ∷ l')) λ _ → F unit} {F unit} @@ -295,9 +295,9 @@ module QuickSort (M : Comparable) where ( bind (F _) (choose (x ∷ xs)) λ _ → step⋆ (length xs + length xs ²) ) - ≤⁻⟨ bind-irr-monoˡ-≤⁻ (choose/is-bounded x xs) ⟩ + ≲⟨ bind-irr-monoˡ-≤⁻ (choose/is-bounded x xs) ⟩ step⋆ (length xs + length xs ²) - ≤⁻⟨ step⋆-mono-≤⁻ (Nat.+-mono-≤ (Nat.n≤1+n (length xs)) (Nat.*-monoʳ-≤ (length xs) (Nat.n≤1+n (length xs)))) ⟩ + ≲⟨ step⋆-mono-≤⁻ (Nat.+-mono-≤ (Nat.n≤1+n (length xs)) (Nat.*-monoʳ-≤ (length xs) (Nat.n≤1+n (length xs)))) ⟩ step⋆ (length (x ∷ xs) + length xs * length (x ∷ xs)) ≡⟨⟩ step⋆ (length (x ∷ xs) ²) @@ -330,7 +330,7 @@ module Lookup {A : tp⁺} where let open ≤⁻-Reasoning (F _) in begin step (F _) 1 (lookup xs i) - ≤⁻⟨ ≤⁻-mono (step (F _) 1) (lemma xs i p) ⟩ + ≲⟨ ≤⁻-mono (step (F _) 1) (lemma xs i p) ⟩ step (F _) 1 (fail (F _)) ≡⟨ fail/step 1 ⟩ fail (F _) @@ -353,7 +353,7 @@ module Pervasive where branch (F bool) (step (F bool) 3 (ret true)) (step (F bool) 12 (ret false)) - ≤⁻⟨ + ≲⟨ ≤⁻-mono (λ e → branch (F bool) e (step (F bool) 12 (ret false))) (step-monoˡ-≤⁻ {F bool} (ret true) (Nat.s≤s (Nat.s≤s (Nat.s≤s Nat.z≤n)))) @@ -370,7 +370,7 @@ module Pervasive where let open ≤⁻-Reasoning (F unit) in begin bind (F unit) e (λ _ → ret triv) - ≤⁻⟨ ≤⁻-mono (λ e → bind (F _) e (λ _ → ret triv)) e/is-bounded ⟩ + ≲⟨ ≤⁻-mono (λ e → bind (F _) e (λ _ → ret triv)) e/is-bounded ⟩ bind (F unit) (step (F bool) 12 (branch (F bool) (ret true) (ret false))) (λ _ → ret triv) ≡⟨⟩ step (F unit) 12 (branch (F unit) (ret triv) (ret triv)) diff --git a/src/Examples/Decalf/ProbabilisticChoice.agda b/src/Examples/Decalf/ProbabilisticChoice.agda index 7ea51b30..b3ac655e 100644 --- a/src/Examples/Decalf/ProbabilisticChoice.agda +++ b/src/Examples/Decalf/ProbabilisticChoice.agda @@ -64,7 +64,7 @@ module _ where let open ≤⁻-Reasoning cost in begin flip cost ½ (step⋆ 0) (step⋆ 1) - ≤⁻⟨ ≤⁻-mono {cost} (λ e → flip cost ½ e (step⋆ 1)) (≤⁺-mono step⋆ (≤⇒≤⁺ (z≤n {1}))) ⟩ + ≲⟨ ≤⁻-mono {cost} (λ e → flip cost ½ e (step⋆ 1)) (≤⁺-mono step⋆ (≤⇒≤⁺ (z≤n {1}))) ⟩ flip cost ½ (step⋆ 1) (step⋆ 1) ≡⟨ flip/same cost (step⋆ 1) {½} ⟩ step⋆ 1 @@ -123,13 +123,13 @@ module _ where ( bind cost bernoulli λ _ → binomial n ) - ≤⁻⟨ ≤⁻-mono (λ e → bind cost e λ _ → binomial n) bernoulli/upper ⟩ + ≲⟨ ≤⁻-mono (λ e → bind cost e λ _ → binomial n) bernoulli/upper ⟩ ( bind cost (step⋆ 1) λ _ → binomial n ) ≡⟨⟩ step cost 1 (binomial n) - ≤⁻⟨ ≤⁻-mono (step cost 1) (binomial/upper n) ⟩ + ≲⟨ ≤⁻-mono (step cost 1) (binomial/upper n) ⟩ step⋆ (suc n) ∎ @@ -161,7 +161,7 @@ sublist/is-bounded {A} (x ∷ xs) = ( bind cost (sublist {A} xs) λ _ → bernoulli ) - ≤⁻⟨ ≤⁻-mono (λ e → bind cost e λ _ → bernoulli) (sublist/is-bounded {A} xs) ⟩ + ≲⟨ ≤⁻-mono (λ e → bind cost e λ _ → bernoulli) (sublist/is-bounded {A} xs) ⟩ ( bind cost (binomial (length xs)) λ _ → bernoulli ) diff --git a/src/Examples/Exp2.agda b/src/Examples/Exp2.agda index 339ed63f..545a8d09 100644 --- a/src/Examples/Exp2.agda +++ b/src/Examples/Exp2.agda @@ -43,7 +43,7 @@ module Slow where begin (bind (F nat) (exp₂ n ∥ exp₂ n) λ (r₁ , r₂) → step (F nat) (1 , 1) (ret (r₁ + r₂))) - ≤⁻⟨ + ≲⟨ ≤⁻-mono₂ (λ e₁ e₂ → bind (F nat) (e₁ ∥ e₂) λ (r₁ , r₂) → step (F nat) (1 , 1) (ret (r₁ + r₂))) (exp₂/is-bounded n) (exp₂/is-bounded n) @@ -90,7 +90,7 @@ module Fast where begin (bind (F nat) (exp₂ n) λ r → step (F nat) (1 , 1) (ret (r + r))) - ≤⁻⟨ ≤⁻-mono (λ e → bind (F nat) e λ r → step (F nat) (1 , 1) (ret (r + r))) (exp₂/is-bounded n) ⟩ + ≲⟨ ≤⁻-mono (λ e → bind (F nat) e λ r → step (F nat) (1 , 1) (ret (r + r))) (exp₂/is-bounded n) ⟩ (bind (F nat) (step (F nat) (n , n) (ret (2 ^ n))) λ r → step (F nat) (1 , 1) (ret (r + r))) ≡⟨⟩ diff --git a/src/Examples/Id.agda b/src/Examples/Id.agda index f501da12..9fbab274 100644 --- a/src/Examples/Id.agda +++ b/src/Examples/Id.agda @@ -52,7 +52,7 @@ module Hard where ≤⁻-mono (step (F nat) 1) $ begin bind (F nat) (id n) (λ n' → ret (suc n')) - ≤⁻⟨ ≤⁻-mono (λ e → bind (F nat) e (ret ∘ suc)) (id/is-bounded n) ⟩ + ≲⟨ ≤⁻-mono (λ e → bind (F nat) e (ret ∘ suc)) (id/is-bounded n) ⟩ bind (F nat) (step (F nat) n (ret n)) (λ n' → ret (suc n')) ≡⟨⟩ step (F nat) n (ret (suc n)) diff --git a/src/Examples/Sorting/Sequential/InsertionSort.agda b/src/Examples/Sorting/Sequential/InsertionSort.agda index 94c8df46..fe0e48ab 100644 --- a/src/Examples/Sorting/Sequential/InsertionSort.agda +++ b/src/Examples/Sorting/Sequential/InsertionSort.agda @@ -118,7 +118,7 @@ sort/is-bounded (x ∷ 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') ) @@ -130,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 index c543c43e..6c4608c3 100644 --- a/src/Examples/Sorting/Sequential/MergeSort.agda +++ b/src/Examples/Sorting/Sequential/MergeSort.agda @@ -37,7 +37,7 @@ sort/clocked (suc k) l h = bind (F (sort-result l)) (split l) λ ((l₁ , l₂) , length₁ , length₂ , l↭l₁++l₂) → let h₁ , h₂ = - let open ≤-Reasoning in + let open N.≤-Reasoning in (begin ⌈log₂ length l₁ ⌉ ≡⟨ Eq.cong ⌈log₂_⌉ length₁ ⟩ @@ -66,7 +66,7 @@ sort/clocked/total (suc k) l h u rewrite Valuable.proof (split/total l u) = ↓ let ((l₁ , l₂) , length₁ , length₂ , l↭l₁++l₂) = Valuable.value (split/total l u) h₁ , h₂ = - let open ≤-Reasoning in + let open N.≤-Reasoning in (begin ⌈log₂ length l₁ ⌉ ≡⟨ Eq.cong ⌈log₂_⌉ length₁ ⟩