Proved sorted permutations are equal (#2748)

* Proved sorted permutations are equal

* Addressed James' and Jacques' feedback

* Minor tweaks

Author: MatthewDaggitt

CHANGELOG.md

@@ -257,17 +257,22 @@ Additions to existing modules
   ```agda
   _≰_ : Rel (Fin n) 0ℓ
   _≮_ : Rel (Fin n) 0ℓ
+  lower : ∀ (i : Fin m) → .(toℕ i ℕ.< n) → Fin n
   ```
 
 * In `Data.Fin.Permutation`:
   ```agda
   cast-id : .(m ≡ n) → Permutation m n
-  swap : Permutation m n → Permutation (suc (suc m)) (suc (suc n))
+  swap : Permutation m n → Permutation (2+ m) (2+ n)
   ```
 
 * In `Data.Fin.Properties`:
   ```agda
-  cast-involutive : .(eq₁ : m ≡ n) .(eq₂ : n ≡ m) → ∀ k → cast eq₁ (cast eq₂ k) ≡ k
+  cast-involutive       : .(eq₁ : m ≡ n) .(eq₂ : n ≡ m) → ∀ k → cast eq₁ (cast eq₂ k) ≡ k
+  inject!-injective     : Injective _≡_ _≡_ inject!
+  inject!-<             : (k : Fin′ i) → inject! k < i
+  lower-injective       : lower i i<n ≡ lower j j<n → i ≡ j
+  injective⇒existsPivot : ∀ (f : Fin n → Fin m) → Injective _≡_ _≡_ f → ∀ (i : Fin n) → ∃ λ j → j ≤ i × i ≤ f j
   ```
 
 * In `Data.Fin.Subset`:
@@ -452,6 +457,11 @@ Additions to existing modules
   map⁻ : AllPairs R (map f xs) → AllPairs (R on f) xs
   ```
 
+* In `Data.List.Relation.Unary.Linked`:
+  ```agda
+  lookup : Transitive R → Linked R xs → Connected R (just x) (head xs) → ∀ i → R x (List.lookup xs i)
+  ```
+
 * In `Data.List.Relation.Unary.Unique.Setoid.Properties`:
   ```agda
   map⁻ : Congruent _≈₁_ _≈₂_ f → Unique R (map f xs) → Unique S xs
@@ -461,3 +471,14 @@ Additions to existing modules
   ```agda
   map⁻ : Unique (map f xs) → Unique xs
   ```
+
+* In `Data.List.Relation.Unary.Sorted.TotalOrder.Properties`:
+  ```agda
+  lookup-mono-≤ : Sorted xs → i Fin.≤ j → lookup xs i ≤ lookup xs j
+  ↗↭↗⇒≋         : Sorted xs → Sorted ys → xs ↭ ys → xs ≋ ys
+  ```
+
+* In `Data.List.Sort.Base`:
+  ```agda
+  SortingAlgorithm.sort-↭ₛ : ∀ xs → sort xs Setoid.↭ xs
+  ```

src/Data/Fin/Base.agda

@@ -121,6 +121,10 @@ lower₁ {zero}  zero    ne = contradiction refl ne
 lower₁ {suc n} zero    _  = zero
 lower₁ {suc n} (suc i) ne = suc (lower₁ i (ne ∘ cong suc))
 
+lower : ∀ (i : Fin m) → .(toℕ i ℕ.< n) → Fin n
+lower {n = suc n} zero    leq = zero
+lower {n = suc n} (suc i) leq = suc (lower i (ℕ.s≤s⁻¹ leq))
+
 -- A strengthening injection into the minimal Fin fibre.
 strengthen : ∀ (i : Fin n) → Fin′ (suc i)
 strengthen zero    = zero

src/Data/Fin/Permutation.agda

@@ -15,7 +15,7 @@ open import Data.Fin.Properties using (punchInᵢ≢i; punchOut-punchIn;
   punchOut-cong; punchOut-cong′; punchIn-punchOut
   ; _≟_; ¬Fin0; cast-involutive; opposite-involutive)
 import Data.Fin.Permutation.Components as PC
-open import Data.Nat.Base using (ℕ; suc; zero)
+open import Data.Nat.Base using (ℕ; suc; zero; 2+)
 open import Data.Product.Base using (_,_; proj₂)
 open import Function.Bundles using (_↔_; Injection; Inverse; mk↔ₛ′)
 open import Function.Construct.Composition using (_↔-∘_)
@@ -261,7 +261,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
 --
 -- 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 : Permutation m n → Permutation (2+ m) (2+ n)
 swap π = transpose 0F 1F ∘ₚ lift₀ (lift₀ π)
 
 ------------------------------------------------------------------------

src/Data/Fin/Properties.agda

@@ -489,6 +489,19 @@ i≤inject₁[j]⇒i≤1+j : i ≤ inject₁ j → i ≤ suc j
 i≤inject₁[j]⇒i≤1+j {i = zero}              _   = z≤n
 i≤inject₁[j]⇒i≤1+j {i = suc i} {j = suc j} i≤j = s≤s (ℕ.m≤n⇒m≤1+n (subst (toℕ i ℕ.≤_) (toℕ-inject₁ j) (ℕ.s≤s⁻¹ i≤j)))
 
+------------------------------------------------------------------------
+-- inject!
+------------------------------------------------------------------------
+
+inject!-injective : ∀ {i : Fin (suc n)} → Injective _≡_ _≡_ (inject! {i = i})
+inject!-injective {n = suc n} {i = suc i} {0F}    {0F}    refl = refl
+inject!-injective {n = suc n} {i = suc i} {suc x} {suc y} eq =
+  cong suc (inject!-injective (suc-injective eq))
+
+inject!-< : ∀ {i : Fin (suc n)} (k : Fin′ i) → inject! k < i
+inject!-< {suc n} {suc i} 0F      = s≤s z≤n
+inject!-< {suc n} {suc i} (suc k) = s≤s (inject!-< k)
+
 ------------------------------------------------------------------------
 -- lower₁
 ------------------------------------------------------------------------
@@ -537,6 +550,17 @@ 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))
 
