tightened the paramterisation of ↭-shift

src/Data/List/Relation/Binary/BagAndSetEquality.agda

@@ -537,21 +537,18 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
 
   lemma : ∀ {xs ys} (inv : x ∷ xs ∼[ bag ] x ∷ ys) {z} →
           Well-behaved (Inverse.to (∼→⊎↔⊎ inv {z}))
-  lemma {xs} inv {b = z∈xs} {a = p} {a′ = q} hyp₁ hyp₂ with
-    zero                                                                  ≡⟨⟩
-    index-of {xs = x ∷ xs} (here p)                                       ≡⟨⟩
-    index-of {xs = x ∷ xs} (to (∷↔ _) $ inj₁ p)                         ≡⟨ ≡.cong (index-of ∘ (to (∷↔ (_ ≡_)))) $ ≡.sym $
-                                                                               to-from (∼→⊎↔⊎ inv) {x = inj₁ p} hyp₂ ⟩
+  lemma {xs} inv {b = z∈xs} {a = p} {a′ = q} hyp₁ hyp₂ with begin
+    zero                                                              ≡⟨⟩
+    index-of {xs = x ∷ xs} (here p)                                   ≡⟨⟩
+    index-of {xs = x ∷ xs} (to (∷↔ _) $ inj₁ p)                       ≡⟨ ≡.cong (index-of ∘ (to (∷↔ (_ ≡_)))) $ ≡.sym $ to-from (∼→⊎↔⊎ inv) {x = inj₁ p} hyp₂ ⟩
     index-of {xs = x ∷ xs} (to (∷↔ _) $ (from (∼→⊎↔⊎ inv) $ inj₁ q))  ≡⟨ ≡.cong index-of $
                                                                                strictlyInverseˡ (∷↔ _) (from inv (here q)) ⟩
-    index-of {xs = x ∷ xs} (to (SK-sym inv) $ here q)                   ≡⟨ index-equality-preserved (SK-sym inv) refl ⟩
-    index-of {xs = x ∷ xs} (to (SK-sym inv) $ here p)                   ≡⟨ ≡.cong index-of $ ≡.sym $
-                                                                               strictlyInverseˡ (∷↔ _) (from inv (here p)) ⟩
-    index-of {xs = x ∷ xs} (to (∷↔ _) (from (∼→⊎↔⊎ inv) $ inj₁ p))  ≡⟨ ≡.cong (index-of ∘ (to (∷↔ (_ ≡_)))) $
-                                                                               to-from (∼→⊎↔⊎ inv) {x = inj₂ z∈xs} hyp₁ ⟩
-    index-of {xs = x ∷ xs} (to (∷↔ _) $ inj₂ z∈xs)                      ≡⟨⟩
-    index-of {xs = x ∷ xs} (there z∈xs)                                   ≡⟨⟩
-    suc (index-of {xs = xs} z∈xs)                                         ∎
+    index-of {xs = x ∷ xs} (to (SK-sym inv) $ here q)                 ≡⟨ index-equality-preserved (SK-sym inv) refl ⟩
+    index-of {xs = x ∷ xs} (to (SK-sym inv) $ here p)                 ≡⟨ ≡.cong index-of $ ≡.sym $ strictlyInverseˡ (∷↔ _) (from inv (here p)) ⟩
+    index-of {xs = x ∷ xs} (to (∷↔ _) (from (∼→⊎↔⊎ inv) $ inj₁ p))    ≡⟨ ≡.cong (index-of ∘ (to (∷↔ (_ ≡_)))) $ to-from (∼→⊎↔⊎ inv) {x = inj₂ z∈xs} hyp₁ ⟩
+    index-of {xs = x ∷ xs} (to (∷↔ _) $ inj₂ z∈xs)                    ≡⟨⟩
+    index-of {xs = x ∷ xs} (there z∈xs)                               ≡⟨⟩
+    suc (index-of {xs = xs} z∈xs)                                     ∎
     where
     open Inverse
     open ≡-Reasoning
@@ -591,7 +588,7 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
 ... | zs₁ , zs₂ , p rewrite p = begin
   x ∷ xs           <⟨ ∼bag⇒↭ (drop-cons (↔-trans eq (comm zs₁ (x ∷ zs₂)))) ⟩
   x ∷ (zs₂ ++ zs₁) <⟨ ++-comm zs₂ zs₁ ⟩
-  x ∷ (zs₁ ++ zs₂) ↭⟨ shift x zs₁ zs₂ ⟨
+  x ∷ (zs₁ ++ zs₂) ↭⟨ ↭-shift zs₁ zs₂ ⟨
   zs₁ ++ x ∷ zs₂   ∎
   where
   open CommutativeMonoid (commutativeMonoid bag A)

src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda

@@ -52,15 +52,9 @@ open ↭ public
 -- legacy variation in implicit/explicit parametrisation
   hiding (shift; map⁺)
 
