Simplify merge function

1 files changed, 11 insertions, 29 deletions

diff --git a/FinMerge.agda b/FinMerge.agda
index d8b38fd..b483fc8 100644
--- a/FinMerge.agda
+++ b/FinMerge.agda
@@ -1,15 +1,16 @@
 module FinMerge where
 
 open import Data.Empty using (⊥-elim)
-open import Data.Fin using (Fin; splitAt; join; fromℕ<; cast; toℕ; #_) renaming (_<_ to _<′_)
+open import Data.Fin using (Fin; fromℕ<; toℕ; #_)
 open import Data.Fin.Properties using (¬Fin0)
 open import Data.Nat using (ℕ; _+_; _≤_; _<_ ; z<s)
-open import Data.Nat.Properties using (+-comm; <⇒≤)
+open import Data.Nat.Properties using (≤-trans)
 open import Data.Sum.Base using (_⊎_)
 open import Data.Product using (_×_; _,_; Σ-syntax; map₂)
 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)
 
 
 _<_≤_ : ℕ → ℕ → ℕ → Set
@@ -40,41 +41,22 @@ private
   variable
     m n : ℕ
 
--- Send the 0th index of the right set to the specified index of the left
-merge0 : (i : Fin m) → Fin m ⊎ Fin (ℕ.suc n) → Fin m ⊎ Fin n
-merge0 i (_⊎_.inj₁ x) = _⊎_.inj₁ x
-merge0 i (_⊎_.inj₂ Fin.zero) = _⊎_.inj₁ i
-merge0 i (_⊎_.inj₂ (Fin.suc y)) = _⊎_.inj₂ y
-
--- Split a natural number into two parts
-splitℕ : m ≤ n → Σ[ m′ ∈ ℕ ] n ≡ m + m′
-splitℕ  _≤_.z≤n = _ , refl
-splitℕ (_≤_.s≤s le) = map₂ (cong ℕ.suc) (splitℕ le)
+-- Send the specified m to nothing
+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)
 
 -- Merge two elements of a finite set
 merge : {i j : ℕ} → i < j ≤ n → Fin (ℕ.suc n) → Fin n
-merge {n} {i} {j} (lt , le) x with splitℕ le
-... | j′ , n≡j+j′ =
-    cast (sym n≡j+j′) $
-    join j j′ $
-    merge0 (fromℕ< lt) $
-    splitAt j $
-    cast Sn≡j+Sj′ x
-  where
-    open ≡-Reasoning
-    Sn≡j+Sj′ : ℕ.suc n ≡ j + ℕ.suc j′
-    Sn≡j+Sj′ = begin
-        ℕ.suc n         ≡⟨ cong ℕ.suc (n≡j+j′) ⟩
-        ℕ.suc (j + j′)  ≡⟨ cong ℕ.suc (+-comm j j′) ⟩
-        ℕ.suc (j′ + j)  ≡⟨⟩
-        ℕ.suc j′ + j    ≡⟨ +-comm (ℕ.suc j′) j ⟩
-        j + ℕ.suc j′ ∎
+merge (lt , le) x = fromMaybe (fromℕ< (≤-trans lt le)) (pluck le x)
 
 -- Glue together the image of two finite-set functions
 glue : (Fin m → Fin n) → (Fin m → Fin n) → Σ[ x ∈ ℕ ] (Fin n → Fin x)
 glue {ℕ.zero} {n} _ _ = n , id
 glue {ℕ.suc _} {ℕ.zero} f _ = ⊥-elim (¬Fin0 (f (# 0)))
-glue {ℕ.suc _} {ℕ.suc n} f g with glue (f ∘ Fin.suc) (g ∘ Fin.suc)
+glue {ℕ.suc _} {ℕ.suc _} f g with glue (f ∘ Fin.suc) (g ∘ Fin.suc)
 ... | ℕ.zero , h = ⊥-elim (¬Fin0 (h (# 0)))
 ... | ℕ.suc x , h with compare (h (f (# 0))) (h (g (# 0)))
 ...     | less (f0<g0 , _≤_.s≤s g0<n) = x , merge (f0<g0 , g0<n) ∘ h