From e0c327dc7a7c9ebb79172e1139ebd97880df21d9 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 19 Sep 2023 10:15:21 +0100 Subject: [PATCH 01/28] removed `import` dependency --- src/Data/Fin/Base.agda | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index b591301ac0..199f3dbe0b 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -12,7 +12,6 @@ module Data.Fin.Base where open import Data.Bool.Base using (Bool; true; false; T; not) -open import Data.Empty using (⊥-elim) open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; z Date: Tue, 19 Sep 2023 10:26:06 +0100 Subject: [PATCH 02/28] two easy lemmas --- src/Data/Fin/Properties.agda | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index bcb1cd4745..b42904e8de 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -547,12 +547,21 @@ inject≤-idempotent {_} {suc n} {suc o} zero _ _ _ = refl inject≤-idempotent {_} {suc n} {suc o} (suc i) (s≤s m≤n) (s≤s n≤o) (s≤s m≤o) = cong suc (inject≤-idempotent i m≤n n≤o m≤o) +inject≤-trans : ∀ (i : Fin m) (m≤n : m ℕ.≤ n) (n≤o : n ℕ.≤ o) → + inject≤ (inject≤ i m≤n) n≤o ≡ inject≤ i (ℕₚ.≤-trans m≤n n≤o) +inject≤-trans i m≤n n≤o = inject≤-idempotent i m≤n n≤o _ + inject≤-injective : ∀ (m≤n m≤n′ : m ℕ.≤ n) i j → inject≤ i m≤n ≡ inject≤ j m≤n′ → i ≡ j inject≤-injective (s≤s p) (s≤s q) zero zero eq = refl inject≤-injective (s≤s p) (s≤s q) (suc i) (suc j) eq = cong suc (inject≤-injective p q i j (suc-injective eq)) +inject≤-irrelevant : ∀ (m≤n m≤n′ : m ℕ.≤ n) i → + inject≤ i m≤n ≡ inject≤ i m≤n′ +inject≤-irrelevant (s≤s p) (s≤s q) zero = refl +inject≤-irrelevant (s≤s p) (s≤s q) (suc i) = cong suc (inject≤-irrelevant p q i) + ------------------------------------------------------------------------ -- pred ------------------------------------------------------------------------ From 323d4224cc3de716973d6b419a44c1002b4c4e3d Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 19 Sep 2023 10:27:36 +0100 Subject: [PATCH 03/28] `fix-whitespace` --- src/Data/Fin/Properties.agda | 2 +- src/Data/Vec/Base.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index b42904e8de..af2f4d0dfc 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -549,7 +549,7 @@ inject≤-idempotent {_} {suc n} {suc o} (suc i) (s≤s m≤n) (s≤s n≤o) (s inject≤-trans : ∀ (i : Fin m) (m≤n : m ℕ.≤ n) (n≤o : n ℕ.≤ o) → inject≤ (inject≤ i m≤n) n≤o ≡ inject≤ i (ℕₚ.≤-trans m≤n n≤o) -inject≤-trans i m≤n n≤o = inject≤-idempotent i m≤n n≤o _ +inject≤-trans i m≤n n≤o = inject≤-idempotent i m≤n n≤o _ inject≤-injective : ∀ (m≤n m≤n′ : m ℕ.≤ n) i j → inject≤ i m≤n ≡ inject≤ j m≤n′ → i ≡ j diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index 6752ec1b06..ed8817c66e 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -272,7 +272,7 @@ drop m xs = proj₁ (proj₂ (splitAt m xs)) group : ∀ n k (xs : Vec A (n * k)) → ∃ λ (xss : Vec (Vec A k) n) → xs ≡ concat xss group zero k [] = ([] , refl) -group (suc n) k xs = +group (suc n) k xs = let ys , zs , eq-split = splitAt k xs in let zss , eq-group = group n k zs in (ys ∷ zss) , trans eq-split (cong (ys ++_) eq-group) From 6de7983cb01191f39428982536ad9919281a9d87 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 19 Sep 2023 11:21:35 +0100 Subject: [PATCH 04/28] simplified `import` dependencies --- src/Data/Vec/Properties.agda | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 8113d0a932..9688bd7ad6 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -22,15 +22,14 @@ open import Data.Sum.Base using ([_,_]′) open import Data.Sum.Properties using ([,]-map) open import Data.Vec.Base open import Function.Base --- open import Function.Inverse using (_↔_; inverse) open import Function.Bundles using (_↔_; mk↔′) open import Level using (Level) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; _≗_; refl; sym; trans; cong; cong₂; subst; module ≡-Reasoning) open import Relation.Unary using (Pred; Decidable) -open import Relation.Nullary.Decidable using (Dec; does; yes; no; _×-dec_; map′) -open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary.Decidable.Core using (Dec; does; yes; no; _×-dec_; map′) +open import Relation.Nullary.Negation.Core using (contradiction) open ≡-Reasoning From f492da721410c6e9283921bc3a0e15aecb8d5b1e Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 19 Sep 2023 11:27:56 +0100 Subject: [PATCH 05/28] placeholder deprecation --- CHANGELOG.md | 2 ++ src/Data/Vec/Properties.agda | 19 ++++++++++++++++--- 2 files changed, 18 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b1e8ab2fa6..433da16384 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1427,6 +1427,8 @@ Deprecated names sum-++-commute ↦ sum-++ take-drop-id ↦ take++drop≡id + + lookup-inject≤-take ↦ lookup-take-inject≤ ``` and the type of the proof `zipWith-comm` has been generalised from: ``` diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 9688bd7ad6..3e7dd1db42 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -170,10 +170,15 @@ lookup⇒[]= (suc i) (_ ∷ xs) p = there (lookup⇒[]= i xs p) []=⇒lookup∘lookup⇒[]= (x ∷ xs) zero refl = refl []=⇒lookup∘lookup⇒[]= (x ∷ xs) (suc i) p = []=⇒lookup∘lookup⇒[]= xs i p -lookup-inject≤-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) → +lookup-take-inject≤ : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) → + lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i +lookup-take-inject≤ (suc m) m≤m+n zero (x ∷ xs) = refl +lookup-take-inject≤ (suc m) (s≤s m≤m+n) (suc i) (x ∷ xs) = lookup-take-inject≤ m m≤m+n i xs + +lookup-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) → lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i -lookup-inject≤-take (suc m) m≤m+n zero (x ∷ xs) = refl -lookup-inject≤-take (suc m) (s≤s m≤m+n) (suc i) (x ∷ xs) = lookup-inject≤-take m m≤m+n i xs +lookup-take (suc m) m≤m+n zero (x ∷ xs) = refl +lookup-take (suc m) (s≤s m≤m+n) (suc i) (x ∷ xs) = lookup-take-inject≤ m m≤m+n i xs ------------------------------------------------------------------------ -- updateAt (_[_]%=_) @@ -1271,3 +1276,11 @@ drop-distr-map = drop-map "Warning: drop-distr-map was deprecated in v2.0. Please use drop-map instead." #-} +lookup-inject≤-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) → + lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i +lookup-inject≤-take m m≤m+n i xs = lookup-take-inject≤ m m≤m+n i xs +{-# WARNING_ON_USAGE lookup-inject≤-take +"Warning: lookup-inject≤-take was deprecated in v2.0. +Please use lookup-take-inject≤ instead." +#-} + From 1aa2fe011f419261cb6e23d580c34c6979ecfdac Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 19 Sep 2023 11:40:11 +0100 Subject: [PATCH 06/28] flipped equality; made `m` implicit --- src/Data/Vec/Properties.agda | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 3e7dd1db42..ef48e2483d 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -170,16 +170,17 @@ lookup⇒[]= (suc i) (_ ∷ xs) p = there (lookup⇒[]= i xs p) []=⇒lookup∘lookup⇒[]= (x ∷ xs) zero refl = refl []=⇒lookup∘lookup⇒[]= (x ∷ xs) (suc i) p = []=⇒lookup∘lookup⇒[]= xs i p -lookup-take-inject≤ : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) → - lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i -lookup-take-inject≤ (suc m) m≤m+n zero (x ∷ xs) = refl -lookup-take-inject≤ (suc m) (s≤s m≤m+n) (suc i) (x ∷ xs) = lookup-take-inject≤ m m≤m+n i xs - -lookup-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) → - lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i -lookup-take (suc m) m≤m+n zero (x ∷ xs) = refl -lookup-take (suc m) (s≤s m≤m+n) (suc i) (x ∷ xs) = lookup-take-inject≤ m m≤m+n i xs - +lookup-take-inject≤ : ∀ (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) → + lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i m≤m+n) +lookup-take-inject≤ m≤m+n zero (x ∷ xs) = refl +lookup-take-inject≤ (s≤s m≤m+n) (suc i) (x ∷ xs) = lookup-take-inject≤ m≤m+n i xs +{- +lookup-take : (m≤n : m ≤ n) (i : Fin m) → + let less-than-or-equal {k} refl = ≤⇒≤″ m≤n in + (xs : Vec A (m + k)) → + lookup (take m xs) i ≡ lookup (cast ? xs) (Fin.inject≤ i m≤n) +lookup-take m≤n i xs = ? +-} ------------------------------------------------------------------------ -- updateAt (_[_]%=_) @@ -1278,7 +1279,7 @@ Please use drop-map instead." #-} lookup-inject≤-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) → lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i -lookup-inject≤-take m m≤m+n i xs = lookup-take-inject≤ m m≤m+n i xs +lookup-inject≤-take m m≤m+n i xs = sym (lookup-take-inject≤ m≤m+n i xs) {-# WARNING_ON_USAGE lookup-inject≤-take "Warning: lookup-inject≤-take was deprecated in v2.0. Please use lookup-take-inject≤ instead." From bd388416a6df4d024dc10e0623ce9ba2c829025e Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 19 Sep 2023 11:43:30 +0100 Subject: [PATCH 07/28] renamed lemma --- src/Data/Vec/Properties.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index ef48e2483d..a5aa1609a9 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -170,10 +170,10 @@ lookup⇒[]= (suc i) (_ ∷ xs) p = there (lookup⇒[]= i xs p) []=⇒lookup∘lookup⇒[]= (x ∷ xs) zero refl = refl []=⇒lookup∘lookup⇒[]= (x ∷ xs) (suc i) p = []=⇒lookup∘lookup⇒[]= xs i p -lookup-take-inject≤ : ∀ (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) → +lookup-take-inject≤′ : ∀ (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) → lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i m≤m+n) -lookup-take-inject≤ m≤m+n zero (x ∷ xs) = refl -lookup-take-inject≤ (s≤s m≤m+n) (suc i) (x ∷ xs) = lookup-take-inject≤ m≤m+n i xs +lookup-take-inject≤′ _ zero (_ ∷ _) = refl +lookup-take-inject≤′ (s≤s m≤m+n) (suc i) (x ∷ xs) = lookup-take-inject≤′ m≤m+n i xs {- lookup-take : (m≤n : m ≤ n) (i : Fin m) → let less-than-or-equal {k} refl = ≤⇒≤″ m≤n in @@ -1279,7 +1279,7 @@ Please use drop-map instead." #-} lookup-inject≤-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) → lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i -lookup-inject≤-take m m≤m+n i xs = sym (lookup-take-inject≤ m≤m+n i xs) +lookup-inject≤-take m m≤m+n i xs = sym (lookup-take-inject≤′ m≤m+n i xs) {-# WARNING_ON_USAGE lookup-inject≤-take "Warning: lookup-inject≤-take was deprecated in v2.0. Please use lookup-take-inject≤ instead." From 4239216ad8942e119da13ef35e63da365641d732 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 19 Sep 2023 11:47:16 +0100 Subject: [PATCH 08/28] reordered arguments --- src/Data/Vec/Properties.agda | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index a5aa1609a9..62e7ebf25b 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -170,10 +170,14 @@ lookup⇒[]= (suc i) (_ ∷ xs) p = there (lookup⇒[]= i xs p) []=⇒lookup∘lookup⇒[]= (x ∷ xs) zero refl = refl []=⇒lookup∘lookup⇒[]= (x ∷ xs) (suc i) p = []=⇒lookup∘lookup⇒[]= xs i p -lookup-take-inject≤′ : ∀ (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) → +lookup-take-inject≤′ : ∀ (m≤m+n : m ≤ m + n) (xs : Vec A (m + n)) (i : Fin m) → lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i m≤m+n) -lookup-take-inject≤′ _ zero (_ ∷ _) = refl -lookup-take-inject≤′ (s≤s m≤m+n) (suc i) (x ∷ xs) = lookup-take-inject≤′ m≤m+n i xs +lookup-take-inject≤′ _ (_ ∷ _) zero = refl +lookup-take-inject≤′ (s≤s m≤m+n) (x ∷ xs) (suc i) = lookup-take-inject≤′ m≤m+n xs i + +lookup-take-inject≤ : ∀ m (xs : Vec A (m + n)) (i : Fin m) → + lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i ?) +lookup-take-inject≤ m xs i = lookup-take-inject≤′ ? xs i {- lookup-take : (m≤n : m ≤ n) (i : Fin m) → let less-than-or-equal {k} refl = ≤⇒≤″ m≤n in @@ -1279,7 +1283,7 @@ Please use drop-map instead." #-} lookup-inject≤-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) → lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i -lookup-inject≤-take m m≤m+n i xs = sym (lookup-take-inject≤′ m≤m+n i xs) +lookup-inject≤-take m m≤m+n i xs = sym (lookup-take-inject≤′ m≤m+n xs i) {-# WARNING_ON_USAGE lookup-inject≤-take "Warning: lookup-inject≤-take was deprecated in v2.0. Please use lookup-take-inject≤ instead." From 0781379c978a5958350d636f4db2692203b0070f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 19 Sep 2023 11:50:40 +0100 Subject: [PATCH 09/28] inserted canonical proof --- src/Data/Vec/Properties.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 62e7ebf25b..7e5d1bfe9d 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -15,7 +15,7 @@ open import Data.List.Base as List using (List) import Data.List.Properties as Listₚ open import Data.Nat.Base open import Data.Nat.Properties - using (+-assoc; m≤n⇒m≤1+n; ≤-refl; ≤-trans; suc-injective; +-comm; +-suc) + using (+-assoc; m≤n⇒m≤1+n; m≤m+n; ≤-refl; ≤-trans; suc-injective; +-comm; +-suc) open import Data.Product.Base as Prod using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry) open import Data.Sum.Base using ([_,_]′) @@ -175,9 +175,9 @@ lookup-take-inject≤′ : ∀ (m≤m+n : m ≤ m + n) (xs : Vec A (m + n)) (i : lookup-take-inject≤′ _ (_ ∷ _) zero = refl lookup-take-inject≤′ (s≤s m≤m+n) (x ∷ xs) (suc i) = lookup-take-inject≤′ m≤m+n xs i -lookup-take-inject≤ : ∀ m (xs : Vec A (m + n)) (i : Fin m) → - lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i ?) -lookup-take-inject≤ m xs i = lookup-take-inject≤′ ? xs i +lookup-take-inject≤ : ∀ m {n} (xs : Vec A (m + n)) (i : Fin m) → + lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n)) +lookup-take-inject≤ m xs i = lookup-take-inject≤′ (m≤m+n m _) xs i {- lookup-take : (m≤n : m ≤ n) (i : Fin m) → let less-than-or-equal {k} refl = ≤⇒≤″ m≤n in From be4951d49ac1449a25da3a3753974e86cc7f60d6 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 19 Sep 2023 11:59:05 +0100 Subject: [PATCH 10/28] tidy up --- CHANGELOG.md | 5 ++++- src/Data/Vec/Properties.agda | 12 ++---------- 2 files changed, 6 insertions(+), 11 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 433da16384..847dfedebc 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1428,7 +1428,7 @@ Deprecated names take-drop-id ↦ take++drop≡id - lookup-inject≤-take ↦ lookup-take-inject≤ + lookup-inject≤-take ↦ lookup-take-inject≤′ ``` and the type of the proof `zipWith-comm` has been generalised from: ``` @@ -2719,6 +2719,9 @@ Additions to existing modules cast-fromList : cast _ (fromList xs) ≡ fromList ys fromList-map : cast _ (fromList (List.map f xs)) ≡ map f (fromList xs) fromList-++ : cast _ (fromList (xs List.++ ys)) ≡ fromList xs ++ fromList ys + + lookup-take-inject≤ : (xs : Vec A (m + n)) (i : Fin m) → + lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n)) ``` * Added new proofs in `Data.Vec.Membership.Propositional.Properties`: diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 7e5d1bfe9d..23ba4eb935 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -178,13 +178,7 @@ lookup-take-inject≤′ (s≤s m≤m+n) (x ∷ xs) (suc i) = lookup-take-inject lookup-take-inject≤ : ∀ m {n} (xs : Vec A (m + n)) (i : Fin m) → lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n)) lookup-take-inject≤ m xs i = lookup-take-inject≤′ (m≤m+n m _) xs i -{- -lookup-take : (m≤n : m ≤ n) (i : Fin m) → - let less-than-or-equal {k} refl = ≤⇒≤″ m≤n in - (xs : Vec A (m + k)) → - lookup (take m xs) i ≡ lookup (cast ? xs) (Fin.inject≤ i m≤n) -lookup-take m≤n i xs = ? --} + ------------------------------------------------------------------------ -- updateAt (_[_]%=_) @@ -1254,13 +1248,11 @@ sum-++-commute = sum-++ "Warning: sum-++-commute was deprecated in v2.0. Please use sum-++ instead." #-} - take-drop-id = take++drop≡id {-# WARNING_ON_USAGE take-drop-id "Warning: take-drop-id was deprecated in v2.0. Please use take++drop≡id instead." #-} - take-distr-zipWith = take-zipWith {-# WARNING_ON_USAGE take-distr-zipWith "Warning: take-distr-zipWith was deprecated in v2.0. @@ -1286,6 +1278,6 @@ lookup-inject≤-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m lookup-inject≤-take m m≤m+n i xs = sym (lookup-take-inject≤′ m≤m+n xs i) {-# WARNING_ON_USAGE lookup-inject≤-take "Warning: lookup-inject≤-take was deprecated in v2.0. -Please use lookup-take-inject≤ instead." +Please use lookup-take-inject≤′ instead." #-} From b4ce98f12f3c28d8c9dcf345c45ef902b8c7212a Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 19 Sep 2023 12:19:32 +0100 Subject: [PATCH 11/28] =?UTF-8?q?definition=20of=20`take=E2=89=A4`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CHANGELOG.md | 1 + src/Data/Vec/Properties.agda | 13 ++++++++++++- 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 847dfedebc..d2ecead012 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2722,6 +2722,7 @@ Additions to existing modules lookup-take-inject≤ : (xs : Vec A (m + n)) (i : Fin m) → lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n)) + take≤ : (m≤n : m ≤ n) (xs : Vec A n) → Vec A m ``` * Added new proofs in `Data.Vec.Membership.Propositional.Properties`: diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 23ba4eb935..aae20592b5 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -15,7 +15,7 @@ open import Data.List.Base as List using (List) import Data.List.Properties as Listₚ open import Data.Nat.Base open import Data.Nat.Properties - using (+-assoc; m≤n⇒m≤1+n; m≤m+n; ≤-refl; ≤-trans; suc-injective; +-comm; +-suc) + using (+-assoc; m≤n⇒m≤1+n; m≤m+n; ≤-refl; ≤-trans; ≤⇒≤″; suc-injective; +-comm; +-suc) open import Data.Product.Base as Prod using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry) open import Data.Sum.Base using ([_,_]′) @@ -179,6 +179,17 @@ lookup-take-inject≤ : ∀ m {n} (xs : Vec A (m + n)) (i : Fin m) → lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n)) lookup-take-inject≤ m xs i = lookup-take-inject≤′ (m≤m+n m _) xs i +-- provisional definition + +take≤ : (m≤n : m ≤ n) (xs : Vec A n) → Vec A m +take≤ {m} m≤n xs = let less-than-or-equal {k} eq = ≤⇒≤″ m≤n in take m (cast (sym eq) xs) +{- +lookup-take : (m≤n : m ≤ n) (i : Fin m) → + let less-than-or-equal {k} refl = ≤⇒≤″ m≤n in + (xs : Vec A (m + k)) → + lookup (take m xs) i ≡ lookup (cast ? xs) (Fin.inject≤ i m≤n) +lookup-take m≤n i xs = ? +-} ------------------------------------------------------------------------ -- updateAt (_[_]%=_) From 6214cb002ec0c944221d6c6ef6b2e205fc39c737 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 19 Sep 2023 12:47:11 +0100 Subject: [PATCH 12/28] added definition of `cast-sym` --- CHANGELOG.md | 3 ++- src/Data/Vec/Properties.agda | 18 +++++++----------- 2 files changed, 9 insertions(+), 12 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index d2ecead012..f8f547c5de 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2700,12 +2700,13 @@ Additions to existing modules cast-is-id : cast eq xs ≡ xs subst-is-cast : subst (Vec A) eq xs ≡ cast eq xs + cast-sym : ys ≡ cast eq xs → xs ≡ cast (sym eq) ys 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 - cast-reverse : cast eq ∘ reverse ≗ reverse ∘ cast eq + cast-reverse : cast eq ∘ reverse ≗ reverse ∘ cast eq zipwith-++ : zipWith f (xs ++ ys) (xs' ++ ys') ≡ zipWith f xs xs' ++ zipWith f ys ys' diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index aae20592b5..a9548da8ce 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -179,17 +179,6 @@ lookup-take-inject≤ : ∀ m {n} (xs : Vec A (m + n)) (i : Fin m) → lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n)) lookup-take-inject≤ m xs i = lookup-take-inject≤′ (m≤m+n m _) xs i --- provisional definition - -take≤ : (m≤n : m ≤ n) (xs : Vec A n) → Vec A m -take≤ {m} m≤n xs = let less-than-or-equal {k} eq = ≤⇒≤″ m≤n in take m (cast (sym eq) xs) -{- -lookup-take : (m≤n : m ≤ n) (i : Fin m) → - let less-than-or-equal {k} refl = ≤⇒≤″ m≤n in - (xs : Vec A (m + k)) → - lookup (take m xs) i ≡ lookup (cast ? xs) (Fin.inject≤ i m≤n) -lookup-take m≤n i xs = ? --} ------------------------------------------------------------------------ -- updateAt (_[_]%=_) @@ -362,6 +351,13 @@ cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (suc-injective eq) xs) subst-is-cast : (eq : m ≡ n) (xs : Vec A m) → subst (Vec A) eq xs ≡ cast eq xs subst-is-cast refl xs = sym (cast-is-id refl xs) +cast-sym : (eq : m ≡ n) {xs : Vec A m} {ys : Vec A n} → + ys ≡ cast eq xs → xs ≡ cast (sym eq) ys +cast-sym eq {xs = []} {ys = []} _ = refl +cast-sym eq {xs = x ∷ xs} {ys = y ∷ ys} xxs≡[eq]yys + with x≡y , xs≡[eq]ys ← ∷-injective xxs≡[eq]yys + = cong₂ _∷_ (sym x≡y) (cast-sym (suc-injective eq) xs≡[eq]ys) + cast-trans : .(eq₁ : m ≡ n) .(eq₂ : n ≡ o) (xs : Vec A m) → cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs cast-trans {m = zero} {n = zero} {o = zero} eq₁ eq₂ [] = refl From 5534d81ef3a4d18d63af1ef7c0c33aea8dff418f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 19 Sep 2023 14:26:34 +0100 Subject: [PATCH 13/28] tidy up --- CHANGELOG.md | 1 - 1 file changed, 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f8f547c5de..a21d6b89d0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2723,7 +2723,6 @@ Additions to existing modules lookup-take-inject≤ : (xs : Vec A (m + n)) (i : Fin m) → lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n)) - take≤ : (m≤n : m ≤ n) (xs : Vec A n) → Vec A m ``` * Added new proofs in `Data.Vec.Membership.Propositional.Properties`: From e114a990d4b1833393c2fa96b6227b7bb95187e8 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 19 Sep 2023 23:05:24 +0100 Subject: [PATCH 14/28] =?UTF-8?q?re-added=20`take=E2=89=A4`=20etc.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CHANGELOG.md | 3 +++ src/Data/Vec/Properties.agda | 16 +++++++++++++++- 2 files changed, 18 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a21d6b89d0..87d14de014 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2723,6 +2723,9 @@ Additions to existing modules lookup-take-inject≤ : (xs : Vec A (m + n)) (i : Fin m) → lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n)) + take≤ : (m≤n : m ≤ n) (xs : Vec A n) → Vec A m + take≤-irrelevant : (xs : Vec A n) → take≤ m≤n₁ xs ≡ take≤ m≤n₂ xs + take≤-unfold : (xs : Vec A (m + n)) → take≤ (m≤m+n m n) xs ≡ take m xs ``` * Added new proofs in `Data.Vec.Membership.Propositional.Properties`: diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index a9548da8ce..a2a44c96e4 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -15,7 +15,7 @@ open import Data.List.Base as List using (List) import Data.List.Properties as Listₚ open import Data.Nat.Base open import Data.Nat.Properties - using (+-assoc; m≤n⇒m≤1+n; m≤m+n; ≤-refl; ≤-trans; ≤⇒≤″; suc-injective; +-comm; +-suc) + using (+-assoc; m≤n⇒m≤1+n; m≤m+n; ≤-refl; ≤-trans; ≤-irrelevant; ≤⇒≤″; suc-injective; +-comm; +-suc) open import Data.Product.Base as Prod using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry) open import Data.Sum.Base using ([_,_]′) @@ -179,6 +179,20 @@ lookup-take-inject≤ : ∀ m {n} (xs : Vec A (m + n)) (i : Fin m) → lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n)) lookup-take-inject≤ m xs i = lookup-take-inject≤′ (m≤m+n m _) xs i +------------------------------------------------------------------------ +-- take≤: provisional definition: where should this go? + +take≤ : (m≤n : m ≤ n) (xs : Vec A n) → Vec A m +take≤ {m = m} m≤n xs = let less-than-or-equal eq = ≤⇒≤″ m≤n in take m (cast (sym eq) xs) + +take≤-irrelevant : (m≤n₁ m≤n₂ : m ≤ n) (xs : Vec A n) → + take≤ m≤n₁ xs ≡ take≤ m≤n₂ xs +take≤-irrelevant m≤n₁ m≤n₂ xs with refl ← ≤-irrelevant m≤n₁ m≤n₂ = refl + +take≤-unfold : (xs : Vec A (m + n)) → take≤ (m≤m+n m n) xs ≡ take m xs +take≤-unfold {m = zero} _ = refl +take≤-unfold {m = suc m} (x ∷ xs) = cong (x ∷_) (take≤-unfold xs) + ------------------------------------------------------------------------ -- updateAt (_[_]%=_) From d1b8f22f3ca51fd32c89b5e4724bbf1178e722bb Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 19 Sep 2023 23:45:40 +0100 Subject: [PATCH 15/28] renamed things to align with issue #2090 --- CHANGELOG.md | 4 +++- src/Data/Vec/Properties.agda | 14 +++++++------- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 87d14de014..9e5c8849a2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2721,7 +2721,9 @@ Additions to existing modules fromList-map : cast _ (fromList (List.map f xs)) ≡ map f (fromList xs) fromList-++ : cast _ (fromList (xs List.++ ys)) ≡ fromList xs ++ fromList ys - lookup-take-inject≤ : (xs : Vec A (m + n)) (i : Fin m) → + lookup-take-inject≤ : (m≤m+n : m ≤ m + n) (xs : Vec A (m + n)) (i : Fin m) → + lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i m≤m+n) + lookup-take : (xs : Vec A (m + n)) (i : Fin m) → lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n)) take≤ : (m≤n : m ≤ n) (xs : Vec A n) → Vec A m take≤-irrelevant : (xs : Vec A n) → take≤ m≤n₁ xs ≡ take≤ m≤n₂ xs diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index a2a44c96e4..bd414f5e7d 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -170,14 +170,14 @@ lookup⇒[]= (suc i) (_ ∷ xs) p = there (lookup⇒[]= i xs p) []=⇒lookup∘lookup⇒[]= (x ∷ xs) zero refl = refl []=⇒lookup∘lookup⇒[]= (x ∷ xs) (suc i) p = []=⇒lookup∘lookup⇒[]= xs i p -lookup-take-inject≤′ : ∀ (m≤m+n : m ≤ m + n) (xs : Vec A (m + n)) (i : Fin m) → +lookup-take-inject≤ : (m≤m+n : m ≤ m + n) (xs : Vec A (m + n)) (i : Fin m) → lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i m≤m+n) -lookup-take-inject≤′ _ (_ ∷ _) zero = refl -lookup-take-inject≤′ (s≤s m≤m+n) (x ∷ xs) (suc i) = lookup-take-inject≤′ m≤m+n xs i +lookup-take-inject≤ _ (_ ∷ _) zero = refl +lookup-take-inject≤ (s≤s m≤m+n) (x ∷ xs) (suc i) = lookup-take-inject≤ m≤m+n xs i -lookup-take-inject≤ : ∀ m {n} (xs : Vec A (m + n)) (i : Fin m) → - lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n)) -lookup-take-inject≤ m xs i = lookup-take-inject≤′ (m≤m+n m _) xs i +lookup-take : ∀ m {n} (xs : Vec A (m + n)) (i : Fin m) → + lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n)) +lookup-take m xs i = lookup-take-inject≤ (m≤m+n m _) xs i ------------------------------------------------------------------------ -- take≤: provisional definition: where should this go? @@ -1296,7 +1296,7 @@ Please use drop-map instead." #-} lookup-inject≤-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) → lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i -lookup-inject≤-take m m≤m+n i xs = sym (lookup-take-inject≤′ m≤m+n xs i) +lookup-inject≤-take m m≤m+n i xs = sym (lookup-take-inject≤ m≤m+n xs i) {-# WARNING_ON_USAGE lookup-inject≤-take "Warning: lookup-inject≤-take was deprecated in v2.0. Please use lookup-take-inject≤′ instead." From 1645d5ff348b2e0b3cbe40bfc45b4799b991e8c1 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Wed, 20 Sep 2023 16:31:33 +0100 Subject: [PATCH 16/28] Typo in deprecation warning! --- src/Data/Vec/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index bd414f5e7d..bc00df2fd3 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -1299,6 +1299,6 @@ lookup-inject≤-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m lookup-inject≤-take m m≤m+n i xs = sym (lookup-take-inject≤ m≤m+n xs i) {-# WARNING_ON_USAGE lookup-inject≤-take "Warning: lookup-inject≤-take was deprecated in v2.0. -Please use lookup-take-inject≤′ instead." +Please use lookup-take-inject≤ instead." #-} From 2e7c74547f28ceba8e29dd5569f0cabc3512f867 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 23 Sep 2023 07:55:10 +0100 Subject: [PATCH 17/28] `cast-sym` made irrelevant in its `eq` argument --- src/Data/Vec/Properties.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index bc00df2fd3..402c0376dc 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -365,12 +365,12 @@ cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (suc-injective eq) xs) subst-is-cast : (eq : m ≡ n) (xs : Vec A m) → subst (Vec A) eq xs ≡ cast eq xs subst-is-cast refl xs = sym (cast-is-id refl xs) -cast-sym : (eq : m ≡ n) {xs : Vec A m} {ys : Vec A n} → +cast-sym : .(eq : m ≡ n) {xs : Vec A m} {ys : Vec A n} → ys ≡ cast eq xs → xs ≡ cast (sym eq) ys cast-sym eq {xs = []} {ys = []} _ = refl -cast-sym eq {xs = x ∷ xs} {ys = y ∷ ys} xxs≡[eq]yys - with x≡y , xs≡[eq]ys ← ∷-injective xxs≡[eq]yys - = cong₂ _∷_ (sym x≡y) (cast-sym (suc-injective eq) xs≡[eq]ys) +cast-sym eq {xs = x ∷ xs} {ys = y ∷ ys} xxs≡[eq]yys = + let x≡y , xs≡[eq]ys = ∷-injective xxs≡[eq]yys + in cong₂ _∷_ (sym x≡y) (cast-sym (suc-injective eq) xs≡[eq]ys) cast-trans : .(eq₁ : m ≡ n) .(eq₂ : n ≡ o) (xs : Vec A m) → cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs From 7bd01c0de86314030477811299fc9af646e5bc7e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 23 Sep 2023 08:03:29 +0100 Subject: [PATCH 18/28] further deprecation typo --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9e5c8849a2..a65ac5d17d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1428,7 +1428,7 @@ Deprecated names take-drop-id ↦ take++drop≡id - lookup-inject≤-take ↦ lookup-take-inject≤′ + lookup-inject≤-take ↦ lookup-take-inject≤ ``` and the type of the proof `zipWith-comm` has been generalised from: ``` From ad9bc2402c72f45304add539a7fc37efd655a385 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 23 Sep 2023 08:12:29 +0100 Subject: [PATCH 19/28] re-oriented equations in `cast-sym` --- CHANGELOG.md | 2 +- src/Data/Fin/Base.agda | 2 +- src/Data/Vec/Properties.agda | 10 +++++----- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a65ac5d17d..224b6296ba 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2700,7 +2700,7 @@ Additions to existing modules cast-is-id : cast eq xs ≡ xs subst-is-cast : subst (Vec A) eq xs ≡ cast eq xs - cast-sym : ys ≡ cast eq xs → xs ≡ cast (sym eq) ys + cast-sym : cast eq xs ≡ ys → cast (sym eq) ys ≡ 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 diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index 199f3dbe0b..2d5b0f638e 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -114,7 +114,7 @@ inject₁ zero = zero inject₁ (suc i) = suc (inject₁ i) inject≤ : Fin m → m ℕ.≤ n → Fin n -inject≤ {_} {suc n} zero _ = zero +inject≤ {_} {suc n} zero _ = zero inject≤ {_} {suc n} (suc i) (s≤s m≤n) = suc (inject≤ i m≤n) -- lower₁ "i" _ = "i". diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 402c0376dc..3d49e81e1a 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -186,7 +186,7 @@ take≤ : (m≤n : m ≤ n) (xs : Vec A n) → Vec A m take≤ {m = m} m≤n xs = let less-than-or-equal eq = ≤⇒≤″ m≤n in take m (cast (sym eq) xs) take≤-irrelevant : (m≤n₁ m≤n₂ : m ≤ n) (xs : Vec A n) → - take≤ m≤n₁ xs ≡ take≤ m≤n₂ xs + take≤ m≤n₁ xs ≡ take≤ m≤n₂ xs take≤-irrelevant m≤n₁ m≤n₂ xs with refl ← ≤-irrelevant m≤n₁ m≤n₂ = refl take≤-unfold : (xs : Vec A (m + n)) → take≤ (m≤m+n m n) xs ≡ take m xs @@ -366,11 +366,11 @@ subst-is-cast : (eq : m ≡ n) (xs : Vec A m) → subst (Vec A) eq xs ≡ cast e subst-is-cast refl xs = sym (cast-is-id refl xs) cast-sym : .(eq : m ≡ n) {xs : Vec A m} {ys : Vec A n} → - ys ≡ cast eq xs → xs ≡ cast (sym eq) ys + cast eq xs ≡ ys → cast (sym eq) ys ≡ xs cast-sym eq {xs = []} {ys = []} _ = refl -cast-sym eq {xs = x ∷ xs} {ys = y ∷ ys} xxs≡[eq]yys = - let x≡y , xs≡[eq]ys = ∷-injective xxs≡[eq]yys - in cong₂ _∷_ (sym x≡y) (cast-sym (suc-injective eq) xs≡[eq]ys) +cast-sym eq {xs = x ∷ xs} {ys = y ∷ ys} xxs[eq]≡yys = + let x≡y , xs[eq]≡ys = ∷-injective xxs[eq]≡yys + in cong₂ _∷_ (sym x≡y) (cast-sym (suc-injective eq) xs[eq]≡ys) cast-trans : .(eq₁ : m ≡ n) .(eq₂ : n ≡ o) (xs : Vec A m) → cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs From 439bf83c0a56bd1212f824fb2dce12987ef460a7 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 24 Sep 2023 14:42:12 +0100 Subject: [PATCH 20/28] refactored `lookup-take` etc. in terms of `truncate` etc. --- CHANGELOG.md | 11 +++----- src/Data/Vec/Base.agda | 2 +- src/Data/Vec/Properties.agda | 49 +++++++++++++++++++++--------------- 3 files changed, 34 insertions(+), 28 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 224b6296ba..c59f878641 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2721,13 +2721,10 @@ Additions to existing modules fromList-map : cast _ (fromList (List.map f xs)) ≡ map f (fromList xs) fromList-++ : cast _ (fromList (xs List.++ ys)) ≡ fromList xs ++ fromList ys - lookup-take-inject≤ : (m≤m+n : m ≤ m + n) (xs : Vec A (m + n)) (i : Fin m) → - lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i m≤m+n) - lookup-take : (xs : Vec A (m + n)) (i : Fin m) → - lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n)) - take≤ : (m≤n : m ≤ n) (xs : Vec A n) → Vec A m - take≤-irrelevant : (xs : Vec A n) → take≤ m≤n₁ xs ≡ take≤ m≤n₂ xs - take≤-unfold : (xs : Vec A (m + n)) → take≤ (m≤m+n m n) xs ≡ take m xs + truncate≡take : .(eq : n ≡ m + o) → truncate m≤n xs ≡ take m (cast eq xs) + take≡truncate : take m xs ≡ truncate (m≤m+n m n) xs + lookup-truncate : lookup (truncate m≤n xs) i ≡ lookup xs (Fin.inject≤ i m≤n) + lookup-take-inject≤ : lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i m≤m+n) ``` * Added new proofs in `Data.Vec.Membership.Propositional.Properties`: diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index ed8817c66e..507ac05463 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -290,7 +290,7 @@ uncons (x ∷ xs) = x , xs -- Take the first 'm' elements of a vector. truncate : ∀ {m n} → m ≤ n → Vec A n → Vec A m -truncate z≤n _ = [] +truncate {m = zero} _ _ = [] truncate (s≤s le) (x ∷ xs) = x ∷ (truncate le xs) -- Pad out a vector with extra elements. diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 3d49e81e1a..e85baac047 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -121,6 +121,20 @@ truncate-trans : ∀ {p} (m≤n : m ≤ n) (n≤p : n ≤ p) (xs : Vec A p) → truncate-trans z≤n n≤p xs = refl truncate-trans (s≤s m≤n) (s≤s n≤p) (x ∷ xs) = cong (x ∷_) (truncate-trans m≤n n≤p xs) +truncate-irrelevant : (m≤n₁ m≤n₂ : m ≤ n) → truncate {A = A} m≤n₁ ≗ truncate m≤n₂ +truncate-irrelevant {m = zero} m≤n₁ m≤n₂ _ = refl +truncate-irrelevant (s≤s m≤n₁) (s≤s m≤n₂) (x ∷ xs) = cong (x ∷_) (truncate-irrelevant m≤n₁ m≤n₂ xs) + +truncate≡take : (m≤n : m ≤ n) (xs : Vec A n) .(eq : n ≡ m + o) → + truncate m≤n xs ≡ take m (cast eq xs) +truncate≡take z≤n _ eq = refl +truncate≡take (s≤s m≤n) (x ∷ xs) eq = cong (x ∷_) (truncate≡take m≤n xs (suc-injective eq)) + +take≡truncate : ∀ m (xs : Vec A (m + n)) → + take m xs ≡ truncate (m≤m+n m n) xs +take≡truncate zero _ = refl +take≡truncate (suc m) (x ∷ xs) = cong (x ∷_) (take≡truncate m xs) + ------------------------------------------------------------------------ -- pad @@ -170,28 +184,23 @@ lookup⇒[]= (suc i) (_ ∷ xs) p = there (lookup⇒[]= i xs p) []=⇒lookup∘lookup⇒[]= (x ∷ xs) zero refl = refl []=⇒lookup∘lookup⇒[]= (x ∷ xs) (suc i) p = []=⇒lookup∘lookup⇒[]= xs i p +lookup-truncate : (m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) → + lookup (truncate m≤n xs) i ≡ lookup xs (Fin.inject≤ i m≤n) +lookup-truncate (s≤s m≤m+n) (_ ∷ _) zero = refl +lookup-truncate (s≤s m≤m+n) (_ ∷ xs) (suc i) = lookup-truncate m≤m+n xs i + lookup-take-inject≤ : (m≤m+n : m ≤ m + n) (xs : Vec A (m + n)) (i : Fin m) → lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i m≤m+n) -lookup-take-inject≤ _ (_ ∷ _) zero = refl -lookup-take-inject≤ (s≤s m≤m+n) (x ∷ xs) (suc i) = lookup-take-inject≤ m≤m+n xs i - -lookup-take : ∀ m {n} (xs : Vec A (m + n)) (i : Fin m) → - lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n)) -lookup-take m xs i = lookup-take-inject≤ (m≤m+n m _) xs i - ------------------------------------------------------------------------- --- take≤: provisional definition: where should this go? - -take≤ : (m≤n : m ≤ n) (xs : Vec A n) → Vec A m -take≤ {m = m} m≤n xs = let less-than-or-equal eq = ≤⇒≤″ m≤n in take m (cast (sym eq) xs) - -take≤-irrelevant : (m≤n₁ m≤n₂ : m ≤ n) (xs : Vec A n) → - take≤ m≤n₁ xs ≡ take≤ m≤n₂ xs -take≤-irrelevant m≤n₁ m≤n₂ xs with refl ← ≤-irrelevant m≤n₁ m≤n₂ = refl - -take≤-unfold : (xs : Vec A (m + n)) → take≤ (m≤m+n m n) xs ≡ take m xs -take≤-unfold {m = zero} _ = refl -take≤-unfold {m = suc m} (x ∷ xs) = cong (x ∷_) (take≤-unfold xs) +lookup-take-inject≤ {m = m} m≤m+n xs i = begin + lookup (take m xs) i + ≡⟨ cong (λ ys → lookup ys i) (take≡truncate m xs) ⟩ + lookup (truncate _ xs) i + ≡⟨ cong (λ ys → lookup ys i) (truncate-irrelevant _ _ xs) ⟩ + lookup (truncate m≤m+n xs) i + ≡⟨ lookup-truncate m≤m+n xs i ⟩ + lookup xs (Fin.inject≤ i m≤m+n) + ∎ + where open ≡-Reasoning ------------------------------------------------------------------------ -- updateAt (_[_]%=_) From 6540d5a08590876f29e401b8e36b99d1b7d2bbac Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 24 Sep 2023 15:04:11 +0100 Subject: [PATCH 21/28] final version? --- CHANGELOG.md | 2 +- src/Data/Vec/Properties.agda | 26 +++++++++++++++----------- 2 files changed, 16 insertions(+), 12 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index c59f878641..d37b086174 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2724,7 +2724,7 @@ Additions to existing modules truncate≡take : .(eq : n ≡ m + o) → truncate m≤n xs ≡ take m (cast eq xs) take≡truncate : take m xs ≡ truncate (m≤m+n m n) xs lookup-truncate : lookup (truncate m≤n xs) i ≡ lookup xs (Fin.inject≤ i m≤n) - lookup-take-inject≤ : lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i m≤m+n) + lookup-take-inject≤ : lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n)) ``` * Added new proofs in `Data.Vec.Membership.Propositional.Properties`: diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index e85baac047..a19f1ef8ec 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -11,6 +11,7 @@ module Data.Vec.Properties where open import Algebra.Definitions open import Data.Bool.Base using (true; false) open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_; _↑ʳ_) +open import Data.Fin.Properties as Fin using (inject≤-irrelevant) open import Data.List.Base as List using (List) import Data.List.Properties as Listₚ open import Data.Nat.Base @@ -189,18 +190,15 @@ lookup-truncate : (m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) → lookup-truncate (s≤s m≤m+n) (_ ∷ _) zero = refl lookup-truncate (s≤s m≤m+n) (_ ∷ xs) (suc i) = lookup-truncate m≤m+n xs i -lookup-take-inject≤ : (m≤m+n : m ≤ m + n) (xs : Vec A (m + n)) (i : Fin m) → - lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i m≤m+n) -lookup-take-inject≤ {m = m} m≤m+n xs i = begin - lookup (take m xs) i +lookup-take-inject≤ : (xs : Vec A (m + n)) (i : Fin m) → + lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n)) +lookup-take-inject≤ {m = m} {n = n} xs i = begin + lookup (take _ xs) i ≡⟨ cong (λ ys → lookup ys i) (take≡truncate m xs) ⟩ lookup (truncate _ xs) i - ≡⟨ cong (λ ys → lookup ys i) (truncate-irrelevant _ _ xs) ⟩ - lookup (truncate m≤m+n xs) i - ≡⟨ lookup-truncate m≤m+n xs i ⟩ - lookup xs (Fin.inject≤ i m≤m+n) - ∎ - where open ≡-Reasoning + ≡⟨ lookup-truncate (m≤m+n m n) xs i ⟩ + lookup xs (Fin.inject≤ i (m≤m+n m n)) + ∎ where open ≡-Reasoning ------------------------------------------------------------------------ -- updateAt (_[_]%=_) @@ -1305,7 +1303,13 @@ Please use drop-map instead." #-} lookup-inject≤-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) → lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i -lookup-inject≤-take m m≤m+n i xs = sym (lookup-take-inject≤ m≤m+n xs i) +lookup-inject≤-take m m≤m+n i xs = sym (begin + lookup (take m xs) i + ≡⟨ lookup-take-inject≤ xs i ⟩ + lookup xs (Fin.inject≤ i _) + ≡⟨ cong (lookup xs) (inject≤-irrelevant _ _ i) ⟩ + lookup xs (Fin.inject≤ i m≤m+n) + ∎) where open ≡-Reasoning {-# WARNING_ON_USAGE lookup-inject≤-take "Warning: lookup-inject≤-take was deprecated in v2.0. Please use lookup-take-inject≤ instead." From b7a82d31f7bbb59cf73cda2a9d1a1c66a54aa401 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 26 Sep 2023 06:58:46 +0100 Subject: [PATCH 22/28] simplified `Irrelevant` proofs --- src/Data/Fin/Properties.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index af2f4d0dfc..f198b90f1b 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -559,8 +559,7 @@ inject≤-injective (s≤s p) (s≤s q) (suc i) (suc j) eq = inject≤-irrelevant : ∀ (m≤n m≤n′ : m ℕ.≤ n) i → inject≤ i m≤n ≡ inject≤ i m≤n′ -inject≤-irrelevant (s≤s p) (s≤s q) zero = refl -inject≤-irrelevant (s≤s p) (s≤s q) (suc i) = cong suc (inject≤-irrelevant p q i) +inject≤-irrelevant m≤n m≤n′ i rewrite ℕₚ.≤-irrelevant m≤n m≤n′ = refl ------------------------------------------------------------------------ -- pred From 0c46dfad34b9552463a4adcc8ba924e163586f53 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 26 Sep 2023 07:09:33 +0100 Subject: [PATCH 23/28] simplified `Irrelevant` proofs; removed some cruft --- src/Data/Vec/Properties.agda | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index a19f1ef8ec..3e3ad53683 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -10,8 +10,8 @@ module Data.Vec.Properties where open import Algebra.Definitions open import Data.Bool.Base using (true; false) -open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_; _↑ʳ_) -open import Data.Fin.Properties as Fin using (inject≤-irrelevant) +open import Data.Fin.Base as Fin + using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_; _↑ʳ_) open import Data.List.Base as List using (List) import Data.List.Properties as Listₚ open import Data.Nat.Base @@ -123,8 +123,7 @@ truncate-trans z≤n n≤p xs = refl truncate-trans (s≤s m≤n) (s≤s n≤p) (x ∷ xs) = cong (x ∷_) (truncate-trans m≤n n≤p xs) truncate-irrelevant : (m≤n₁ m≤n₂ : m ≤ n) → truncate {A = A} m≤n₁ ≗ truncate m≤n₂ -truncate-irrelevant {m = zero} m≤n₁ m≤n₂ _ = refl -truncate-irrelevant (s≤s m≤n₁) (s≤s m≤n₂) (x ∷ xs) = cong (x ∷_) (truncate-irrelevant m≤n₁ m≤n₂ xs) +truncate-irrelevant m≤n₁ m≤n₂ xs rewrite ≤-irrelevant m≤n₁ m≤n₂ = refl truncate≡take : (m≤n : m ≤ n) (xs : Vec A n) .(eq : n ≡ m + o) → truncate m≤n xs ≡ take m (cast eq xs) @@ -430,9 +429,9 @@ map-updateAt (x ∷ xs) (suc i) eq = cong (_ ∷_) (map-updateAt xs i eq) map-insert : ∀ (f : A → B) (x : A) (xs : Vec A n) (i : Fin (suc n)) → map f (insert xs i x) ≡ insert (map f xs) i (f x) -map-insert f _ [] Fin.zero = refl -map-insert f _ (x' ∷ xs) Fin.zero = refl -map-insert f x (x' ∷ xs) (Fin.suc i) = cong (_ ∷_) (map-insert f x xs i) +map-insert f _ [] zero = refl +map-insert f _ (x' ∷ xs) zero = refl +map-insert f x (x' ∷ xs) (suc i) = cong (_ ∷_) (map-insert f x xs i) map-[]≔ : ∀ (f : A → B) (xs : Vec A n) (i : Fin n) → map f (xs [ i ]≔ x) ≡ map f xs [ i ]≔ f x @@ -1307,7 +1306,7 @@ lookup-inject≤-take m m≤m+n i xs = sym (begin lookup (take m xs) i ≡⟨ lookup-take-inject≤ xs i ⟩ lookup xs (Fin.inject≤ i _) - ≡⟨ cong (lookup xs) (inject≤-irrelevant _ _ i) ⟩ + ≡⟨ cong ((lookup xs) ∘ (Fin.inject≤ i)) (≤-irrelevant _ _) ⟩ lookup xs (Fin.inject≤ i m≤m+n) ∎) where open ≡-Reasoning {-# WARNING_ON_USAGE lookup-inject≤-take From c448d53df07cf9161d7f87fb916321f092cdc30c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 26 Sep 2023 07:15:51 +0100 Subject: [PATCH 24/28] turn `rewrite` in to `cong` --- src/Data/Fin/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index f198b90f1b..28a20abcca 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -559,7 +559,7 @@ inject≤-injective (s≤s p) (s≤s q) (suc i) (suc j) eq = inject≤-irrelevant : ∀ (m≤n m≤n′ : m ℕ.≤ n) i → inject≤ i m≤n ≡ inject≤ i m≤n′ -inject≤-irrelevant m≤n m≤n′ i rewrite ℕₚ.≤-irrelevant m≤n m≤n′ = refl +inject≤-irrelevant m≤n m≤n′ i = cong (inject≤ i) (ℕₚ.≤-irrelevant m≤n m≤n′) ------------------------------------------------------------------------ -- pred From 04bce7498e79caf535ece0f028b157bba8f41f45 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 26 Sep 2023 07:16:30 +0100 Subject: [PATCH 25/28] turn `rewrite` in to `cong` --- src/Data/Vec/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 3e3ad53683..d0fefbc84f 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -123,7 +123,7 @@ truncate-trans z≤n n≤p xs = refl truncate-trans (s≤s m≤n) (s≤s n≤p) (x ∷ xs) = cong (x ∷_) (truncate-trans m≤n n≤p xs) truncate-irrelevant : (m≤n₁ m≤n₂ : m ≤ n) → truncate {A = A} m≤n₁ ≗ truncate m≤n₂ -truncate-irrelevant m≤n₁ m≤n₂ xs rewrite ≤-irrelevant m≤n₁ m≤n₂ = refl +truncate-irrelevant m≤n₁ m≤n₂ xs = cong (λ m≤n → truncate m≤n xs) (≤-irrelevant m≤n₁ m≤n₂) truncate≡take : (m≤n : m ≤ n) (xs : Vec A n) .(eq : n ≡ m + o) → truncate m≤n xs ≡ take m (cast eq xs) From 6e121ba48c08679347462e772fdfb00729b67c03 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 26 Sep 2023 07:20:07 +0100 Subject: [PATCH 26/28] better deprecation warning advice --- src/Data/Vec/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index d0fefbc84f..7776bfbf5f 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -1311,6 +1311,6 @@ lookup-inject≤-take m m≤m+n i xs = sym (begin ∎) where open ≡-Reasoning {-# WARNING_ON_USAGE lookup-inject≤-take "Warning: lookup-inject≤-take was deprecated in v2.0. -Please use lookup-take-inject≤ instead." +Please use lookup-take-inject≤ or lookup-truncate, take≡truncate instead." #-} From d4d7054e4bde6357833e0b23ea0c9d2a56e6b685 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 26 Sep 2023 07:27:11 +0100 Subject: [PATCH 27/28] updated `Data.Fin.Properties` --- CHANGELOG.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index d37b086174..2c864a76b2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2155,6 +2155,9 @@ Additions to existing modules cast-trans : cast eq₂ (cast eq₁ k) ≡ cast (trans eq₁ eq₂) k fromℕ≢inject₁ : {i : Fin n} → fromℕ n ≢ inject₁ i + + inject≤-trans : inject≤ (inject≤ i m≤n) n≤o ≡ inject≤ i (≤-trans m≤n n≤o) + inject≤-irrelevant : inject≤ i m≤n ≡ inject≤ i m≤n′ ``` * Added new functions in `Data.Integer.Base`: From 824b744ab8ccccd01f18a085fc8e88bc1a89dbea Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Tue, 26 Sep 2023 13:03:20 +0100 Subject: [PATCH 28/28] Update Properties.agda: restored renaming from master --- src/Data/Vec/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 35745e95d1..c5b92ec2a1 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -23,7 +23,7 @@ open import Data.Sum.Base using ([_,_]′) open import Data.Sum.Properties using ([,]-map) open import Data.Vec.Base open import Function.Base -open import Function.Bundles using (_↔_; mk↔′) +open import Function.Bundles using (_↔_; mk↔ₛ′) open import Level using (Level) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality