Some preparatory proofs for proving sorting+permutation is equality #2724 (#2725)

* Some preparatory proofs for proving sorting+permutation is equality

* Minor tweaks

* Addressed feedback

* Fix bugs

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

Co-authored-by: jamesmckinna <[email protected]>

* Addressed James feedback

* fix: `2+` pattern plus `onIndices-lookup` in `CHANGELOG`

---------

Co-authored-by: jamesmckinna <[email protected]>
Co-authored-by: jamesmckinna <[email protected]>

Author: MatthewDaggitt

CHANGELOG.md

@@ -239,6 +239,23 @@ Additions to existing modules
   ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b
   ```
 
+* In `Data.Fin.Base`:
+  ```agda
+  _≰_ : Rel (Fin n) 0ℓ
+  _≮_ : Rel (Fin n) 0ℓ
+  ```
+
+* In `Data.Fin.Permutation`:
+  ```agda
+  cast-id : .(m ≡ n) → Permutation m n
+  swap : Permutation m n → Permutation (suc (suc m)) (suc (suc n))
+  ```
+
+* In `Data.Fin.Properties`:
+  ```agda
+  cast-involutive : .(eq₁ : m ≡ n) .(eq₂ : n ≡ m) → ∀ k → cast eq₁ (cast eq₂ k) ≡ k
+  ```
+
 * In `Data.Fin.Subset`:
   ```agda
   _⊇_ : Subset n → Subset n → Set
@@ -275,14 +292,31 @@ Additions to existing modules
   map-downFrom : ∀ (f : ℕ → A) n → map f (downFrom n) ≡ applyDownFrom f n
   ```
 
+* In `Data.List.Relation.Binary.Permutation.Homogeneous`:
+  ```agda
+  onIndices : Permutation R xs ys → Fin.Permutation (length xs) (length ys)
+  ```
+
 * In `Data.List.Relation.Binary.Permutation.Propositional`:
   ```agda
   ↭⇒↭ₛ′ : IsEquivalence _≈_ → _↭_ ⇒ _↭ₛ′_
   ```
 
+* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
+  ```agda
+  xs↭ys⇒|xs|≡|ys| : xs ↭ ys → length xs ≡ length ys
+  ¬x∷xs↭[] : ¬ (x ∷ xs ↭ [])
+  onIndices-lookup : ∀ i → lookup xs i ≈ lookup ys (Inverse.to (onIndices xs↭ys) i)
+  ```
+
 * In `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
   ```agda
   filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
+        ```
+
+* In `Data.List.Relation.Binary.Pointwise.Properties`:
+  ```agda
+  lookup-cast : Pointwise R xs ys → .(∣xs∣≡∣ys∣ : length xs ≡ length ys) → ∀ i → R (lookup xs i) (lookup ys (cast ∣xs∣≡∣ys∣ i))
   ```
 
 * In `Data.List.NonEmpty.Properties`:

src/Data/Fin/Base.agda

@@ -19,7 +19,7 @@ open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
 open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
-open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 
 private
   variable
@@ -271,7 +271,7 @@ pinch {suc n} (suc i) (suc j) = suc (pinch i j)
 ------------------------------------------------------------------------
 -- Order relations
 
-infix 4 _≤_ _≥_ _<_ _>_
+infix 4 _≤_ _≥_ _<_ _>_ _≰_ _≮_
 
 _≤_ : IRel Fin 0ℓ
 i ≤ j = toℕ i ℕ.≤ toℕ j
@@ -285,6 +285,11 @@ i < j = toℕ i ℕ.< toℕ j
 _>_ : IRel Fin 0ℓ
 i > j = toℕ i ℕ.> toℕ j
 
+_≰_ : ∀ {n} → Rel (Fin n) 0ℓ
+i ≰ j = ¬ (i ≤ j)
+
+_≮_ : ∀ {n} → Rel (Fin n) 0ℓ
+i ≮ j = ¬ (i < j)
 
 ------------------------------------------------------------------------
 -- An ordering view.

src/Data/Fin/Permutation.agda

@@ -9,10 +9,10 @@
 module Data.Fin.Permutation where
 
 open import Data.Bool.Base using (true; false)
-open import Data.Fin.Base using (Fin; suc; opposite; punchIn; punchOut)
-open import Data.Fin.Patterns using (0F)
+open import Data.Fin.Base using (Fin; suc; cast; opposite; punchIn; punchOut)
+open import Data.Fin.Patterns using (0F; 1F)
 open import Data.Fin.Properties using (punchInᵢ≢i; punchOut-punchIn;
-  punchOut-cong; punchOut-cong′; punchIn-punchOut; _≟_; ¬Fin0)
+  punchOut-cong; punchOut-cong′; punchIn-punchOut; _≟_; ¬Fin0; cast-involutive)
 import Data.Fin.Permutation.Components as PC
 open import Data.Nat.Base using (ℕ; suc; zero)
 open import Data.Product.Base using (_,_; proj₂)
@@ -22,7 +22,7 @@ open import Function.Construct.Identity using (↔-id)
 open import Function.Construct.Symmetry using (↔-sym)
 open import Function.Definitions using (StrictlyInverseˡ; StrictlyInverseʳ)
 open import Function.Properties.Inverse using (↔⇒↣)
-open import Function.Base using (_∘_)
+open import Function.Base using (_∘_; _∘′_)
 open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary using (does; ¬_; yes; no)
@@ -57,11 +57,15 @@ Permutation′ n = Permutation n n
 ------------------------------------------------------------------------
 -- Helper functions
 
-permutation : ∀ (f : Fin m → Fin n) (g : Fin n → Fin m) →
-              StrictlyInverseˡ _≡_ f g → StrictlyInverseʳ _≡_ f g → Permutation m n
+permutation : ∀ (f : Fin m → Fin n)
+              (g : Fin n → Fin m) →
+              StrictlyInverseˡ _≡_ f g →
+              StrictlyInverseʳ _≡_ f g →
+              Permutation m n
 permutation = mk↔ₛ′
 
 infixl 5 _⟨$⟩ʳ_ _⟨$⟩ˡ_
+
 _⟨$⟩ʳ_ : Permutation m n → Fin m → Fin n
 _⟨$⟩ʳ_ = Inverse.to
 
@@ -75,44 +79,61 @@ inverseʳ : ∀ (π : Permutation m n) {i} → π ⟨$⟩ʳ (π ⟨$⟩ˡ i) ≡
 inverseʳ π = Inverse.inverseˡ π refl
 
 ------------------------------------------------------------------------
--- Equality
+-- Equality over permutations
 
 infix 6 _≈_
+
 _≈_ : Rel (Permutation m n) 0ℓ
 π ≈ ρ = ∀ i → π ⟨$⟩ʳ i ≡ ρ ⟨$⟩ʳ i
 
 ------------------------------------------------------------------------
--- Example permutations
+-- Permutation properties
 
--- Identity
-
-id : Permutation′ n
+id : Permutation n n
 id = ↔-id _
 
--- Transpose two indices
-
-transpose : Fin n → Fin n → Permutation′ n
-transpose i j = permutation (PC.transpose i j) (PC.transpose j i) (λ _ → PC.transpose-inverse _ _) (λ _ → PC.transpose-inverse _ _)
+flip : Permutation m n → Permutation n m
+flip = ↔-sym
 
--- Reverse the order of indices
+infixr 9 _∘ₚ_
 
-reverse : Permutation′ n
-reverse = permutation opposite opposite PC.reverse-involutive PC.reverse-involutive
+_∘ₚ_ : Permutation m n → Permutation n o → Permutation m o
+π₁ ∘ₚ π₂ = π₂ ↔-∘ π₁
 
 ------------------------------------------------------------------------
--- Operations
+-- Non-trivial identity
 
--- Composition
+cast-id : .(m ≡ n) → Permutation m n
+cast-id m≡n = permutation
+  (cast m≡n)
+  (cast (sym m≡n))
+  (cast-involutive m≡n (sym m≡n))
+  (cast-involutive (sym m≡n) m≡n)
 
-infixr 9 _∘ₚ_
-_∘ₚ_ : Permutation m n → Permutation n o → Permutation m o
-π₁ ∘ₚ π₂ = π₂ ↔-∘ π₁
+------------------------------------------------------------------------
+-- Transposition
 
--- Flip
+-- Transposes two elements in the permutation, keeping the remainder
+-- of the permutation the same
+transpose : Fin n → Fin n → Permutation n n
+transpose i j = permutation
+  (PC.transpose i j)
+  (PC.transpose j i)
+  (λ _ → PC.transpose-inverse _ _)
+  (λ _ → PC.transpose-inverse _ _)
 
-flip : Permutation m n → Permutation n m
-flip = ↔-sym
+------------------------------------------------------------------------
+-- Reverse
 
+-- Reverses a permutation
+reverse : Permutation n n
+reverse = permutation
+  opposite
+  opposite
+  PC.reverse-involutive
+  PC.reverse-involutive
+
+------------------------------------------------------------------------
 -- Element removal
 --
 -- `remove k [0 ↦ i₀, …, k ↦ iₖ, …, n ↦ iₙ]` yields
@@ -159,8 +180,14 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′
     punchOut {i = πʳ i} {punchIn (πʳ i) j}                         _  ≡⟨ punchOut-punchIn (πʳ i) ⟩
     j                                                                 ∎
 
--- lift: takes a permutation m → n and creates a permutation (suc m) → (suc n)
+------------------------------------------------------------------------
+-- Lifting
+
+-- Takes a permutation m → n and creates a permutation (suc m) → (suc n)
 -- by mapping 0 to 0 and applying the input permutation to everything else
+--
+-- Note: should be refactored as a special-case when we add the
+-- concatenation of two permutations
 lift₀ : Permutation m n → Permutation (suc m) (suc n)
 lift₀ {m} {n} π = permutation to from inverseˡ′ inverseʳ′
   where
@@ -180,6 +207,9 @@ lift₀ {m} {n} π = permutation to from inverseˡ′ inverseʳ′
   inverseˡ′ 0F      = refl
   inverseˡ′ (suc j) = cong suc (inverseʳ π)
 
+------------------------------------------------------------------------
+-- Insertion
+
 -- insert i j π is the permutation that maps i to j and otherwise looks like π
 -- it's roughly an inverse of remove
 insert : ∀ {m n} → Fin (suc m) → Fin (suc n) → Permutation m n → Permutation (suc m) (suc n)
@@ -221,6 +251,18 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
     punchIn j (punchOut j≢k)                                               ≡⟨ punchIn-punchOut j≢k ⟩
     k                                                                      ∎
 
+------------------------------------------------------------------------
+-- Swapping
+
+-- Takes a permutation m → n and creates a permutation
+-- suc (suc m) → suc (suc n) by mapping 0 to 1 and 1 to 0 and
+-- then applying the input permutation to everything else
+--
+-- Note: should be refactored as a special-case when we add the
+-- concatenation of two permutations
+swap : Permutation m n → Permutation (suc (suc m)) (suc (suc n))
+swap π = transpose 0F 1F ∘ₚ lift₀ (lift₀ π)
+
 ------------------------------------------------------------------------
 -- Other properties
 

src/Data/Fin/Properties.agda

@@ -279,6 +279,10 @@ cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ zero = refl
 cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (suc k) =
   cong suc (cast-trans (ℕ.suc-injective eq₁) (ℕ.suc-injective eq₂) k)
 
+cast-involutive : .(eq₁ : m ≡ n) .(eq₂ : n ≡ m) →
+                  ∀ k → cast eq₁ (cast eq₂ k) ≡ k
+cast-involutive eq₁ eq₂ k = trans (cast-trans eq₂ eq₁ k) (cast-is-id refl k)
+
 ------------------------------------------------------------------------
 -- Properties of _≤_
 ------------------------------------------------------------------------

src/Data/List/Relation/Binary/Permutation/Homogeneous.agda

@@ -8,12 +8,15 @@
 
 module Data.List.Relation.Binary.Permutation.Homogeneous where
 
-open import Data.List.Base using (List; _∷_)
+open import Data.List.Base using (List; _∷_; length)
 open import Data.List.Relation.Binary.Pointwise.Base as Pointwise
   using (Pointwise)
 import Data.List.Relation.Binary.Pointwise.Properties as Pointwise
 open import Data.Nat.Base using (ℕ; suc; _+_)
+open import Data.Fin.Base using (Fin; zero; suc; cast)
+import Data.Fin.Permutation as Fin
 open import Level using (Level; _⊔_)
+open import Function.Base using (_∘_)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Structures using (IsEquivalence)
@@ -23,6 +26,7 @@ private
   variable
     a r s : Level
     A : Set a
+    R S : Rel A r
 
 data Permutation {A : Set a} (R : Rel A r) : Rel (List A) (a ⊔ r) where
   refl  : ∀ {xs ys} → Pointwise R xs ys → Permutation R xs ys
@@ -33,37 +37,39 @@ data Permutation {A : Set a} (R : Rel A r) : Rel (List A) (a ⊔ r) where
 ------------------------------------------------------------------------
 -- The Permutation relation is an equivalence
 
-module _ {R : Rel A r}  where
+sym : Symmetric R → Symmetric (Permutation R)
+sym R-sym (refl xs∼ys)           = refl (Pointwise.symmetric R-sym xs∼ys)
+sym R-sym (prep x∼x′ xs↭ys)      = prep (R-sym x∼x′) (sym R-sym xs↭ys)
+sym R-sym (swap x∼x′ y∼y′ xs↭ys) = swap (R-sym y∼y′) (R-sym x∼x′) (sym R-sym xs↭ys)
+sym R-sym (trans xs↭ys ys↭zs)    = trans (sym R-sym ys↭zs) (sym R-sym xs↭ys)
 
-  sym : Symmetric R → Symmetric (Permutation R)
-  sym R-sym (refl xs∼ys)           = refl (Pointwise.symmetric R-sym xs∼ys)
-  sym R-sym (prep x∼x′ xs↭ys)      = prep (R-sym x∼x′) (sym R-sym xs↭ys)
-  sym R-sym (swap x∼x′ y∼y′ xs↭ys) = swap (R-sym y∼y′) (R-sym x∼x′) (sym R-sym xs↭ys)
-  sym R-sym (trans xs↭ys ys↭zs)    = trans (sym R-sym ys↭zs) (sym R-sym xs↭ys)
+isEquivalence : Reflexive R → Symmetric R → IsEquivalence (Permutation R)
+isEquivalence R-refl R-sym = record
+  { refl  = refl (Pointwise.refl R-refl)
+  ; sym   = sym R-sym
+  ; trans = trans
+  }
 
-  isEquivalence : Reflexive R → Symmetric R → IsEquivalence (Permutation R)
-  isEquivalence R-refl R-sym = record
-    { refl  = refl (Pointwise.refl R-refl)
-    ; sym   = sym R-sym
-    ; trans = trans
-    }
+setoid : Reflexive R → Symmetric R → Setoid _ _
+setoid {R = R} R-refl R-sym = record
+  { isEquivalence = isEquivalence {R = R} R-refl R-sym
+  }
 
-  setoid : Reflexive R → Symmetric R → Setoid _ _
-  setoid R-refl R-sym = record
-    { isEquivalence = isEquivalence R-refl R-sym
-    }
-
-map : ∀ {R : Rel A r} {S : Rel A s} →
-      (R ⇒ S) → (Permutation R ⇒ Permutation S)
+map : (R ⇒ S) → (Permutation R ⇒ Permutation S)
 map R⇒S (refl xs∼ys)         = refl (Pointwise.map R⇒S xs∼ys)
 map R⇒S (prep e xs∼ys)       = prep (R⇒S e) (map R⇒S xs∼ys)
 map R⇒S (swap e₁ e₂ xs∼ys)   = swap (R⇒S e₁) (R⇒S e₂) (map R⇒S xs∼ys)
 map R⇒S (trans xs∼ys ys∼zs)  = trans (map R⇒S xs∼ys) (map R⇒S ys∼zs)
 
 -- Measures the number of constructors, can be useful for termination proofs
-
-steps : ∀ {R : Rel A r} {xs ys} → Permutation R xs ys → ℕ
+steps : ∀ {xs ys} → Permutation R xs ys → ℕ
 steps (refl _)            = 1
 steps (prep _ xs↭ys)      = suc (steps xs↭ys)
 steps (swap _ _ xs↭ys)    = suc (steps xs↭ys)
 steps (trans xs↭ys ys↭zs) = steps xs↭ys + steps ys↭zs
+
+onIndices : ∀ {xs ys} → Permutation R xs ys → Fin.Permutation (length xs) (length ys)
+onIndices (refl ≋)          = Fin.cast-id (Pointwise.Pointwise-length ≋)
+onIndices (prep e xs↭ys)   = Fin.lift₀ (onIndices xs↭ys)
+onIndices (swap e f xs↭ys) = Fin.swap (onIndices xs↭ys)
+onIndices (trans ↭₁ ↭₂)   = onIndices ↭₁ Fin.∘ₚ onIndices ↭₂

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

@@ -31,7 +31,7 @@ open ≋ S using (_≋_; _∷_; ≋-refl; ≋-sym; ≋-trans)
 -- Definition, based on `Homogeneous`
 
 open Homogeneous public
-  using (refl; prep; swap; trans)
+  using (refl; prep; swap; trans; onIndices)
 
 infix 3 _↭_