+------------------------------------------------------------------------
+-- lower
+------------------------------------------------------------------------
+
+lower-injective : ∀ (i j : Fin m)
+                  .{i<n : toℕ i ℕ.< n} .{j<n : toℕ j ℕ.< n}  →
+                  lower i i<n ≡ lower j j<n → i ≡ j
+lower-injective {n = suc n} zero    zero    eq = refl
+lower-injective {n = suc n} (suc i) (suc j) eq =
+  cong suc (lower-injective i j (suc-injective eq))
+
 ------------------------------------------------------------------------
 -- inject≤
 ------------------------------------------------------------------------
@@ -1038,6 +1062,24 @@ cantor-schröder-bernstein : ∀ {f : Fin m → Fin n} {g : Fin n → Fin m} →
 cantor-schröder-bernstein f-inj g-inj = ℕ.≤-antisym
   (injective⇒≤ f-inj) (injective⇒≤ g-inj)
 
+injective⇒existsPivot : ∀ {f : Fin n → Fin m} → Injective _≡_ _≡_ f →
+                        ∀ (i : Fin n) → ∃ λ j → j ≤ i × i ≤ f j
+injective⇒existsPivot {f = f} f-injective i
+  with any? (λ j → j ≤? i ×-dec i ≤? f j)
+... | yes result = result
+... | no ¬result = contradiction (injective⇒≤ f∘inject!-injective) ℕ.1+n≰n
+  where
+  fj<i : (j : Fin′ (suc i)) → f (inject! j) < i
+  fj<i j with f (inject! j) <? i
+  ... | yes fj<i = fj<i
+  ... | no  fj≮i = contradiction (_  , ℕ.s≤s⁻¹ (inject!-< j) , ℕ.≮⇒≥ fj≮i) ¬result
+
+  f∘inject! : Fin′ (suc i) → Fin′ i
+  f∘inject! j = lower (f (inject! j)) (fj<i j)
+
+  f∘inject!-injective : Injective _≡_ _≡_ f∘inject!
+  f∘inject!-injective = inject!-injective ∘ f-injective ∘ lower-injective _ _
+
 ------------------------------------------------------------------------
 -- Effectful
 ------------------------------------------------------------------------

src/Data/List/Relation/Unary/Linked.agda

@@ -11,6 +11,7 @@ module Data.List.Relation.Unary.Linked {a} {A : Set a} where
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.Product.Base as Prod using (_,_; _×_; uncurry; <_,_>)
+open import Data.Fin.Base using (zero; suc)
 open import Data.Maybe.Base using (just)
 open import Data.Maybe.Relation.Binary.Connected
   using (Connected; just; just-nothing)
@@ -26,6 +27,7 @@ open import Relation.Nullary.Decidable using (yes; no; map′; _×-dec_)
 private
   variable
     p q r ℓ : Level
+    R : Rel A ℓ
 
 ------------------------------------------------------------------------
 -- Definition
@@ -92,6 +94,14 @@ module _ {P : Rel A p} {Q : Rel A q} where
   unzip : Linked (P ∩ᵇ Q) ⊆ Linked P ∩ᵘ Linked Q
   unzip = unzipWith id
 
