Strengthen permutation sort theorem

4 files changed, 73 insertions, 44 deletions

diff --git a/Data/Circuit/Convert.agda b/Data/Circuit/Convert.agda
index 497b0cd..ce6de69 100644
--- a/Data/Circuit/Convert.agda
+++ b/Data/Circuit/Convert.agda
@@ -5,16 +5,24 @@ module Data.Circuit.Convert where
 open import Data.Nat.Base using (ℕ)
 open import Data.Circuit.Gate using (Gate; GateLabel; cast-gate; cast-gate-is-id; subst-is-cast-gate)
 open import Data.Fin.Base using (Fin)
-open import Function.Bundles using (Equivalence)
 open import Data.Hypergraph.Edge GateLabel using (Edge)
-open import Data.Hypergraph.Base GateLabel using (Hypergraph; sortHypergraph)
+open import Data.Hypergraph.Base GateLabel using (Hypergraph; sortHypergraph; mkHypergraph)
 open import Data.Hypergraph.Setoid GateLabel using (Hypergraph-Setoid; ≈-Hypergraph)
 open import Data.Permutation using (fromList-↭; toList-↭)
 open import Data.List using (length)
 open import Data.Vec.Functional using (toVec; fromVec; toList; fromList)
-open import Function.Base using (_∘_; id; _$_)
-
+open import Function.Bundles using (Equivalence; _↔_)
+open import Function.Base using (_∘_; id)
+open import Data.List.Relation.Binary.Permutation.Homogeneous using (Permutation)
+open import Data.Product.Base using (proj₁; proj₂; _×_)
+open import Data.Fin.Permutation using (flip; _⟨$⟩ˡ_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
+
+import Function.Reasoning as →-Reasoning
+import Data.List.Relation.Binary.Permutation.Propositional as L
+import Data.Vec.Functional.Relation.Binary.Permutation as V
 import DecorationFunctor.Hypergraph.Labeled as LabeledHypergraph
+
 open LabeledHypergraph using (Hypergraph-same) renaming (Hypergraph to Hypergraph′; Hypergraph-setoid to Hypergraph-Setoid′)
 
 to : {v : ℕ} → Hypergraph v → Hypergraph′ v
@@ -37,9 +45,6 @@ from {v} H = record
     asEdge : Fin h → Edge v
     asEdge e = record { label = l e ; ports = toVec (j e) }
 
-open import Data.Product.Base using (proj₁; proj₂)
-open import Data.Fin.Permutation using (flip)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 to-cong : {v : ℕ} {H H′ : Hypergraph v} → ≈-Hypergraph H H′ → Hypergraph-same (to H) (to H′)
 to-cong {v} {H} {H′} ≈H = record
     { ↔h = flip ρ
@@ -49,8 +54,6 @@ to-cong {v} {H} {H′} ≈H = record
     }
   where
     open Edge using (arity; ports; label)
-    open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_)
-    open import Function.Bundles using (_↔_)
     open ≈-Hypergraph ≈H
     open import Data.Fin.Permutation using (_⟨$⟩ʳ_; _⟨$⟩ˡ_; Permutation′; inverseʳ)
     open import Data.Fin.Base using (cast)
@@ -87,11 +90,9 @@ to-cong {v} {H} {H′} ≈H = record
           ≡.refl
 
 module _ {v : ℕ} where
-  open import Data.Hypergraph.Edge GateLabel using (decTotalOrder; ≈-Edge; ≈-Edge⇒≡)
+  open import Data.Hypergraph.Edge GateLabel using (decTotalOrder; ≈-Edge; ≈-Edge-IsEquivalence; ≈-Edge⇒≡)
   open import Data.List.Sort (decTotalOrder {v}) using (sort; sort-↭)
   open import Data.Permutation.Sort (decTotalOrder {v}) using (sorted-≋)
-  open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_)
-  open import Data.Vec.Functional.Relation.Binary.Permutation using () renaming (_↭_ to _↭′_)
   open import Data.List.Relation.Binary.Pointwise using (Pointwise; Pointwise-≡⇒≡; map)
   open import Data.Product.Base using (_,_)
   open import Data.Hypergraph.Label using (HypergraphLabel)
