From 4ffc3b6e51d76af3e0d77b934cd1cea4e486264e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 26 Sep 2024 06:50:32 +0100 Subject: [PATCH 1/2] [DRY] refactoring --- CHANGELOG.md | 7 +++- .../Membership/Propositional/Properties.agda | 36 +++++++++++-------- 2 files changed, 28 insertions(+), 15 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a513e4978f..4ffd060929 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -59,6 +59,11 @@ Deprecated names normalise-correct ↦ Algebra.Solver.Monoid.Normal.correct ``` +* In `Data.List.Membership.Propositional.Properties`: + ```agda + map∷-decomp ↦ map∷⁻ + ``` + * In `Data.Vec.Properties`: ```agda ++-assoc _ ↦ ++-assoc-eqFree @@ -146,8 +151,8 @@ Additions to existing modules ∈-concatMap⁻ : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs ++-∈⇔ : v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys) []∉map∷ : [] ∉ map (x ∷_) xss + map∷⁻ : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × xs ≡ y ∷ ys map∷-decomp∈ : (x ∷ xs) ∈ map (y ∷_) xss → x ≡ y × xs ∈ xss - map∷-decomp : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × y ∷ ys ≡ xs ∈-map∷⁻ : xs ∈ map (x ∷_) xss → x ∈ xs ∉[] : x ∉ [] deduplicate-∈⇔ : z ∈ xs ⇔ z ∈ deduplicate _≈?_ xs diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda index 39204f19e2..6740b561ce 100644 --- a/src/Data/List/Membership/Propositional/Properties.agda +++ b/src/Data/List/Membership/Propositional/Properties.agda @@ -454,22 +454,30 @@ module _ {R : A → A → Set ℓ} where ------------------------------------------------------------------------ -- nested lists +map∷⁻ : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × xs ≡ y ∷ ys +map∷⁻ = ∈-map⁻ (_ ∷_) + []∉map∷ : (List A ∋ []) ∉ map (x ∷_) xss -[]∉map∷ {xss = _ ∷ _} (there p) = []∉map∷ p +[]∉map∷ p with () ← map∷⁻ p map∷-decomp∈ : (List A ∋ x ∷ xs) ∈ map (y ∷_) xss → x ≡ y × xs ∈ xss -map∷-decomp∈ {xss = _ ∷ _} = λ where - (here refl) → refl , here refl - (there p) → map₂ there $ map∷-decomp∈ p - -map∷-decomp : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × y ∷ ys ≡ xs -map∷-decomp {xss = _ ∷ _} (here refl) = -, here refl , refl -map∷-decomp {xs = []} {xss = _ ∷ _} (there xs∈) = contradiction xs∈ []∉map∷ -map∷-decomp {xs = x ∷ xs} {xss = _ ∷ _} (there xs∈) = - let eq , p = map∷-decomp∈ xs∈ - in -, there p , cong (_∷ _) (sym eq) +map∷-decomp∈ p with _ , xs∈xss , refl ← map∷⁻ p = refl , xs∈xss ∈-map∷⁻ : xs ∈ map (x ∷_) xss → x ∈ xs -∈-map∷⁻ {xss = _ ∷ _} = λ where - (here refl) → here refl - (there p) → ∈-map∷⁻ p +∈-map∷⁻ p with _ , _ , refl ← map∷⁻ p = here refl + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.2 + +map∷-decomp : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × y ∷ ys ≡ xs +map∷-decomp p = let ys , ys∈xss , eq = map∷⁻ p in ys , ys∈xss , sym eq +{-# WARNING_ON_USAGE map∷-decomp +"Warning: map∷-decomp was deprecated in v2.2. +Please use map∷⁻ instead." +#-} From 254f9fd30775dab0fdf70621dbed96613afae85d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 26 Sep 2024 12:04:09 +0100 Subject: [PATCH 2/2] remove deprecations; leave lemma renamed --- CHANGELOG.md | 5 ----- .../Membership/Propositional/Properties.agda | 16 ---------------- 2 files changed, 21 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4ffd060929..12aaa4bd44 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -59,11 +59,6 @@ Deprecated names normalise-correct ↦ Algebra.Solver.Monoid.Normal.correct ``` -* In `Data.List.Membership.Propositional.Properties`: - ```agda - map∷-decomp ↦ map∷⁻ - ``` - * In `Data.Vec.Properties`: ```agda ++-assoc _ ↦ ++-assoc-eqFree diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda index 6740b561ce..d0072290fa 100644 --- a/src/Data/List/Membership/Propositional/Properties.agda +++ b/src/Data/List/Membership/Propositional/Properties.agda @@ -465,19 +465,3 @@ map∷-decomp∈ p with _ , xs∈xss , refl ← map∷⁻ p = refl , xs∈xss ∈-map∷⁻ : xs ∈ map (x ∷_) xss → x ∈ xs ∈-map∷⁻ p with _ , _ , refl ← map∷⁻ p = here refl - - ------------------------------------------------------------------------- --- DEPRECATED NAMES ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- Version 2.2 - -map∷-decomp : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × y ∷ ys ≡ xs -map∷-decomp p = let ys , ys∈xss , eq = map∷⁻ p in ys , ys∈xss , sym eq -{-# WARNING_ON_USAGE map∷-decomp -"Warning: map∷-decomp was deprecated in v2.2. -Please use map∷⁻ instead." -#-}