+lookup : ∀ {x xs} → Transitive R → Linked R xs →
+         Connected R (just x) (List.head xs) →
+         ∀ i → R x (List.lookup xs i)
+lookup trans [-]       (just Rvx) zero    = Rvx
+lookup trans (x ∷ xs↗) (just Rvx) zero    = Rvx
+lookup trans (x ∷ xs↗) (just Rvx) (suc i) =
+  lookup trans xs↗ (just (trans Rvx x)) i
+
 ------------------------------------------------------------------------
 -- Properties of predicates preserved by Linked
 

src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda

@@ -14,20 +14,34 @@ open import Data.List.Relation.Unary.AllPairs using (AllPairs)
 open import Data.List.Relation.Unary.Linked as Linked
   using (Linked; []; [-]; _∷_; _∷′_; head′; tail)
 import Data.List.Relation.Unary.Linked.Properties as Linked
+import Data.List.Relation.Binary.Equality.Setoid as Equality
 import Data.List.Relation.Binary.Sublist.Setoid as Sublist
 import Data.List.Relation.Binary.Sublist.Setoid.Properties as SublistProperties
-open import Data.List.Relation.Unary.Sorted.TotalOrder hiding (head)
-
+import Data.List.Relation.Binary.Permutation.Setoid as Permutation
+import Data.List.Relation.Binary.Permutation.Setoid.Properties as PermutationProperties
+import Data.List.Relation.Binary.Pointwise as Pointwise
+open import Data.List.Relation.Unary.Sorted.TotalOrder as Sorted hiding (head)
+
+open import Data.Fin.Base as Fin hiding (_<_; _≤_)
+import Data.Fin.Properties as Fin
+open import Data.Fin.Permutation
+open import Data.Product using (_,_)
 open import Data.Maybe.Base using (just; nothing)
 open import Data.Maybe.Relation.Binary.Connected using (Connected; just)
-open import Data.Nat.Base using (ℕ; zero; suc; _<_)
-
+open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s; zero; suc)
+import Data.Nat.Properties as ℕ
+open import Function.Base using (_∘_; const)
+open import Function.Bundles using (Inverse)
+open import Function.Consequences.Propositional using (inverseʳ⇒injective)
 open import Level using (Level)
-open import Relation.Binary.Core using (_Preserves_⟶_)
+open import Relation.Binary.Core using (_Preserves_⟶_; Rel)
 open import Relation.Binary.Bundles using (TotalOrder; DecTotalOrder; Preorder)
 import Relation.Binary.Properties.TotalOrder as TotalOrderProperties
+import Relation.Binary.Reasoning.PartialOrder as PosetReasoning
 open import Relation.Unary using (Pred; Decidable)
+open import Relation.Nullary using (contradiction)
 open import Relation.Nullary.Decidable using (yes; no)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 
 private
   variable
@@ -80,7 +94,7 @@ module _ (O : TotalOrder a ℓ₁ ℓ₂) where
 module _ (O : TotalOrder a ℓ₁ ℓ₂) where
   open TotalOrder O
 
-  applyUpTo⁺₁ : ∀ f n → (∀ {i} → suc i < n → f i ≤ f (suc i)) →
+  applyUpTo⁺₁ : ∀ f n → (∀ {i} → suc i ℕ.< n → f i ≤ f (suc i)) →
                 Sorted O (applyUpTo f n)
   applyUpTo⁺₁ = Linked.applyUpTo⁺₁
 
@@ -94,7 +108,7 @@ module _ (O : TotalOrder a ℓ₁ ℓ₂) where
 module _ (O : TotalOrder a ℓ₁ ℓ₂) where
   open TotalOrder O
 
-  applyDownFrom⁺₁ : ∀ f n → (∀ {i} → suc i < n → f (suc i) ≤ f i) →
+  applyDownFrom⁺₁ : ∀ f n → (∀ {i} → suc i ℕ.< n → f (suc i) ≤ f i) →
                     Sorted O (applyDownFrom f n)
   applyDownFrom⁺₁ = Linked.applyDownFrom⁺₁
 
@@ -150,3 +164,48 @@ module _ (O : TotalOrder a ℓ₁ ℓ₂) {P : Pred _ p} (P? : Decidable P) wher
 
   filter⁺ : ∀ {xs} → Sorted O xs → Sorted O (filter P? xs)
   filter⁺ = Linked.filter⁺ P? trans