@@ -172,21 +173,24 @@ module _ {v : ℕ} where
           cast _ (toVec (H′.j e ∘ fincast _)) ≡⟨ cast-toVec (≗a′ e) (H′.j e) ⟩
           toVec (H′.j e)                      ∎
 
-      H∘ρ≗H′ : (e : Fin H′.h) → asEdge H (flip ↔h Data.Fin.Permutation.⟨$⟩ʳ e) ≡ asEdge H′ e
+      H∘ρ≗H′ : (e : Fin H′.h) → asEdge H (↔h ⟨$⟩ˡ e) ≡ asEdge H′ e
       H∘ρ≗H′ e = ≈-Edge⇒≡ record
           { ≡arity = ≗a′ e
           ; ≡label = ≗l′ e
           ; ≡ports = ≗p′ e
           }
 
+      open Hypergraph using (edges)
+      open →-Reasoning
       ≡sorted : sortHypergraph (from H) ≡ sortHypergraph (from H′)
       ≡sorted =
-          ≡.cong (λ x → record { edges = x } ) $
-          Pointwise-≡⇒≡ $
-          map ≈-Edge⇒≡ $
-          sorted-≋ $
-          toList-↭ $
-          flip ↔h , H∘ρ≗H′
+             flip ↔h , H∘ρ≗H′             ∶ asEdge H V.↭ asEdge H′
+          |> toList-↭                     ∶ toList (asEdge H) L.↭ toList (asEdge H′)
+          |> L.↭⇒↭ₛ′ ≈-Edge-IsEquivalence ∶ Permutation ≈-Edge (edges (from H)) (edges (from H′))
+          |> sorted-≋                     ∶ Pointwise ≈-Edge (sort (edges (from H))) (sort (edges (from H′)))
+          |> map ≈-Edge⇒≡                 ∶ Pointwise _≡_ (sort (edges (from H))) (sort (edges (from H′)))
+          |> Pointwise-≡⇒≡                ∶ sort (edges (from H)) ≡ sort (edges (from H′))
+          |> ≡.cong mkHypergraph          ∶ sortHypergraph (from H) ≡ sortHypergraph (from H′)
 
 equiv : (v : ℕ) → Equivalence (Hypergraph-Setoid v) (Hypergraph-Setoid′ v)
 equiv v = record
diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda
index 5cf5388..6988cf0 100644
--- a/Data/Hypergraph/Base.agda
+++ b/Data/Hypergraph/Base.agda
@@ -12,6 +12,7 @@ open import Data.String using (String; unlines)
 import Data.List.Sort as Sort
 
 record Hypergraph (v : ℕ) : Set where
+  constructor mkHypergraph
   field
     edges : List (Edge v)
 
diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda
index cbf61e6..13b9278 100644
--- a/Data/Hypergraph/Edge.agda
+++ b/Data/Hypergraph/Edge.agda
@@ -80,6 +80,14 @@ record ≈-Edge {n : ℕ} (E E′ : Edge n) : Set where
     module i≈j = ≈-Edge i≈j
     module j≈k = ≈-Edge j≈k
 
+open import Relation.Binary using (IsEquivalence)
+≈-Edge-IsEquivalence : {v : ℕ} → IsEquivalence (≈-Edge {v})
+≈-Edge-IsEquivalence = record
+    { refl = ≈-Edge-refl
+    ; sym = ≈-Edge-sym
+    ; trans = ≈-Edge-trans
+    }
+
 open HL using (_[_<_])
 _<<_ : {v a : ℕ} → Rel (Vec (Fin v) a) 0ℓ
 _<<_ {v} = Lex.Lex-< _≡_ (Fin._<_ {v})
