Add merge and unmerge properties

3 files changed, 145 insertions, 11 deletions

diff --git a/FinMerge.agda b/FinMerge.agda
index c75e982..d7b3f0b 100644
--- a/FinMerge.agda
+++ b/FinMerge.agda
@@ -11,7 +11,7 @@ open import Data.Product using (_×_; _,_; Σ-syntax; map₂; proj₁; proj₂)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym)
 open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning)
 open import Function using (id ; _∘_ ; _$_)
-open import Data.Maybe.Base using (Maybe; just; nothing; fromMaybe)
+open import Data.Maybe.Base using (Maybe; just; nothing; fromMaybe; map)
 
 open import Util using (_<_<_; _<_≤_; toℕ<; Ordering; less; equal; greater; compare)
 
@@ -25,7 +25,7 @@ pluck : m ≤ n → Fin (ℕ.suc n) → Maybe (Fin n)
 pluck z≤n Fin.zero = nothing
 pluck z≤n (Fin.suc x) = just x
 pluck (s≤s m) Fin.zero = just Fin.zero
-pluck (s≤s m) (Fin.suc x) = Data.Maybe.Base.map Fin.suc (pluck m x)
+pluck (s≤s m) (Fin.suc x) = map Fin.suc (pluck m x)
 
 -- Send nothing to the specified m
 unpluck : m ≤ n → Maybe (Fin n) → Fin (ℕ.suc n)
@@ -39,7 +39,7 @@ unpluck (s≤s m) (just (Fin.suc x)) = Fin.suc (unpluck m (just x))
 merge : {i j : ℕ} → i < j ≤ n → Fin (ℕ.suc n) → Fin n
 merge (lt , le) x = fromMaybe (fromℕ< (≤-trans lt le)) (pluck le x)
 
--- Merge two elements of a finite set
+-- Left-adjoint to merge
 unmerge : {i j : ℕ} → i < j ≤ n → Fin n → Fin (ℕ.suc n)
 unmerge (lt , le) x = unpluck le (just x)
 
@@ -48,6 +48,7 @@ glue-once {n} (less (i<j , s≤s j≤n)) = n , merge (i<j , j≤n)
 glue-once {n} (equal i≡j) = ℕ.suc n , id
 glue-once {n} (greater (j<i , s≤s i≤n)) = n , merge (j<i , i≤n)
 
+-- Merge and unmerge
 glue-unglue-once
     : {i j : Fin (ℕ.suc n)}
     → Ordering i j
diff --git a/FinMerge/Properties.agda b/FinMerge/Properties.agda
index 9123460..c250abb 100644
--- a/FinMerge/Properties.agda
+++ b/FinMerge/Properties.agda
@@ -9,12 +9,12 @@ open import Data.Nat.Properties using (≤-trans; <⇒≢)
 open import Data.Product using (_,_; proj₁; proj₂; Σ-syntax)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong-app; sym; _≢_)
 open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning)
-open import Data.Maybe.Base using (Maybe; nothing; just; fromMaybe)
+open import Data.Maybe.Base using (Maybe; map; nothing; just; fromMaybe)
 open import Function using (id;  _∘_)
 
 open import Util using (_<_<_; _<_≤_; toℕ<; Ordering; less; equal; greater; compare)
 
-open import FinMerge using (merge; pluck; glue-once; glue-unglue-once; glue-iter)
+open import FinMerge using (merge; unmerge; pluck; glue-once; glue-unglue-once; glue-iter)
 
 
 private
@@ -29,14 +29,14 @@ pluck-<
     → (m≤n : m ≤ n)
     → (x<m : toℕ x < m)
     → pluck m≤n x ≡ just (lower₁ x (not-n (x<m , m≤n)))
-pluck-< {_} {_} {Fin.zero} (_≤_.s≤s m≤n) (_≤_.s≤s x<m) = refl
-pluck-< {_} {_} {Fin.suc x} (_≤_.s≤s m≤n) (_≤_.s≤s x<m) = ≡
+pluck-< {_} {_} {Fin.zero} (s≤s m≤n) (s≤s x<m) = refl
+pluck-< {_} {_} {Fin.suc x} (s≤s m≤n) (s≤s x<m) = ≡
   where
     open ≡-Reasoning