+
+------------------------------------------------------------------------
+-- lookup
+
+module _ (O : TotalOrder a ℓ₁ ℓ₂) where
+  open TotalOrder O
+
+  lookup-mono-≤ : ∀ {xs} → Sorted O xs →
+                  ∀ {i j} → i Fin.≤ j → lookup xs i ≤ lookup xs j
+  lookup-mono-≤ {x ∷ xs} xs↗ {zero}  {zero}  z≤n       = refl
+  lookup-mono-≤ {x ∷ xs} xs↗ {zero}  {suc j} z≤n       = Linked.lookup trans xs↗ (just refl) (suc j)
+  lookup-mono-≤ {x ∷ xs} xs↗ {suc i} {suc j} (s≤s i≤j) = lookup-mono-≤ (Sorted.tail O {y = x} xs↗) i≤j
+
+------------------------------------------------------------------------
+-- Relationship to binary relations
+------------------------------------------------------------------------
+
+module _ (O : TotalOrder a ℓ₁ ℓ₂) where
+  open TotalOrder O
+  open Equality Eq.setoid
+  open Permutation Eq.setoid hiding (refl; trans)
+  open PermutationProperties Eq.setoid
+  open PosetReasoning poset
+
+  -- Proof that any two sorted lists that are a permutation of each
+  -- other are pointwise equal
+  ↗↭↗⇒≋ : ∀ {xs ys} → Sorted O xs → Sorted O ys → xs ↭ ys → xs ≋ ys
+  ↗↭↗⇒≋ {xs} {ys} xs↗ ys↗ xs↭ys = Pointwise.lookup⁻
+    (xs↭ys⇒|xs|≡|ys| xs↭ys)
+    (λ i≡j → antisym
+      (↗↭↗⇒≤ (↭-sym xs↭ys) ys↗ xs↗ (≡.sym i≡j))
+      (↗↭↗⇒≤ xs↭ys  xs↗ ys↗ i≡j))
+    where
+    ↗↭↗⇒≤ : ∀ {xs ys}
+              (xs↭ys : xs ↭ ys) →
+              Sorted O xs → Sorted O ys →
+              ∀ {i j} → toℕ i ≡ toℕ j →
+              lookup ys j ≤ lookup xs i
+    ↗↭↗⇒≤ {xs} {ys} xs↭ys xs↗ ys↗ {i} {j} i≡j
+      with Fin.injective⇒existsPivot (inverseʳ⇒injective _ (Inverse.inverseʳ (onIndices xs↭ys))) i
+    ... | (k , k≤i , i≤π[k]) = begin
+      lookup ys j                         ≤⟨ lookup-mono-≤ O ys↗ (≡.subst (ℕ._≤ _) i≡j i≤π[k]) ⟩
+      lookup ys (onIndices xs↭ys ⟨$⟩ʳ k)  ≈⟨ onIndices-lookup xs↭ys k ⟨
+      lookup xs k                         ≤⟨ lookup-mono-≤ O xs↗ k≤i ⟩
+      lookup xs i                         ∎

src/Data/List/Sort/Base.agda

@@ -13,11 +13,14 @@ module Data.List.Sort.Base
   where
 
 open import Data.List.Base using (List)
-open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_)
+open import Data.List.Relation.Binary.Permutation.Propositional
+  using (_↭_; ↭⇒↭ₛ)
+import Data.List.Relation.Binary.Permutation.Homogeneous as Homo
 open import Level using (_⊔_)
 
 open TotalOrder totalOrder renaming (Carrier to A)
 open import Data.List.Relation.Unary.Sorted.TotalOrder totalOrder
+import Data.List.Relation.Binary.Permutation.Setoid Eq.setoid as S
 
 ------------------------------------------------------------------------
 -- Definition of a sorting algorithm
@@ -26,8 +29,17 @@ record SortingAlgorithm : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
   field
     sort   : List A → List A
 
-    -- The output of `sort` is a permutation of the input
+    -- The output of `sort` is a propositional permutation of the input.
+    -- Note that the choice of using a propositional equality here
+    -- is very deliberate. A sorting algorithm should only be capable
+    -- of altering the order of the elements of the list, and should not
+    -- be capable of altering the elements themselves in any way.
     sort-↭ : ∀ xs → sort xs ↭ xs
 
     -- The output of `sort` is sorted.
     sort-↗ : ∀ xs → Sorted (sort xs)
+
+  -- Lists are also permutations under the setoid versions of
+  -- permutation.
+  sort-↭ₛ : ∀ xs → sort xs S.↭ xs
+  sort-↭ₛ xs = Homo.map Eq.reflexive (↭⇒↭ₛ (sort-↭ xs))