From 385a651adf7503b015ce61a3545bd7376504a627 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 10:40:42 +0100 Subject: [PATCH 01/48] resolves issue #626; begins addressing issue #509 --- src/Data/List/Properties.agda | 85 +++++++++++++++++++++++++---------- 1 file changed, 61 insertions(+), 24 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 898f29f85f..a61319a0b3 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -9,7 +9,7 @@ {-# OPTIONS --without-K --safe #-} -module Data.List.Properties where +module Data.List.PropertiesNEW where open import Algebra.Bundles open import Algebra.Definitions as AlgebraicDefinitions using (Involutive) @@ -19,6 +19,7 @@ open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ; inject₁) open import Data.List.Base as List open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Relation.Unary.All using (All; []; _∷_) + renaming (tabulate to All-local) open import Data.List.Relation.Unary.Any using (Any; here; there) open import Data.Maybe.Base using (Maybe; just; nothing) open import Data.Nat.Base @@ -79,35 +80,41 @@ module _ {x y : A} {xs ys : List A} where ------------------------------------------------------------------------ -- map +map-id-local : ∀ {f : A → A} {xs} → All (λ x → f x ≡ x) xs → map f xs ≡ xs +map-id-local [] = refl +map-id-local (fx≡x ∷ pxs) = cong₂ _∷_ fx≡x (map-id-local pxs) + map-id : map id ≗ id {A = List A} map-id [] = refl map-id (x ∷ xs) = cong (x ∷_) (map-id xs) -map-id₂ : ∀ {f : A → A} {xs} → All (λ x → f x ≡ x) xs → map f xs ≡ xs -map-id₂ [] = refl -map-id₂ (fx≡x ∷ pxs) = cong₂ _∷_ fx≡x (map-id₂ pxs) +map-id' : map id ≗ id {A = List A} +map-id' xs = map-id-local (All-local λ _ → refl) -map-++-commute : ∀ (f : A → B) xs ys → +map-++ : ∀ (f : A → B) xs ys → map f (xs ++ ys) ≡ map f xs ++ map f ys -map-++-commute f [] ys = refl -map-++-commute f (x ∷ xs) ys = cong (f x ∷_) (map-++-commute f xs ys) +map-++ f [] ys = refl +map-++ f (x ∷ xs) ys = cong (f x ∷_) (map-++ f xs ys) + +map-cong-local : ∀ {f g : A → B} {xs} → + All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs +map-cong-local [] = refl +map-cong-local (fx≡gx ∷ fxs≡gxs) = cong₂ _∷_ fx≡gx (map-cong-local fxs≡gxs) map-cong : ∀ {f g : A → B} → f ≗ g → map f ≗ map g map-cong f≗g [] = refl map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (map-cong f≗g xs) -map-cong₂ : ∀ {f g : A → B} {xs} → - All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs -map-cong₂ [] = refl -map-cong₂ (fx≡gx ∷ fxs≡gxs) = cong₂ _∷_ fx≡gx (map-cong₂ fxs≡gxs) +map-cong' : ∀ {f g : A → B} → f ≗ g → map f ≗ map g +map-cong' f≗g xs = map-cong-local (All-local λ _ → f≗g _) length-map : ∀ (f : A → B) xs → length (map f xs) ≡ length xs length-map f [] = refl length-map f (x ∷ xs) = cong suc (length-map f xs) -map-compose : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f -map-compose [] = refl -map-compose (x ∷ xs) = cong (_ ∷_) (map-compose xs) +map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f +map-∘ [] = refl +map-∘ (x ∷ xs) = cong (_ ∷_) (map-∘ xs) map-injective : ∀ {f : A → B} → Injective _≡_ _≡_ f → Injective _≡_ _≡_ (map f) map-injective finj {[]} {[]} eq = refl @@ -260,16 +267,16 @@ module _ {f g : These A B → C} where alignWith-map : (g : D → A) (h : E → B) → ∀ xs ys → alignWith f (map g xs) (map h ys) ≡ alignWith (f ∘′ These.map g h) xs ys - alignWith-map g h [] ys = sym (map-compose ys) - alignWith-map g h xs@(_ ∷ _) [] = sym (map-compose xs) + alignWith-map g h [] ys = sym (map-∘ ys) + alignWith-map g h xs@(_ ∷ _) [] = sym (map-∘ xs) alignWith-map g h (x ∷ xs) (y ∷ ys) = cong₂ _∷_ refl (alignWith-map g h xs ys) map-alignWith : ∀ (g : C → D) → ∀ xs ys → map g (alignWith f xs ys) ≡ alignWith (g ∘′ f) xs ys - map-alignWith g [] ys = sym (map-compose ys) - map-alignWith g xs@(_ ∷ _) [] = sym (map-compose xs) + map-alignWith g [] ys = sym (map-∘ ys) + map-alignWith g xs@(_ ∷ _) [] = sym (map-∘ xs) map-alignWith g (x ∷ xs) (y ∷ ys) = cong₂ _∷_ refl (map-alignWith g xs ys) @@ -496,7 +503,7 @@ concat-map : ∀ {f : A → B} → concat ∘ map (map f) ≗ map f ∘ concat concat-map {f = f} xss = begin concat (map (map f) xss) ≡⟨ cong concat (map-is-foldr xss) ⟩ concat (foldr (λ xs → map f xs ∷_) [] xss) ≡⟨ foldr-fusion concat [] (λ _ _ → refl) xss ⟩ - foldr (λ ys → map f ys ++_) [] xss ≡⟨ sym (foldr-fusion (map f) [] (map-++-commute f) xss) ⟩ + foldr (λ ys → map f ys ++_) [] xss ≡⟨ sym (foldr-fusion (map f) [] (map-++ f) xss) ⟩ map f (concat xss) ∎ concat-++ : (xss yss : List (List A)) → concat xss ++ concat yss ≡ concat (xss ++ yss) @@ -518,10 +525,10 @@ concat-[-] (x ∷ xs) = cong (x ∷_) (concat-[-] xs) ------------------------------------------------------------------------ -- sum -sum-++-commute : ∀ xs ys → sum (xs ++ ys) ≡ sum xs + sum ys -sum-++-commute [] ys = refl -sum-++-commute (x ∷ xs) ys = begin - x + sum (xs ++ ys) ≡⟨ cong (x +_) (sum-++-commute xs ys) ⟩ +sum-++ : ∀ xs ys → sum (xs ++ ys) ≡ sum xs + sum ys +sum-++ [] ys = refl +sum-++ (x ∷ xs) ys = begin + x + sum (xs ++ ys) ≡⟨ cong (x +_) (sum-++ xs ys) ⟩ x + (sum xs + sum ys) ≡⟨ sym (+-assoc x _ _) ⟩ (x + sum xs) + sum ys ∎ @@ -564,7 +571,7 @@ scanl-defn f e (x ∷ xs) = cong (e ∷_) (begin map (foldl f (f e x)) (inits xs) ≡⟨ refl ⟩ map (foldl f e ∘ (x ∷_)) (inits xs) - ≡⟨ map-compose (inits xs) ⟩ + ≡⟨ map-∘ (inits xs) ⟩ map (foldl f e) (map (x ∷_) (inits xs)) ∎) @@ -1004,6 +1011,36 @@ module _ {x y : A} where -- Version 2.0 +map-id₂ = map-id-local +{-# WARNING_ON_USAGE map-id₂ +"Warning: map-id₂ was deprecated in v2.0. +Please use map-id-local instead." +#-} + +map-cong₂ = map-cong-local +{-# WARNING_ON_USAGE map-id₂ +"Warning: map-cong₂ was deprecated in v2.0. +Please use map-cong-local instead." +#-} + +map-compose = map-∘ +{-# WARNING_ON_USAGE map-compose +"Warning: map-compose was deprecated in v2.0. +Please use map-∘ instead." +#-} + +map-++-commute = map-++ +{-# WARNING_ON_USAGE map-++-commute +"Warning: map-++-commute was deprecated in v2.0. +Please use map-++ instead." +#-} + +sum-++-commute = sum-++ +{-# WARNING_ON_USAGE sum-++-commute +"Warning: map-++-commute was deprecated in v2.0. +Please use map-++ instead." +#-} + zipWith-identityˡ = zipWith-zeroˡ {-# WARNING_ON_USAGE zipWith-identityˡ "Warning: zipWith-identityˡ was deprecated in v2.0. From 0b28fa15795c10539300bc766ba5c93daa273c69 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 14:31:02 +0100 Subject: [PATCH 02/48] tidied up 'local' properties --- src/Data/List/Properties.agda | 23 ++++++++--------------- 1 file changed, 8 insertions(+), 15 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index a61319a0b3..7d50753707 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -9,7 +9,7 @@ {-# OPTIONS --without-K --safe #-} -module Data.List.PropertiesNEW where +module Data.List.Properties where open import Algebra.Bundles open import Algebra.Definitions as AlgebraicDefinitions using (Involutive) @@ -19,7 +19,6 @@ open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ; inject₁) open import Data.List.Base as List open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Relation.Unary.All using (All; []; _∷_) - renaming (tabulate to All-local) open import Data.List.Relation.Unary.Any using (Any; here; there) open import Data.Maybe.Base using (Maybe; just; nothing) open import Data.Nat.Base @@ -80,33 +79,27 @@ module _ {x y : A} {xs ys : List A} where ------------------------------------------------------------------------ -- map -map-id-local : ∀ {f : A → A} {xs} → All (λ x → f x ≡ x) xs → map f xs ≡ xs -map-id-local [] = refl -map-id-local (fx≡x ∷ pxs) = cong₂ _∷_ fx≡x (map-id-local pxs) - map-id : map id ≗ id {A = List A} map-id [] = refl map-id (x ∷ xs) = cong (x ∷_) (map-id xs) -map-id' : map id ≗ id {A = List A} -map-id' xs = map-id-local (All-local λ _ → refl) +map-id-local : ∀ {f : A → A} {xs} → All (λ x → f x ≡ x) xs → map f xs ≡ xs +map-id-local [] = refl +map-id-local (fx≡x ∷ pxs) = cong₂ _∷_ fx≡x (map-id-local pxs) map-++ : ∀ (f : A → B) xs ys → map f (xs ++ ys) ≡ map f xs ++ map f ys map-++ f [] ys = refl map-++ f (x ∷ xs) ys = cong (f x ∷_) (map-++ f xs ys) -map-cong-local : ∀ {f g : A → B} {xs} → - All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs -map-cong-local [] = refl -map-cong-local (fx≡gx ∷ fxs≡gxs) = cong₂ _∷_ fx≡gx (map-cong-local fxs≡gxs) - map-cong : ∀ {f g : A → B} → f ≗ g → map f ≗ map g map-cong f≗g [] = refl map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (map-cong f≗g xs) -map-cong' : ∀ {f g : A → B} → f ≗ g → map f ≗ map g -map-cong' f≗g xs = map-cong-local (All-local λ _ → f≗g _) +map-cong-local : ∀ {f g : A → B} {xs} → + All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs +map-cong-local [] = refl +map-cong-local (fx≡gx ∷ fxs≡gxs) = cong₂ _∷_ fx≡gx (map-cong-local fxs≡gxs) length-map : ∀ (f : A → B) xs → length (map f xs) ≡ length xs length-map f [] = refl From a05d59df02a64b73e057b6797fb1c9336857f772 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 14:45:33 +0100 Subject: [PATCH 03/48] knock-on changes --- src/Data/Fin/Substitution/List.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Fin/Substitution/List.agda b/src/Data/Fin/Substitution/List.agda index 1ce9ee7340..dddce8b278 100644 --- a/src/Data/Fin/Substitution/List.agda +++ b/src/Data/Fin/Substitution/List.agda @@ -39,7 +39,7 @@ appLemmas = record ts ∎ ; /-⊙ = λ {_ _ _ ρ₁ ρ₂} ts → begin ts // ρ₁ ⊙ ρ₂ ≡⟨ map-cong L./-⊙ ts ⟩ - map (λ σ → σ / ρ₁ / ρ₂) ts ≡⟨ map-compose ts ⟩ + map (λ σ → σ / ρ₁ / ρ₂) ts ≡⟨ map-∘ ts ⟩ ts // ρ₁ // ρ₂ ∎ } From 55e8b643106f06f3a4380d49cd8b983d4aa35360 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 14:50:29 +0100 Subject: [PATCH 04/48] knock-on changes --- src/Data/List/NonEmpty/Properties.agda | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda index e961fc402b..f14fe8e533 100644 --- a/src/Data/List/NonEmpty/Properties.agda +++ b/src/Data/List/NonEmpty/Properties.agda @@ -60,7 +60,7 @@ toList->>= : ∀ (f : A → List⁺ B) (xs : List⁺ A) → (toList xs ⋆>>= toList ∘ f) ≡ toList (xs >>= f) toList->>= f (x ∷ xs) = begin List.concat (List.map (toList ∘ f) (x ∷ xs)) - ≡⟨ cong List.concat $ List.map-compose {g = toList} (x ∷ xs) ⟩ + ≡⟨ cong List.concat $ List.map-∘ {g = toList} (x ∷ xs) ⟩ List.concat (List.map toList (List.map f (x ∷ xs))) ∎ @@ -110,8 +110,8 @@ length-map f (_ ∷ xs) = cong suc (List.length-map f xs) map-cong : ∀ {f g : A → B} → f ≗ g → map f ≗ map g map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (List.map-cong f≗g xs) -map-compose : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f -map-compose (x ∷ xs) = cong (_ ∷_) (List.map-compose xs) +map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f +map-∘ (x ∷ xs) = cong (_ ∷_) (List.map-∘ xs) ------------------------------------------------------------------------ -- groupSeqs @@ -142,3 +142,17 @@ module _ {P : Pred A p} (P? : Decidable P) where ... | false | inj₁ _ ∷ _ | hyp = cong (x ∷_) hyp ... | false | inj₂ _ ∷ _ | hyp = cong (x ∷_) hyp +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +map-compose = map-∘ +{-# WARNING_ON_USAGE map-compose +"Warning: map-compose was deprecated in v2.0. +Please use map-∘ instead." +#-} + From eb9e3eef89fe32673566db34221f4d9538b01029 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 15:02:27 +0100 Subject: [PATCH 05/48] knock-on changes --- src/Data/List/Properties.agda | 20 ++++++-- src/Data/List/Zipper/Properties.agda | 71 +++++++++++++++++++++------- 2 files changed, 71 insertions(+), 20 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 7d50753707..17f4159c86 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -927,9 +927,9 @@ unfold-reverse x xs = ʳ++-defn xs -- reverse is an involution with respect to append. -reverse-++-commute : (xs ys : List A) → +reverse-++ : (xs ys : List A) → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs -reverse-++-commute xs ys = begin +reverse-++ xs ys = begin reverse (xs ++ ys) ≡⟨⟩ (xs ++ ys) ʳ++ [] ≡⟨ ʳ++-++ xs ⟩ ys ʳ++ xs ʳ++ [] ≡⟨⟩ @@ -960,8 +960,8 @@ length-reverse xs = begin length xs + 0 ≡⟨ +-identityʳ _ ⟩ length xs ∎ -reverse-map-commute : (f : A → B) → map f ∘ reverse ≗ reverse ∘ map f -reverse-map-commute f xs = begin +reverse-map : (f : A → B) → map f ∘ reverse ≗ reverse ∘ map f +reverse-map f xs = begin map f (reverse xs) ≡⟨⟩ map f (xs ʳ++ []) ≡⟨ map-ʳ++ f xs ⟩ map f xs ʳ++ [] ≡⟨⟩ @@ -1034,6 +1034,18 @@ sum-++-commute = sum-++ Please use map-++ instead." #-} +reverse-map-commute = reverse-map +{-# WARNING_ON_USAGE reverse-map-commute +"Warning: reverse-map-commute was deprecated in v2.0. +Please use reverse-map instead." +#-} + +reverse-++-commute = reverse-++ +{-# WARNING_ON_USAGE reverse-++-commute +"Warning: reverse-++-commute was deprecated in v2.0. +Please use reverse-++ instead." +#-} + zipWith-identityˡ = zipWith-zeroˡ {-# WARNING_ON_USAGE zipWith-identityˡ "Warning: zipWith-identityˡ was deprecated in v2.0. diff --git a/src/Data/List/Zipper/Properties.agda b/src/Data/List/Zipper/Properties.agda index 7da32c5b89..549ee034f7 100644 --- a/src/Data/List/Zipper/Properties.agda +++ b/src/Data/List/Zipper/Properties.agda @@ -46,12 +46,12 @@ module _ {a} {A : Set a} where -- Applying reverse does correspond to reversing the represented list - toList-reverse-commute : (zp : Zipper A) → toList (reverse zp) ≡ List.reverse (toList zp) - toList-reverse-commute (mkZipper ctx val) = begin + toList-reverse : (zp : Zipper A) → toList (reverse zp) ≡ List.reverse (toList zp) + toList-reverse (mkZipper ctx val) = begin List.reverse val List.++ ctx ≡⟨ cong (List.reverse val List.++_) (sym (reverse-involutive ctx)) ⟩ List.reverse val List.++ List.reverse (List.reverse ctx) - ≡⟨ sym (reverse-++-commute (List.reverse ctx) val) ⟩ + ≡⟨ sym (reverse-++ (List.reverse ctx) val) ⟩ List.reverse (List.reverse ctx List.++ val) ∎ @@ -61,10 +61,10 @@ module _ {a} {A : Set a} where -- _ˡ++_ properties - toList-ˡ++-commute : ∀ xs (zp : Zipper A) → toList (xs ˡ++ zp) ≡ xs List.++ toList zp - toList-ˡ++-commute xs (mkZipper ctx val) = begin + toList-ˡ++ : ∀ xs (zp : Zipper A) → toList (xs ˡ++ zp) ≡ xs List.++ toList zp + toList-ˡ++ xs (mkZipper ctx val) = begin List.reverse (ctx List.++ List.reverse xs) List.++ val - ≡⟨ cong (List._++ _) (reverse-++-commute ctx (List.reverse xs)) ⟩ + ≡⟨ cong (List._++ _) (reverse-++ ctx (List.reverse xs)) ⟩ (List.reverse (List.reverse xs) List.++ List.reverse ctx) List.++ val ≡⟨ ++-assoc (List.reverse (List.reverse xs)) (List.reverse ctx) val ⟩ List.reverse (List.reverse xs) List.++ List.reverse ctx List.++ val @@ -77,7 +77,7 @@ module _ {a} {A : Set a} where (ctx List.++ List.reverse ys) List.++ List.reverse xs ≡⟨ ++-assoc ctx _ _ ⟩ ctx List.++ List.reverse ys List.++ List.reverse xs - ≡⟨ cong (ctx List.++_) (sym (reverse-++-commute xs ys)) ⟩ + ≡⟨ cong (ctx List.++_) (sym (reverse-++ xs ys)) ⟩ ctx List.++ List.reverse (xs List.++ ys) ∎ @@ -88,7 +88,7 @@ module _ {a} {A : Set a} where List.reverse xs List.++ List.reverse ys List.++ ctx ≡⟨ sym (++-assoc (List.reverse xs) (List.reverse ys) ctx) ⟩ (List.reverse xs List.++ List.reverse ys) List.++ ctx - ≡⟨ cong (List._++ ctx) (sym (reverse-++-commute ys xs)) ⟩ + ≡⟨ cong (List._++ ctx) (sym (reverse-++ ys xs)) ⟩ List.reverse (ys List.++ xs) List.++ ctx ∎ @@ -99,8 +99,8 @@ module _ {a} {A : Set a} where -- _++ʳ_ properties - toList-++ʳ-commute : ∀ (zp : Zipper A) xs → toList (zp ++ʳ xs) ≡ toList zp List.++ xs - toList-++ʳ-commute (mkZipper ctx val) xs = begin + toList-++ʳ : ∀ (zp : Zipper A) xs → toList (zp ++ʳ xs) ≡ toList zp List.++ xs + toList-++ʳ (mkZipper ctx val) xs = begin List.reverse ctx List.++ val List.++ xs ≡⟨ sym (++-assoc (List.reverse ctx) val xs) ⟩ (List.reverse ctx List.++ val) List.++ xs @@ -115,20 +115,59 @@ module _ {a} {A : Set a} where module _ {a b} {A : Set a} {B : Set b} where - toList-map-commute : ∀ (f : A → B) zp → toList (map f zp) ≡ List.map f (toList zp) - toList-map-commute f zp@(mkZipper ctx val) = begin + toList-map : ∀ (f : A → B) zp → toList (map f zp) ≡ List.map f (toList zp) + toList-map f zp@(mkZipper ctx val) = begin List.reverse (List.map f ctx) List.++ List.map f val - ≡⟨ cong (List._++ _) (sym (reverse-map-commute f ctx)) ⟩ + ≡⟨ cong (List._++ _) (sym (reverse-map f ctx)) ⟩ List.map f (List.reverse ctx) List.++ List.map f val - ≡⟨ sym (map-++-commute f (List.reverse ctx) val) ⟩ + ≡⟨ sym (map-++ f (List.reverse ctx) val) ⟩ List.map f (List.reverse ctx List.++ val) ∎ - toList-foldr-commute : ∀ (c : A → B → B) n zp → foldr c n zp ≡ List.foldr c n (toList zp) - toList-foldr-commute c n (mkZipper ctx val) = begin + toList-foldr : ∀ (c : A → B → B) n zp → foldr c n zp ≡ List.foldr c n (toList zp) + toList-foldr c n (mkZipper ctx val) = begin List.foldl (flip c) (List.foldr c n val) ctx ≡⟨ sym (reverse-foldr c (List.foldr c n val) ctx) ⟩ List.foldr c (List.foldr c n val) (List.reverse ctx) ≡⟨ sym (foldr-++ c n (List.reverse ctx) val) ⟩ List.foldr c n (List.reverse ctx List.++ val) ∎ + +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +toList-reverse-commute = toList-reverse +{-# WARNING_ON_USAGE toList-reverse-commute +"Warning: toList-reverse-commute was deprecated in v2.0. +Please use toList-reverse instead." +#-} + +toList-ˡ++-commute = toList-ˡ++ +{-# WARNING_ON_USAGE toList-ˡ++-commute +"Warning: toList-ˡ++-commute was deprecated in v2.0. +Please use toList-ˡ++ instead." +#-} + +toList-++ʳ-commute = toList-++ʳ +{-# WARNING_ON_USAGE toList-++ʳ-commute +"Warning: toList-++ʳ-commute was deprecated in v2.0. +Please use toList-++ʳ instead." +#-} + +toList-map-commute = toList-map +{-# WARNING_ON_USAGE toList-map-commute +"Warning: toList-map-commute was deprecated in v2.0. +Please use toList-map instead." +#-} + +toList-foldr-commute = toList-foldr +{-# WARNING_ON_USAGE toList-foldr-commute +"Warning: toList-foldr-commute was deprecated in v2.0. +Please use toList-foldr instead." +#-} + From f35c323633aef9aabc9938fb1c308452bb0776c8 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 15:33:14 +0100 Subject: [PATCH 06/48] more knock-on changes --- .../List/Relation/Binary/Suffix/Heterogeneous/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda index 8438609c61..36aa5259f6 100644 --- a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda @@ -42,7 +42,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where fromPrefix {as} {bs} p with Prefix.toView p ... | Prefix._++_ {cs} rs ds = subst (Suffix R (reverse as)) - (sym (Listₚ.reverse-++-commute cs ds)) + (sym (Listₚ.reverse-++ cs ds)) (Suffix.fromView (reverse ds Suffix.++ Pw.reverse⁺ rs)) fromPrefix-rev : ∀ {as bs} → Prefix R (reverse as) (reverse bs) → @@ -58,7 +58,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where toPrefix-rev {as} {bs} s with Suffix.toView s ... | Suffix._++_ cs {ds} rs = subst (Prefix R (reverse as)) - (sym (Listₚ.reverse-++-commute cs ds)) + (sym (Listₚ.reverse-++ cs ds)) (Prefix.fromView (Pw.reverse⁺ rs Prefix.++ reverse cs)) toPrefix : ∀ {as bs} → Suffix R (reverse as) (reverse bs) → From 41ae9f0a66669ba8b2a1199bdcf82ad6978e50e6 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 16:32:19 +0100 Subject: [PATCH 07/48] more knock-on changes --- src/Data/Tree/Rose/Properties.agda | 27 +++++++++++++++++++++------ 1 file changed, 21 insertions(+), 6 deletions(-) diff --git a/src/Data/Tree/Rose/Properties.agda b/src/Data/Tree/Rose/Properties.agda index 51d19732dc..de8add35e4 100644 --- a/src/Data/Tree/Rose/Properties.agda +++ b/src/Data/Tree/Rose/Properties.agda @@ -30,16 +30,16 @@ private ------------------------------------------------------------------------ -- map properties -map-compose : (f : A → B) (g : B → C) → +map-∘ : (f : A → B) (g : B → C) → map {i = i} (g ∘′ f) ≗ map {i = i} g ∘′ map {i = i} f -map-compose f g (node a ts) = cong (node (g (f a))) $ begin - List.map (map (g ∘′ f)) ts ≡⟨ Listₚ.map-cong (map-compose f g) ts ⟩ - List.map (map g ∘ map f) ts ≡⟨ Listₚ.map-compose ts ⟩ +map-∘ f g (node a ts) = cong (node (g (f a))) $ begin + List.map (map (g ∘′ f)) ts ≡⟨ Listₚ.map-cong (map-∘ f g) ts ⟩ + List.map (map g ∘ map f) ts ≡⟨ Listₚ.map-∘ ts ⟩ List.map (map g) (List.map (map f) ts) ∎ depth-map : (f : A → B) (t : Rose A i) → depth {i = i} (map {i = i} f t) ≡ depth {i = i} t depth-map f (node a ts) = cong (suc ∘′ max 0) $ begin - List.map depth (List.map (map f) ts) ≡˘⟨ Listₚ.map-compose ts ⟩ + List.map depth (List.map (map f) ts) ≡˘⟨ Listₚ.map-∘ ts ⟩ List.map (depth ∘′ map f) ts ≡⟨ Listₚ.map-cong (depth-map f) ts ⟩ List.map depth ts ∎ @@ -49,6 +49,21 @@ depth-map f (node a ts) = cong (suc ∘′ max 0) $ begin foldr-map : (f : A → B) (n : B → List C → C) (ts : Rose A i) → foldr {i = i} n (map {i = i} f ts) ≡ foldr {i = i} (n ∘′ f) ts foldr-map f n (node a ts) = cong (n (f a)) $ begin - List.map (foldr n) (List.map (map f) ts) ≡˘⟨ Listₚ.map-compose ts ⟩ + List.map (foldr n) (List.map (map f) ts) ≡˘⟨ Listₚ.map-∘ ts ⟩ List.map (foldr n ∘′ map f) ts ≡⟨ Listₚ.map-cong (foldr-map f n) ts ⟩ List.map (foldr (n ∘′ f)) ts ∎ + +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +map-compose = map-∘ +{-# WARNING_ON_USAGE map-compose +"Warning: map-compose was deprecated in v2.0. +Please use map-∘ instead." +#-} + From 2b8fc52fd6ea9fe8592a9e0478c25ad060ea1c4f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 16:35:08 +0100 Subject: [PATCH 08/48] more knock-on changes --- src/Data/List/NonEmpty/Properties.agda | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda index f14fe8e533..5b6c41c50b 100644 --- a/src/Data/List/NonEmpty/Properties.agda +++ b/src/Data/List/NonEmpty/Properties.agda @@ -96,10 +96,10 @@ drop-+-++⁺ : ∀ (xs : List A) ys → drop+ (List.length xs) (xs ++⁺ ys) ≡ drop-+-++⁺ [] ys = refl drop-+-++⁺ (x ∷ xs) ys = drop-+-++⁺ xs ys -map-++⁺-commute : ∀ (f : A → B) xs ys → +map-++⁺ : ∀ (f : A → B) xs ys → map f (xs ++⁺ ys) ≡ List.map f xs ++⁺ map f ys -map-++⁺-commute f [] ys = refl -map-++⁺-commute f (x ∷ xs) ys = cong (λ zs → f x ∷ toList zs) (map-++⁺-commute f xs ys) +map-++⁺ f [] ys = refl +map-++⁺ f (x ∷ xs) ys = cong (λ zs → f x ∷ toList zs) (map-++⁺ f xs ys) ------------------------------------------------------------------------ -- map @@ -156,3 +156,9 @@ map-compose = map-∘ Please use map-∘ instead." #-} +map-++⁺-commute = map-++⁺ +{-# WARNING_ON_USAGE map-++⁺-commute +"Warning: map-++⁺-commute was deprecated in v2.0. +Please use map-++⁺ instead." +#-} + From 05fac98d6f003425a519e1cfc976d4e3b9d24c28 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 17:10:05 +0100 Subject: [PATCH 09/48] trailing whitespace --- src/Data/List/NonEmpty/Properties.agda | 1 - src/Data/List/Zipper/Properties.agda | 1 - src/Data/Tree/Rose/Properties.agda | 1 - 3 files changed, 3 deletions(-) diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda index 5b6c41c50b..938e721002 100644 --- a/src/Data/List/NonEmpty/Properties.agda +++ b/src/Data/List/NonEmpty/Properties.agda @@ -161,4 +161,3 @@ map-++⁺-commute = map-++⁺ "Warning: map-++⁺-commute was deprecated in v2.0. Please use map-++⁺ instead." #-} - diff --git a/src/Data/List/Zipper/Properties.agda b/src/Data/List/Zipper/Properties.agda index 549ee034f7..30ea57a9c2 100644 --- a/src/Data/List/Zipper/Properties.agda +++ b/src/Data/List/Zipper/Properties.agda @@ -170,4 +170,3 @@ toList-foldr-commute = toList-foldr "Warning: toList-foldr-commute was deprecated in v2.0. Please use toList-foldr instead." #-} - diff --git a/src/Data/Tree/Rose/Properties.agda b/src/Data/Tree/Rose/Properties.agda index de8add35e4..a7ab845999 100644 --- a/src/Data/Tree/Rose/Properties.agda +++ b/src/Data/Tree/Rose/Properties.agda @@ -66,4 +66,3 @@ map-compose = map-∘ "Warning: map-compose was deprecated in v2.0. Please use map-∘ instead." #-} - From 00e17114db1f2102ce29fd67903d5df45c1c7dc5 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 17:29:27 +0100 Subject: [PATCH 10/48] yet more... --- src/Data/Maybe/Properties.agda | 56 ++++++++++++++++++++++++++-------- 1 file changed, 44 insertions(+), 12 deletions(-) diff --git a/src/Data/Maybe/Properties.agda b/src/Data/Maybe/Properties.agda index 018e364899..2ade049d6e 100644 --- a/src/Data/Maybe/Properties.agda +++ b/src/Data/Maybe/Properties.agda @@ -47,31 +47,31 @@ map-id : map id ≗ id {A = Maybe A} map-id (just x) = refl map-id nothing = refl -map-id₂ : ∀ {f : A → A} {mx} → All (λ x → f x ≡ x) mx → map f mx ≡ mx -map-id₂ (just eq) = cong just eq -map-id₂ nothing = refl +map-id-local : ∀ {f : A → A} {mx} → All (λ x → f x ≡ x) mx → map f mx ≡ mx +map-id-local (just eq) = cong just eq +map-id-local nothing = refl -map-<∣>-commute : ∀ (f : A → B) mx my → +map-<∣> : ∀ (f : A → B) mx my → map f (mx <∣> my) ≡ map f mx <∣> map f my -map-<∣>-commute f (just x) my = refl -map-<∣>-commute f nothing my = refl +map-<∣> f (just x) my = refl +map-<∣> f nothing my = refl map-cong : {f g : A → B} → f ≗ g → map f ≗ map g map-cong f≗g (just x) = cong just (f≗g x) map-cong f≗g nothing = refl -map-cong₂ : ∀ {f g : A → B} {mx} → +map-cong-local : ∀ {f g : A → B} {mx} → All (λ x → f x ≡ g x) mx → map f mx ≡ map g mx -map-cong₂ (just eq) = cong just eq -map-cong₂ nothing = refl +map-cong-local (just eq) = cong just eq +map-cong-local nothing = refl map-injective : ∀ {f : A → B} → Injective _≡_ _≡_ f → Injective _≡_ _≡_ (map f) map-injective f-inj {nothing} {nothing} p = refl map-injective f-inj {just x} {just y} p = cong just (f-inj (just-injective p)) -map-compose : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f -map-compose (just x) = refl -map-compose nothing = refl +map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f +map-∘ (just x) = refl +map-∘ nothing = refl map-nothing : ∀ {f : A → B} {ma} → ma ≡ nothing → map f ma ≡ nothing map-nothing refl = refl @@ -149,3 +149,35 @@ module _ (A : Set a) where <∣>-monoid = record { isMonoid = <∣>-isMonoid } + +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +map-id₂ = map-id-local +{-# WARNING_ON_USAGE map-id₂ +"Warning: map-id₂ was deprecated in v2.0. +Please use map-id-local instead." +#-} + +map-cong₂ = map-cong-local +{-# WARNING_ON_USAGE map-id₂ +"Warning: map-cong₂ was deprecated in v2.0. +Please use map-cong-local instead." +#-} + +map-compose = map-∘ +{-# WARNING_ON_USAGE map-compose +"Warning: map-compose was deprecated in v2.0. +Please use map-∘ instead." +#-} + +map-<∣>-commute = map-<∣> +{-# WARNING_ON_USAGE map-<∣>-commute +"Warning: map-<∣>-commute was deprecated in v2.0. +Please use map-<∣> instead." +#-} From de758c831c04a575427d88912b6c67ca724aaa0e Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 11:35:30 +0100 Subject: [PATCH 11/48] first steps in #1686: nonzero for Fin/Vec --- src/Data/Fin/Base.agda | 68 ++++++++++++++++++++++++++++++++++++ src/Data/Fin/Properties.agda | 13 +++++-- src/Data/Vec/Base.agda | 22 ++++++++++++ src/Data/Vec/Properties.agda | 31 ++++++++++++++-- 4 files changed, 129 insertions(+), 5 deletions(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index ce93b67b01..10e8c301c3 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -11,6 +11,7 @@ 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; uncurry) open import Data.Sum.Base using ([_,_]′) -open import Data.Sum.Properties using ([,]-map-commute) +open import Data.Sum.Properties + renaming ([,]-map-commute to [,]-map) + hiding (≡-dec; map-id; map-cong) open import Data.Vec.Base open import Function.Base open import Function.Inverse using (_↔_; inverse) @@ -483,7 +485,7 @@ lookup-splitAt zero [] ys i = refl lookup-splitAt (suc m) (x ∷ xs) ys zero = refl lookup-splitAt (suc m) (x ∷ xs) ys (suc i) = trans (lookup-splitAt m xs ys i) - (sym ([,]-map-commute (Fin.splitAt m i))) + (sym ([,]-map (Fin.splitAt m i))) ------------------------------------------------------------------------ -- concat @@ -1014,12 +1016,22 @@ insert-lookup : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) → insert-lookup xs zero v = refl insert-lookup (x ∷ xs) (suc i) v = insert-lookup xs i v +NZinsert-lookup : .{{_ : NonZero n}} → + (xs : Vec A (pred n)) (i : Fin n) (v : A) → + lookup (NZinsert xs i v) i ≡ v +NZinsert-lookup {n = suc n} = insert-lookup + insert-punchIn : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) (j : Fin n) → lookup (insert xs i v) (Fin.punchIn i j) ≡ lookup xs j insert-punchIn xs zero v j = refl insert-punchIn (x ∷ xs) (suc i) v zero = refl insert-punchIn (x ∷ xs) (suc i) v (suc j) = insert-punchIn xs i v j +NZinsert-punchIn : .{{_ : NonZero n}} → + (xs : Vec A (pred n)) (i : Fin n) (v : A) (j : Fin (pred n)) → + lookup (NZinsert xs i v) (Fin.NZpunchIn i j) ≡ lookup xs j +NZinsert-punchIn {n = suc n} = insert-punchIn + remove-punchOut : ∀ (xs : Vec A (suc n)) {i} {j} (i≢j : i ≢ j) → lookup (remove xs i) (Fin.punchOut i≢j) ≡ lookup xs j remove-punchOut (x ∷ xs) {zero} {zero} i≢j = contradiction refl i≢j @@ -1028,6 +1040,11 @@ remove-punchOut (x ∷ y ∷ xs) {suc i} {zero} i≢j = refl remove-punchOut (x ∷ y ∷ xs) {suc i} {suc j} i≢j = remove-punchOut (y ∷ xs) (i≢j ∘ cong suc) +NZremove-punchOut : .{{_ : NonZero n}} → + ∀ (xs : Vec A n) {i} {j} (i≢j : i ≢ j) → + lookup (NZremove xs i) (Fin.NZpunchOut i≢j) ≡ lookup xs j +NZremove-punchOut {n = suc n} = remove-punchOut + ------------------------------------------------------------------------ -- remove @@ -1038,12 +1055,22 @@ remove-insert (x ∷ xs) (suc zero) v = refl remove-insert (x ∷ y ∷ xs) (suc (suc i)) v = cong (x ∷_) (remove-insert (y ∷ xs) (suc i) v) +NZremove-insert : .{{_ : NonZero n}} → + ∀ (xs : Vec A (pred n)) (i : Fin n) (v : A) → + NZremove (NZinsert xs i v) i ≡ xs +NZremove-insert {n = suc n} = remove-insert + insert-remove : ∀ (xs : Vec A (suc n)) (i : Fin (suc n)) → insert (remove xs i) i (lookup xs i) ≡ xs insert-remove (x ∷ xs) zero = refl insert-remove (x ∷ y ∷ xs) (suc i) = cong (x ∷_) (insert-remove (y ∷ xs) i) +NZinsert-remove : .{{_ : NonZero n}} → + ∀ (xs : Vec A n) (i : Fin n) → + NZinsert (NZremove xs i) i (lookup xs i) ≡ xs +NZinsert-remove {n = suc n} = insert-remove + ------------------------------------------------------------------------ -- Conversion function From ef995995ffb1ef9ef933ab557dec7447e7df9f2f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 12:59:59 +0100 Subject: [PATCH 12/48] more nonzero properties for Fin --- src/Data/Fin/Base.agda | 14 ++++++++--- src/Data/Fin/Properties.agda | 45 ++++++++++++++++++++++++++++++++++-- 2 files changed, 54 insertions(+), 5 deletions(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index 10e8c301c3..86f8c152e2 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -43,6 +43,11 @@ data Fin : ℕ → Set where NZzero : .{{ℕ.NonZero n}} → Fin n NZzero {n = suc n} = zero +-- uniform successor + +NZsuc : .{{ℕ.NonZero n}} → Fin (ℕ.pred n) → Fin n +NZsuc {n = suc n} = suc + -- NonZero predicate isZero : (i : Fin (suc n)) → Bool @@ -169,6 +174,9 @@ inject₁ : Fin n → Fin (suc n) inject₁ zero = zero inject₁ (suc i) = suc (inject₁ i) +NZinject₁ : .{{_ : ℕ.NonZero n}} → Fin (ℕ.pred n) → Fin n +NZinject₁ {n = suc n} = inject₁ + inject≤ : Fin m → m ℕ.≤ n → Fin n inject≤ {_} {suc n} zero _ = zero inject≤ {_} {suc n} (suc i) (s≤s m≤n) = suc (inject≤ i m≤n) @@ -178,10 +186,10 @@ inject≤ {_} {suc n} (suc i) (s≤s m≤n) = suc (inject≤ i m≤n) lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n lower₁ {zero} zero ne = ⊥-elim (ne refl) lower₁ {suc n} zero _ = zero -lower₁ {suc n} (suc i) ne = suc (lower₁ i λ x → ne (cong suc x)) +lower₁ {suc n} (suc i) ne = suc (lower₁ i (ne ∘ cong suc)) -NZlower₁ : .{{ℕ.NonZero n}} → (i : Fin n) → (ℕ.pred n) ≢ toℕ i → Fin (ℕ.pred n) -NZlower₁ {n = suc n} i = lower₁ i +NZlower₁ : .{{ℕ.NonZero n}} → (i : Fin n) → n ≢ suc (toℕ i) → Fin (ℕ.pred n) +NZlower₁ {n = suc n} i ne = lower₁ i (ne ∘ cong suc) -- A strengthening injection into the minimal Fin fibre. strengthen : ∀ (i : Fin n) → Fin′ (suc i) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 644d65f99d..c4e8cfee67 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -203,7 +203,7 @@ fromℕ-toℕ (suc i) = cong suc (fromℕ-toℕ i) ≤fromℕ : ∀ (i : Fin (ℕ.suc n)) → i ≤ fromℕ n ≤fromℕ i = subst (toℕ i ℕ.≤_) (sym (toℕ-fromℕ _)) (toℕ≤pred[n] i) -NZ≤fromℕ : ∀ .{{_ : ℕ.NonZero n}} (i : Fin n) → i ≤ fromℕ (ℕ.pred n) +NZ≤fromℕ : .{{_ : ℕ.NonZero n}} (i : Fin n) → i ≤ fromℕ (ℕ.pred n) NZ≤fromℕ {n = suc n} i = ≤fromℕ i ------------------------------------------------------------------------ @@ -491,6 +491,11 @@ inject₁-lower₁ {suc n} zero _ = refl inject₁-lower₁ {suc n} (suc i) n+1≢i+1 = cong suc (inject₁-lower₁ i (n+1≢i+1 ∘ cong suc)) +NZinject₁-lower₁ : .{{_ : ℕ.NonZero n}} → + ∀ (i : Fin n) (n≢i+1 : n ≢ suc (toℕ i)) → + NZinject₁ (NZlower₁ i n≢i+1) ≡ i +NZinject₁-lower₁ {n = suc n} i n≢i+1 = inject₁-lower₁ i (n≢i+1 ∘ cong suc) + lower₁-inject₁′ : ∀ (i : Fin n) (n≢i : n ≢ toℕ (inject₁ i)) → lower₁ (inject₁ i) n≢i ≡ i lower₁-inject₁′ zero _ = refl @@ -508,10 +513,20 @@ lower₁-irrelevant {suc n} zero _ _ = refl lower₁-irrelevant {suc n} (suc i) _ _ = cong suc (lower₁-irrelevant i _ _) +NZlower₁-irrelevant : .{{_ : ℕ.NonZero n}} → + ∀ (i : Fin n) (n≢i₁+1 n≢i₂+1 : n ≢ suc (toℕ i)) → + NZlower₁ i n≢i₁+1 ≡ NZlower₁ i n≢i₂+1 +NZlower₁-irrelevant {n = suc n} i n≢i₁+1 n≢i₂+1 = lower₁-irrelevant i (n≢i₁+1 ∘ cong suc) (n≢i₂+1 ∘ cong suc) + inject₁≡⇒lower₁≡ : ∀ {i : Fin n} {j : Fin (ℕ.suc n)} → (n≢j : n ≢ toℕ j) → inject₁ i ≡ j → lower₁ j n≢j ≡ i inject₁≡⇒lower₁≡ n≢j i≡j = inject₁-injective (trans (inject₁-lower₁ _ n≢j) (sym i≡j)) +NZinject₁≡⇒lower₁≡ : .{{_ : ℕ.NonZero n}} → + ∀ {i : Fin (ℕ.pred n)} {j : Fin n} → + (n≢j+1 : n ≢ suc (toℕ j)) → NZinject₁ i ≡ j → NZlower₁ j n≢j+1 ≡ i +NZinject₁≡⇒lower₁≡ {n = suc n} n≢j+1 = inject₁≡⇒lower₁≡ (n≢j+1 ∘ cong suc) + ------------------------------------------------------------------------ -- inject≤ ------------------------------------------------------------------------ @@ -545,7 +560,7 @@ pred< : ∀ (i : Fin (suc n)) → i ≢ zero → pred i < i pred< zero i≢0 = contradiction refl i≢0 pred< (suc i) _ = ≤̄⇒inject₁< ℕₚ.≤-refl -NZpred< : ∀ .{{_ : ℕ.NonZero n}} (i : Fin n) → i ≢ NZzero → pred i < i +NZpred< : ∀ .{{_ : ℕ.NonZero n}} → (i : Fin n) → i ≢ NZzero → pred i < i NZpred< {n = suc n} i = pred< i ------------------------------------------------------------------------ @@ -821,6 +836,11 @@ punchOut-cong {_} zero {suc j} {suc k} = suc-injective punchOut-cong {suc n} (suc i) {zero} {zero} _ = refl punchOut-cong {suc n} (suc i) {suc j} {suc k} = cong suc ∘ punchOut-cong i ∘ suc-injective +NZpunchOut-cong : .{{_ : ℕ.NonZero n}} → + ∀ (i : Fin n) {j k} {i≢j : i ≢ j} {i≢k : i ≢ k} → + j ≡ k → NZpunchOut i≢j ≡ NZpunchOut i≢k +NZpunchOut-cong {n = suc n} = punchOut-cong + -- An alternative to 'punchOut-cong' in the which the new inequality argument is -- specific. Useful for enabling the omission of that argument during equational -- reasoning. @@ -829,6 +849,11 @@ punchOut-cong′ : ∀ (i : Fin (suc n)) {j k} {p : i ≢ j} (q : j ≡ k) → punchOut p ≡ punchOut (p ∘ sym ∘ trans q ∘ sym) punchOut-cong′ i q = punchOut-cong i q +NZpunchOut-cong′ : .{{_ : ℕ.NonZero n}} → + ∀ (i : Fin n) {j k} {p : i ≢ j} (q : j ≡ k) → + NZpunchOut p ≡ NZpunchOut (p ∘ sym ∘ trans q ∘ sym) +NZpunchOut-cong′ {n = suc n} = punchOut-cong′ + punchOut-injective : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) → punchOut i≢j ≡ punchOut i≢k → j ≡ k @@ -839,6 +864,12 @@ punchOut-injective {suc n} {suc i} {zero} {zero} _ _ _ = refl punchOut-injective {suc n} {suc i} {suc j} {suc k} i≢j i≢k pⱼ≡pₖ = cong suc (punchOut-injective (i≢j ∘ cong suc) (i≢k ∘ cong suc) (suc-injective pⱼ≡pₖ)) +NZpunchOut-injective : .{{_ : ℕ.NonZero n}} → + ∀ {i j k : Fin n} + (i≢j : i ≢ j) (i≢k : i ≢ k) → + NZpunchOut i≢j ≡ NZpunchOut i≢k → j ≡ k +NZpunchOut-injective {n = suc n} = punchOut-injective + punchIn-punchOut : ∀ {i j : Fin (suc n)} (i≢j : i ≢ j) → punchIn i (punchOut i≢j) ≡ j punchIn-punchOut {_} {zero} {zero} 0≢0 = contradiction refl 0≢0 @@ -847,6 +878,11 @@ punchIn-punchOut {suc m} {suc i} {zero} i≢j = refl punchIn-punchOut {suc m} {suc i} {suc j} i≢j = cong suc (punchIn-punchOut (i≢j ∘ cong suc)) +NZpunchIn-punchOut : .{{_ : ℕ.NonZero n}} → + ∀ {i j : Fin n} (i≢j : i ≢ j) → + NZpunchIn i (NZpunchOut i≢j) ≡ j +NZpunchIn-punchOut {n = suc n} = punchIn-punchOut + punchOut-punchIn : ∀ i {j : Fin n} → punchOut {i = i} {j = punchIn i j} (punchInᵢ≢i i j ∘ sym) ≡ j punchOut-punchIn zero {j} = refl punchOut-punchIn (suc i) {zero} = refl @@ -886,6 +922,11 @@ pinch-injective {i = suc i} {suc j} {suc k} 1+i≢j 1+i≢k eq = (pinch-injective (1+i≢j ∘ cong suc) (1+i≢k ∘ cong suc) (suc-injective eq)) +NZpinch-injective : .{{_ : ℕ.NonZero n}} → + ∀ {i : Fin (ℕ.pred n)} {j k : Fin n} → + NZsuc i ≢ j → NZsuc i ≢ k → NZpinch i j ≡ NZpinch i k → j ≡ k +NZpinch-injective {n = suc n} = pinch-injective + ------------------------------------------------------------------------ -- Quantification ------------------------------------------------------------------------ From be2144ea32da7a3b3450cecbca7ee776fb9a4e21 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 13:28:16 +0100 Subject: [PATCH 13/48] whitespace; n-suc i operation for Fin --- src/Data/Fin/Base.agda | 7 +++++++ src/Data/Fin/Properties.agda | 2 +- src/Data/Vec/Properties.agda | 2 +- 3 files changed, 9 insertions(+), 2 deletions(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index 86f8c152e2..aa22f1b121 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -301,6 +301,13 @@ _ℕ-ℕ_ : (n : ℕ) → Fin (suc n) → ℕ n ℕ-ℕ zero = n suc n ℕ-ℕ suc i = n ℕ-ℕ i +-- n ℕ-suc "i" = n ∸ (suc i) + +infixl 6 _ℕ-suc_ + +_ℕ-suc_ : (n : ℕ) → Fin n → ℕ +suc n ℕ-suc i = n ℕ-ℕ i + -- pred "i" = "pred i". pred : Fin n → Fin n diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index c4e8cfee67..c670033e7e 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -922,7 +922,7 @@ pinch-injective {i = suc i} {suc j} {suc k} 1+i≢j 1+i≢k eq = (pinch-injective (1+i≢j ∘ cong suc) (1+i≢k ∘ cong suc) (suc-injective eq)) -NZpinch-injective : .{{_ : ℕ.NonZero n}} → +NZpinch-injective : .{{_ : ℕ.NonZero n}} → ∀ {i : Fin (ℕ.pred n)} {j k : Fin n} → NZsuc i ≢ j → NZsuc i ≢ k → NZpinch i j ≡ NZpinch i k → j ≡ k NZpinch-injective {n = suc n} = pinch-injective diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 4803b67048..2297a66ef3 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -1030,7 +1030,7 @@ insert-punchIn (x ∷ xs) (suc i) v (suc j) = insert-punchIn xs i v j NZinsert-punchIn : .{{_ : NonZero n}} → (xs : Vec A (pred n)) (i : Fin n) (v : A) (j : Fin (pred n)) → lookup (NZinsert xs i v) (Fin.NZpunchIn i j) ≡ lookup xs j -NZinsert-punchIn {n = suc n} = insert-punchIn +NZinsert-punchIn {n = suc n} = insert-punchIn remove-punchOut : ∀ (xs : Vec A (suc n)) {i} {j} (i≢j : i ≢ j) → lookup (remove xs i) (Fin.punchOut i≢j) ≡ lookup xs j From 7fa306af7388114d9a167972b002027394087fc1 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 14:04:26 +0100 Subject: [PATCH 14/48] additional property of n-suc i operation for Fin --- src/Data/Fin/Properties.agda | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index c670033e7e..654a542b38 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -807,6 +807,9 @@ nℕ-ℕi≤n (suc n) (suc i) = begin suc n ∎ where open ℕₚ.≤-Reasoning +nℕ-suci≤n : ∀ n i → n ℕ-suc i ℕ.< n +nℕ-suci≤n (suc n) i = s Date: Mon, 19 Sep 2022 14:57:00 +0100 Subject: [PATCH 15/48] removed dependency on Data.Fin.Base --- src/Data/List/Membership/Setoid.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda index 3896a9004d..e8476d9a44 100644 --- a/src/Data/List/Membership/Setoid.agda +++ b/src/Data/List/Membership/Setoid.agda @@ -11,7 +11,6 @@ open import Relation.Binary module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where open import Function.Base using (_∘_; id; flip) -open import Data.Fin.Base using (Fin; zero; suc) open import Data.List.Base as List using (List; []; _∷_; length; lookup) open import Data.List.Relation.Unary.Any using (Any; index; map; here; there) From 3233be9530ea04ced19d39e5879b3c31eb2e7c22 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 14:59:23 +0100 Subject: [PATCH 16/48] lightened dependency on Data.Fin.Base --- src/Data/List/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 17f4159c86..b092bde78c 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -15,7 +15,7 @@ open import Algebra.Bundles open import Algebra.Definitions as AlgebraicDefinitions using (Involutive) import Algebra.Structures as AlgebraicStructures open import Data.Bool.Base using (Bool; false; true; not; if_then_else_) -open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ; inject₁) +open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ) open import Data.List.Base as List open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Relation.Unary.All using (All; []; _∷_) From 1526c50b34177ad313495062e8ad15b1e496654b Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 15:01:35 +0100 Subject: [PATCH 17/48] =?UTF-8?q?additional=20property=20of=20=E2=84=95-?= =?UTF-8?q?=E2=84=95=20operation=20for=20Fin?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Fin/Properties.agda | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 654a542b38..0e08ffebf1 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -799,6 +799,10 @@ toℕ‿ℕ- (suc n) (suc i) = toℕ‿ℕ- n i -- _ℕ-ℕ_ ------------------------------------------------------------------------ +ℕ-ℕ≡toℕ‿ℕ- : ∀ n i → n ℕ-ℕ i ≡ toℕ (n ℕ- i) +ℕ-ℕ≡toℕ‿ℕ- n zero = sym (toℕ-fromℕ n) +ℕ-ℕ≡toℕ‿ℕ- (suc n) (suc i) = ℕ-ℕ≡toℕ‿ℕ- n i + nℕ-ℕi≤n : ∀ n i → n ℕ-ℕ i ℕ.≤ n nℕ-ℕi≤n n zero = ℕₚ.≤-refl nℕ-ℕi≤n (suc n) (suc i) = begin From 7dcdf0a1ae0fe1bc925cba0f7b0ee4c26999db20 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 15:05:46 +0100 Subject: [PATCH 18/48] removed dependency on Data.Fin.Base --- src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda index 08f1b35dc2..335894a701 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda @@ -14,7 +14,6 @@ module Data.List.Relation.Binary.Permutation.Setoid.Properties open import Algebra open import Data.Bool.Base using (true; false) -open import Data.Fin.Base using (Fin) open import Data.List.Base as List hiding (head; tail) open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise; head; tail) From 511e466bf74a27d2c09a2a77cf7846a8ee7aa0f3 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 15:33:00 +0100 Subject: [PATCH 19/48] added NZhead NZtail --- src/Data/Vec/Recursive.agda | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/Data/Vec/Recursive.agda b/src/Data/Vec/Recursive.agda index 7ce3621c9c..c10b48c063 100644 --- a/src/Data/Vec/Recursive.agda +++ b/src/Data/Vec/Recursive.agda @@ -19,7 +19,7 @@ module Data.Vec.Recursive where open import Level using (Level; lift) open import Function.Bundles using (mk↔′) open import Function.Properties.Inverse using (↔-isEquivalence; ↔-refl; ↔-sym; ↔-trans) -open import Data.Nat.Base as Nat using (ℕ; zero; suc) +open import Data.Nat.Base as Nat using (ℕ; NonZero; zero; suc; pred) open import Data.Nat.Properties using (+-comm; *-comm) open import Data.Empty.Polymorphic open import Data.Fin.Base as Fin using (Fin; zero; suc) @@ -74,12 +74,21 @@ uncons : ∀ n → A ^ suc n → A × A ^ n uncons 0 a = a , lift tt uncons (suc n) (a , as) = a , as +NZuncons : ∀ n → .{{_ : NonZero n}} → A ^ n → A × A ^ (pred n) +NZuncons (suc n) = uncons n + head : ∀ n → A ^ suc n → A head n as = proj₁ (uncons n as) +NZhead : ∀ n → .{{_ : NonZero n}} → A ^ n → A +NZhead (suc n) = head n + tail : ∀ n → A ^ suc n → A ^ n tail n as = proj₂ (uncons n as) +NZtail : ∀ n → .{{_ : NonZero n}} → A ^ n → A ^ (pred n) +NZtail (suc n) = tail n + fromVec : ∀[ Vec A ⇒ (A ^_) ] fromVec = Vec.foldr (_ ^_) (cons _) _ From 762c2ba88cc3f4f7059dc6d795515fa4eb3b222e Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 15:44:39 +0100 Subject: [PATCH 20/48] removed dependency on Data.Nat.Base --- src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda b/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda index 4d8330590d..8fc0a267db 100644 --- a/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda +++ b/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda @@ -9,7 +9,6 @@ module Data.Vec.Relation.Binary.Pointwise.Extensional where open import Data.Fin.Base using (zero; suc) -open import Data.Nat.Base using (zero; suc) open import Data.Vec.Base as Vec hiding ([_]; head; tail; map) open import Data.Vec.Relation.Binary.Pointwise.Inductive as Inductive using ([]; _∷_) @@ -73,8 +72,8 @@ module _ {_∼_ : REL A B ℓ} where extensional⇒inductive : ∀ {n} {xs : Vec A n} {ys : Vec B n} → Pointwise _∼_ xs ys → IPointwise _∼_ xs ys - extensional⇒inductive {zero} {[]} {[]} xs∼ys = [] - extensional⇒inductive {suc n} {x ∷ xs} {y ∷ ys} xs∼ys = + extensional⇒inductive {xs = []} {[]} xs∼ys = [] + extensional⇒inductive {xs = x ∷ xs} {y ∷ ys} xs∼ys = (head xs∼ys) ∷ extensional⇒inductive (tail xs∼ys) inductive⇒extensional : ∀ {n} {xs : Vec A n} {ys : Vec B n} → From 1b0d5a162e40f543f4048c80c24dc4b169855be9 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 18:17:46 +0100 Subject: [PATCH 21/48] lightened dependency on Data.Fin.Base --- src/Data/Vec/Relation/Unary/All.agda | 14 ++++++++++++-- src/Data/Vec/Relation/Unary/All/Properties.agda | 14 ++++++-------- src/Data/Vec/Relation/Unary/Any.agda | 12 ++++++++++-- src/Data/Vec/Relation/Unary/Any/Properties.agda | 11 +++++------ 4 files changed, 33 insertions(+), 18 deletions(-) diff --git a/src/Data/Vec/Relation/Unary/All.agda b/src/Data/Vec/Relation/Unary/All.agda index c263276074..dfa30f1829 100644 --- a/src/Data/Vec/Relation/Unary/All.agda +++ b/src/Data/Vec/Relation/Unary/All.agda @@ -8,8 +8,7 @@ module Data.Vec.Relation.Unary.All where -open import Data.Nat.Base using (ℕ; zero; suc) -open import Data.Fin.Base using (Fin; zero; suc) +open import Data.Nat.Base using (ℕ; NonZero; zero; suc) open import Data.Product as Prod using (_×_; _,_; uncurry; <_,_>) open import Data.Sum.Base as Sum using (inj₁; inj₂) open import Data.Vec.Base as Vec using (Vec; []; _∷_) @@ -53,9 +52,16 @@ data All {A : Set a} (P : Pred A p) : Vec A n → Set (p ⊔ a) where head : All P (x ∷ xs) → P x head (px ∷ pxs) = px +NZhead : .{{nz : NonZero n}} → All P xs → P (Vec.NZhead {{nz}} xs) +NZhead {n = suc n} pxs@(_ ∷ _) = head pxs + tail : All P (x ∷ xs) → All P xs tail (px ∷ pxs) = pxs +NZtail : .{{nz : NonZero n}} → + All P xs → All P (Vec.NZtail {{nz}} xs) +NZtail {n = suc n} pxs@(_ ∷ _) = tail pxs + reduce : (f : ∀ {x} → P x → B) → ∀ {n} {xs : Vec A n} → All P xs → Vec B n reduce f [] = [] reduce f (px ∷ pxs) = f px ∷ reduce f pxs @@ -63,6 +69,10 @@ reduce f (px ∷ pxs) = f px ∷ reduce f pxs uncons : All P (x ∷ xs) → P x × All P xs uncons = < head , tail > +NZuncons : .{{nz : NonZero n}} → + All P xs → P (Vec.NZhead {{nz}} xs) × All P (Vec.NZtail {{nz}} xs) +NZuncons = < NZhead , NZtail > + map : P ⊆ Q → All P ⊆ All Q {n} map g [] = [] map g (px ∷ pxs) = g px ∷ map g pxs diff --git a/src/Data/Vec/Relation/Unary/All/Properties.agda b/src/Data/Vec/Relation/Unary/All/Properties.agda index 446073cc24..b6734ea33c 100644 --- a/src/Data/Vec/Relation/Unary/All/Properties.agda +++ b/src/Data/Vec/Relation/Unary/All/Properties.agda @@ -9,7 +9,7 @@ module Data.Vec.Relation.Unary.All.Properties where open import Data.Nat.Base using (ℕ; zero; suc; _+_) -open import Data.Fin.Base using (Fin; zero; suc) +open import Data.Fin.Base using (zero; suc) open import Data.List.Base using ([]; _∷_) open import Data.List.Relation.Unary.All as List using ([]; _∷_) open import Data.Product as Prod using (_×_; _,_; uncurry; uncurry′) @@ -37,7 +37,7 @@ private ------------------------------------------------------------------------ -- lookup -lookup⁺ : (i : Fin n) → All P xs → P (Vec.lookup xs i) +lookup⁺ : ∀ i → All P xs → P (Vec.lookup xs i) lookup⁺ zero (px ∷ pxs) = px lookup⁺ (suc i) (px ∷ pxs) = lookup⁺ i pxs @@ -133,15 +133,13 @@ module _ {_~_ : REL A B p} where module _ {P : A → Set p} where - tabulate⁺ : ∀ {n} {f : Fin n → A} → - (∀ i → P (f i)) → All P (tabulate f) + tabulate⁺ : ∀ {n} {f} → (∀ i → P (f i)) → All P (tabulate {n = n} f) tabulate⁺ {zero} Pf = [] tabulate⁺ {suc n} Pf = Pf zero ∷ tabulate⁺ (Pf ∘ suc) - tabulate⁻ : ∀ {n} {f : Fin n → A} → - All P (tabulate f) → (∀ i → P (f i)) - tabulate⁻ {suc n} (px ∷ _) zero = px - tabulate⁻ {suc n} (_ ∷ pf) (suc i) = tabulate⁻ pf i + tabulate⁻ : ∀ {n} {f} → All P (tabulate {n = n} f) → (∀ i → P (f i)) + tabulate⁻ (px ∷ _) zero = px + tabulate⁻ (_ ∷ pf) (suc i) = tabulate⁻ pf i ------------------------------------------------------------------------ -- take and drop diff --git a/src/Data/Vec/Relation/Unary/Any.agda b/src/Data/Vec/Relation/Unary/Any.agda index 5a65a74dd6..38f560105d 100644 --- a/src/Data/Vec/Relation/Unary/Any.agda +++ b/src/Data/Vec/Relation/Unary/Any.agda @@ -9,8 +9,8 @@ module Data.Vec.Relation.Unary.Any {a} {A : Set a} where open import Data.Empty -open import Data.Fin.Base -open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Fin.Base using (Fin; zero; suc) +open import Data.Nat.Base using (ℕ; NonZero; zero; suc) open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) open import Data.Vec.Base as Vec using (Vec; []; [_]; _∷_) open import Data.Product as Prod using (∃; _,_) @@ -44,11 +44,19 @@ head : ∀ {x} → ¬ Any P xs → Any P (x ∷ xs) → P x head ¬pxs (here px) = px head ¬pxs (there pxs) = contradiction pxs ¬pxs +NZhead : .{{nz : NonZero n}} → + ¬ Any P (Vec.NZtail {{nz}} xs) → Any P xs → P (Vec.NZhead {{nz}} xs) +NZhead {n = suc n} {xs = _ ∷ _} ¬pxs = head ¬pxs + -- If the head does not satisfy the predicate, then the tail will. tail : ∀ {x} → ¬ P x → Any P (x ∷ xs) → Any P xs tail ¬px (here px) = ⊥-elim (¬px px) tail ¬px (there pxs) = pxs +NZtail : .{{nz : NonZero n}} → + ¬ P (Vec.NZhead {{nz}} xs) → Any P xs → Any P (Vec.NZtail {{nz}} xs) +NZtail {n = suc n} {xs = _ ∷ _} ¬px = tail ¬px + -- Convert back and forth with sum toSum : ∀ {x} → Any P (x ∷ xs) → P x ⊎ Any P xs toSum (here px) = inj₁ px diff --git a/src/Data/Vec/Relation/Unary/Any/Properties.agda b/src/Data/Vec/Relation/Unary/Any/Properties.agda index a300c44d55..f87dc9273b 100644 --- a/src/Data/Vec/Relation/Unary/Any/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Any/Properties.agda @@ -9,7 +9,7 @@ module Data.Vec.Relation.Unary.Any.Properties where open import Data.Nat.Base using (suc; zero) -open import Data.Fin.Base using (Fin; zero; suc) +open import Data.Fin.Base using (zero; suc) open import Data.Empty using (⊥) open import Data.List.Base using ([]; _∷_) import Data.List.Relation.Unary.Any as List @@ -357,14 +357,13 @@ module _ {P : Pred A p} where module _ {P : Pred A p} where - tabulate⁺ : ∀ {n} {f : Fin n → A} i → P (f i) → Any P (tabulate f) + tabulate⁺ : ∀ {n} {f} i → P (f i) → Any P (tabulate {n = n} f) tabulate⁺ zero p = here p tabulate⁺ (suc i) p = there (tabulate⁺ i p) - tabulate⁻ : ∀ {n} {f : Fin n → A} → - Any P (tabulate f) → ∃ λ i → P (f i) - tabulate⁻ {suc n} (here p) = zero , p - tabulate⁻ {suc n} (there p) = Prod.map suc id (tabulate⁻ p) + tabulate⁻ : ∀ {n} {f} → Any P (tabulate {n = n} f) → ∃ λ i → P (f i) + tabulate⁻ (here p) = zero , p + tabulate⁻ (there p) = Prod.map suc id (tabulate⁻ p) ------------------------------------------------------------------------ -- mapWith∈ From af5eed6999f47e71c66b3d68bb9a1c31e5e46c44 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 18:29:37 +0100 Subject: [PATCH 22/48] lightened dependencies on Data.Fin.Base/Properties --- .../Vec/Relation/Unary/Linked/Properties.agda | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda index e972937619..5d7b708f5b 100644 --- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda @@ -14,10 +14,10 @@ open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_) import Data.Vec.Relation.Unary.All.Properties as Allₚ open import Data.Vec.Relation.Unary.Linked as Linked using (Linked; []; [-]; _∷_) -open import Data.Fin.Base using (Fin; zero; suc; _<_) -open import Data.Fin.Properties using (suc-injective) -open import Data.Nat.Base using (ℕ; zero; suc) -open import Data.Nat.Properties using (<-pred) -- ≤-refl; ≤-pred; ≤-step) +open import Data.Fin.Base using (zero; suc; _<_) +--open import Data.Fin.Properties using (suc-injective) +open import Data.Nat.Base using (ℕ; NonZero; zero; suc) +open import Data.Nat.Properties using (<-pred) open import Level using (Level) open import Function.Base using (_∘_; flip; _on_) open import Relation.Binary using (Rel; Transitive; DecSetoid) @@ -44,7 +44,12 @@ module _ (trans : Transitive R) where Linked⇒All Rvx [-] = Rvx ∷ [] Linked⇒All Rvx (Rxy ∷ Rxs) = Rvx ∷ Linked⇒All (trans Rvx Rxy) Rxs - lookup : ∀ {i j : Fin n} {xs} → i < j → + NZLinked⇒All : .{{nz : NonZero n}} → + ∀ {v} {xs : Vec _ n} → R v (NZhead {{nz}} xs) → + Linked R xs → All (R v) xs + NZLinked⇒All {n = suc n} = Linked⇒All {n = n} + + lookup : ∀ {i j} {xs : Vec _ n} → i < j → Linked R xs → R (Vec.lookup xs i) (Vec.lookup xs j) lookup {i = zero} {j = suc j} i Date: Mon, 19 Sep 2022 18:33:15 +0100 Subject: [PATCH 23/48] lightened dependencies on Data.Fin.Base --- .../Vec/Relation/Unary/Unique/Propositional/Properties.agda | 3 +-- src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda | 6 +++--- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda b/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda index 9a57cff263..b0719a3bf2 100644 --- a/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda @@ -8,7 +8,6 @@ module Data.Vec.Relation.Unary.Unique.Propositional.Properties where -open import Data.Fin.Base using (Fin) open import Data.Vec.Base open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_) open import Data.Vec.Relation.Unary.AllPairs as AllPairs using (AllPairs) @@ -57,7 +56,7 @@ module _ {A : Set a} where module _ {A : Set a} where - tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ {i j} → f i ≡ f j → i ≡ j) → Unique (tabulate f) + tabulate⁺ : ∀ {n} {f} → (∀ {i j} → f i ≡ f j → i ≡ j) → Unique (tabulate {n = n} f) tabulate⁺ = Setoid.tabulate⁺ (setoid A) ------------------------------------------------------------------------ diff --git a/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda b/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda index 10f736cea2..8a7ef7d897 100644 --- a/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda @@ -8,7 +8,7 @@ module Data.Vec.Relation.Unary.Unique.Setoid.Properties where -open import Data.Fin.Base using (Fin; zero; suc) +open import Data.Fin.Base using (zero; suc) open import Data.Vec.Base as Vec open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_) import Data.Vec.Relation.Unary.All.Properties as Allₚ @@ -58,8 +58,8 @@ module _ (S : Setoid a ℓ) where open Setoid S renaming (Carrier to A) - tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ {i j} → f i ≈ f j → i ≡ j) → - Unique S (tabulate f) + tabulate⁺ : ∀ {n} {f} → (∀ {i j} → f i ≈ f j → i ≡ j) → + Unique S (tabulate {n = n} f) tabulate⁺ f-inj = AllPairsₚ.tabulate⁺ (_∘ f-inj) ------------------------------------------------------------------------ From 1fee86234f52b5cd156c643b0dfcff888adf5d0d Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 18:34:19 +0100 Subject: [PATCH 24/48] lightened dependencies on Data.Fin.Base --- src/Data/Vec/Relation/Unary/Linked/Properties.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda index 5d7b708f5b..2c99e9f8a2 100644 --- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda @@ -15,7 +15,6 @@ import Data.Vec.Relation.Unary.All.Properties as Allₚ open import Data.Vec.Relation.Unary.Linked as Linked using (Linked; []; [-]; _∷_) open import Data.Fin.Base using (zero; suc; _<_) ---open import Data.Fin.Properties using (suc-injective) open import Data.Nat.Base using (ℕ; NonZero; zero; suc) open import Data.Nat.Properties using (<-pred) open import Level using (Level) From 258aceaf196b15ce30eb6a1726d3b052b799d58a Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 18:37:19 +0100 Subject: [PATCH 25/48] removed dependency on Data.Fin.Base --- src/Data/Vec/Relation/Unary/AllPairs/Properties.agda | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda b/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda index f7b3a8584b..38eb8cdaa4 100644 --- a/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda +++ b/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda @@ -14,7 +14,6 @@ open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_) import Data.Vec.Relation.Unary.All.Properties as Allₚ open import Data.Vec.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_) open import Data.Bool.Base using (true; false) -open import Data.Fin.Base using (Fin) open import Data.Fin.Properties using (suc-injective) open import Data.Nat.Base using (zero; suc; _+_) open import Function using (_∘_) @@ -83,8 +82,8 @@ module _ {R : Rel A ℓ} where module _ {R : Rel A ℓ} where - tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ {i j} → i ≢ j → R (f i) (f j)) → - AllPairs R (tabulate f) + tabulate⁺ : ∀ {n} {f} → (∀ {i j} → i ≢ j → R (f i) (f j)) → + AllPairs R (tabulate {n = n} f) tabulate⁺ {zero} fᵢ~fⱼ = [] tabulate⁺ {suc n} fᵢ~fⱼ = Allₚ.tabulate⁺ (λ j → fᵢ~fⱼ λ()) ∷ From 12ee2b0f3cbaaf9b08a9308281d023db99c7da99 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 18:58:50 +0100 Subject: [PATCH 26/48] added NonZero instances --- .../Properties/CommutativeMonoid/Sum.agda | 4 +++ src/Data/Vec/Functional.agda | 25 +++++++++++++++++-- 2 files changed, 27 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Properties/CommutativeMonoid/Sum.agda b/src/Algebra/Properties/CommutativeMonoid/Sum.agda index 54731cfb5b..c7ebf558fd 100644 --- a/src/Algebra/Properties/CommutativeMonoid/Sum.agda +++ b/src/Algebra/Properties/CommutativeMonoid/Sum.agda @@ -59,6 +59,10 @@ sum-remove {suc n} {suc i} xs = begin ∑t = sum t ∑t′ = sum (remove i t) +NZsum-remove : ∀ {n} {{nz : NonZero n}} {i : Fin n} t → sum t ≈ t i + sum (NZremove {{nz}} i t) + +NZsum-remove {n = suc n} = sum-remove + -- The '∑' operator distributes over addition. ∑-distrib-+ : ∀ {n} (f g : Vector Carrier n) → ∑[ i < n ] (f i + g i) ≈ ∑[ i < n ] f i + ∑[ i < n ] g i ∑-distrib-+ {zero} f g = sym (+-identityˡ _) diff --git a/src/Data/Vec/Functional.agda b/src/Data/Vec/Functional.agda index 06a19bf92b..873b327790 100644 --- a/src/Data/Vec/Functional.agda +++ b/src/Data/Vec/Functional.agda @@ -15,9 +15,9 @@ module Data.Vec.Functional where -open import Data.Fin.Base +open import Data.Fin.Base hiding (NonZero; pred) open import Data.List.Base as L using (List) -open import Data.Nat.Base as ℕ using (ℕ; zero; suc) +open import Data.Nat.Base as ℕ using (ℕ; NonZero; zero; suc; pred) open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂; uncurry) open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]) open import Data.Vec.Base as V using (Vec) @@ -72,12 +72,21 @@ length {n = n} _ = n head : ∀ {n} → Vector A (suc n) → A head xs = xs zero +NZhead : ∀ {n} {{_ : NonZero n}} → Vector A n → A +NZhead {n = suc n} = head + tail : ∀ {n} → Vector A (suc n) → Vector A n tail xs = xs ∘ suc +NZtail : ∀ {n} {{_ : NonZero n}} → Vector A n → Vector A (pred n) +NZtail {n = suc n} = tail + uncons : ∀ {n} → Vector A (suc n) → A × Vector A n uncons xs = head xs , tail xs +NZuncons : ∀ {n} {{_ : NonZero n}} → Vector A n → A × Vector A (pred n) +NZuncons {n = suc n} = uncons + replicate : ∀ {n} → A → Vector A n replicate = const @@ -87,9 +96,15 @@ insert {n = n} xs zero v (suc j) = xs j insert {n = suc n} xs (suc i) v zero = head xs insert {n = suc n} xs (suc i) v (suc j) = insert (tail xs) i v j +NZinsert : ∀ {n} {{_ : NonZero n}} → Vector A (pred n) → Fin n → A → Vector A n +NZinsert {n = suc n} = insert + remove : ∀ {n} → Fin (suc n) → Vector A (suc n) → Vector A n remove i t = t ∘ punchIn i +NZremove : ∀ {n} {{_ : NonZero n}} → Fin n → Vector A n → Vector A (pred n) +NZremove {n = suc n} i t = t ∘ NZpunchIn i + updateAt : ∀ {n} → Fin n → (A → A) → Vector A n → Vector A n updateAt {n = suc n} zero f xs zero = f (head xs) updateAt {n = suc n} zero f xs (suc j) = xs (suc j) @@ -149,8 +164,14 @@ reverse xs = xs ∘ opposite init : ∀ {n} → Vector A (suc n) → Vector A n init xs = xs ∘ inject₁ +NZinit : ∀ {n} {{_ : NonZero n}} → Vector A n → Vector A (pred n) +NZinit {n = suc n} = init + last : ∀ {n} → Vector A (suc n) → A last {n = n} xs = xs (fromℕ n) +NZlast : ∀ {n} {{_ : NonZero n}} → Vector A n → A +NZlast {n = suc n} = last + transpose : ∀ {m n} → Vector (Vector A n) m → Vector (Vector A m) n transpose = flip From b0fcbb7769680f8567e73085c4ac9d99b3b14dc7 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 19:10:53 +0100 Subject: [PATCH 27/48] tidying up import order --- src/Data/Nat/DivMod/WithK.agda | 2 +- src/Data/Vec/Functional.agda | 2 +- src/Data/Vec/Recursive.agda | 2 +- src/Data/Vec/Relation/Unary/All.agda | 2 +- src/Data/Vec/Relation/Unary/Any.agda | 2 +- src/Data/Vec/Relation/Unary/Linked/Properties.agda | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Data/Nat/DivMod/WithK.agda b/src/Data/Nat/DivMod/WithK.agda index 3fc45ec291..458a7eef33 100644 --- a/src/Data/Nat/DivMod/WithK.agda +++ b/src/Data/Nat/DivMod/WithK.agda @@ -8,7 +8,7 @@ module Data.Nat.DivMod.WithK where -open import Data.Nat using (ℕ; NonZero; _+_; _*_; _≟_; zero; suc) +open import Data.Nat using (ℕ; NonZero; _+_; _*_; _≟_) open import Data.Nat.DivMod hiding (_mod_; _divMod_) open import Data.Nat.Properties using (≤⇒≤″) open import Data.Nat.WithK diff --git a/src/Data/Vec/Functional.agda b/src/Data/Vec/Functional.agda index 873b327790..96ba80c435 100644 --- a/src/Data/Vec/Functional.agda +++ b/src/Data/Vec/Functional.agda @@ -17,7 +17,7 @@ module Data.Vec.Functional where open import Data.Fin.Base hiding (NonZero; pred) open import Data.List.Base as L using (List) -open import Data.Nat.Base as ℕ using (ℕ; NonZero; zero; suc; pred) +open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero; pred) open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂; uncurry) open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]) open import Data.Vec.Base as V using (Vec) diff --git a/src/Data/Vec/Recursive.agda b/src/Data/Vec/Recursive.agda index c10b48c063..8a6a4c7ab0 100644 --- a/src/Data/Vec/Recursive.agda +++ b/src/Data/Vec/Recursive.agda @@ -19,7 +19,7 @@ module Data.Vec.Recursive where open import Level using (Level; lift) open import Function.Bundles using (mk↔′) open import Function.Properties.Inverse using (↔-isEquivalence; ↔-refl; ↔-sym; ↔-trans) -open import Data.Nat.Base as Nat using (ℕ; NonZero; zero; suc; pred) +open import Data.Nat.Base as Nat using (ℕ; zero; suc; NonZero; pred) open import Data.Nat.Properties using (+-comm; *-comm) open import Data.Empty.Polymorphic open import Data.Fin.Base as Fin using (Fin; zero; suc) diff --git a/src/Data/Vec/Relation/Unary/All.agda b/src/Data/Vec/Relation/Unary/All.agda index dfa30f1829..957e2a6299 100644 --- a/src/Data/Vec/Relation/Unary/All.agda +++ b/src/Data/Vec/Relation/Unary/All.agda @@ -8,7 +8,7 @@ module Data.Vec.Relation.Unary.All where -open import Data.Nat.Base using (ℕ; NonZero; zero; suc) +open import Data.Nat.Base using (ℕ; zero; suc; NonZero) open import Data.Product as Prod using (_×_; _,_; uncurry; <_,_>) open import Data.Sum.Base as Sum using (inj₁; inj₂) open import Data.Vec.Base as Vec using (Vec; []; _∷_) diff --git a/src/Data/Vec/Relation/Unary/Any.agda b/src/Data/Vec/Relation/Unary/Any.agda index 38f560105d..aace996c86 100644 --- a/src/Data/Vec/Relation/Unary/Any.agda +++ b/src/Data/Vec/Relation/Unary/Any.agda @@ -10,7 +10,7 @@ module Data.Vec.Relation.Unary.Any {a} {A : Set a} where open import Data.Empty open import Data.Fin.Base using (Fin; zero; suc) -open import Data.Nat.Base using (ℕ; NonZero; zero; suc) +open import Data.Nat.Base using (ℕ; zero; suc; NonZero) open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) open import Data.Vec.Base as Vec using (Vec; []; [_]; _∷_) open import Data.Product as Prod using (∃; _,_) diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda index 2c99e9f8a2..d2741256d7 100644 --- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda @@ -15,7 +15,7 @@ import Data.Vec.Relation.Unary.All.Properties as Allₚ open import Data.Vec.Relation.Unary.Linked as Linked using (Linked; []; [-]; _∷_) open import Data.Fin.Base using (zero; suc; _<_) -open import Data.Nat.Base using (ℕ; NonZero; zero; suc) +open import Data.Nat.Base using (ℕ; zero; suc; NonZero) open import Data.Nat.Properties using (<-pred) open import Level using (Level) open import Function.Base using (_∘_; flip; _on_) From e9b36e817f904c11fbb75ddfd9a11bec4a5a06e8 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 19:28:22 +0100 Subject: [PATCH 28/48] lightened dependencies on Data.Fin.Base/properties; rmeoved dependency on Data.Nat.Base --- src/Data/Vec/Functional/Relation/Unary/All.agda | 4 +--- .../Vec/Functional/Relation/Unary/All/Properties.agda | 11 +++++------ src/Data/Vec/Functional/Relation/Unary/Any.agda | 4 ++-- 3 files changed, 8 insertions(+), 11 deletions(-) diff --git a/src/Data/Vec/Functional/Relation/Unary/All.agda b/src/Data/Vec/Functional/Relation/Unary/All.agda index 7c6e418a6d..7a1d0412be 100644 --- a/src/Data/Vec/Functional/Relation/Unary/All.agda +++ b/src/Data/Vec/Functional/Relation/Unary/All.agda @@ -8,9 +8,7 @@ module Data.Vec.Functional.Relation.Unary.All where -open import Data.Fin.Base -open import Data.Fin.Properties -open import Data.Nat.Base +open import Data.Fin.Properties using (all?) open import Data.Product using (_,_) open import Data.Vec.Functional as VF hiding (map) open import Level using (Level) diff --git a/src/Data/Vec/Functional/Relation/Unary/All/Properties.agda b/src/Data/Vec/Functional/Relation/Unary/All/Properties.agda index 5ce23f962a..d9b288a4d3 100644 --- a/src/Data/Vec/Functional/Relation/Unary/All/Properties.agda +++ b/src/Data/Vec/Functional/Relation/Unary/All/Properties.agda @@ -8,9 +8,8 @@ module Data.Vec.Functional.Relation.Unary.All.Properties where -open import Data.Fin.Base -open import Data.Fin.Properties -open import Data.Nat.Base +open import Data.Fin.Base using (zero; suc; _↑ˡ_; _↑ʳ_; splitAt) +open import Data.Fin.Properties using (splitAt-↑ˡ; splitAt-↑ʳ) open import Data.Product as Σ using (_×_; _,_; proj₁; proj₂; uncurry) open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]) open import Data.Vec.Functional as VF hiding (map) @@ -38,7 +37,7 @@ module _ {P : Pred A p} {Q : Pred B q} {f : A → B} where ------------------------------------------------------------------------ -- replicate -module _ {P : Pred A p} {x : A} {n : ℕ} where +module _ {P : Pred A p} {x : A} {n} where replicate⁺ : P x → All P (replicate {n = n} x) replicate⁺ = const @@ -87,14 +86,14 @@ tail⁺ P ps = ps ∘ suc ------------------------------------------------------------------------ -- ++ -module _ (P : Pred A p) {m n : ℕ} {xs : Vector A m} {ys : Vector A n} where +module _ (P : Pred A p) {m n} {xs : Vector A m} {ys : Vector A n} where ++⁺ : All P xs → All P ys → All P (xs ++ ys) ++⁺ pxs pys i with splitAt m i ... | inj₁ i′ = pxs i′ ... | inj₂ j′ = pys j′ -module _ (P : Pred A p) {m n : ℕ} (xs : Vector A m) {ys : Vector A n} where +module _ (P : Pred A p) {m n} (xs : Vector A m) {ys : Vector A n} where ++⁻ˡ : All P (xs ++ ys) → All P xs ++⁻ˡ ps i with ps (i ↑ˡ n) diff --git a/src/Data/Vec/Functional/Relation/Unary/Any.agda b/src/Data/Vec/Functional/Relation/Unary/Any.agda index e50cb24eee..23bf65afc5 100644 --- a/src/Data/Vec/Functional/Relation/Unary/Any.agda +++ b/src/Data/Vec/Functional/Relation/Unary/Any.agda @@ -8,8 +8,8 @@ module Data.Vec.Functional.Relation.Unary.Any where -open import Data.Fin.Base -open import Data.Fin.Properties +open import Data.Fin.Base using (zero; suc) +open import Data.Fin.Properties using (any?) open import Data.Nat.Base open import Data.Product as Σ using (Σ; ∃; _×_; _,_; proj₁; proj₂) open import Data.Vec.Functional as VF hiding (map) From 2d2f83636b1dc463710ea061ed2865ca89835d03 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 19:31:41 +0100 Subject: [PATCH 29/48] removed dependencies on Data.Fin.Base; lightened dependency on Data.Nat.Base --- src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda b/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda index f248ac57d1..ccc8e3c00c 100644 --- a/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda +++ b/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda @@ -6,8 +6,7 @@ {-# OPTIONS --without-K --safe #-} -open import Data.Fin.Base -open import Data.Nat.Base +open import Data.Nat.Base using (ℕ) open import Data.Vec.Functional as VF hiding (map) open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise) From 70caf177125c66f122512f4379780378421e67b9 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 19:38:38 +0100 Subject: [PATCH 30/48] lightened/removed dependencies on Data.Fin.Base/Data.Nat.Base --- src/Data/Vec/Functional/Relation/Binary/Pointwise.agda | 2 -- .../Functional/Relation/Binary/Pointwise/Properties.agda | 6 +++--- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/Data/Vec/Functional/Relation/Binary/Pointwise.agda b/src/Data/Vec/Functional/Relation/Binary/Pointwise.agda index 360dc46540..645dafadec 100644 --- a/src/Data/Vec/Functional/Relation/Binary/Pointwise.agda +++ b/src/Data/Vec/Functional/Relation/Binary/Pointwise.agda @@ -8,8 +8,6 @@ module Data.Vec.Functional.Relation.Binary.Pointwise where -open import Data.Fin.Base -open import Data.Nat.Base open import Data.Vec.Functional as VF hiding (map) open import Level using (Level) open import Relation.Binary diff --git a/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda b/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda index 75edf115fd..7be16938dd 100644 --- a/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda +++ b/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda @@ -8,9 +8,9 @@ module Data.Vec.Functional.Relation.Binary.Pointwise.Properties where -open import Data.Fin.Base -open import Data.Fin.Properties -open import Data.Nat.Base +open import Data.Fin.Base using (zero; suc; _↑ˡ_; _↑ʳ_; splitAt) +open import Data.Fin.Properties using (all?; splitAt-↑ˡ; splitAt-↑ʳ) +open import Data.Nat.Base using (ℕ; zero; suc) open import Data.Product using (_×_; _,_; proj₁; proj₂) open import Data.Product.Relation.Binary.Pointwise.NonDependent using () renaming (Pointwise to ×-Pointwise) From 467c2a34c0ccf425dd5ac92ed2e7032bc02784d5 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 19:46:23 +0100 Subject: [PATCH 31/48] lightened/removed dependencies on Data.Fin.Base/Data.Nat.Base --- .../Relation/Unary/Unique/Propositional/Properties.agda | 7 +++---- src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda | 7 +++---- 2 files changed, 6 insertions(+), 8 deletions(-) diff --git a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda index ea113da0da..79ee20a73c 100644 --- a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda +++ b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda @@ -8,14 +8,13 @@ module Data.List.Relation.Unary.Unique.Propositional.Properties where -open import Data.Fin.Base using (Fin) open import Data.List.Base open import Data.List.Relation.Binary.Disjoint.Propositional open import Data.List.Relation.Unary.All as All using (All; []; _∷_) open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs) open import Data.List.Relation.Unary.Unique.Propositional import Data.List.Relation.Unary.Unique.Setoid.Properties as Setoid -open import Data.Nat.Base +open import Data.Nat.Base using (_<_) open import Data.Nat.Properties using (<⇒≢) open import Data.Product using (_×_; _,_) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (≡⇒≡×≡) @@ -132,8 +131,8 @@ downFrom⁺ n = applyDownFrom⁺₁ id n (λ j Date: Mon, 19 Sep 2022 19:50:44 +0100 Subject: [PATCH 32/48] removed dependencies on Data.Fin.Base --- src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda index 2435b34168..7494b55795 100644 --- a/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda +++ b/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda @@ -6,7 +6,6 @@ {-# OPTIONS --without-K --safe #-} -open import Data.Fin hiding (_≟_) open import Data.List.Base open import Data.List.Membership.Setoid.Properties as Membership open import Data.List.Relation.Unary.Any using (index) @@ -85,5 +84,5 @@ module _ (S? : DecSetoid a ℓ₁) where module _ (S : Setoid a ℓ₁) where lookup-surjective : ∀ {xs} → IsEnumeration S xs → - Surjective {A = Fin (length xs)} _≡_ (_≈_ S) (lookup xs) + Surjective _≡_ (_≈_ S) (lookup xs) lookup-surjective _∈xs y = index (y ∈xs) , sym S (lookup-index (y ∈xs)) From ebe02a4325c97ea43e855188e4da46d7792bad6f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 19:52:56 +0100 Subject: [PATCH 33/48] removed dependencies on Data.Fin.Base --- src/Data/List/Relation/Unary/Linked/Properties.agda | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Data/List/Relation/Unary/Linked/Properties.agda b/src/Data/List/Relation/Unary/Linked/Properties.agda index 4bb2d4bf92..d00b76a329 100644 --- a/src/Data/List/Relation/Unary/Linked/Properties.agda +++ b/src/Data/List/Relation/Unary/Linked/Properties.agda @@ -16,8 +16,6 @@ import Data.List.Relation.Unary.AllPairs.Properties as AllPairs open import Data.List.Relation.Unary.All using (All; []; _∷_) open import Data.List.Relation.Unary.Linked as Linked using (Linked; []; [-]; _∷_) -open import Data.Fin.Base using (Fin) -open import Data.Fin.Properties using (suc-injective) open import Data.Nat.Base using (zero; suc; _<_; z Date: Mon, 19 Sep 2022 22:07:15 +0100 Subject: [PATCH 34/48] lightened dependencies on Data.Fin.Base --- src/Data/List/Relation/Unary/All/Properties.agda | 8 +++----- src/Data/List/Relation/Unary/Any.agda | 2 +- src/Data/List/Relation/Unary/Any/Properties.agda | 6 +++--- 3 files changed, 7 insertions(+), 9 deletions(-) diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda index 9a94e100f3..7741c97fa9 100644 --- a/src/Data/List/Relation/Unary/All/Properties.agda +++ b/src/Data/List/Relation/Unary/All/Properties.agda @@ -12,7 +12,7 @@ open import Axiom.Extensionality.Propositional using (Extensionality) open import Data.Bool.Base using (Bool; T; true; false) open import Data.Bool.Properties using (T-∧) open import Data.Empty -open import Data.Fin.Base using (Fin; zero; suc) +open import Data.Fin.Base using (zero; suc) open import Data.List.Base as List hiding (lookup) open import Data.List.Properties as Listₚ using (partition-defn) open import Data.List.Membership.Propositional @@ -553,13 +553,11 @@ applyDownFrom⁺₂ f n Pf = applyDownFrom⁺₁ f n (λ _ → Pf _) ------------------------------------------------------------------------ -- tabulate -tabulate⁺ : ∀ {n} {f : Fin n → A} → - (∀ i → P (f i)) → All P (tabulate f) +tabulate⁺ : ∀ {n} {f} → (∀ i → P (f i)) → All P (tabulate {n = n} f) tabulate⁺ {n = zero} Pf = [] tabulate⁺ {n = suc _} Pf = Pf zero ∷ tabulate⁺ (Pf ∘ suc) -tabulate⁻ : ∀ {n} {f : Fin n → A} → - All P (tabulate f) → (∀ i → P (f i)) +tabulate⁻ : ∀ {n} {f} → All P (tabulate {n = n} f) → (∀ i → P (f i)) tabulate⁻ (px ∷ _) zero = px tabulate⁻ (_ ∷ pf) (suc i) = tabulate⁻ pf i diff --git a/src/Data/List/Relation/Unary/Any.agda b/src/Data/List/Relation/Unary/Any.agda index 40398a3b8e..02f7219229 100644 --- a/src/Data/List/Relation/Unary/Any.agda +++ b/src/Data/List/Relation/Unary/Any.agda @@ -9,7 +9,7 @@ module Data.List.Relation.Unary.Any where open import Data.Empty -open import Data.Fin.Base +open import Data.Fin.Base using (Fin; zero; suc) open import Data.List.Base as List using (List; []; [_]; _∷_) open import Data.Product as Prod using (∃; _,_) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂) diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda index 8e05fc6492..4e1d640947 100644 --- a/src/Data/List/Relation/Unary/Any/Properties.agda +++ b/src/Data/List/Relation/Unary/Any/Properties.agda @@ -11,7 +11,7 @@ module Data.List.Relation.Unary.Any.Properties where open import Data.Bool.Base using (Bool; false; true; T) open import Data.Bool.Properties using (T-∨; T-≡) open import Data.Empty using (⊥) -open import Data.Fin.Base using (Fin; zero; suc) +open import Data.Fin.Base using (zero; suc) open import Data.List.Base as List open import Data.List.Properties using (ʳ++-defn) open import Data.List.Effectful using (monad) @@ -511,11 +511,11 @@ module _ {P : A → Set p} where ------------------------------------------------------------------------ -- tabulate -tabulate⁺ : ∀ {n} {f : Fin n → A} i → P (f i) → Any P (tabulate f) +tabulate⁺ : ∀ {n} {f} i → P (f i) → Any P (tabulate {n = n} f) tabulate⁺ zero p = here p tabulate⁺ (suc i) p = there (tabulate⁺ i p) -tabulate⁻ : ∀ {n} {f : Fin n → A} → Any P (tabulate f) → ∃ λ i → P (f i) +tabulate⁻ : ∀ {n} {f} → Any P (tabulate {n = n} f) → ∃ λ i → P (f i) tabulate⁻ {n = suc _} (here p) = zero , p tabulate⁻ {n = suc _} (there p) = Prod.map suc id (tabulate⁻ p) From 10e3f9d93e9e3038df49643659c1e9a3d4b842e4 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 19 Sep 2022 22:09:36 +0100 Subject: [PATCH 35/48] lightened dependencies on Data.Fin.Base --- src/Data/List/Relation/Unary/AllPairs/Properties.agda | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties.agda b/src/Data/List/Relation/Unary/AllPairs/Properties.agda index e9c0b84424..01d2aea103 100644 --- a/src/Data/List/Relation/Unary/AllPairs/Properties.agda +++ b/src/Data/List/Relation/Unary/AllPairs/Properties.agda @@ -13,7 +13,6 @@ open import Data.List.Relation.Unary.All as All using (All; []; _∷_) import Data.List.Relation.Unary.All.Properties as All open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_) open import Data.Bool.Base using (true; false) -open import Data.Fin.Base using (Fin) open import Data.Fin.Properties using (suc-injective) open import Data.Nat.Base using (zero; suc; _<_; z≤n; s≤s) open import Data.Nat.Properties using (≤-refl; ≤-step) @@ -114,8 +113,8 @@ module _ {R : Rel A ℓ} where module _ {R : Rel A ℓ} where - tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ {i j} → i ≢ j → R (f i) (f j)) → - AllPairs R (tabulate f) + tabulate⁺ : ∀ {n} {f} → (∀ {i j} → i ≢ j → R (f i) (f j)) → + AllPairs R (tabulate {n = n} f) tabulate⁺ {zero} fᵢ~fⱼ = [] tabulate⁺ {suc n} fᵢ~fⱼ = All.tabulate⁺ (λ j → fᵢ~fⱼ λ()) ∷ From 3494c509ec26147608327f9a60efa6aef177b14b Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 29 Sep 2022 14:53:19 +0100 Subject: [PATCH 36/48] narrowed dependency on Fin --- src/Data/Vec/Relation/Unary/Linked/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda index 6416753888..ecf9f96a34 100644 --- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda @@ -14,7 +14,7 @@ open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_) import Data.Vec.Relation.Unary.All.Properties as Allₚ open import Data.Vec.Relation.Unary.Linked as Linked using (Linked; []; [-]; _∷_) -open import Data.Fin.Base using (Fin; zero; suc; _<_) +open import Data.Fin.Base using (zero; suc; _<_) open import Data.Nat.Base using (ℕ; zero; suc; NonZero) open import Data.Nat.Properties using (<-pred) open import Level using (Level) @@ -48,7 +48,7 @@ module _ (trans : Transitive R) where Linked R xs → All (R v) xs NZLinked⇒All {n = suc n} = Linked⇒All {n = n} - lookup⁺ : ∀ {i j : Fin n} {xs} → + lookup⁺ : ∀ {i j} {xs : Vec _ n} → Linked R xs → i < j → R (lookup xs i) (lookup xs j) lookup⁺ {i = zero} {j = suc j} (rx ∷ rxs) i Date: Thu, 29 Sep 2022 14:58:32 +0100 Subject: [PATCH 37/48] removed NZ ahead of subsequent PR --- src/Data/Vec/Relation/Unary/Linked/Properties.agda | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda index ecf9f96a34..3935a263c4 100644 --- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda @@ -43,11 +43,6 @@ module _ (trans : Transitive R) where Linked⇒All Rvx [-] = Rvx ∷ [] Linked⇒All Rvx (Rxy ∷ Rxs) = Rvx ∷ Linked⇒All (trans Rvx Rxy) Rxs - NZLinked⇒All : .{{nz : NonZero n}} → - ∀ {v} {xs : Vec _ n} → R v (NZhead {{nz}} xs) → - Linked R xs → All (R v) xs - NZLinked⇒All {n = suc n} = Linked⇒All {n = n} - lookup⁺ : ∀ {i j} {xs : Vec _ n} → Linked R xs → i < j → R (lookup xs i) (lookup xs j) From e69f126008de7da80b2e0af3b343415de1848c05 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 29 Sep 2022 15:00:51 +0100 Subject: [PATCH 38/48] narrowed dependency on Fin --- src/Data/Vec/Relation/Unary/All/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Vec/Relation/Unary/All/Properties.agda b/src/Data/Vec/Relation/Unary/All/Properties.agda index 345208ee2c..70c39b0c0d 100644 --- a/src/Data/Vec/Relation/Unary/All/Properties.agda +++ b/src/Data/Vec/Relation/Unary/All/Properties.agda @@ -9,7 +9,7 @@ module Data.Vec.Relation.Unary.All.Properties where open import Data.Nat.Base using (ℕ; zero; suc; _+_) -open import Data.Fin.Base using (Fin; zero; suc) +open import Data.Fin.Base using (zero; suc) open import Data.List.Base using ([]; _∷_) open import Data.List.Relation.Unary.All as List using ([]; _∷_) open import Data.Product as Prod using (_×_; _,_; uncurry; uncurry′) @@ -37,7 +37,7 @@ private ------------------------------------------------------------------------ -- lookup -lookup⁺ : All P xs → (i : Fin n) → P (Vec.lookup xs i) +lookup⁺ : All P xs → ∀ i → P (Vec.lookup xs i) lookup⁺ (px ∷ _) zero = px lookup⁺ (_ ∷ pxs) (suc i) = lookup⁺ pxs i From 146e6735df574b62fd328f95bbf57cf678f2673b Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 29 Sep 2022 15:47:41 +0100 Subject: [PATCH 39/48] removed NZ ahead of subsequent PR --- .../Properties/CommutativeMonoid/Sum.agda | 4 - src/Data/Fin/Base.agda | 74 ------------------- src/Data/Fin/Properties.agda | 47 ------------ src/Data/Vec/Base.agda | 22 ------ src/Data/Vec/Functional.agda | 23 +----- src/Data/Vec/Properties.agda | 25 ------- src/Data/Vec/Recursive.agda | 9 --- src/Data/Vec/Relation/Unary/All.agda | 11 --- src/Data/Vec/Relation/Unary/Any.agda | 8 -- 9 files changed, 1 insertion(+), 222 deletions(-) diff --git a/src/Algebra/Properties/CommutativeMonoid/Sum.agda b/src/Algebra/Properties/CommutativeMonoid/Sum.agda index c7ebf558fd..54731cfb5b 100644 --- a/src/Algebra/Properties/CommutativeMonoid/Sum.agda +++ b/src/Algebra/Properties/CommutativeMonoid/Sum.agda @@ -59,10 +59,6 @@ sum-remove {suc n} {suc i} xs = begin ∑t = sum t ∑t′ = sum (remove i t) -NZsum-remove : ∀ {n} {{nz : NonZero n}} {i : Fin n} t → sum t ≈ t i + sum (NZremove {{nz}} i t) - -NZsum-remove {n = suc n} = sum-remove - -- The '∑' operator distributes over addition. ∑-distrib-+ : ∀ {n} (f g : Vector Carrier n) → ∑[ i < n ] (f i + g i) ≈ ∑[ i < n ] f i + ∑[ i < n ] g i ∑-distrib-+ {zero} f g = sym (+-identityˡ _) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index aa22f1b121..f0c298ea0b 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -38,62 +38,6 @@ data Fin : ℕ → Set where zero : Fin (suc n) suc : (i : Fin n) → Fin (suc n) --- uniform zero - -NZzero : .{{ℕ.NonZero n}} → Fin n -NZzero {n = suc n} = zero - --- uniform successor - -NZsuc : .{{ℕ.NonZero n}} → Fin (ℕ.pred n) → Fin n -NZsuc {n = suc n} = suc - --- NonZero predicate - -isZero : (i : Fin (suc n)) → Bool -isZero zero = true -isZero (suc i) = false - --- uniform version - -NZisZero : (i : Fin n) → Bool -NZisZero {n = zero} () -NZisZero {n = suc n} i = isZero {n} i - -record NonZero (i : Fin n) : Set where - field - nonZero : T (not (NZisZero i)) - --- Instances - -instance - nonZero : ∀ {i} → NonZero {suc n} (suc i) - nonZero = _ - --- Constructors - -≢-nonZero : ∀ {{_ : ℕ.NonZero n}} {i} → i ≢ NZzero → NonZero {n} i -≢-nonZero {i = zero} 0≢0 = contradiction refl 0≢0 -≢-nonZero {i = suc i} i≢0 = _ - --- Destructors - -≢-nonZero⁻¹ : ∀ {{_ : ℕ.NonZero n}} i → .{{NonZero {n} i}} → i ≢ NZzero -≢-nonZero⁻¹ (suc i) () - --- Bool-valued equality - -infix 4 _=ᵇ_ _NZ=ᵇ_ - -_=ᵇ_ : ∀ {n} (i j : Fin (suc n)) → Bool -zero =ᵇ zero = true -_=ᵇ_ {n = suc n} (suc i) (suc j) = _=ᵇ_ {n = n} i j -_ =ᵇ _ = false - -_NZ=ᵇ_ : ∀ {n} (i j : Fin n) → Bool -_NZ=ᵇ_ {n = zero} () () -_NZ=ᵇ_ {n = suc n} = _=ᵇ_ {n = n} - -- A conversion: toℕ "i" = i. toℕ : Fin n → ℕ @@ -167,16 +111,10 @@ inject! : ∀ {i : Fin (suc n)} → Fin′ i → Fin n inject! {n = suc _} {i = suc _} zero = zero inject! {n = suc _} {i = suc _} (suc j) = suc (inject! j) -NZinject! : .{{_ : ℕ.NonZero n}} → {i : Fin n} → Fin′ i → Fin (ℕ.pred n) -NZinject! {n = suc n} = inject! - inject₁ : Fin n → Fin (suc n) inject₁ zero = zero inject₁ (suc i) = suc (inject₁ i) -NZinject₁ : .{{_ : ℕ.NonZero n}} → Fin (ℕ.pred n) → Fin n -NZinject₁ {n = suc n} = inject₁ - inject≤ : Fin m → m ℕ.≤ n → Fin n inject≤ {_} {suc n} zero _ = zero inject≤ {_} {suc n} (suc i) (s≤s m≤n) = suc (inject≤ i m≤n) @@ -188,9 +126,6 @@ lower₁ {zero} zero ne = ⊥-elim (ne refl) lower₁ {suc n} zero _ = zero lower₁ {suc n} (suc i) ne = suc (lower₁ i (ne ∘ cong suc)) -NZlower₁ : .{{ℕ.NonZero n}} → (i : Fin n) → n ≢ suc (toℕ i) → Fin (ℕ.pred n) -NZlower₁ {n = suc n} i ne = lower₁ i (ne ∘ cong suc) - -- A strengthening injection into the minimal Fin fibre. strengthen : ∀ (i : Fin n) → Fin′ (suc i) strengthen zero = zero @@ -330,9 +265,6 @@ punchOut {_} {zero} {suc j} _ = j punchOut {suc _} {suc i} {zero} _ = zero punchOut {suc _} {suc i} {suc j} i≢j = suc (punchOut (i≢j ∘ cong suc)) -NZpunchOut : .{{ℕ.NonZero n}} → {i j : Fin n} → i ≢ j → Fin (ℕ.pred n) -NZpunchOut {n = suc n} = punchOut - -- The function f(i,j) = if j≥i then j+1 else j punchIn : Fin (suc n) → Fin n → Fin (suc n) @@ -340,9 +272,6 @@ punchIn zero j = suc j punchIn (suc i) zero = zero punchIn (suc i) (suc j) = suc (punchIn i j) -NZpunchIn : .{{ℕ.NonZero n}} → Fin n → Fin (ℕ.pred n) → Fin n -NZpunchIn {n = suc n} = punchIn - -- The function f(i,j) such that f(i,j) = if j≤i then j else j-1 pinch : Fin n → Fin (suc n) → Fin n @@ -350,9 +279,6 @@ pinch {suc n} _ zero = zero pinch {suc n} zero (suc j) = j pinch {suc n} (suc i) (suc j) = suc (pinch i j) -NZpinch : .{{ℕ.NonZero n}} → Fin (ℕ.pred n) → Fin n → Fin (ℕ.pred n) -NZpinch {n = suc n} = pinch - ------------------------------------------------------------------------ -- Order relations diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 7e6787e7c8..b9f680b7b2 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -202,9 +202,6 @@ fromℕ-toℕ (suc i) = cong suc (fromℕ-toℕ i) ≤fromℕ : ∀ (i : Fin (ℕ.suc n)) → i ≤ fromℕ n ≤fromℕ i = subst (toℕ i ℕ.≤_) (sym (toℕ-fromℕ _)) (toℕ≤pred[n] i) -NZ≤fromℕ : .{{_ : ℕ.NonZero n}} (i : Fin n) → i ≤ fromℕ (ℕ.pred n) -NZ≤fromℕ {n = suc n} i = ≤fromℕ i - ------------------------------------------------------------------------ -- fromℕ< ------------------------------------------------------------------------ @@ -490,11 +487,6 @@ inject₁-lower₁ {suc n} zero _ = refl inject₁-lower₁ {suc n} (suc i) n+1≢i+1 = cong suc (inject₁-lower₁ i (n+1≢i+1 ∘ cong suc)) -NZinject₁-lower₁ : .{{_ : ℕ.NonZero n}} → - ∀ (i : Fin n) (n≢i+1 : n ≢ suc (toℕ i)) → - NZinject₁ (NZlower₁ i n≢i+1) ≡ i -NZinject₁-lower₁ {n = suc n} i n≢i+1 = inject₁-lower₁ i (n≢i+1 ∘ cong suc) - lower₁-inject₁′ : ∀ (i : Fin n) (n≢i : n ≢ toℕ (inject₁ i)) → lower₁ (inject₁ i) n≢i ≡ i lower₁-inject₁′ zero _ = refl @@ -512,20 +504,10 @@ lower₁-irrelevant {suc n} zero _ _ = refl lower₁-irrelevant {suc n} (suc i) _ _ = cong suc (lower₁-irrelevant i _ _) -NZlower₁-irrelevant : .{{_ : ℕ.NonZero n}} → - ∀ (i : Fin n) (n≢i₁+1 n≢i₂+1 : n ≢ suc (toℕ i)) → - NZlower₁ i n≢i₁+1 ≡ NZlower₁ i n≢i₂+1 -NZlower₁-irrelevant {n = suc n} i n≢i₁+1 n≢i₂+1 = lower₁-irrelevant i (n≢i₁+1 ∘ cong suc) (n≢i₂+1 ∘ cong suc) - inject₁≡⇒lower₁≡ : ∀ {i : Fin n} {j : Fin (ℕ.suc n)} → (n≢j : n ≢ toℕ j) → inject₁ i ≡ j → lower₁ j n≢j ≡ i inject₁≡⇒lower₁≡ n≢j i≡j = inject₁-injective (trans (inject₁-lower₁ _ n≢j) (sym i≡j)) -NZinject₁≡⇒lower₁≡ : .{{_ : ℕ.NonZero n}} → - ∀ {i : Fin (ℕ.pred n)} {j : Fin n} → - (n≢j+1 : n ≢ suc (toℕ j)) → NZinject₁ i ≡ j → NZlower₁ j n≢j+1 ≡ i -NZinject₁≡⇒lower₁≡ {n = suc n} n≢j+1 = inject₁≡⇒lower₁≡ (n≢j+1 ∘ cong suc) - ------------------------------------------------------------------------ -- inject≤ ------------------------------------------------------------------------ @@ -559,9 +541,6 @@ pred< : ∀ (i : Fin (suc n)) → i ≢ zero → pred i < i pred< zero i≢0 = contradiction refl i≢0 pred< (suc i) _ = ≤̄⇒inject₁< ℕₚ.≤-refl -NZpred< : ∀ .{{_ : ℕ.NonZero n}} → (i : Fin n) → i ≢ NZzero → pred i < i -NZpred< {n = suc n} i = pred< i - ------------------------------------------------------------------------ -- splitAt ------------------------------------------------------------------------ @@ -842,11 +821,6 @@ punchOut-cong {_} zero {suc j} {suc k} = suc-injective punchOut-cong {suc n} (suc i) {zero} {zero} _ = refl punchOut-cong {suc n} (suc i) {suc j} {suc k} = cong suc ∘ punchOut-cong i ∘ suc-injective -NZpunchOut-cong : .{{_ : ℕ.NonZero n}} → - ∀ (i : Fin n) {j k} {i≢j : i ≢ j} {i≢k : i ≢ k} → - j ≡ k → NZpunchOut i≢j ≡ NZpunchOut i≢k -NZpunchOut-cong {n = suc n} = punchOut-cong - -- An alternative to 'punchOut-cong' in the which the new inequality argument is -- specific. Useful for enabling the omission of that argument during equational -- reasoning. @@ -855,11 +829,6 @@ punchOut-cong′ : ∀ (i : Fin (suc n)) {j k} {p : i ≢ j} (q : j ≡ k) → punchOut p ≡ punchOut (p ∘ sym ∘ trans q ∘ sym) punchOut-cong′ i q = punchOut-cong i q -NZpunchOut-cong′ : .{{_ : ℕ.NonZero n}} → - ∀ (i : Fin n) {j k} {p : i ≢ j} (q : j ≡ k) → - NZpunchOut p ≡ NZpunchOut (p ∘ sym ∘ trans q ∘ sym) -NZpunchOut-cong′ {n = suc n} = punchOut-cong′ - punchOut-injective : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) → punchOut i≢j ≡ punchOut i≢k → j ≡ k @@ -870,12 +839,6 @@ punchOut-injective {suc n} {suc i} {zero} {zero} _ _ _ = refl punchOut-injective {suc n} {suc i} {suc j} {suc k} i≢j i≢k pⱼ≡pₖ = cong suc (punchOut-injective (i≢j ∘ cong suc) (i≢k ∘ cong suc) (suc-injective pⱼ≡pₖ)) -NZpunchOut-injective : .{{_ : ℕ.NonZero n}} → - ∀ {i j k : Fin n} - (i≢j : i ≢ j) (i≢k : i ≢ k) → - NZpunchOut i≢j ≡ NZpunchOut i≢k → j ≡ k -NZpunchOut-injective {n = suc n} = punchOut-injective - punchIn-punchOut : ∀ {i j : Fin (suc n)} (i≢j : i ≢ j) → punchIn i (punchOut i≢j) ≡ j punchIn-punchOut {_} {zero} {zero} 0≢0 = contradiction refl 0≢0 @@ -884,11 +847,6 @@ punchIn-punchOut {suc m} {suc i} {zero} i≢j = refl punchIn-punchOut {suc m} {suc i} {suc j} i≢j = cong suc (punchIn-punchOut (i≢j ∘ cong suc)) -NZpunchIn-punchOut : .{{_ : ℕ.NonZero n}} → - ∀ {i j : Fin n} (i≢j : i ≢ j) → - NZpunchIn i (NZpunchOut i≢j) ≡ j -NZpunchIn-punchOut {n = suc n} = punchIn-punchOut - punchOut-punchIn : ∀ i {j : Fin n} → punchOut {i = i} {j = punchIn i j} (punchInᵢ≢i i j ∘ sym) ≡ j punchOut-punchIn zero {j} = refl punchOut-punchIn (suc i) {zero} = refl @@ -928,11 +886,6 @@ pinch-injective {i = suc i} {suc j} {suc k} 1+i≢j 1+i≢k eq = (pinch-injective (1+i≢j ∘ cong suc) (1+i≢k ∘ cong suc) (suc-injective eq)) -NZpinch-injective : .{{_ : ℕ.NonZero n}} → - ∀ {i : Fin (ℕ.pred n)} {j k : Fin n} → - NZsuc i ≢ j → NZsuc i ≢ k → NZpinch i j ≡ NZpinch i k → j ≡ k -NZpinch-injective {n = suc n} = pinch-injective - ------------------------------------------------------------------------ -- Quantification ------------------------------------------------------------------------ diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index 25e59c0eb3..9a7668014b 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -53,15 +53,9 @@ length {n = n} _ = n head : Vec A (1 + n) → A head (x ∷ xs) = x -NZhead : .{{_ : NonZero n}} → Vec A n → A -NZhead {n = suc n} = head - tail : Vec A (1 + n) → Vec A n tail (x ∷ xs) = xs -NZtail : .{{_ : NonZero n}} → Vec A n → Vec A (pred n) -NZtail {n = suc n} = tail - lookup : Vec A n → Fin n → A lookup (x ∷ xs) zero = x lookup (x ∷ xs) (suc i) = lookup xs i @@ -74,16 +68,10 @@ insert : Vec A n → Fin (suc n) → A → Vec A (suc n) insert xs zero v = v ∷ xs insert (x ∷ xs) (suc i) v = x ∷ insert xs i v -NZinsert : .{{_ : NonZero n}} → Vec A (pred n) → Fin n → A → Vec A n -NZinsert {n = suc n} = insert - remove : Vec A (suc n) → Fin (suc n) → Vec A n remove (_ ∷ xs) zero = xs remove (x ∷ y ∷ xs) (suc i) = x ∷ remove (y ∷ xs) i -NZremove : .{{_ : NonZero n}} → Vec A n → Fin n → Vec A (pred n) -NZremove {n = suc n} = remove - updateAt : Fin n → (A → A) → Vec A n → Vec A n updateAt zero f (x ∷ xs) = f x ∷ xs updateAt (suc i) f (x ∷ xs) = x ∷ updateAt i f xs @@ -295,10 +283,6 @@ split (x ∷ y ∷ xs) = Prod.map (x ∷_) (y ∷_) (split xs) uncons : Vec A (suc n) → A × Vec A n uncons (x ∷ xs) = x , xs -NZuncons : .{{_ : NonZero n}} → - Vec A n → A × Vec A (pred n) -NZuncons {n = suc n} = uncons - ------------------------------------------------------------------------ -- Operations involving ≤ @@ -357,16 +341,10 @@ init : Vec A (1 + n) → Vec A n init xs with initLast xs ... | (ys , y , refl) = ys -NZinit : ∀ .{{_ : NonZero n}} → (xs : Vec A n) → Vec A (pred n) -NZinit {n = suc n} = init - last : Vec A (1 + n) → A last xs with initLast xs ... | (ys , y , refl) = y -NZlast : ∀ .{{_ : NonZero n}} → (xs : Vec A n) → A -NZlast {n = suc n} = last - ------------------------------------------------------------------------ -- Other operations diff --git a/src/Data/Vec/Functional.agda b/src/Data/Vec/Functional.agda index 96ba80c435..1696e6b482 100644 --- a/src/Data/Vec/Functional.agda +++ b/src/Data/Vec/Functional.agda @@ -15,7 +15,7 @@ module Data.Vec.Functional where -open import Data.Fin.Base hiding (NonZero; pred) +open import Data.Fin.Base open import Data.List.Base as L using (List) open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero; pred) open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂; uncurry) @@ -72,21 +72,12 @@ length {n = n} _ = n head : ∀ {n} → Vector A (suc n) → A head xs = xs zero -NZhead : ∀ {n} {{_ : NonZero n}} → Vector A n → A -NZhead {n = suc n} = head - tail : ∀ {n} → Vector A (suc n) → Vector A n tail xs = xs ∘ suc -NZtail : ∀ {n} {{_ : NonZero n}} → Vector A n → Vector A (pred n) -NZtail {n = suc n} = tail - uncons : ∀ {n} → Vector A (suc n) → A × Vector A n uncons xs = head xs , tail xs -NZuncons : ∀ {n} {{_ : NonZero n}} → Vector A n → A × Vector A (pred n) -NZuncons {n = suc n} = uncons - replicate : ∀ {n} → A → Vector A n replicate = const @@ -96,15 +87,9 @@ insert {n = n} xs zero v (suc j) = xs j insert {n = suc n} xs (suc i) v zero = head xs insert {n = suc n} xs (suc i) v (suc j) = insert (tail xs) i v j -NZinsert : ∀ {n} {{_ : NonZero n}} → Vector A (pred n) → Fin n → A → Vector A n -NZinsert {n = suc n} = insert - remove : ∀ {n} → Fin (suc n) → Vector A (suc n) → Vector A n remove i t = t ∘ punchIn i -NZremove : ∀ {n} {{_ : NonZero n}} → Fin n → Vector A n → Vector A (pred n) -NZremove {n = suc n} i t = t ∘ NZpunchIn i - updateAt : ∀ {n} → Fin n → (A → A) → Vector A n → Vector A n updateAt {n = suc n} zero f xs zero = f (head xs) updateAt {n = suc n} zero f xs (suc j) = xs (suc j) @@ -164,14 +149,8 @@ reverse xs = xs ∘ opposite init : ∀ {n} → Vector A (suc n) → Vector A n init xs = xs ∘ inject₁ -NZinit : ∀ {n} {{_ : NonZero n}} → Vector A n → Vector A (pred n) -NZinit {n = suc n} = init - last : ∀ {n} → Vector A (suc n) → A last {n = n} xs = xs (fromℕ n) -NZlast : ∀ {n} {{_ : NonZero n}} → Vector A n → A -NZlast {n = suc n} = last - transpose : ∀ {m n} → Vector (Vector A n) m → Vector (Vector A m) n transpose = flip diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index bee794350a..459880d8cf 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -1013,22 +1013,12 @@ insert-lookup : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) → insert-lookup xs zero v = refl insert-lookup (x ∷ xs) (suc i) v = insert-lookup xs i v -NZinsert-lookup : .{{_ : NonZero n}} → - (xs : Vec A (pred n)) (i : Fin n) (v : A) → - lookup (NZinsert xs i v) i ≡ v -NZinsert-lookup {n = suc n} = insert-lookup - insert-punchIn : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) (j : Fin n) → lookup (insert xs i v) (Fin.punchIn i j) ≡ lookup xs j insert-punchIn xs zero v j = refl insert-punchIn (x ∷ xs) (suc i) v zero = refl insert-punchIn (x ∷ xs) (suc i) v (suc j) = insert-punchIn xs i v j -NZinsert-punchIn : .{{_ : NonZero n}} → - (xs : Vec A (pred n)) (i : Fin n) (v : A) (j : Fin (pred n)) → - lookup (NZinsert xs i v) (Fin.NZpunchIn i j) ≡ lookup xs j -NZinsert-punchIn {n = suc n} = insert-punchIn - remove-punchOut : ∀ (xs : Vec A (suc n)) {i} {j} (i≢j : i ≢ j) → lookup (remove xs i) (Fin.punchOut i≢j) ≡ lookup xs j remove-punchOut (x ∷ xs) {zero} {zero} i≢j = contradiction refl i≢j @@ -1037,11 +1027,6 @@ remove-punchOut (x ∷ y ∷ xs) {suc i} {zero} i≢j = refl remove-punchOut (x ∷ y ∷ xs) {suc i} {suc j} i≢j = remove-punchOut (y ∷ xs) (i≢j ∘ cong suc) -NZremove-punchOut : .{{_ : NonZero n}} → - ∀ (xs : Vec A n) {i} {j} (i≢j : i ≢ j) → - lookup (NZremove xs i) (Fin.NZpunchOut i≢j) ≡ lookup xs j -NZremove-punchOut {n = suc n} = remove-punchOut - ------------------------------------------------------------------------ -- remove @@ -1052,22 +1037,12 @@ remove-insert (x ∷ xs) (suc zero) v = refl remove-insert (x ∷ y ∷ xs) (suc (suc i)) v = cong (x ∷_) (remove-insert (y ∷ xs) (suc i) v) -NZremove-insert : .{{_ : NonZero n}} → - ∀ (xs : Vec A (pred n)) (i : Fin n) (v : A) → - NZremove (NZinsert xs i v) i ≡ xs -NZremove-insert {n = suc n} = remove-insert - insert-remove : ∀ (xs : Vec A (suc n)) (i : Fin (suc n)) → insert (remove xs i) i (lookup xs i) ≡ xs insert-remove (x ∷ xs) zero = refl insert-remove (x ∷ y ∷ xs) (suc i) = cong (x ∷_) (insert-remove (y ∷ xs) i) -NZinsert-remove : .{{_ : NonZero n}} → - ∀ (xs : Vec A n) (i : Fin n) → - NZinsert (NZremove xs i) i (lookup xs i) ≡ xs -NZinsert-remove {n = suc n} = insert-remove - ------------------------------------------------------------------------ -- Conversion function diff --git a/src/Data/Vec/Recursive.agda b/src/Data/Vec/Recursive.agda index 0290c4a1bc..b30089d33c 100644 --- a/src/Data/Vec/Recursive.agda +++ b/src/Data/Vec/Recursive.agda @@ -74,21 +74,12 @@ uncons : ∀ n → A ^ suc n → A × A ^ n uncons 0 a = a , lift tt uncons (suc n) (a , as) = a , as -NZuncons : ∀ n → .{{_ : NonZero n}} → A ^ n → A × A ^ (pred n) -NZuncons (suc n) = uncons n - head : ∀ n → A ^ suc n → A head n as = proj₁ (uncons n as) -NZhead : ∀ n → .{{_ : NonZero n}} → A ^ n → A -NZhead (suc n) = head n - tail : ∀ n → A ^ suc n → A ^ n tail n as = proj₂ (uncons n as) -NZtail : ∀ n → .{{_ : NonZero n}} → A ^ n → A ^ (pred n) -NZtail (suc n) = tail n - fromVec : ∀[ Vec A ⇒ (A ^_) ] fromVec = Vec.foldr (_ ^_) (cons _) _ diff --git a/src/Data/Vec/Relation/Unary/All.agda b/src/Data/Vec/Relation/Unary/All.agda index 957e2a6299..b16340ef6b 100644 --- a/src/Data/Vec/Relation/Unary/All.agda +++ b/src/Data/Vec/Relation/Unary/All.agda @@ -52,16 +52,9 @@ data All {A : Set a} (P : Pred A p) : Vec A n → Set (p ⊔ a) where head : All P (x ∷ xs) → P x head (px ∷ pxs) = px -NZhead : .{{nz : NonZero n}} → All P xs → P (Vec.NZhead {{nz}} xs) -NZhead {n = suc n} pxs@(_ ∷ _) = head pxs - tail : All P (x ∷ xs) → All P xs tail (px ∷ pxs) = pxs -NZtail : .{{nz : NonZero n}} → - All P xs → All P (Vec.NZtail {{nz}} xs) -NZtail {n = suc n} pxs@(_ ∷ _) = tail pxs - reduce : (f : ∀ {x} → P x → B) → ∀ {n} {xs : Vec A n} → All P xs → Vec B n reduce f [] = [] reduce f (px ∷ pxs) = f px ∷ reduce f pxs @@ -69,10 +62,6 @@ reduce f (px ∷ pxs) = f px ∷ reduce f pxs uncons : All P (x ∷ xs) → P x × All P xs uncons = < head , tail > -NZuncons : .{{nz : NonZero n}} → - All P xs → P (Vec.NZhead {{nz}} xs) × All P (Vec.NZtail {{nz}} xs) -NZuncons = < NZhead , NZtail > - map : P ⊆ Q → All P ⊆ All Q {n} map g [] = [] map g (px ∷ pxs) = g px ∷ map g pxs diff --git a/src/Data/Vec/Relation/Unary/Any.agda b/src/Data/Vec/Relation/Unary/Any.agda index aace996c86..a54991976f 100644 --- a/src/Data/Vec/Relation/Unary/Any.agda +++ b/src/Data/Vec/Relation/Unary/Any.agda @@ -44,19 +44,11 @@ head : ∀ {x} → ¬ Any P xs → Any P (x ∷ xs) → P x head ¬pxs (here px) = px head ¬pxs (there pxs) = contradiction pxs ¬pxs -NZhead : .{{nz : NonZero n}} → - ¬ Any P (Vec.NZtail {{nz}} xs) → Any P xs → P (Vec.NZhead {{nz}} xs) -NZhead {n = suc n} {xs = _ ∷ _} ¬pxs = head ¬pxs - -- If the head does not satisfy the predicate, then the tail will. tail : ∀ {x} → ¬ P x → Any P (x ∷ xs) → Any P xs tail ¬px (here px) = ⊥-elim (¬px px) tail ¬px (there pxs) = pxs -NZtail : .{{nz : NonZero n}} → - ¬ P (Vec.NZhead {{nz}} xs) → Any P xs → Any P (Vec.NZtail {{nz}} xs) -NZtail {n = suc n} {xs = _ ∷ _} ¬px = tail ¬px - -- Convert back and forth with sum toSum : ∀ {x} → Any P (x ∷ xs) → P x ⊎ Any P xs toSum (here px) = inj₁ px From 3e3182a655025592726b2066ec3819039b636f21 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 29 Sep 2022 16:22:48 +0100 Subject: [PATCH 40/48] fixed typo --- src/Data/Fin/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index b9f680b7b2..78944213da 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -789,8 +789,8 @@ nℕ-ℕi≤n (suc n) (suc i) = begin suc n ∎ where open ℕₚ.≤-Reasoning -nℕ-suci≤n : ∀ n i → n ℕ-suc i ℕ.< n -nℕ-suci≤n (suc n) i = s Date: Thu, 29 Sep 2022 16:40:25 +0100 Subject: [PATCH 41/48] added one function and two new proofs to CHANGELOG --- CHANGELOG.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 850ae0ae4d..bf7dc0cb55 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1431,6 +1431,8 @@ Other minor changes funToFin : (Fin m → Fin n) → Fin (n ^ m) quotient : Fin (m * n) → Fin m remainder : Fin (m * n) → Fin n + + _ℕ-suc_ : (n : ℕ) → Fin n → ℕ ``` * Added new proofs in `Data.Fin.Induction`: @@ -1479,6 +1481,9 @@ Other minor changes combine-surjective : ∀ i → ∃₂ λ j k → combine j k ≡ i combine-monoˡ-< : i < j → combine i k < combine j l + ℕ-ℕ≡toℕ‿ℕ- : n ℕ-ℕ i ≡ toℕ (n ℕ- i) + nℕ-suci Date: Wed, 5 Oct 2022 17:17:28 +0100 Subject: [PATCH 42/48] revert additions to Fin.Base/Properties --- src/Data/Fin/Base.agda | 7 ------- src/Data/Fin/Properties.agda | 3 --- 2 files changed, 10 deletions(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index f0c298ea0b..06c4581337 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -236,13 +236,6 @@ _ℕ-ℕ_ : (n : ℕ) → Fin (suc n) → ℕ n ℕ-ℕ zero = n suc n ℕ-ℕ suc i = n ℕ-ℕ i --- n ℕ-suc "i" = n ∸ (suc i) - -infixl 6 _ℕ-suc_ - -_ℕ-suc_ : (n : ℕ) → Fin n → ℕ -suc n ℕ-suc i = n ℕ-ℕ i - -- pred "i" = "pred i". pred : Fin n → Fin n diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 78944213da..b6837a00f6 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -789,9 +789,6 @@ nℕ-ℕi≤n (suc n) (suc i) = begin suc n ∎ where open ℕₚ.≤-Reasoning -nℕ-suci Date: Wed, 5 Oct 2022 17:27:21 +0100 Subject: [PATCH 43/48] reverted CHANGELOG --- CHANGELOG.md | 3 --- 1 file changed, 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5f91c4a227..5fa258f6f3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1468,8 +1468,6 @@ Other minor changes funToFin : (Fin m → Fin n) → Fin (n ^ m) quotient : Fin (m * n) → Fin m remainder : Fin (m * n) → Fin n - - _ℕ-suc_ : (n : ℕ) → Fin n → ℕ ``` * Added new proofs in `Data.Fin.Induction`: @@ -1519,7 +1517,6 @@ Other minor changes combine-monoˡ-< : i < j → combine i k < combine j l ℕ-ℕ≡toℕ‿ℕ- : n ℕ-ℕ i ≡ toℕ (n ℕ- i) - nℕ-suci Date: Thu, 6 Oct 2022 13:46:42 +0100 Subject: [PATCH 44/48] reverted tabulate properties --- .../List/Relation/Binary/Equality/Setoid.agda | 15 ++++++++------- .../List/Relation/Unary/All/Properties.agda | 6 +++--- .../Relation/Unary/AllPairs/Properties.agda | 5 +++-- .../List/Relation/Unary/Any/Properties.agda | 6 +++--- .../Unary/Unique/Propositional/Properties.agda | 5 +++-- .../Unary/Unique/Setoid/Properties.agda | 11 +++++------ src/Data/Vec/Properties.agda | 18 +++++++++--------- .../Vec/Relation/Unary/All/Properties.agda | 6 +++--- .../Relation/Unary/AllPairs/Properties.agda | 5 +++-- .../Vec/Relation/Unary/Any/Properties.agda | 6 +++--- .../Unary/Unique/Propositional/Properties.agda | 3 ++- .../Unary/Unique/Setoid/Properties.agda | 14 +++++++------- 12 files changed, 52 insertions(+), 48 deletions(-) diff --git a/src/Data/List/Relation/Binary/Equality/Setoid.agda b/src/Data/List/Relation/Binary/Equality/Setoid.agda index cd1a6d86d1..feaa48e6dc 100644 --- a/src/Data/List/Relation/Binary/Equality/Setoid.agda +++ b/src/Data/List/Relation/Binary/Equality/Setoid.agda @@ -11,7 +11,7 @@ open import Relation.Binary using (Setoid) module Data.List.Relation.Binary.Equality.Setoid {a ℓ} (S : Setoid a ℓ) where -open import Data.Fin.Base +open import Data.Fin.Base using (Fin) open import Data.List.Base open import Data.List.Relation.Binary.Pointwise as PW using (Pointwise) open import Data.List.Relation.Unary.Unique.Setoid S using (Unique) @@ -129,13 +129,14 @@ concat⁺ = PW.concat⁺ ------------------------------------------------------------------------ -- tabulate -tabulate⁺ : ∀ {n} {f : Fin n → A} {g : Fin n → A} → - (∀ i → f i ≈ g i) → tabulate f ≋ tabulate g -tabulate⁺ = PW.tabulate⁺ +module _ {n} {f g : Fin n → A} + where + + tabulate⁺ : (∀ i → f i ≈ g i) → tabulate f ≋ tabulate g + tabulate⁺ = PW.tabulate⁺ -tabulate⁻ : ∀ {n} {f : Fin n → A} {g : Fin n → A} → - tabulate f ≋ tabulate g → (∀ i → f i ≈ g i) -tabulate⁻ = PW.tabulate⁻ + tabulate⁻ : tabulate f ≋ tabulate g → (∀ i → f i ≈ g i) + tabulate⁻ = PW.tabulate⁻ ------------------------------------------------------------------------ -- filter diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda index 1c28e21b9d..ee4b19ee9c 100644 --- a/src/Data/List/Relation/Unary/All/Properties.agda +++ b/src/Data/List/Relation/Unary/All/Properties.agda @@ -12,7 +12,7 @@ open import Axiom.Extensionality.Propositional using (Extensionality) open import Data.Bool.Base using (Bool; T; true; false) open import Data.Bool.Properties using (T-∧) open import Data.Empty -open import Data.Fin.Base using (zero; suc) +open import Data.Fin.Base using (Fin; zero; suc) open import Data.List.Base as List hiding (lookup) open import Data.List.Properties as Listₚ using (partition-defn) open import Data.List.Membership.Propositional @@ -551,11 +551,11 @@ applyDownFrom⁺₂ f n Pf = applyDownFrom⁺₁ f n (λ _ → Pf _) ------------------------------------------------------------------------ -- tabulate -tabulate⁺ : ∀ {n} {f} → (∀ i → P (f i)) → All P (tabulate {n = n} f) +tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ i → P (f i)) → All P (tabulate f) tabulate⁺ {n = zero} Pf = [] tabulate⁺ {n = suc _} Pf = Pf zero ∷ tabulate⁺ (Pf ∘ suc) -tabulate⁻ : ∀ {n} {f} → All P (tabulate {n = n} f) → (∀ i → P (f i)) +tabulate⁻ : ∀ {n} {f : Fin n → A} → All P (tabulate f) → (∀ i → P (f i)) tabulate⁻ (px ∷ _) zero = px tabulate⁻ (_ ∷ pf) (suc i) = tabulate⁻ pf i diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties.agda b/src/Data/List/Relation/Unary/AllPairs/Properties.agda index 01d2aea103..e9c0b84424 100644 --- a/src/Data/List/Relation/Unary/AllPairs/Properties.agda +++ b/src/Data/List/Relation/Unary/AllPairs/Properties.agda @@ -13,6 +13,7 @@ open import Data.List.Relation.Unary.All as All using (All; []; _∷_) import Data.List.Relation.Unary.All.Properties as All open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_) open import Data.Bool.Base using (true; false) +open import Data.Fin.Base using (Fin) open import Data.Fin.Properties using (suc-injective) open import Data.Nat.Base using (zero; suc; _<_; z≤n; s≤s) open import Data.Nat.Properties using (≤-refl; ≤-step) @@ -113,8 +114,8 @@ module _ {R : Rel A ℓ} where module _ {R : Rel A ℓ} where - tabulate⁺ : ∀ {n} {f} → (∀ {i j} → i ≢ j → R (f i) (f j)) → - AllPairs R (tabulate {n = n} f) + tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ {i j} → i ≢ j → R (f i) (f j)) → + AllPairs R (tabulate f) tabulate⁺ {zero} fᵢ~fⱼ = [] tabulate⁺ {suc n} fᵢ~fⱼ = All.tabulate⁺ (λ j → fᵢ~fⱼ λ()) ∷ diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda index 1c26c287cf..eac897890f 100644 --- a/src/Data/List/Relation/Unary/Any/Properties.agda +++ b/src/Data/List/Relation/Unary/Any/Properties.agda @@ -11,7 +11,7 @@ module Data.List.Relation.Unary.Any.Properties where open import Data.Bool.Base using (Bool; false; true; T) open import Data.Bool.Properties using (T-∨; T-≡) open import Data.Empty using (⊥) -open import Data.Fin.Base using (zero; suc) +open import Data.Fin.Base using (Fin; zero; suc) open import Data.List.Base as List open import Data.List.Properties using (ʳ++-defn) open import Data.List.Effectful using (monad) @@ -511,11 +511,11 @@ module _ {P : A → Set p} where ------------------------------------------------------------------------ -- tabulate -tabulate⁺ : ∀ {n} {f} i → P (f i) → Any P (tabulate {n = n} f) +tabulate⁺ : ∀ {n} {f : Fin n → A} i → P (f i) → Any P (tabulate f) tabulate⁺ zero p = here p tabulate⁺ (suc i) p = there (tabulate⁺ i p) -tabulate⁻ : ∀ {n} {f} → Any P (tabulate {n = n} f) → ∃ λ i → P (f i) +tabulate⁻ : ∀ {n} {f : Fin n → A} → Any P (tabulate f) → ∃ λ i → P (f i) tabulate⁻ {n = suc _} (here p) = zero , p tabulate⁻ {n = suc _} (there p) = Prod.map suc id (tabulate⁻ p) diff --git a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda index 79ee20a73c..c9ac3bff73 100644 --- a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda +++ b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda @@ -14,6 +14,7 @@ open import Data.List.Relation.Unary.All as All using (All; []; _∷_) open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs) open import Data.List.Relation.Unary.Unique.Propositional import Data.List.Relation.Unary.Unique.Setoid.Properties as Setoid +open import Data.Fin.Base using (Fin) open import Data.Nat.Base using (_<_) open import Data.Nat.Properties using (<⇒≢) open import Data.Product using (_×_; _,_) @@ -131,8 +132,8 @@ downFrom⁺ n = applyDownFrom⁺₁ id n (λ j; uncurry) open import Data.Sum.Base using ([_,_]′) @@ -396,7 +396,7 @@ toList-cast {n = suc _} eq (x ∷ xs) = cast-is-id : .(eq : m ≡ m) (xs : Vec A m) → cast eq xs ≡ xs cast-is-id eq [] = refl -cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (ℕₚ.suc-injective eq) xs) +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) @@ -405,7 +405,7 @@ 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 cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (x ∷ xs) = - cong (x ∷_) (cast-trans (ℕₚ.suc-injective eq₁) (ℕₚ.suc-injective eq₂) xs) + cong (x ∷_) (cast-trans (suc-injective eq₁) (suc-injective eq₂) xs) ------------------------------------------------------------------------ -- map @@ -422,7 +422,7 @@ map-cast : (f : A → B) .(eq : m ≡ n) (xs : Vec A m) → map f (cast eq xs) ≡ cast eq (map f xs) map-cast {n = zero} f eq [] = refl map-cast {n = suc _} f eq (x ∷ xs) - = cong (f x ∷_) (map-cast f (ℕₚ.suc-injective eq) xs) + = cong (f x ∷_) (map-cast f (suc-injective eq) xs) map-++ : ∀ (f : A → B) (xs : Vec A m) (ys : Vec A n) → map f (xs ++ ys) ≡ map f xs ++ map f ys @@ -518,19 +518,19 @@ lookup-cast : .(eq : m ≡ n) (xs : Vec A m) (i : Fin m) → lookup (cast eq xs) (Fin.cast eq i) ≡ lookup xs i lookup-cast {n = suc _} eq (x ∷ _) zero = refl lookup-cast {n = suc _} eq (_ ∷ xs) (suc i) = - lookup-cast (ℕₚ.suc-injective eq) xs i + lookup-cast (suc-injective eq) xs i lookup-cast₁ : .(eq : m ≡ n) (xs : Vec A m) (i : Fin n) → lookup (cast eq xs) i ≡ lookup xs (Fin.cast (sym eq) i) lookup-cast₁ eq (x ∷ _) zero = refl lookup-cast₁ eq (_ ∷ xs) (suc i) = - lookup-cast₁ (ℕₚ.suc-injective eq) xs i + lookup-cast₁ (suc-injective eq) xs i lookup-cast₂ : .(eq : m ≡ n) (xs : Vec A n) (i : Fin m) → lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i lookup-cast₂ {n = suc _} eq (x ∷ _) zero = refl lookup-cast₂ {n = suc _} eq (_ ∷ xs) (suc i) = - lookup-cast₂ (ℕₚ.suc-injective eq) xs i + lookup-cast₂ (suc-injective eq) xs i lookup-concat : ∀ (xss : Vec (Vec A m) n) i j → lookup (concat xss) (Fin.combine i j) ≡ lookup (lookup xss i) j diff --git a/src/Data/Vec/Relation/Unary/All/Properties.agda b/src/Data/Vec/Relation/Unary/All/Properties.agda index 70c39b0c0d..591beffde4 100644 --- a/src/Data/Vec/Relation/Unary/All/Properties.agda +++ b/src/Data/Vec/Relation/Unary/All/Properties.agda @@ -9,7 +9,7 @@ module Data.Vec.Relation.Unary.All.Properties where open import Data.Nat.Base using (ℕ; zero; suc; _+_) -open import Data.Fin.Base using (zero; suc) +open import Data.Fin.Base using (Fin; zero; suc) open import Data.List.Base using ([]; _∷_) open import Data.List.Relation.Unary.All as List using ([]; _∷_) open import Data.Product as Prod using (_×_; _,_; uncurry; uncurry′) @@ -133,11 +133,11 @@ module _ {_~_ : REL A B p} where module _ {P : A → Set p} where - tabulate⁺ : ∀ {n} {f} → (∀ i → P (f i)) → All P (tabulate {n = n} f) + tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ i → P (f i)) → All P (tabulate f) tabulate⁺ {zero} Pf = [] tabulate⁺ {suc n} Pf = Pf zero ∷ tabulate⁺ (Pf ∘ suc) - tabulate⁻ : ∀ {n} {f} → All P (tabulate {n = n} f) → (∀ i → P (f i)) + tabulate⁻ : ∀ {n} {f : Fin n → A} → All P (tabulate f) → (∀ i → P (f i)) tabulate⁻ (px ∷ _) zero = px tabulate⁻ (_ ∷ pf) (suc i) = tabulate⁻ pf i diff --git a/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda b/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda index 38eb8cdaa4..f7b3a8584b 100644 --- a/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda +++ b/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda @@ -14,6 +14,7 @@ open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_) import Data.Vec.Relation.Unary.All.Properties as Allₚ open import Data.Vec.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_) open import Data.Bool.Base using (true; false) +open import Data.Fin.Base using (Fin) open import Data.Fin.Properties using (suc-injective) open import Data.Nat.Base using (zero; suc; _+_) open import Function using (_∘_) @@ -82,8 +83,8 @@ module _ {R : Rel A ℓ} where module _ {R : Rel A ℓ} where - tabulate⁺ : ∀ {n} {f} → (∀ {i j} → i ≢ j → R (f i) (f j)) → - AllPairs R (tabulate {n = n} f) + tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ {i j} → i ≢ j → R (f i) (f j)) → + AllPairs R (tabulate f) tabulate⁺ {zero} fᵢ~fⱼ = [] tabulate⁺ {suc n} fᵢ~fⱼ = Allₚ.tabulate⁺ (λ j → fᵢ~fⱼ λ()) ∷ diff --git a/src/Data/Vec/Relation/Unary/Any/Properties.agda b/src/Data/Vec/Relation/Unary/Any/Properties.agda index f87dc9273b..22d112674a 100644 --- a/src/Data/Vec/Relation/Unary/Any/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Any/Properties.agda @@ -9,7 +9,7 @@ module Data.Vec.Relation.Unary.Any.Properties where open import Data.Nat.Base using (suc; zero) -open import Data.Fin.Base using (zero; suc) +open import Data.Fin.Base using (Fin; zero; suc) open import Data.Empty using (⊥) open import Data.List.Base using ([]; _∷_) import Data.List.Relation.Unary.Any as List @@ -357,11 +357,11 @@ module _ {P : Pred A p} where module _ {P : Pred A p} where - tabulate⁺ : ∀ {n} {f} i → P (f i) → Any P (tabulate {n = n} f) + tabulate⁺ : ∀ {n} {f : Fin n → A} i → P (f i) → Any P (tabulate f) tabulate⁺ zero p = here p tabulate⁺ (suc i) p = there (tabulate⁺ i p) - tabulate⁻ : ∀ {n} {f} → Any P (tabulate {n = n} f) → ∃ λ i → P (f i) + tabulate⁻ : ∀ {n} {f : Fin n → A} → Any P (tabulate f) → ∃ λ i → P (f i) tabulate⁻ (here p) = zero , p tabulate⁻ (there p) = Prod.map suc id (tabulate⁻ p) diff --git a/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda b/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda index b0719a3bf2..acd1b916c8 100644 --- a/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda @@ -13,6 +13,7 @@ open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_) open import Data.Vec.Relation.Unary.AllPairs as AllPairs using (AllPairs) open import Data.Vec.Relation.Unary.Unique.Propositional import Data.Vec.Relation.Unary.Unique.Setoid.Properties as Setoid +open import Data.Fin.Base using(Fin) open import Data.Nat.Base open import Data.Nat.Properties using (<⇒≢) open import Data.Product using (_×_; _,_) @@ -56,7 +57,7 @@ module _ {A : Set a} where module _ {A : Set a} where - tabulate⁺ : ∀ {n} {f} → (∀ {i j} → f i ≡ f j → i ≡ j) → Unique (tabulate {n = n} f) + tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ {i j} → f i ≡ f j → i ≡ j) → Unique (tabulate f) tabulate⁺ = Setoid.tabulate⁺ (setoid A) ------------------------------------------------------------------------ diff --git a/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda b/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda index f256f2ae9d..7166a8af45 100644 --- a/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda @@ -8,14 +8,14 @@ module Data.Vec.Relation.Unary.Unique.Setoid.Properties where -open import Data.Fin.Base using (zero; suc) +open import Data.Fin.Base using (Fin; zero; suc) open import Data.Vec.Base as Vec open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_) import Data.Vec.Relation.Unary.All.Properties as Allₚ open import Data.Vec.Relation.Unary.AllPairs as AllPairs using (AllPairs) open import Data.Vec.Relation.Unary.Unique.Setoid import Data.Vec.Relation.Unary.AllPairs.Properties as AllPairsₚ -open import Data.Nat.Base +open import Data.Nat.Base using (ℕ; _+_) open import Function.Base using (_∘_; id) open import Level using (Level) open import Relation.Binary using (Rel; Setoid) @@ -33,8 +33,8 @@ private module _ (S : Setoid a ℓ₁) (R : Setoid b ℓ₂) where - open Setoid S renaming (Carrier to A; _≈_ to _≈₁_) - open Setoid R renaming (Carrier to B; _≈_ to _≈₂_) + open Setoid S renaming (_≈_ to _≈₁_) + open Setoid R renaming (_≈_ to _≈₂_) map⁺ : ∀ {f} → (∀ {x y} → f x ≈₂ f y → x ≈₁ y) → ∀ {n xs} → Unique S {n} xs → Unique R {n} (map f xs) @@ -58,8 +58,8 @@ module _ (S : Setoid a ℓ) where open Setoid S renaming (Carrier to A) - tabulate⁺ : ∀ {n} {f} → (∀ {i j} → f i ≈ f j → i ≡ j) → - Unique S (tabulate {n = n} f) + tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ {i j} → f i ≈ f j → i ≡ j) → + Unique S (tabulate f) tabulate⁺ f-inj = AllPairsₚ.tabulate⁺ (_∘ f-inj) ------------------------------------------------------------------------ @@ -67,7 +67,7 @@ module _ (S : Setoid a ℓ) where module _ (S : Setoid a ℓ) where - open Setoid S renaming (Carrier to A) + open Setoid S lookup-injective : ∀ {n xs} → Unique S {n} xs → ∀ i j → lookup xs i ≈ lookup xs j → i ≡ j lookup-injective (px ∷ pxs) zero zero eq = P.refl From 490223b307ec1a7dd414330b4865f40e9c88cd08 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 6 Oct 2022 14:19:38 +0100 Subject: [PATCH 45/48] restored line breaks --- src/Data/Vec/Relation/Unary/All/Properties.agda | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Data/Vec/Relation/Unary/All/Properties.agda b/src/Data/Vec/Relation/Unary/All/Properties.agda index 591beffde4..b25a860c68 100644 --- a/src/Data/Vec/Relation/Unary/All/Properties.agda +++ b/src/Data/Vec/Relation/Unary/All/Properties.agda @@ -133,11 +133,13 @@ module _ {_~_ : REL A B p} where module _ {P : A → Set p} where - tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ i → P (f i)) → All P (tabulate f) + tabulate⁺ : ∀ {n} {f : Fin n → A} → + (∀ i → P (f i)) → All P (tabulate f) tabulate⁺ {zero} Pf = [] tabulate⁺ {suc n} Pf = Pf zero ∷ tabulate⁺ (Pf ∘ suc) - tabulate⁻ : ∀ {n} {f : Fin n → A} → All P (tabulate f) → (∀ i → P (f i)) + tabulate⁻ : ∀ {n} {f : Fin n → A} → + All P (tabulate f) → (∀ i → P (f i)) tabulate⁻ (px ∷ _) zero = px tabulate⁻ (_ ∷ pf) (suc i) = tabulate⁻ pf i From 77edef78ea3a1cf6c9904baf32bc7b8a0cdc60c8 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 6 Oct 2022 14:20:31 +0100 Subject: [PATCH 46/48] restored line breaks --- src/Data/List/Relation/Unary/All/Properties.agda | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda index ee4b19ee9c..5b9cdb8871 100644 --- a/src/Data/List/Relation/Unary/All/Properties.agda +++ b/src/Data/List/Relation/Unary/All/Properties.agda @@ -551,11 +551,13 @@ applyDownFrom⁺₂ f n Pf = applyDownFrom⁺₁ f n (λ _ → Pf _) ------------------------------------------------------------------------ -- tabulate -tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ i → P (f i)) → All P (tabulate f) +tabulate⁺ : ∀ {n} {f : Fin n → A} → + (∀ i → P (f i)) → All P (tabulate f) tabulate⁺ {n = zero} Pf = [] tabulate⁺ {n = suc _} Pf = Pf zero ∷ tabulate⁺ (Pf ∘ suc) -tabulate⁻ : ∀ {n} {f : Fin n → A} → All P (tabulate f) → (∀ i → P (f i)) +tabulate⁻ : ∀ {n} {f : Fin n → A} → + All P (tabulate f) → (∀ i → P (f i)) tabulate⁻ (px ∷ _) zero = px tabulate⁻ (_ ∷ pf) (suc i) = tabulate⁻ pf i From 284a04e10d565cc9d1fffb56251299777b4ef838 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 6 Oct 2022 14:25:03 +0100 Subject: [PATCH 47/48] restored line breaks --- src/Data/Vec/Relation/Unary/Any/Properties.agda | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Data/Vec/Relation/Unary/Any/Properties.agda b/src/Data/Vec/Relation/Unary/Any/Properties.agda index 22d112674a..9faa49d464 100644 --- a/src/Data/Vec/Relation/Unary/Any/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Any/Properties.agda @@ -361,7 +361,8 @@ module _ {P : Pred A p} where tabulate⁺ zero p = here p tabulate⁺ (suc i) p = there (tabulate⁺ i p) - tabulate⁻ : ∀ {n} {f : Fin n → A} → Any P (tabulate f) → ∃ λ i → P (f i) + tabulate⁻ : ∀ {n} {f : Fin n → A} → + Any P (tabulate f) → ∃ λ i → P (f i) tabulate⁻ (here p) = zero , p tabulate⁻ (there p) = Prod.map suc id (tabulate⁻ p) From fa7aae04bbec1694ef5f1f2246ce1d724decdf08 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 6 Oct 2022 14:30:20 +0100 Subject: [PATCH 48/48] trimming --- src/Data/Vec/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index b645c21070..97d27767cb 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -528,8 +528,8 @@ lookup-cast₁ eq (_ ∷ xs) (suc i) = lookup-cast₂ : .(eq : m ≡ n) (xs : Vec A n) (i : Fin m) → lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i -lookup-cast₂ {n = suc _} eq (x ∷ _) zero = refl -lookup-cast₂ {n = suc _} eq (_ ∷ xs) (suc i) = +lookup-cast₂ eq (x ∷ _) zero = refl +lookup-cast₂ eq (_ ∷ xs) (suc i) = lookup-cast₂ (suc-injective eq) xs i lookup-concat : ∀ (xss : Vec (Vec A m) n) i j →