-    ≡ : pluck (_≤_.s≤s m≤n) (Fin.suc x)
+    ≡ : pluck (s≤s m≤n) (Fin.suc x)
         ≡ just (lower₁ (Fin.suc x) (not-n (s≤s x<m , s≤s m≤n)))
     ≡ = begin
-        pluck (_≤_.s≤s m≤n) (Fin.suc x) ≡⟨⟩
+        pluck (s≤s m≤n) (Fin.suc x) ≡⟨⟩
         Data.Maybe.Base.map Fin.suc (pluck m≤n x)
             ≡⟨ cong (Data.Maybe.Base.map Fin.suc) (pluck-< m≤n x<m) ⟩
         Data.Maybe.Base.map Fin.suc (just (lower₁ x (not-n (x<m , m≤n)))) ≡⟨⟩
@@ -159,3 +159,136 @@ lemma₂ {_} {ℕ.suc n} f g =
   in
     ≡
   where open ≡-Reasoning
+
+j-to-i′
+    : {i : ℕ}
+    → {j : Fin (ℕ.suc n)}
+    → ((i<j , j≤n) : i < toℕ j ≤ n)
+    → merge (i<j , j≤n) j ≡ fromℕ< (≤-trans i<j j≤n)
+j-to-i′ (i<j , j≤n) = cong (fromMaybe (fromℕ< (≤-trans i<j j≤n))) (j-to-nothing j≤n)
+  where
+    j-to-nothing : {j : Fin (ℕ.suc n)} → (j≤n : toℕ j ≤ n) → pluck j≤n j ≡ nothing
+    j-to-nothing {ℕ.zero} {Fin.zero} z≤n = refl
+    j-to-nothing {ℕ.suc n} {Fin.zero} z≤n = refl
+    j-to-nothing {ℕ.suc n} {Fin.suc j} (s≤s j≤n) = cong (map Fin.suc) (j-to-nothing j≤n)
+
+unmerge-i
+    : {i j : Fin (ℕ.suc n)}
+    → ((i<j , j≤n) : toℕ i < toℕ j ≤ n)
+    → unmerge (i<j , j≤n) (fromℕ< (≤-trans i<j j≤n)) ≡ i
+unmerge-i {ℕ.suc n} {Fin.zero} {Fin.suc j} (s≤s i<j , s≤s j≤n) = refl
+unmerge-i {ℕ.suc n} {Fin.suc i} {Fin.suc j} (s≤s i<j , s≤s j≤n) = cong Fin.suc (unmerge-i (i<j , j≤n))
+
+unmerge-k-<
+    : {i j k : Fin (ℕ.suc n)}
+    → ((i<j , j≤n) : toℕ i < toℕ j ≤ n)
+    → (k<j : toℕ k < toℕ j)
+    → unmerge (i<j , j≤n) (fromℕ< (≤-trans k<j j≤n)) ≡ k
+unmerge-k-< {ℕ.suc n} {i} {Fin.suc j} {Fin.zero} (_ , s≤s j≤n) (s≤s k<j)  = refl
+unmerge-k-< {ℕ.suc n} {Fin.zero} {Fin.suc (Fin.suc j)} {Fin.suc k} (s≤s z≤n , s≤s j≤n) (s≤s k<j) = cong Fin.suc (unmerge-k-< (s≤s z≤n , j≤n) k<j)
+unmerge-k-< {ℕ.suc n} {Fin.suc i} {Fin.suc j} {Fin.suc k} (s≤s i<j , s≤s j≤n) (s≤s k<j) = cong Fin.suc (unmerge-k-< (i<j , j≤n) k<j)
+
+k-to-k-<
+    : {i j k : Fin (ℕ.suc n)}
+    → ((i<j , j≤n) : toℕ i < toℕ j ≤ n)
+    → (k<j : toℕ k < toℕ j)
+    → merge (i<j , j≤n) k ≡ fromℕ< (≤-trans k<j j≤n)
+k-to-k-< (i<j , j≤n) k<j = cong (fromMaybe (fromℕ< (≤-trans i<j j≤n))) (k-to-just (k<j , j≤n))
+  where
+    k-to-just
+        : {j k : Fin (ℕ.suc n)}
+        → ((k<j , j≤n) : toℕ k < toℕ j ≤ n)
+        → pluck j≤n k ≡ just (fromℕ< (≤-trans k<j j≤n))
+    k-to-just {ℕ.suc n} {Fin.suc j} {Fin.zero} (s≤s k<j , s≤s j≤n) = refl
+    k-to-just {ℕ.suc n} {Fin.suc j} {Fin.suc k} (s≤s k<j , s≤s j≤n) = cong (map Fin.suc) (k-to-just (k<j , j≤n))
+
+sk-to-k->
+    : {i j : Fin (ℕ.suc n)}
+    → {k : Fin n}
+    → ((i<j , j≤n) : toℕ i < toℕ j ≤ n)
+    → (j<sk : toℕ j < ℕ.suc (toℕ k))
+    → merge (i<j , j≤n) (Fin.suc k) ≡ k
+sk-to-k-> (i<j , j≤n) j<sk = cong (fromMaybe (fromℕ< (≤-trans i<j j≤n))) (sk-to-just j≤n j<sk)
+  where
+    sk-to-just
+        : {n : ℕ}
+        → {j : Fin (ℕ.suc n)}
+        → {k : Fin n}
+        → (j≤n : toℕ j ≤ n)
+        → (j<sk : toℕ j < ℕ.suc (toℕ k))
+        → pluck j≤n (Fin.suc k) ≡ just k
+    sk-to-just {ℕ.suc _} {Fin.zero} {Fin.zero} z≤n (s≤s _) = refl
+    sk-to-just {ℕ.suc _} {Fin.zero} {Fin.suc _} z≤n (s≤s _) = refl
+    sk-to-just {ℕ.suc _} {Fin.suc _} {Fin.suc _} (s≤s j≤n) (s≤s j<sk) = cong (map Fin.suc) (sk-to-just j≤n j<sk)
+
+unmerge-k->
+    : {i j : Fin (ℕ.suc n)}
+    → {k : Fin n}
+    → ((i<j , j≤n) : toℕ i < toℕ j ≤ n)
+    → (j<sk : toℕ j < ℕ.suc (toℕ k))
+    → unmerge (i<j , j≤n) k ≡ Fin.suc k
+unmerge-k-> {ℕ.suc n} {Fin.zero} {Fin.suc Fin.zero} {Fin.suc k} (s≤s z≤n , s≤s z≤n) (s≤s j<sk) = refl
+unmerge-k-> {ℕ.suc n} {Fin.zero} {Fin.suc (Fin.suc j)} {Fin.suc k} (s≤s z≤n , s≤s j≤n) (s≤s j<sk) = cong Fin.suc (unmerge-k-> (s≤s z≤n , j≤n) j<sk)
+unmerge-k-> {ℕ.suc n} {Fin.suc i} {Fin.suc j} {Fin.suc k} (s≤s i<j , s≤s j≤n) (s≤s j<sk) = cong Fin.suc (unmerge-k-> (i<j , j≤n) j<sk)
+
+unmerge-merge-<
+    : {i j k : Fin (ℕ.suc n)}
+    → (i<j≤n : toℕ i < toℕ j ≤ n)
+    → (k<j : toℕ k < toℕ j)
+    → unmerge i<j≤n (merge i<j≤n k) ≡ k
+unmerge-merge-< {n} {i} {j} {k} i<j≤n@(_ , j≤n) k<j = ≡
+  where
+    open ≡-Reasoning
+    ≡ : unmerge i<j≤n (merge i<j≤n k) ≡ k
+    ≡ = begin
+        unmerge i<j≤n (merge i<j≤n k)             ≡⟨ cong (unmerge i<j≤n) (k-to-k-< i<j≤n k<j) ⟩
+        unmerge i<j≤n (fromℕ< (≤-trans k<j j≤n))  ≡⟨ unmerge-k-< i<j≤n k<j ⟩
+        k                                         ∎
+
+unmerge-merge-=
+    : {i j k : Fin (ℕ.suc n)}
+    → (i<j≤n : toℕ i < toℕ j ≤ n)
+    → k ≡ j
+    → unmerge i<j≤n (merge i<j≤n k) ≡ i
+unmerge-merge-= {_} {i} {j} {k} i<j≤n@(i<j , j≤n) k≡j = ≡
+  where
+    open ≡-Reasoning
+    ≡ : unmerge i<j≤n (merge i<j≤n k) ≡ i
+    ≡ = begin
+        unmerge i<j≤n (merge i<j≤n k)             ≡⟨ cong (unmerge i<j≤n ∘ merge i<j≤n) k≡j ⟩
+        unmerge i<j≤n (merge i<j≤n j)             ≡⟨ cong (unmerge i<j≤n) (j-to-i′ i<j≤n) ⟩
+        unmerge i<j≤n (fromℕ< (≤-trans i<j j≤n))  ≡⟨ unmerge-i i<j≤n ⟩
+        i                                         ∎
+
+unmerge-merge->
+    : {i j k : Fin (ℕ.suc n)}
+    → (i<j≤n : toℕ i < toℕ j ≤ n)
+    → (j<k : toℕ j < toℕ k)
+    → unmerge i<j≤n (merge i<j≤n k) ≡ k
+unmerge-merge-> {n} {i} {j} {Fin.suc k} i<j≤n j<k = ≡
+  where
+    open ≡-Reasoning
+    ≡ : unmerge i<j≤n (merge i<j≤n (Fin.suc k)) ≡ Fin.suc k
+    ≡ = begin
+        unmerge i<j≤n (merge i<j≤n (Fin.suc k)) ≡⟨ cong (unmerge i<j≤n) (sk-to-k-> i<j≤n j<k) ⟩
+        unmerge i<j≤n k                         ≡⟨ unmerge-k-> i<j≤n j<k ⟩
+        Fin.suc k                               ∎
+
+unmerge-merge
+    : {i j k : Fin (ℕ.suc n)}
+    → (i<j≤n : toℕ i < toℕ j ≤ n)
+    → (f : Fin (ℕ.suc n) → Fin m)
+    → f i ≡ f j
+    → f (unmerge i<j≤n (merge i<j≤n k)) ≡ f k
+unmerge-merge {n} {m} {i} {j} {k} i<j≤n f fi≡fj with (compare k j)
+... | less (k<j , _) = cong f (unmerge-merge-< i<j≤n k<j)
+... | greater (j<k , _) = cong f (unmerge-merge-> i<j≤n j<k)
+... | equal k≡j = ≡
+  where
+    open ≡-Reasoning
+    ≡ : f (unmerge i<j≤n (merge i<j≤n k)) ≡ f k
+    ≡ = begin
+        f (unmerge i<j≤n (merge i<j≤n k)) ≡⟨ cong f (unmerge-merge-= i<j≤n k≡j) ⟩
+        f i                               ≡⟨ fi≡fj ⟩
+        f j                               ≡⟨ cong f (sym k≡j) ⟩
+        f k                               ∎
diff --git a/Util.agda b/Util.agda
index 0c79b17..d7053c5 100644
--- a/Util.agda
+++ b/Util.agda
@@ -27,6 +27,6 @@ compare Fin.zero Fin.zero = equal refl
 compare Fin.zero j@(Fin.suc _) = less (z<s , toℕ< j)
 compare i@(Fin.suc _) Fin.zero = greater (z<s , toℕ< i)
 compare (Fin.suc i) (Fin.suc j) with compare i j
-... | less (i<j , j<n) = less (_≤_.s≤s i<j , _≤_.s≤s j<n)
+... | less (i<j , j<n) = less (s≤s i<j , s≤s j<n)
 ... | equal i≡j = equal (cong Fin.suc i≡j)
-... | greater (j<i , i<n) = greater (_≤_.s≤s j<i , _≤_.s≤s i<n)
+... | greater (j<i , i<n) = greater (s≤s j<i , s≤s i<n)