@@ -300,11 +308,7 @@ tri x y | tri> x≮y x≢y y<x = tri> ¬x<y (λ x≡y → x≢y (≡arity x≡y)
 isStrictTotalOrder : {v : ℕ} → IsStrictTotalOrder (≈-Edge {v}) (<-Edge {v})
 isStrictTotalOrder = record
     { isStrictPartialOrder = record
-        { isEquivalence = record
-            { refl = ≈-Edge-refl
-            ; sym = ≈-Edge-sym
-            ; trans = ≈-Edge-trans
-            }
+        { isEquivalence = ≈-Edge-IsEquivalence
         ; irrefl = <-Edge-irrefl
         ; trans = <-Edge-trans
         ; <-resp-≈ = <-Edge-respʳ-≈ , <-Edge-respˡ-≈
diff --git a/Data/Permutation/Sort.agda b/Data/Permutation/Sort.agda
index 977443a..658997d 100644
--- a/Data/Permutation/Sort.agda
+++ b/Data/Permutation/Sort.agda
@@ -14,20 +14,23 @@ open DecTotalOrder dto
     )
   renaming (Carrier to A; trans to ≤-trans; reflexive to ≤-reflexive)
 
-open import Data.Fin.Base using (Fin)
+open import Data.Nat.Base using (ℕ)
 open import Data.List.Base using (List; _++_; [_])
 open import Data.List.Membership.Setoid Eq.setoid using (_∈_)
 open import Data.List.Relation.Binary.Pointwise using (module Pointwise)
-open import Data.List.Relation.Binary.Equality.Setoid Eq.setoid using (_≋_; ≋-refl; ≋-sym; ≋-trans)
+open import Data.List.Relation.Binary.Equality.Setoid Eq.setoid using (_≋_; ≋-refl; ≋-sym; ≋-trans; ≋-length; Any-resp-≋)
 open import Data.List.Relation.Unary.Linked using (Linked)
 open import Data.List.Relation.Unary.Sorted.TotalOrder totalOrder using (Sorted)
-open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭-trans; ↭-sym)
-open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (↭-length)
+open import Data.List.Relation.Binary.Permutation.Homogeneous using (map)
+open import Data.List.Relation.Binary.Permutation.Propositional using () renaming (_↭_ to _↭′_)
+open import Data.List.Relation.Binary.Permutation.Setoid Eq.setoid using (_↭_; ↭-trans; ↭-sym; refl; prep; swap; trans; ↭-reflexive-≋)
+open import Data.List.Relation.Binary.Permutation.Setoid.Properties Eq.setoid using (∈-resp-↭)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+open import Data.List.Relation.Binary.Permutation.Setoid.Properties (≡.setoid A) using (map⁺)
 open import Data.List.Relation.Unary.Any using (Any)
 open import Data.List.Sort dto using (sort; sort-↭; sort-↗)
 open import Relation.Nullary.Decidable.Core using (yes; no)
-open Fin
-open _↭_
+open ℕ
 open Any
 open List
 open Linked
@@ -110,29 +113,43 @@ insert-remove {x₀ ∷ x₁ ∷ xs} {x} (x₀≤x₁ ∷ s-xs) (there x∈xs) w
           x₁≤x = head-≤ s-xs x∈xs
 ... | no x≰x₀ = Eq.refl ∷ insert-remove s-xs x∈xs
 
-apply : {xs ys : List A} {x : A} → xs ↭ ys → x ∈ xs → x ∈ ys
-apply refl x-in-xs = x-in-xs
-apply (prep x xs↭ys) (here px) = here px
-apply (prep x xs↭ys) (there x-in-xs) = there (apply xs↭ys x-in-xs)
-apply (swap x y xs↭ys) (here px) = there (here px)
-apply (swap x y xs↭ys) (there (here px)) = here px
-apply (swap x y xs↭ys) (there (there x-in-xs)) = there (there (apply xs↭ys x-in-xs))
-apply (trans xs↭ys ys↭zs) x-in-xs = apply ys↭zs (apply xs↭ys x-in-xs)
+open import Data.List.Base using (length)
+open import Function.Base using (_∘_; flip; id)
+open import Data.List.Relation.Binary.Permutation.Propositional using (↭⇒↭ₛ)
+
+∈-resp-≋ : {xs ys : List A} {x : A} → xs ≋ ys → x ∈ xs → x ∈ ys
+∈-resp-≋ = Any-resp-≋ (flip Eq.trans)
+
+≋-remove
+    : {xs ys : List A}
+      {x : A}
+    → (xs≋ys : xs ≋ ys)
+    → (x∈xs : x ∈ xs)
+    → let x∈ys = ∈-resp-≋ xs≋ys x∈xs in
+      remove xs x∈xs ≋ remove ys x∈ys
+≋-remove (x≈y ∷ xs≋ys) (here px) = xs≋ys
+≋-remove (x≈y ∷ xs≋ys) (there x∈xs) = x≈y ∷ ≋-remove xs≋ys x∈xs
 
 ↭-remove
     : {xs ys : List A}
       {x : A}
     → (xs↭ys : xs ↭ ys)
     → (x∈xs : x ∈ xs)
-    → let x∈ys = apply xs↭ys x∈xs in
+    → let x∈ys = ∈-resp-↭ xs↭ys x∈xs in
       remove xs x∈xs ↭ remove ys x∈ys
-↭-remove refl x∈xs = refl
+↭-remove (refl xs≋ys) x∈xs = ↭-reflexive-≋ (≋-remove xs≋ys x∈xs)
 ↭-remove (prep x xs↭ys) (here px) = xs↭ys
 ↭-remove (prep x xs↭ys) (there x∈xs) = prep x (↭-remove xs↭ys x∈xs)
 ↭-remove (swap x y xs↭ys) (here px) = prep y xs↭ys
 ↭-remove (swap x y xs↭ys) (there (here px)) = prep x xs↭ys
 ↭-remove (swap x y xs↭ys) (there (there x∈xs)) = swap x y (↭-remove xs↭ys x∈xs)
-↭-remove (trans xs↭ys ys↭zs) x∈xs = trans (↭-remove xs↭ys x∈xs) (↭-remove ys↭zs (apply xs↭ys x∈xs))
+↭-remove (trans xs↭ys ys↭zs) x∈xs = trans (↭-remove xs↭ys x∈xs) (↭-remove ys↭zs (∈-resp-↭ xs↭ys x∈xs))
+
+↭-length : ∀ {xs ys : List A} → xs ↭ ys → length xs ≡ length ys
+↭-length (refl xs≋ys)    = ≋-length xs≋ys
+↭-length (prep x lr)     = ≡.cong suc (↭-length lr)
+↭-length (swap x y lr)   = ≡.cong (suc ∘ suc) (↭-length lr)
+↭-length (trans lr₁ lr₂) = ≡.trans (↭-length lr₁) (↭-length lr₂)
 
 sorted-unique
     : {xs ys : List A}
@@ -147,7 +164,7 @@ sorted-unique xs@{x ∷ xs′} {ys} xs↭ys s-xs s-ys = ≋-trans ≋xs (≋-tra
     x∈xs : x ∈ xs
     x∈xs = here Eq.refl
     x∈ys : x ∈ ys
-    x∈ys = apply xs↭ys x∈xs
+    x∈ys = ∈-resp-↭ xs↭ys x∈xs
     s-xs′ : Sorted (remove xs x∈xs)
     s-xs′ = remove-sorted s-xs x∈xs
     s-ys′ : Sorted (remove ys x∈ys)
@@ -170,7 +187,10 @@ sorted-≋
 sorted-≋ {xs} {ys} xs↭ys =
     sorted-unique
       (↭-trans
-        (sort-↭ xs)
-        (↭-trans xs↭ys (↭-sym (sort-↭ ys))))
+        (⇒↭ (sort-↭ xs))
+        (↭-trans xs↭ys (↭-sym (⇒↭ (sort-↭ ys)))))
       (sort-↗ xs)
       (sort-↗ ys)
+  where
+    ⇒↭ : {xs ys : List A} → xs ↭′ ys → xs ↭ ys
+    ⇒↭ = map Eq.reflexive ∘ ↭⇒↭ₛ