-------------------------------------------------------------------------
--- Some useful lemmas
-
-shift : ∀ v (xs ys : List A) → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
-shift v = ↭-shift {v = v}
-
 {- not sure we need either of these for their proofs?
 ------------------------------------------------------------------------
--- Some other useful lemmas, optimised for the Propositional case
+-- Some useful lemmas, optimised for the Propositional case
 
 drop-mid-≡ : ∀ {x : A} ws xs {ys} {zs} →
              ws ++ [ x ] ++ ys ≡ xs ++ [ x ] ++ zs →
@@ -200,4 +194,12 @@ module _  {B : Set b} (f : A → B) where
 Please use ↭-[]-invʳ instead."
 #-}
 
+shift : ∀ v xs ys → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
+shift v xs ys = ↭-shift {v = v} xs {ys}
+{-# WARNING_ON_USAGE shift
+"Warning: shift was deprecated in v2.1.
+Please use ↭-shift instead. \\
+NB. Parametrisation has changed to make v and ys implicit."
+#-}
+
 

src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda

@@ -150,8 +150,8 @@ module _ (T : Setoid b r) where
 shift : v ≈ w → ∀ xs ys → xs ++ [ v ] ++ ys ↭ w ∷ xs ++ ys
 shift v≈w xs ys = Properties.shift ≈-refl ≈-sym ≈-trans v≈w xs {ys}
 
-↭-shift : ∀ xs ys → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
-↭-shift = shift ≈-refl
+↭-shift : ∀ xs {ys} → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
+↭-shift xs {ys} = shift ≈-refl xs ys
 
 ++⁺ˡ : ∀ xs {ys zs} → ys ↭ zs → xs ++ ys ↭ xs ++ zs
 ++⁺ˡ []       ys↭zs = ys↭zs
@@ -181,7 +181,7 @@ shift v≈w xs ys = Properties.shift ≈-refl ≈-sym ≈-trans v≈w xs {ys}
 ++-comm []       ys = ↭-sym (++-identityʳ ys)
 ++-comm (x ∷ xs) ys = begin
   x ∷ xs ++ ys   <⟨ ++-comm xs ys ⟩
-  x ∷ ys ++ xs   ↭⟨ ↭-shift ys xs ⟨
+  x ∷ ys ++ xs   ↭⟨ ↭-shift ys ⟨
   ys ++ (x ∷ xs) ∎
   where open PermutationReasoning
 
@@ -297,14 +297,14 @@ module _ (P? : Decidable P) where
   partition-↭ []       = ↭-refl
   partition-↭ (x ∷ xs) with does (P? x)
   ... | true  = ↭-prep x (partition-↭ xs)
-  ... | false = ↭-trans (↭-prep x (partition-↭ xs)) (↭-sym (↭-shift _ _))
+  ... | false = ↭-trans (↭-prep x (partition-↭ xs)) (↭-sym (↭-shift _))
 
 ------------------------------------------------------------------------
 -- _∷ʳ_
 
 ∷↭∷ʳ : ∀ x xs → x ∷ xs ↭ xs ∷ʳ x
 ∷↭∷ʳ x xs = ↭-sym (begin
-  xs ++ [ x ]   ↭⟨ ↭-shift xs [] ⟩
+  xs ++ [ x ]   ↭⟨ ↭-shift xs ⟩
   x ∷ xs ++ []  ≡⟨ List.++-identityʳ _ ⟩
   x ∷ xs        ∎)
   where open PermutationReasoning
@@ -314,7 +314,7 @@ module _ (P? : Decidable P) where
 
 ++↭ʳ++ : ∀ xs ys → xs ++ ys ↭ xs ʳ++ ys
 ++↭ʳ++ []       ys = ↭-refl
-++↭ʳ++ (x ∷ xs) ys = ↭-trans (↭-sym (↭-shift xs ys)) (++↭ʳ++ xs (x ∷ ys))
+++↭ʳ++ (x ∷ xs) ys = ↭-trans (↭-sym (↭-shift xs)) (++↭ʳ++ xs (x ∷ ys))
 
 ------------------------------------------------------------------------
 -- reverse
@@ -342,7 +342,7 @@ module _ (R? : B.Decidable R) where
   ... | true  | rec | _   = ↭-prep x rec
   ... | false | _   | rec = begin
     y ∷ merge R? x∷xs ys <⟨ rec ⟩
-    y ∷ x∷xs ++ ys       ↭⟨ ↭-shift x∷xs ys ⟨
+    y ∷ x∷xs ++ ys       ↭⟨ ↭-shift x∷xs ⟨
     x∷xs ++ y∷ys         ≡⟨ List.++-assoc [ x ] xs y∷ys ⟨
     x∷xs ++ y∷ys         ∎
     where open PermutationReasoning