From 4cf6dd5ce73e68d7584840e4eca64ac570dfd188 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Sat, 19 Aug 2023 22:57:08 +0200 Subject: [PATCH 01/12] added functional vector permutation --- CHANGELOG.md | 4 +++ .../Relation/Binary/Permutation.agda | 26 +++++++++++++++++++ 2 files changed, 30 insertions(+) create mode 100644 src/Data/Vec/Functional/Relation/Binary/Permutation.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 77b00a6ff3..00fd42c4c8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3352,3 +3352,7 @@ This is a full list of proofs that have changed form to use irrelevant instance c ≈⟨ c≈d ⟩ d ∎ ``` +* Added module `Data.Vec.Functional.Relation.Binary.Permutation`: + ```agda + _↭_ : IRel (Vector A) _ + ``` diff --git a/src/Data/Vec/Functional/Relation/Binary/Permutation.agda b/src/Data/Vec/Functional/Relation/Binary/Permutation.agda new file mode 100644 index 0000000000..c220a8833c --- /dev/null +++ b/src/Data/Vec/Functional/Relation/Binary/Permutation.agda @@ -0,0 +1,26 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Permutation relations over Vector +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.Vec.Functional.Relation.Binary.Permutation where + +open import Level using (Level) +open import Data.Product using (Σ-syntax) +open import Data.Fin.Permutation using (Permutation; _⟨$⟩ʳ_) +open import Data.Vec.Functional using (Vector) +open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel) +open import Relation.Binary.PropositionalEquality using (_≡_) + +private + variable + ℓ : Level + A : Set ℓ + +infix 3 _↭_ + +_↭_ : IRel (Vector A) _ +xs ↭ ys = Σ[ ρ ∈ Permutation _ _ ] (∀ i → xs (ρ ⟨$⟩ʳ i) ≡ ys i) From a023d08fa865a210ee1a6e654c3da9ee9b9466c8 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Sat, 19 Aug 2023 22:59:34 +0200 Subject: [PATCH 02/12] added one line to CHANGELOG --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 00fd42c4c8..4843ac328a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3352,6 +3352,7 @@ This is a full list of proofs that have changed form to use irrelevant instance c ≈⟨ c≈d ⟩ d ∎ ``` + * Added module `Data.Vec.Functional.Relation.Binary.Permutation`: ```agda _↭_ : IRel (Vector A) _ From a9898bd663c5638bda5309c95bc3160182d21475 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Sun, 20 Aug 2023 13:02:54 +0200 Subject: [PATCH 03/12] added permutation properties --- CHANGELOG.md | 8 ++++ .../Binary/Permutation/Properties.agda | 44 +++++++++++++++++++ 2 files changed, 52 insertions(+) create mode 100644 src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 4843ac328a..33be07433f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3357,3 +3357,11 @@ This is a full list of proofs that have changed form to use irrelevant instance ```agda _↭_ : IRel (Vector A) _ ``` + +* Added new file `Data.Vec.Functional.Relation.Binary.Permutation.Properties`: + ```agda + ↭-refl : xs ↭ xs + ↭-reflexive : xs ≡ ys → xs ↭ ys + ↭-sym : xs ↭ ys → ys ↭ xs + ↭-trans : xs ↭ ys → ys ↭ zs → xs ↭ zs + ``` diff --git a/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda b/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda new file mode 100644 index 0000000000..adc7c7dd6d --- /dev/null +++ b/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda @@ -0,0 +1,44 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of permutation +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.Vec.Functional.Relation.Binary.Permutation.Properties where + +open import Level using (Level) +open import Data.Product using (_,_; proj₁; proj₂) +open import Data.Nat using (ℕ) +open import Data.Fin.Permutation using (id; flip; _⟨$⟩ʳ_; inverseʳ; _∘ₚ_) +open import Data.Vec.Functional +open import Data.Vec.Functional.Relation.Binary.Permutation +open import Relation.Binary.PropositionalEquality + using (refl; trans; _≡_; cong; module ≡-Reasoning) + +open ≡-Reasoning + +private + variable + ℓ : Level + A : Set ℓ + n : ℕ + xs ys zs : Vector A n + +↭-refl : xs ↭ xs +↭-refl = id , λ _ → refl + +↭-reflexive : xs ≡ ys → xs ↭ ys +↭-reflexive refl = ↭-refl + +↭-sym : xs ↭ ys → ys ↭ xs +proj₁ (↭-sym (xs↭ys , _)) = flip xs↭ys +proj₂ (↭-sym {xs = xs} {ys = ys} (xs↭ys , xs↭ys≡)) i = begin + ys (flip xs↭ys ⟨$⟩ʳ i) ≡˘⟨ xs↭ys≡ _ ⟩ + xs (xs↭ys ⟨$⟩ʳ (flip xs↭ys ⟨$⟩ʳ i)) ≡⟨ cong xs (inverseʳ xs↭ys) ⟩ + xs i ∎ + +↭-trans : xs ↭ ys → ys ↭ zs → xs ↭ zs +proj₁ (↭-trans (xs↭ys , _) (ys↭zs , _)) = ys↭zs ∘ₚ xs↭ys +proj₂ (↭-trans (_ , xs↭ys) (_ , ys↭zs)) _ = trans (xs↭ys _) (ys↭zs _) From 219913cb612ef7b7594f64fbbff20215d99a2076 Mon Sep 17 00:00:00 2001 From: Guilherme Silva Date: Sun, 11 Feb 2024 20:42:53 +0100 Subject: [PATCH 04/12] Added Base to imports Co-authored-by: Nathan van Doorn --- .../Functional/Relation/Binary/Permutation/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda b/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda index adc7c7dd6d..70e46425e9 100644 --- a/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda +++ b/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda @@ -9,8 +9,8 @@ module Data.Vec.Functional.Relation.Binary.Permutation.Properties where open import Level using (Level) -open import Data.Product using (_,_; proj₁; proj₂) -open import Data.Nat using (ℕ) +open import Data.Product.Base using (_,_; proj₁; proj₂) +open import Data.Nat.Base using (ℕ) open import Data.Fin.Permutation using (id; flip; _⟨$⟩ʳ_; inverseʳ; _∘ₚ_) open import Data.Vec.Functional open import Data.Vec.Functional.Relation.Binary.Permutation From 1745594447e784f5ccafb60ee8fa905424339dd2 Mon Sep 17 00:00:00 2001 From: Guilherme Silva Date: Sun, 11 Feb 2024 20:43:15 +0100 Subject: [PATCH 05/12] Added Base to import Co-authored-by: Nathan van Doorn --- src/Data/Vec/Functional/Relation/Binary/Permutation.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Vec/Functional/Relation/Binary/Permutation.agda b/src/Data/Vec/Functional/Relation/Binary/Permutation.agda index c220a8833c..4dfd9518a3 100644 --- a/src/Data/Vec/Functional/Relation/Binary/Permutation.agda +++ b/src/Data/Vec/Functional/Relation/Binary/Permutation.agda @@ -9,7 +9,7 @@ module Data.Vec.Functional.Relation.Binary.Permutation where open import Level using (Level) -open import Data.Product using (Σ-syntax) +open import Data.Product.Base using (Σ-syntax) open import Data.Fin.Permutation using (Permutation; _⟨$⟩ʳ_) open import Data.Vec.Functional using (Vector) open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel) From 370a1699acf9eb2e735857ebcd9613a145b755ae Mon Sep 17 00:00:00 2001 From: Guilherme Silva Date: Sun, 11 Feb 2024 20:43:31 +0100 Subject: [PATCH 06/12] Added core to import Co-authored-by: Nathan van Doorn --- src/Data/Vec/Functional/Relation/Binary/Permutation.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Vec/Functional/Relation/Binary/Permutation.agda b/src/Data/Vec/Functional/Relation/Binary/Permutation.agda index 4dfd9518a3..58ee430d86 100644 --- a/src/Data/Vec/Functional/Relation/Binary/Permutation.agda +++ b/src/Data/Vec/Functional/Relation/Binary/Permutation.agda @@ -13,7 +13,7 @@ open import Data.Product.Base using (Σ-syntax) open import Data.Fin.Permutation using (Permutation; _⟨$⟩ʳ_) open import Data.Vec.Functional using (Vector) open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel) -open import Relation.Binary.PropositionalEquality using (_≡_) +open import Relation.Binary.PropositionalEquality.Core using (_≡_) private variable From ec6776255cb1d40611627ba890689ab90519a482 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Sun, 11 Feb 2024 20:49:17 +0100 Subject: [PATCH 07/12] added definitions --- .../Relation/Binary/Permutation/Properties.agda | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda b/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda index 70e46425e9..143c9d0b5d 100644 --- a/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda +++ b/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda @@ -16,6 +16,7 @@ open import Data.Vec.Functional open import Data.Vec.Functional.Relation.Binary.Permutation open import Relation.Binary.PropositionalEquality using (refl; trans; _≡_; cong; module ≡-Reasoning) +open import Relation.Binary.Indexed.Heterogeneous.Definitions open ≡-Reasoning @@ -26,19 +27,19 @@ private n : ℕ xs ys zs : Vector A n -↭-refl : xs ↭ xs +↭-refl : Reflexive (Vector A) _↭_ ↭-refl = id , λ _ → refl ↭-reflexive : xs ≡ ys → xs ↭ ys ↭-reflexive refl = ↭-refl -↭-sym : xs ↭ ys → ys ↭ xs +↭-sym : Symmetric (Vector A) _↭_ proj₁ (↭-sym (xs↭ys , _)) = flip xs↭ys -proj₂ (↭-sym {xs = xs} {ys = ys} (xs↭ys , xs↭ys≡)) i = begin +proj₂ (↭-sym {x = xs} {ys} (xs↭ys , xs↭ys≡)) i = begin ys (flip xs↭ys ⟨$⟩ʳ i) ≡˘⟨ xs↭ys≡ _ ⟩ xs (xs↭ys ⟨$⟩ʳ (flip xs↭ys ⟨$⟩ʳ i)) ≡⟨ cong xs (inverseʳ xs↭ys) ⟩ xs i ∎ -↭-trans : xs ↭ ys → ys ↭ zs → xs ↭ zs +↭-trans : Transitive (Vector A) _↭_ proj₁ (↭-trans (xs↭ys , _) (ys↭zs , _)) = ys↭zs ∘ₚ xs↭ys proj₂ (↭-trans (_ , xs↭ys) (_ , ys↭zs)) _ = trans (xs↭ys _) (ys↭zs _) From 349e4083e6fe30be9f1dd0a433c0d93e8d477371 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Sun, 11 Feb 2024 23:22:02 +0100 Subject: [PATCH 08/12] removed unnecessary zs --- .../Vec/Functional/Relation/Binary/Permutation/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda b/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda index 143c9d0b5d..df5970dff3 100644 --- a/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda +++ b/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda @@ -25,7 +25,7 @@ private ℓ : Level A : Set ℓ n : ℕ - xs ys zs : Vector A n + xs ys : Vector A n ↭-refl : Reflexive (Vector A) _↭_ ↭-refl = id , λ _ → refl From 603cec1c9c7b10e65265ee552ef59d73771527b6 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 12 Feb 2024 10:25:57 +0100 Subject: [PATCH 09/12] renamed types in changelog --- CHANGELOG.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 33be07433f..aa219385bf 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3360,8 +3360,8 @@ This is a full list of proofs that have changed form to use irrelevant instance * Added new file `Data.Vec.Functional.Relation.Binary.Permutation.Properties`: ```agda - ↭-refl : xs ↭ xs + ↭-refl : Reflexive (Vector A) _↭_ ↭-reflexive : xs ≡ ys → xs ↭ ys - ↭-sym : xs ↭ ys → ys ↭ xs - ↭-trans : xs ↭ ys → ys ↭ zs → xs ↭ zs + ↭-sym : Symmetric (Vector A) _↭_ + ↭-trans : Transitive (Vector A) _↭_ ``` From b68ce5454c841fe2b7419c097c1c6f8f7afc29a0 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 12 Feb 2024 13:51:00 +0100 Subject: [PATCH 10/12] removed unnecessary code --- CHANGELOG.md | 832 +-------------------------------------------------- 1 file changed, 1 insertion(+), 831 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 23e4964a0a..4bf5a6e13d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -123,836 +123,6 @@ Additions to existing modules nonZeroDivisor : DivMod dividend divisor → NonZero divisor ``` -* Added new proofs in `Data.Nat.Properties`: - ```agda - m≤n+o⇒m∸n≤o : ∀ m n {o} → m ≤ n + o → m ∸ n ≤ o - m>=_ : Vec A n → (A → Vec B n) → Vec B n - join : Vec (Vec A n) n → Vec A n - - _ʳ++_ : Vec A m → Vec A n → Vec A (m + n) - - cast : .(eq : m ≡ n) → Vec A m → Vec A n - ``` - -* Added new instance in `Data.Vec.Categorical`: - ```agda - monad : RawMonad (λ (A : Set a) → Vec A n) - ``` - -* Added new proofs in `Data.Vec.Properties`: - ```agda - padRight-refl : padRight ≤-refl a xs ≡ xs - padRight-replicate : replicate a ≡ padRight le a (replicate a) - padRight-trans : padRight (≤-trans m≤n n≤p) a xs ≡ padRight n≤p a (padRight m≤n a xs) - - truncate-refl : truncate ≤-refl xs ≡ xs - truncate-trans : truncate (≤-trans m≤n n≤p) xs ≡ truncate m≤n (truncate n≤p xs) - truncate-padRight : truncate m≤n (padRight m≤n a xs) ≡ xs - - map-const : map (const x) xs ≡ replicate x - map-⊛ : map f xs ⊛ map g xs ≡ map (f ˢ g) xs - map-++ : map f (xs ++ ys) ≡ map f xs ++ map f ys - map-is-foldr : map f ≗ foldr (Vec B) (λ x ys → f x ∷ ys) [] - map-∷ʳ : map f (xs ∷ʳ x) ≡ (map f xs) ∷ʳ (f x) - map-reverse : map f (reverse xs) ≡ reverse (map f xs) - map-ʳ++ : map f (xs ʳ++ ys) ≡ map f xs ʳ++ map f ys - map-insert : map f (insert xs i x) ≡ insert (map f xs) i (f x) - toList-map : toList (map f xs) ≡ List.map f (toList xs) - - lookup-concat : lookup (concat xss) (combine i j) ≡ lookup (lookup xss i) j - - ⊛-is->>= : fs ⊛ xs ≡ fs >>= flip map xs - lookup-⊛* : lookup (fs ⊛* xs) (combine i j) ≡ (lookup fs i $ lookup xs j) - ++-is-foldr : xs ++ ys ≡ foldr ((Vec A) ∘ (_+ n)) _∷_ ys xs - []≔-++-↑ʳ : (xs ++ ys) [ m ↑ʳ i ]≔ y ≡ xs ++ (ys [ i ]≔ y) - unfold-ʳ++ : xs ʳ++ ys ≡ reverse xs ++ ys - - foldl-universal : ∀ (h : ∀ {c} (C : ℕ → Set c) (g : FoldlOp A C) (e : C zero) → ∀ {n} → Vec A n → C n) → - (∀ ... → h C g e [] ≡ e) → - (∀ ... → h C g e ∘ (x ∷_) ≗ h (C ∘ suc) g (g e x)) → - h B f e ≗ foldl B f e - foldl-fusion : h d ≡ e → (∀ ... → h (f b x) ≡ g (h b) x) → h ∘ foldl B f d ≗ foldl C g e - foldl-∷ʳ : foldl B f e (ys ∷ʳ y) ≡ f (foldl B f e ys) y - foldl-[] : foldl B f e [] ≡ e - foldl-reverse : foldl B {n} f e ∘ reverse ≗ foldr B (flip f) e - - foldr-[] : foldr B f e [] ≡ e - foldr-++ : foldr B f e (xs ++ ys) ≡ foldr (B ∘ (_+ n)) f (foldr B f e ys) xs - foldr-∷ʳ : foldr B f e (ys ∷ʳ y) ≡ foldr (B ∘ suc) f (f y e) ys - foldr-ʳ++ : foldr B f e (xs ʳ++ ys) ≡ foldl (B ∘ (_+ n)) (flip f) (foldr B f e ys) xs - foldr-reverse : foldr B f e ∘ reverse ≗ foldl B (flip f) e - - ∷ʳ-injective : xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y - ∷ʳ-injectiveˡ : xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys - ∷ʳ-injectiveʳ : xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y - - reverse-∷ : reverse (x ∷ xs) ≡ reverse xs ∷ʳ x - reverse-involutive : Involutive _≡_ reverse - reverse-reverse : reverse xs ≡ ys → reverse ys ≡ xs - reverse-injective : reverse xs ≡ reverse ys → xs ≡ ys - - transpose-replicate : transpose (replicate xs) ≡ map replicate xs - toList-replicate : toList (replicate {n = n} a) ≡ List.replicate n a - - toList-++ : toList (xs ++ ys) ≡ toList xs List.++ toList ys - - toList-cast : toList (cast eq xs) ≡ toList xs - cast-is-id : cast eq xs ≡ xs - subst-is-cast : subst (Vec A) eq xs ≡ cast eq xs - cast-trans : cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs - map-cast : map f (cast eq xs) ≡ cast eq (map f xs) - lookup-cast : lookup (cast eq xs) (Fin.cast eq i) ≡ lookup xs i - lookup-cast₁ : lookup (cast eq xs) i ≡ lookup xs (Fin.cast (sym eq) i) - lookup-cast₂ : lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i - - zipwith-++ : zipWith f (xs ++ ys) (xs' ++ ys') ≡ zipWith f xs xs' ++ zipWith f ys ys' - ``` - -* Added new proofs in `Data.Vec.Membership.Propositional.Properties`: - ```agda - index-∈-fromList⁺ : Any.index (∈-fromList⁺ v∈xs) ≡ indexₗ v∈xs - ``` - -* Added new proofs in `Data.Vec.Functional.Properties`: - ``` - map-updateAt : f ∘ g ≗ h ∘ f → map f (updateAt i g xs) ≗ updateAt i h (map f xs) - ``` - -* Added new proofs in `Data.Vec.Relation.Binary.Lex.Strict`: - ```agda - xs≮[] : ∀ {n} (xs : Vec A n) → ¬ xs < [] - <-respectsˡ : IsPartialEquivalence _≈_ → _≺_ Respectsˡ _≈_ → - ∀ {m n} → _Respectsˡ_ (_<_ {m} {n}) _≋_ - <-respectsʳ : IsPartialEquivalence _≈_ → _≺_ Respectsʳ _≈_ → - ∀ {m n} → _Respectsʳ_ (_<_ {m} {n}) _≋_ - <-wellFounded : Symmetric _≈_ → Transitive _≈_ → _≺_ Respectsʳ _≈_ → WellFounded _≺_ → - ∀ {n} → WellFounded (_<_ {n}) -``` - -* Added new functions in `Data.Vec.Relation.Unary.Any`: - ``` - lookup : Any P xs → A - ``` - -* Added new functions in `Data.Vec.Relation.Unary.All`: - ``` - decide : Π[ P ∪ Q ] → Π[ All P ∪ Any Q ] - ``` - -* Added vector associativity proof to `Data.Vec.Relation.Binary.Equality.Setoid`: - ``` - ++-assoc : (xs ++ ys) ++ zs ≋ xs ++ (ys ++ zs) - ``` - -* Added new functions in `Effect.Monad.State`: - ``` - runState : State s a → s → a × s - evalState : State s a → s → a - execState : State s a → s → s - ``` - -* Added new proofs in `Function.Construct.Symmetry`: - ``` - bijective : Bijective ≈₁ ≈₂ f → Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ f⁻¹ - isBijection : IsBijection ≈₁ ≈₂ f → Congruent ≈₂ ≈₁ f⁻¹ → IsBijection ≈₂ ≈₁ f⁻¹ - isBijection-≡ : IsBijection ≈₁ _≡_ f → IsBijection _≡_ ≈₁ f⁻¹ - bijection : Bijection R S → Congruent IB.Eq₂._≈_ IB.Eq₁._≈_ f⁻¹ → Bijection S R - bijection-≡ : Bijection R (setoid B) → Bijection (setoid B) R - sym-⤖ : A ⤖ B → B ⤖ A - ``` - -* Added new operations in `Function.Strict`: - ``` - _!|>_ : (a : A) → (∀ a → B a) → B a - _!|>′_ : A → (A → B) → B - ``` - -* Added new definition to the `Surjection` module in `Function.Related.Surjection`: - ``` - f⁻ = proj₁ ∘ surjective - ``` - -* Added new operations in `IO`: - ``` - Colist.forM : Colist A → (A → IO B) → IO (Colist B) - Colist.forM′ : Colist A → (A → IO B) → IO ⊤ - - List.forM : List A → (A → IO B) → IO (List B) - List.forM′ : List A → (A → IO B) → IO ⊤ - ``` - -* Added new operations in `IO.Base`: - ``` - lift! : IO A → IO (Lift b A) - _<$_ : B → IO A → IO B - _=<<_ : (A → IO B) → IO A → IO B - _<<_ : IO B → IO A → IO B - lift′ : Prim.IO ⊤ → IO {a} ⊤ - - when : Bool → IO ⊤ → IO ⊤ - unless : Bool → IO ⊤ → IO ⊤ - - whenJust : Maybe A → (A → IO ⊤) → IO ⊤ - untilJust : IO (Maybe A) → IO A - untilRight : (A → IO (A ⊎ B)) → A → IO B - ``` - -* Added new functions in `Reflection.AST.Term`: - ``` - stripPis : Term → List (String × Arg Type) × Term - prependLams : List (String × Visibility) → Term → Term - prependHLams : List String → Term → Term - prependVLams : List String → Term → Term - ``` - -* Added new operations in `Relation.Binary.Construct.Closure.Equivalence`: - ``` - fold : IsEquivalence _∼_ → _⟶_ ⇒ _∼_ → EqClosure _⟶_ ⇒ _∼_ - gfold : IsEquivalence _∼_ → _⟶_ =[ f ]⇒ _∼_ → EqClosure _⟶_ =[ f ]⇒ _∼_ - return : _⟶_ ⇒ EqClosure _⟶_ - join : EqClosure (EqClosure _⟶_) ⇒ EqClosure _⟶_ - _⋆ : _⟶₁_ ⇒ EqClosure _⟶₂_ → EqClosure _⟶₁_ ⇒ EqClosure _⟶₂_ - ``` - -* Added new operations in `Relation.Binary.Construct.Closure.Symmetric`: - ``` - fold : Symmetric _∼_ → _⟶_ ⇒ _∼_ → SymClosure _⟶_ ⇒ _∼_ - gfold : Symmetric _∼_ → _⟶_ =[ f ]⇒ _∼_ → SymClosure _⟶_ =[ f ]⇒ _∼_ - return : _⟶_ ⇒ SymClosure _⟶_ - join : SymClosure (SymClosure _⟶_) ⇒ SymClosure _⟶_ - _⋆ : _⟶₁_ ⇒ SymClosure _⟶₂_ → SymClosure _⟶₁_ ⇒ SymClosure _⟶₂_ - ``` - -* Added new proofs to `Relation.Binary.Lattice.Properties.{Join,Meet}Semilattice`: - ```agda - isPosemigroup : IsPosemigroup _≈_ _≤_ _∨_ - posemigroup : Posemigroup c ℓ₁ ℓ₂ - ≈-dec⇒≤-dec : Decidable _≈_ → Decidable _≤_ - ≈-dec⇒isDecPartialOrder : Decidable _≈_ → IsDecPartialOrder _≈_ _≤_ - ``` - -* Added new proofs to `Relation.Binary.Lattice.Properties.Bounded{Join,Meet}Semilattice`: - ```agda - isCommutativePomonoid : IsCommutativePomonoid _≈_ _≤_ _∨_ ⊥ - commutativePomonoid : CommutativePomonoid c ℓ₁ ℓ₂ - ``` - -* Added new proofs to `Relation.Binary.Properties.Poset`: - ```agda - ≤-dec⇒≈-dec : Decidable _≤_ → Decidable _≈_ - ≤-dec⇒isDecPartialOrder : Decidable _≤_ → IsDecPartialOrder _≈_ _≤_ - ``` - -* Added new proofs in `Relation.Binary.Properties.StrictPartialOrder`: - ```agda - >-strictPartialOrder : StrictPartialOrder s₁ s₂ s₃ - ``` - -* Added new proofs in `Relation.Binary.PropositionalEquality.Properties`: - ``` - subst-application′ : subst Q eq (f x p) ≡ f y (subst P eq p) - sym-cong : sym (cong f p) ≡ cong f (sym p) - ``` - -* Added new proofs in `Relation.Binary.HeterogeneousEquality`: - ``` - subst₂-removable : subst₂ _∼_ eq₁ eq₂ p ≅ p - ``` - -* Added new definitions in `Relation.Unary`: - ``` - _≐_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _ - _≐′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _ - _∖_ : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _ - ``` - -* Added new proofs in `Relation.Unary.Properties`: - ``` - ⊆-reflexive : _≐_ ⇒ _⊆_ - ⊆-antisym : Antisymmetric _≐_ _⊆_ - ⊆-min : Min _⊆_ ∅ - ⊆-max : Max _⊆_ U - ⊂⇒⊆ : _⊂_ ⇒ _⊆_ - ⊂-trans : Trans _⊂_ _⊂_ _⊂_ - ⊂-⊆-trans : Trans _⊂_ _⊆_ _⊂_ - ⊆-⊂-trans : Trans _⊆_ _⊂_ _⊂_ - ⊂-respʳ-≐ : _⊂_ Respectsʳ _≐_ - ⊂-respˡ-≐ : _⊂_ Respectsˡ _≐_ - ⊂-resp-≐ : _⊂_ Respects₂ _≐_ - ⊂-irrefl : Irreflexive _≐_ _⊂_ - ⊂-antisym : Antisymmetric _≐_ _⊂_ - ∅-⊆′ : (P : Pred A ℓ) → ∅ ⊆′ P - ⊆′-U : (P : Pred A ℓ) → P ⊆′ U - ⊆′-refl : Reflexive {A = Pred A ℓ} _⊆′_ - ⊆′-reflexive : _≐′_ ⇒ _⊆′_ - ⊆′-trans : Trans _⊆′_ _⊆′_ _⊆′_ - ⊆′-antisym : Antisymmetric _≐′_ _⊆′_ - ⊆′-min : Min _⊆′_ ∅ - ⊆′-max : Max _⊆′_ U - ⊂′⇒⊆′ : _⊂′_ ⇒ _⊆′_ - ⊂′-trans : Trans _⊂′_ _⊂′_ _⊂′_ - ⊂′-⊆′-trans : Trans _⊂′_ _⊆′_ _⊂′_ - ⊆′-⊂′-trans : Trans _⊆′_ _⊂′_ _⊂′_ - ⊂′-respʳ-≐′ : _⊂′_ Respectsʳ _≐′_ - ⊂′-respˡ-≐′ : _⊂′_ Respectsˡ _≐′_ - ⊂′-resp-≐′ : _⊂′_ Respects₂ _≐′_ - ⊂′-irrefl : Irreflexive _≐′_ _⊂′_ - ⊂′-antisym : Antisymmetric _≐′_ _⊂′_ - ⊆⇒⊆′ : _⊆_ ⇒ _⊆′_ - ⊆′⇒⊆ : _⊆′_ ⇒ _⊆_ - ⊂⇒⊂′ : _⊂_ ⇒ _⊂′_ - ⊂′⇒⊂ : _⊂′_ ⇒ _⊂_ - ≐-refl : Reflexive _≐_ - ≐-sym : Sym _≐_ _≐_ - ≐-trans : Trans _≐_ _≐_ _≐_ - ≐′-refl : Reflexive _≐′_ - ≐′-sym : Sym _≐′_ _≐′_ - ≐′-trans : Trans _≐′_ _≐′_ _≐′_ - ≐⇒≐′ : _≐_ ⇒ _≐′_ - ≐′⇒≐ : _≐′_ ⇒ _≐_ - - U-irrelevant : Irrelevant {A = A} U - ∁-irrelevant : (P : Pred A ℓ) → Irrelevant (∁ P) - ``` - -* Generalised proofs in `Relation.Unary.Properties`: - ``` - ⊆-trans : Trans _⊆_ _⊆_ _⊆_ - ``` - -* Added new proofs in `Relation.Binary.Properties.Setoid`: - ``` - ≈-isPreorder : IsPreorder _≈_ _≈_ - ≈-isPartialOrder : IsPartialOrder _≈_ _≈_ - - ≈-preorder : Preorder a ℓ ℓ - ≈-poset : Poset a ℓ ℓ - ``` - -* Added new definitions in `Relation.Binary.Definitions`: - ``` - Cotransitive _#_ = ∀ {x y} → x # y → ∀ z → (x # z) ⊎ (z # y) - Tight _≈_ _#_ = ∀ x y → (¬ x # y → x ≈ y) × (x ≈ y → ¬ x # y) - - Monotonic₁ _≤_ _⊑_ f = f Preserves _≤_ ⟶ _⊑_ - Antitonic₁ _≤_ _⊑_ f = f Preserves (flip _≤_) ⟶ _⊑_ - Monotonic₂ _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ _≤_ ⟶ _⊑_ ⟶ _≼_ - MonotonicAntitonic _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ _≤_ ⟶ (flip _⊑_) ⟶ _≼_ - AntitonicMonotonic _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ (flip _≤_) ⟶ _⊑_ ⟶ _≼_ - Antitonic₂ _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ (flip _≤_) ⟶ (flip _⊑_) ⟶ _≼_ - Adjoint _≤_ _⊑_ f g = ∀ {x y} → (f x ⊑ y → x ≤ g y) × (x ≤ g y → f x ⊑ y) - ``` - -* Added new definitions in `Relation.Binary.Bundles`: - ``` - record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - ``` - -* Added new definitions in `Relation.Binary.Structures`: - ``` - record IsApartnessRelation (_#_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where - ``` - -* Added new proofs to `Relation.Binary.Consequences`: - ``` - sym⇒¬-sym : Symmetric _∼_ → Symmetric _≁_ - cotrans⇒¬-trans : Cotransitive _∼_ → Transitive _≁_ - irrefl⇒¬-refl : Reflexive _≈_ → Irreflexive _≈_ _∼_ → Reflexive _≁_ - mono₂⇒cong₂ : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ → ∀ {f} → - f Preserves₂ ≤₁ ⟶ ≤₁ ⟶ ≤₂ → - f Preserves₂ ≈₁ ⟶ ≈₁ ⟶ ≈₂ - ``` - -* Added new operations in `Relation.Binary.PropositionalEquality.Properties`: - ``` - J : (B : (y : A) → x ≡ y → Set b) (p : x ≡ y) → B x refl → B y p - dcong : (p : x ≡ y) → subst B p (f x) ≡ f y - dcong₂ : (p : x₁ ≡ x₂) → subst B p y₁ ≡ y₂ → f x₁ y₁ ≡ f x₂ y₂ - dsubst₂ : (p : x₁ ≡ x₂) → subst B p y₁ ≡ y₂ → C x₁ y₁ → C x₂ y₂ - ddcong₂ : (p : x₁ ≡ x₂) (q : subst B p y₁ ≡ y₂) → dsubst₂ C p q (f x₁ y₁) ≡ f x₂ y₂ - - isPartialOrder : IsPartialOrder _≡_ _≡_ - poset : Set a → Poset _ _ _ - ``` - -* Added new operations in `System.Exit`: - ``` - isSuccess : ExitCode → Bool - isFailure : ExitCode → Bool - ``` - -* Added new functions in `Codata.Guarded.Stream`: - ``` - transpose : List (Stream A) → Stream (List A) - transpose⁺ : List⁺ (Stream A) → Stream (List⁺ A) - concat : Stream (List⁺ A) → Stream A - ``` - -* Added new proofs in `Codata.Guarded.Stream.Properties`: - ``` - cong-concat : {ass bss : Stream (List⁺.List⁺ A)} → ass ≈ bss → concat ass ≈ concat bss - map-concat : ∀ (f : A → B) ass → map f (concat ass) ≈ concat (map (List⁺.map f) ass) - lookup-transpose : ∀ n (ass : List (Stream A)) → lookup n (transpose ass) ≡ List.map (lookup n) ass - lookup-transpose⁺ : ∀ n (ass : List⁺ (Stream A)) → lookup n (transpose⁺ ass) ≡ List⁺.map (lookup n) ass - ``` - -* Added new corollaries in `Data.List.Membership.Setoid.Properties`: - ``` - ∈-++⁺∘++⁻ : ∀ {v} xs {ys} (p : v ∈ xs ++ ys) → [ ∈-++⁺ˡ , ∈-++⁺ʳ xs ]′ (∈-++⁻ xs p) ≡ p - ∈-++⁻∘++⁺ : ∀ {v} xs {ys} (p : v ∈ xs ⊎ v ∈ ys) → ∈-++⁻ xs ([ ∈-++⁺ˡ , ∈-++⁺ʳ xs ]′ p) ≡ p - ∈-++↔ : ∀ {v xs ys} → (v ∈ xs ⊎ v ∈ ys) ↔ v ∈ xs ++ ys - ∈-++-comm : ∀ {v} xs ys → v ∈ xs ++ ys → v ∈ ys ++ xs - ∈-++-comm∘++-comm : ∀ {v} xs {ys} (p : v ∈ xs ++ ys) → ∈-++-comm ys xs (∈-++-comm xs ys p) ≡ p - ∈-++↔++ : ∀ {v} xs ys → v ∈ xs ++ ys ↔ v ∈ ys ++ xs - ``` - -* Exposed container combinator conversion functions from `Data.Container.Combinator.Properties` separate from their correctness proofs in `Data.Container.Combinator`: - ``` - to-id : F.id A → ⟦ id ⟧ A - from-id : ⟦ id ⟧ A → F.id A - to-const : (A : Set s) → A → ⟦ const A ⟧ B - from-const : (A : Set s) → ⟦ const A ⟧ B → A - to-∘ : (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) → ⟦ C₁ ⟧ (⟦ C₂ ⟧ A) → ⟦ C₁ ∘ C₂ ⟧ A - from-∘ : (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) → ⟦ C₁ ∘ C₂ ⟧ A → ⟦ C₁ ⟧ (⟦ C₂ ⟧ A) - to-× : (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) → ⟦ C₁ ⟧ A P.× ⟦ C₂ ⟧ A → ⟦ C₁ × C₂ ⟧ A - from-× : (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) → ⟦ C₁ × C₂ ⟧ A → ⟦ C₁ ⟧ A P.× ⟦ C₂ ⟧ A - to-Π : (I : Set i) (Cᵢ : I → Container s p) → (∀ i → ⟦ Cᵢ i ⟧ A) → ⟦ Π I Cᵢ ⟧ A - from-Π : (I : Set i) (Cᵢ : I → Container s p) → ⟦ Π I Cᵢ ⟧ A → ∀ i → ⟦ Cᵢ i ⟧ A - to-⊎ : (C₁ : Container s₁ p) (C₂ : Container s₂ p) → ⟦ C₁ ⟧ A S.⊎ ⟦ C₂ ⟧ A → ⟦ C₁ ⊎ C₂ ⟧ A - from-⊎ : (C₁ : Container s₁ p) (C₂ : Container s₂ p) → ⟦ C₁ ⊎ C₂ ⟧ A → ⟦ C₁ ⟧ A S.⊎ ⟦ C₂ ⟧ A - to-Σ : (I : Set i) (C : I → Container s p) → (∃ λ i → ⟦ C i ⟧ A) → ⟦ Σ I C ⟧ A - from-Σ : (I : Set i) (C : I → Container s p) → ⟦ Σ I C ⟧ A → ∃ λ i → ⟦ C i ⟧ A - ``` - -* Added a non-dependent version of `Function.Base.flip` due to an issue noted in - Pull Request #1812: - ```agda - flip′ : (A → B → C) → (B → A → C) - ``` - -* Added new proofs to `Data.List.Properties` - ```agda - cartesianProductWith-zeroˡ : cartesianProductWith f [] ys ≡ [] - cartesianProductWith-zeroʳ : cartesianProductWith f xs [] ≡ [] - cartesianProductWith-distribʳ-++ : cartesianProductWith f (xs ++ ys) zs ≡ - cartesianProductWith f xs zs ++ cartesianProductWith f ys zs - foldr-map : foldr f x (map g xs) ≡ foldr (g -⟨ f ∣) x xs - foldl-map : foldl f x (map g xs) ≡ foldl (∣ f ⟩- g) x xs - ``` - -NonZero/Positive/Negative changes ---------------------------------- - -This is a full list of proofs that have changed form to use irrelevant instance arguments: - -* In `Data.Nat.Base`: - ``` - ≢-nonZero⁻¹ : ∀ {n} → .(NonZero n) → n ≢ 0 - >-nonZero⁻¹ : ∀ {n} → .(NonZero n) → n > 0 - ``` - -* In `Data.Nat.Properties`: - ``` - *-cancelʳ-≡ : ∀ m n {o} → m * suc o ≡ n * suc o → m ≡ n - *-cancelˡ-≡ : ∀ {m n} o → suc o * m ≡ suc o * n → m ≡ n - *-cancelʳ-≤ : ∀ m n o → m * suc o ≤ n * suc o → m ≤ n - *-cancelˡ-≤ : ∀ {m n} o → suc o * m ≤ suc o * n → m ≤ n - *-monoˡ-< : ∀ n → (_* suc n) Preserves _<_ ⟶ _<_ - *-monoʳ-< : ∀ n → (suc n *_) Preserves _<_ ⟶ _<_ - - m≤m*n : ∀ m {n} → 0 < n → m ≤ m * n - m≤n*m : ∀ m {n} → 0 < n → m ≤ n * m - m⇒∤ : ∀ {m n} → m > suc n → m ∤ suc n - *-cancelˡ-∣ : ∀ {i j} k → suc k * i ∣ suc k * j → i ∣ j - ``` - -* In `Data.Nat.DivMod`: - ``` - m≡m%n+[m/n]*n : ∀ m n → m ≡ m % suc n + (m / suc n) * suc n - m%n≡m∸m/n*n : ∀ m n → m % suc n ≡ m ∸ (m / suc n) * suc n - n%n≡0 : ∀ n → suc n % suc n ≡ 0 - m%n%n≡m%n : ∀ m n → m % suc n % suc n ≡ m % suc n - [m+n]%n≡m%n : ∀ m n → (m + suc n) % suc n ≡ m % suc n - [m+kn]%n≡m%n : ∀ m k n → (m + k * (suc n)) % suc n ≡ m % suc n - m*n%n≡0 : ∀ m n → (m * suc n) % suc n ≡ 0 - m%n 0ℤ - negative⁻¹ : ∀ {i} → Negative i → i < 0ℤ - nonPositive⁻¹ : ∀ {i} → NonPositive i → i ≤ 0ℤ - nonNegative⁻¹ : ∀ {i} → NonNegative i → i ≥ 0ℤ - negative_ - *-monoʳ-<-neg : ∀ n → (_* -[1+ n ]) Preserves _<_ ⟶ _>_ - *-cancelˡ-<-nonPos : ∀ n → NonPositive n → n * i < n * j → i > j - *-cancelʳ-<-nonPos : ∀ n → NonPositive n → i * n < j * n → i > j - - *-distribˡ-⊓-nonNeg : ∀ m j k → + m * (j ⊓ k) ≡ (+ m * j) ⊓ (+ m * k) - *-distribʳ-⊓-nonNeg : ∀ m j k → (j ⊓ k) * + m ≡ (j * + m) ⊓ (k * + m) - *-distribˡ-⊓-nonPos : ∀ i → NonPositive i → ∀ j k → i * (j ⊓ k) ≡ (i * j) ⊔ (i * k) - *-distribʳ-⊓-nonPos : ∀ i → NonPositive i → ∀ j k → (j ⊓ k) * i ≡ (j * i) ⊔ (k * i) - *-distribˡ-⊔-nonNeg : ∀ m j k → + m * (j ⊔ k) ≡ (+ m * j) ⊔ (+ m * k) - *-distribʳ-⊔-nonNeg : ∀ m j k → (j ⊔ k) * + m ≡ (j * + m) ⊔ (k * + m) - *-distribˡ-⊔-nonPos : ∀ i → NonPositive i → ∀ j k → i * (j ⊔ k) ≡ (i * j) ⊓ (i * k) - *-distribʳ-⊔-nonPos : ∀ i → NonPositive i → ∀ j k → (j ⊔ k) * i ≡ (j * i) ⊓ (k * i) - ``` - -* In `Data.Integer.Divisibility`: - ``` - *-cancelˡ-∣ : ∀ k {i j} → k ≢ + 0 → k * i ∣ k * j → i ∣ j - *-cancelʳ-∣ : ∀ k {i j} → k ≢ + 0 → i * k ∣ j * k → i ∣ j - ``` - -* In `Data.Integer.Divisibility.Signed`: - ``` - *-cancelˡ-∣ : ∀ k {i j} → k ≢ + 0 → k * i ∣ k * j → i ∣ j - *-cancelʳ-∣ : ∀ k {i j} → k ≢ + 0 → i * k ∣ j * k → i ∣ j - ``` - -* In `Data.Rational.Unnormalised.Properties`: - ```agda - positive⁻¹ : ∀ {q} → .(Positive q) → q > 0ℚᵘ - nonNegative⁻¹ : ∀ {q} → .(NonNegative q) → q ≥ 0ℚᵘ - negative⁻¹ : ∀ {q} → .(Negative q) → q < 0ℚᵘ - nonPositive⁻¹ : ∀ {q} → .(NonPositive q) → q ≤ 0ℚᵘ - positive⇒nonNegative : ∀ {p} → Positive p → NonNegative p - negative⇒nonPositive : ∀ {p} → Negative p → NonPositive p - negative_ - *-monoʳ-<-neg : ∀ r → Negative r → (r *_) Preserves _<_ ⟶ _>_ - - pos⇒1/pos : ∀ p (p>0 : Positive p) → Positive ((1/ p) {{pos⇒≢0 p p>0}}) - neg⇒1/neg : ∀ p (p<0 : Negative p) → Negative ((1/ p) {{neg⇒≢0 p p<0}}) - - *-distribʳ-⊓-nonNeg : ∀ p → NonNegative p → ∀ q r → (q ⊓ r) * p ≃ (q * p) ⊓ (r * p) - *-distribˡ-⊓-nonNeg : ∀ p → NonNegative p → ∀ q r → p * (q ⊓ r) ≃ (p * q) ⊓ (p * r) - *-distribˡ-⊔-nonNeg : ∀ p → NonNegative p → ∀ q r → p * (q ⊔ r) ≃ (p * q) ⊔ (p * r) - *-distribʳ-⊔-nonNeg : ∀ p → NonNegative p → ∀ q r → (q ⊔ r) * p ≃ (q * p) ⊔ (r * p) - *-distribˡ-⊔-nonPos : ∀ p → NonPositive p → ∀ q r → p * (q ⊔ r) ≃ (p * q) ⊓ (p * r) - *-distribʳ-⊔-nonPos : ∀ p → NonPositive p → ∀ q r → (q ⊔ r) * p ≃ (q * p) ⊓ (r * p) - *-distribˡ-⊓-nonPos : ∀ p → NonPositive p → ∀ q r → p * (q ⊓ r) ≃ (p * q) ⊔ (p * r) - *-distribʳ-⊓-nonPos : ∀ p → NonPositive p → ∀ q r → (q ⊓ r) * p ≃ (q * p) ⊔ (r * p) - ``` - -* In `Data.Rational.Properties`: - ``` - positive⁻¹ : Positive p → p > 0ℚ - nonNegative⁻¹ : NonNegative p → p ≥ 0ℚ - negative⁻¹ : Negative p → p < 0ℚ - nonPositive⁻¹ : NonPositive p → p ≤ 0ℚ - negative q - *-cancelʳ-<-nonPos : ∀ r → NonPositive r → ∀ {p q} → p * r < q * r → p > q - *-monoʳ-≤-nonNeg : ∀ r → NonNegative r → (_* r) Preserves _≤_ ⟶ _≤_ - *-monoˡ-≤-nonNeg : ∀ r → NonNegative r → (r *_) Preserves _≤_ ⟶ _≤_ - *-monoʳ-≤-nonPos : ∀ r → NonPositive r → (_* r) Preserves _≤_ ⟶ _≥_ - *-monoˡ-≤-nonPos : ∀ r → NonPositive r → (r *_) Preserves _≤_ ⟶ _≥_ - *-monoˡ-<-pos : ∀ r → Positive r → (_* r) Preserves _<_ ⟶ _<_ - *-monoʳ-<-pos : ∀ r → Positive r → (r *_) Preserves _<_ ⟶ _<_ - *-monoˡ-<-neg : ∀ r → Negative r → (_* r) Preserves _<_ ⟶ _>_ - *-monoʳ-<-neg : ∀ r → Negative r → (r *_) Preserves _<_ ⟶ _>_ - - *-distribˡ-⊓-nonNeg : ∀ p → NonNegative p → ∀ q r → p * (q ⊓ r) ≡ (p * q) ⊓ (p * r) - *-distribʳ-⊓-nonNeg : ∀ p → NonNegative p → ∀ q r → (q ⊓ r) * p ≡ (q * p) ⊓ (r * p) - *-distribˡ-⊔-nonNeg : ∀ p → NonNegative p → ∀ q r → p * (q ⊔ r) ≡ (p * q) ⊔ (p * r) - *-distribʳ-⊔-nonNeg : ∀ p → NonNegative p → ∀ q r → (q ⊔ r) * p ≡ (q * p) ⊔ (r * p) - *-distribˡ-⊔-nonPos : ∀ p → NonPositive p → ∀ q r → p * (q ⊔ r) ≡ (p * q) ⊓ (p * r) - *-distribʳ-⊔-nonPos : ∀ p → NonPositive p → ∀ q r → (q ⊔ r) * p ≡ (q * p) ⊓ (r * p) - *-distribˡ-⊓-nonPos : ∀ p → NonPositive p → ∀ q r → p * (q ⊓ r) ≡ (p * q) ⊔ (p * r) - *-distribʳ-⊓-nonPos : ∀ p → NonPositive p → ∀ q r → (q ⊓ r) * p ≡ (q * p) ⊔ (r * p) - - pos⇒1/pos : ∀ p (p>0 : Positive p) → Positive ((1/ p) {{pos⇒≢0 p p>0}}) - neg⇒1/neg : ∀ p (p<0 : Negative p) → Negative ((1/ p) {{neg⇒≢0 p p<0}}) - 1/pos⇒pos : ∀ p .{{_ : NonZero p}} → (1/p : Positive (1/ p)) → Positive p - 1/neg⇒neg : ∀ p .{{_ : NonZero p}} → (1/p : Negative (1/ p)) → Negative p - ``` - -* In `Data.List.NonEmpty.Base`: - ```agda - drop+ : ℕ → List⁺ A → List⁺ A - ``` - When drop+ping more than the size of the length of the list, the last element remains. - -* Added new proofs in `Data.List.NonEmpty.Properties`: - ```agda - length-++⁺ : length (xs ++⁺ ys) ≡ length xs + length ys - length-++⁺-tail : length (xs ++⁺ ys) ≡ suc (length xs + length (tail ys)) - ++-++⁺ : (xs ++ ys) ++⁺ zs ≡ xs ++⁺ ys ++⁺ zs - ++⁺-cancelˡ′ : xs ++⁺ zs ≡ ys ++⁺ zs′ → List.length xs ≡ List.length ys → zs ≡ zs′ - ++⁺-cancelˡ : xs ++⁺ ys ≡ xs ++⁺ zs → ys ≡ zs - drop+-++⁺ : drop+ (length xs) (xs ++⁺ ys) ≡ ys - map-++⁺-commute : map f (xs ++⁺ ys) ≡ map f xs ++⁺ map f ys - length-map : length (map f xs) ≡ length xs - map-cong : f ≗ g → map f ≗ map g - map-compose : map (g ∘ f) ≗ map g ∘ map f - ``` - -* Added new functions and proofs in `Data.Nat.GeneralisedArithmetic`: - ```agda - iterate : (A → A) → A → ℕ → A - iterate-is-fold : ∀ (z : A) s m → fold z s m ≡ iterate s z m - ``` - -* Added new proofs to `Function.Properties.Inverse`: - ```agda - Inverse⇒Injection : Inverse S T → Injection S T - ↔⇒↣ : A ↔ B → A ↣ B - ``` - -* Added a new isomorphism to `Data.Fin.Properties`: - ```agda - 2↔Bool : Fin 2 ↔ Bool - ``` - -* Added new isomorphisms to `Data.Unit.Polymorphic.Properties`: - ```agda - ⊤↔⊤* : ⊤ {ℓ} ↔ ⊤* - ``` - -* Added new isomorphisms to `Data.Vec.N-ary`: - ```agda - Vec↔N-ary : ∀ n → (Vec A n → B) ↔ N-ary n A B - ``` - -* Added new isomorphisms to `Data.Vec.Recursive`: - ```agda - lift↔ : ∀ n → A ↔ B → A ^ n ↔ B ^ n - Fin[m^n]↔Fin[m]^n : ∀ m n → Fin (m ^ n) ↔ Fin m Vec.^ n - ``` - -* Added new functions to `Function.Properties.Inverse`: - ```agda - ↔-refl : Reflexive _↔_ - ↔-sym : Symmetric _↔_ - ↔-trans : Transitive _↔_ - ``` - -* Added new isomorphisms to `Function.Properties.Inverse`: - ```agda - ↔-fun : A ↔ B → C ↔ D → (A → C) ↔ (B → D) - ``` - -* Added new function to `Data.Fin.Properties` - ```agda - i≤inject₁[j]⇒i≤1+j : i ≤ inject₁ j → i ≤ suc j - ``` - -* Added new function to `Data.Fin.Induction` - ```agda - <-weakInduction-startingFrom : P i → (∀ j → P (inject₁ j) → P (suc j)) → ∀ {j} → j ≥ i → P j - ``` - -* Added new module to `Data.Rational.Unnormalised.Properties` - ```agda - module ≃-Reasoning = SetoidReasoning ≃-setoid - ``` - -* Added new functions to `Data.Rational.Unnormalised.Properties` - ```agda - 0≠1 : 0ℚᵘ ≠ 1ℚᵘ - ≃-≠-irreflexive : Irreflexive _≃_ _≠_ - ≠-symmetric : Symmetric _≠_ - ≠-cotransitive : Cotransitive _≠_ - ≠⇒invertible : p ≠ q → Invertible _≃_ 1ℚᵘ _*_ (p - q) - ``` - -* Added new structures to `Data.Rational.Unnormalised.Properties` - ```agda - +-*-isHeytingCommutativeRing : IsHeytingCommutativeRing _≃_ _≠_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ - +-*-isHeytingField : IsHeytingField _≃_ _≠_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ - ``` - -* Added new bundles to `Data.Rational.Unnormalised.Properties` - ```agda - +-*-heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ - +-*-heytingField : HeytingField 0ℓ 0ℓ 0ℓ - ``` - -* Added new function to `Data.Vec.Relation.Binary.Pointwise.Inductive` - ```agda - cong-[_]≔ : Pointwise _∼_ xs ys → Pointwise _∼_ (xs [ i ]≔ p) (ys [ i ]≔ p) - ``` - -* Added new function to `Data.Vec.Relation.Binary.Equality.Setoid` - ```agda - map-[]≔ : map f (xs [ i ]≔ p) ≋ map f xs [ i ]≔ f p - ``` - -* Added new function to `Data.List.Relation.Binary.Permutation.Propositional.Properties` - ```agda - ↭-reverse : (xs : List A) → reverse xs ↭ xs - ``` - -* Added new functions to `Algebra.Properties.CommutativeMonoid` - ```agda - invertibleˡ⇒invertibleʳ : LeftInvertible _≈_ 0# _+_ x → RightInvertible _≈_ 0# _+_ x - invertibleʳ⇒invertibleˡ : RightInvertible _≈_ 0# _+_ x → LeftInvertible _≈_ 0# _+_ x - invertibleˡ⇒invertible : LeftInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x - invertibleʳ⇒invertible : RightInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x - ``` - -* Added new functions to `Algebra.Apartness.Bundles` - ```agda - invertibleˡ⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y - invertibleʳ⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y - x#0y#0→xy#0 : x # 0# → y # 0# → x * y # 0# - #-sym : Symmetric _#_ - #-congʳ : x ≈ y → x # z → y # z - #-congˡ : y ≈ z → x # y → x # z - ``` - -* Added new proofs to `Data.List.Relation.Binary.Sublist.Setoid.Properties` - and `Data.List.Relation.Unary.Sorted.TotalOrder.Properties`. - ```agda - ⊆-mergeˡ : ∀ xs ys → xs ⊆ merge _≤?_ xs ys - ⊆-mergeʳ : ∀ xs ys → ys ⊆ merge _≤?_ xs ys - ``` - -* Added new file `Relation.Binary.Reasoning.Base.Apartness` - - This is how to use it: - ```agda - _ : a # d - _ = begin-apartness - a ≈⟨ a≈b ⟩ - b #⟨ b#c ⟩ - c ≈⟨ c≈d ⟩ - d ∎ - ``` * In `Function.Bundles`, added `_⟶ₛ_` as a synonym for `Func` that can be used infix. @@ -967,4 +137,4 @@ This is a full list of proofs that have changed form to use irrelevant instance ↭-reflexive : xs ≡ ys → xs ↭ ys ↭-sym : Symmetric (Vector A) _↭_ ↭-trans : Transitive (Vector A) _↭_ - ``` \ No newline at end of file + ``` From cc83c8747bc8d102d97f070c496f7a26b95e9ff9 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 12 Feb 2024 13:53:44 +0100 Subject: [PATCH 11/12] added more to changelog --- CHANGELOG.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4bf5a6e13d..02a6448a6b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -123,6 +123,21 @@ Additions to existing modules nonZeroDivisor : DivMod dividend divisor → NonZero divisor ``` +* Added new proofs in `Data.Nat.Properties`: + ```agda + m≤n+o⇒m∸n≤o : ∀ m n {o} → m ≤ n + o → m ∸ n ≤ o + m Date: Mon, 12 Feb 2024 14:10:57 +0100 Subject: [PATCH 12/12] added end of changelog --- CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9d2a06119a..d38675a2f4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -198,4 +198,5 @@ Additions to existing modules ↭-refl : Reflexive (Vector A) _↭_ ↭-reflexive : xs ≡ ys → xs ↭ ys ↭-sym : Symmetric (Vector A) _↭_ - ↭-trans : Transitive (Vector A) _↭_ \ No newline at end of file + ↭-trans : Transitive (Vector A) _↭_ + ```