Remove with-abstractions

2 files changed, 71 insertions, 46 deletions

diff --git a/FinMerge.agda b/FinMerge.agda
index c62fe14..c75e982 100644
--- a/FinMerge.agda
+++ b/FinMerge.agda
@@ -4,10 +4,10 @@ module FinMerge where
 open import Data.Empty using (⊥-elim)
 open import Data.Fin using (Fin; fromℕ<; toℕ; #_)
 open import Data.Fin.Properties using (¬Fin0)
-open import Data.Nat using (ℕ; _+_; _≤_; _<_ ; z<s; s≤s)
+open import Data.Nat using (ℕ; _+_; _≤_; z≤n; s≤s; _<_ ; z<s)
 open import Data.Nat.Properties using (≤-trans)
 open import Data.Sum.Base using (_⊎_)
-open import Data.Product using (_×_; _,_; Σ-syntax; map₂; proj₂)
+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 ; _∘_ ; _$_)
@@ -22,20 +22,39 @@ private
 
 -- 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)
+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)
+
+-- Send nothing to the specified m
+unpluck : m ≤ n → Maybe (Fin n) → Fin (ℕ.suc n)
+unpluck z≤n nothing = Fin.zero
+unpluck z≤n (just x) = Fin.suc x
+unpluck (s≤s m) nothing = Fin.suc (unpluck m nothing)
+unpluck (s≤s m) (just Fin.zero) = Fin.zero
+unpluck (s≤s m) (just (Fin.suc x)) = Fin.suc (unpluck m (just x))
 
 -- Merge two elements of a finite set
 merge : {i j : ℕ} → i < j ≤ n → Fin (ℕ.suc n) → Fin n
 merge (lt , le) x = fromMaybe (fromℕ< (≤-trans lt le)) (pluck le x)
 
-glue-once : Fin (ℕ.suc n) → Fin (ℕ.suc n) → Σ[ x ∈ ℕ ] (Fin (ℕ.suc n) → Fin x)
-glue-once {n} f0 g0 with compare f0 g0
-... | less (f0<g0 , s≤s g0≤n) = n , merge (f0<g0 , g0≤n)
-... | equal f0≡g0 = ℕ.suc n , id
-... | greater (g0<f0 , s≤s f0≤n) = n , merge (g0<f0 , f0≤n)
+-- Merge two elements of a finite set
+unmerge : {i j : ℕ} → i < j ≤ n → Fin n → Fin (ℕ.suc n)
+unmerge (lt , le) x = unpluck le (just x)
+
+glue-once : {i j : Fin (ℕ.suc n)} → Ordering i j → Σ[ x ∈ ℕ ] (Fin (ℕ.suc n) → Fin x)
+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)
+
+glue-unglue-once
+    : {i j : Fin (ℕ.suc n)}
+    → Ordering i j
+    → Σ[ x ∈ ℕ ] ((Fin (ℕ.suc n) → Fin x) × (Fin x → Fin (ℕ.suc n)))
+glue-unglue-once {n} (less (i<j , s≤s j≤n)) = n , merge (i<j , j≤n) , unmerge (i<j , j≤n)
+glue-unglue-once {n} (equal i≡j) = ℕ.suc n , id , id
+glue-unglue-once {n} (greater (j<i , s≤s i≤n)) = n , merge (j<i , i≤n) , unmerge (j<i , i≤n)
 
 -- Glue together the image of two finite-set functions
 glue : (Fin m → Fin n) → (Fin m → Fin n) → Σ[ x ∈ ℕ ] (Fin n → Fin x)
@@ -43,7 +62,7 @@ glue {ℕ.zero} {n} _ _ = n , id
 glue {ℕ.suc _} {ℕ.zero} f _ = ⊥-elim (¬Fin0 (f (# 0)))
 glue {ℕ.suc _} {ℕ.suc _} f g with glue (f ∘ Fin.suc) (g ∘ Fin.suc)
 ... | ℕ.zero , h = ⊥-elim (¬Fin0 (h (# 0)))
-... | ℕ.suc _ , h = map₂ (_∘ h) (glue-once (h (f (# 0))) (h (g (# 0))))
+... | ℕ.suc _ , h = map₂ (_∘ h) (glue-once (compare (h (f (# 0))) (h (g (# 0)))))
 
 -- Glue together the image of two finite-set functions, iterative
 glue-iter
@@ -55,5 +74,5 @@ glue-iter
 glue-iter {ℕ.zero} {n} {y} f g h = y , h
 glue-iter {ℕ.suc m} {n} {ℕ.zero} f g h = ⊥-elim (¬Fin0 (f (# 0)))
 glue-iter {ℕ.suc m} {n} {ℕ.suc y} f g h =
-    let p = proj₂ (glue-once (f (# 0)) (g (# 0))) in
+    let p = proj₁ (proj₂ (glue-unglue-once (compare (f (# 0)) (g (# 0))))) in
     glue-iter (p ∘ f ∘ Fin.suc) (p ∘ g ∘ Fin.suc) (p ∘ h)
diff --git a/FinMerge/Properties.agda b/FinMerge/Properties.agda
index 79f8686..9123460 100644
--- a/FinMerge/Properties.agda
+++ b/FinMerge/Properties.agda
@@ -12,9 +12,9 @@ open import Relation.Binary.PropositionalEquality.Properties using (module ≡-R
 open import Data.Maybe.Base using (Maybe; nothing; just; fromMaybe)
 open import Function using (id;  _∘_)
 
-open import Util using (_<_<_; _<_≤_; toℕ<; less; equal; greater; compare)
+open import Util using (_<_<_; _<_≤_; toℕ<; Ordering; less; equal; greater; compare)
 
-open import FinMerge using (merge; pluck; glue-once; glue-iter)
+open import FinMerge using (merge; pluck; glue-once; glue-unglue-once; glue-iter)
 
 
 private
@@ -109,12 +109,20 @@ merge-i-j {_} {i} {j} i<j≤n = ≡
       merge i<j≤n j ∎
 
 glue-once-correct
-    : (f0 g0 : Fin (ℕ.suc n))
-    → proj₂ (glue-once f0 g0) f0 ≡ proj₂ (glue-once f0 g0) g0
-glue-once-correct {n} f0 g0 with compare f0 g0
-... | less (f0<g0 , s≤s g0≤n) = merge-i-j (f0<g0 , g0≤n)
-... | equal f0≡g0 = f0≡g0
-... | greater (g0<f0 , s≤s f0≤n) = sym (merge-i-j (g0<f0 , f0≤n))
+    : {i j : Fin (ℕ.suc n)}
+    → (i?j : Ordering i j)
+    → proj₂ (glue-once i?j) i ≡ proj₂ (glue-once i?j) j
+glue-once-correct (less (i<j , s≤s j≤n)) = merge-i-j (i<j , j≤n)
+glue-once-correct (equal i≡j) = i≡j
+glue-once-correct (greater (j<i , s≤s i≤n)) = sym (merge-i-j (j<i , i≤n))
+
+glue-once-correct′
+    : {i j : Fin (ℕ.suc n)}
+    → (i?j : Ordering i j)
+    → proj₁ (proj₂ (glue-unglue-once i?j)) i ≡ proj₁ (proj₂ (glue-unglue-once i?j)) j
+glue-once-correct′ (less (i<j , s≤s j≤n)) = merge-i-j (i<j , j≤n)
+glue-once-correct′ (equal i≡j) = i≡j
+glue-once-correct′ (greater (j<i , s≤s i≤n)) = sym (merge-i-j (j<i , i≤n))
 
 glue-iter-append
     : {y : ℕ}
@@ -123,33 +131,31 @@ glue-iter-append
     → Σ[ h′ ∈ (Fin y → Fin (proj₁ (glue-iter f g h))) ] (proj₂ (glue-iter f g h) ≡ h′ ∘ h)
 glue-iter-append {ℕ.zero} f g h = id , refl
 glue-iter-append {ℕ.suc m} {_} {ℕ.zero} f g h = ⊥-elim (¬Fin0 (f (# 0)))
-glue-iter-append {ℕ.suc m} {_} {ℕ.suc y} f g h with
-    glue-iter-append
-        (proj₂ (glue-once (f (# 0)) (g (# 0))) ∘ f ∘ Fin.suc)
-        (proj₂ (glue-once (f (# 0)) (g (# 0))) ∘ g ∘ Fin.suc)
-        (proj₂ (glue-once (f (# 0)) (g (# 0))) ∘ h)
-... | h′ , glue-p∘h≡h′∘p∘h = h′ ∘ proj₂ (glue-once (f (# 0)) (g (# 0))) , glue-p∘h≡h′∘p∘h
+glue-iter-append {ℕ.suc m} {_} {ℕ.suc y} f g h =
+  let
+    p = proj₁ (proj₂ (glue-unglue-once (compare (f (# 0)) (g (# 0)))))
+    h′ , glue-p∘h≡h′∘p∘h = glue-iter-append (p ∘ f ∘ Fin.suc) (p ∘ g ∘ Fin.suc) (p ∘ h)
+  in
+    h′ ∘ p , glue-p∘h≡h′∘p∘h
 
 lemma₂
     : (f g : Fin (ℕ.suc m) → Fin n)
     → let p = proj₂ (glue-iter f g id) in p (f (# 0)) ≡ p (g (# 0))
 lemma₂ {_} {ℕ.zero} f g = ⊥-elim (¬Fin0 (f (# 0)))
-lemma₂ {_} {ℕ.suc n} f g with
-    glue-iter-append
-        (proj₂ (glue-once (f (# 0)) (g (# 0))) ∘ f ∘ Fin.suc)
-        (proj₂ (glue-once (f (# 0)) (g (# 0))) ∘ g ∘ Fin.suc)
-        (proj₂ (glue-once (f (# 0)) (g (# 0))))
-... | h′ , glue≡h′∘h = ≡
-      where
-        open ≡-Reasoning
-        p = proj₂ (glue-once (f (# 0)) (g (# 0)))
-        f′ = f ∘ Fin.suc
-        g′ = g ∘ Fin.suc
-        ≡ : proj₂ (glue-iter (p ∘ f′) (p ∘ g′) p) (f Fin.zero)
-          ≡ proj₂ (glue-iter (p ∘ f′) (p ∘ g′) p) (g Fin.zero)
-        ≡ = begin
-            proj₂ (glue-iter (p ∘ f′) (p ∘ g′) p) (f Fin.zero)
-                                  ≡⟨ cong-app glue≡h′∘h (f Fin.zero) ⟩
-            h′ (p (f Fin.zero))   ≡⟨ cong h′ (glue-once-correct (f (# 0)) (g (# 0))) ⟩
-            h′ (p (g Fin.zero))   ≡⟨ sym (cong-app glue≡h′∘h (g Fin.zero)) ⟩
-            proj₂ (glue-iter (p ∘ f′) (p ∘ g′) p) (g Fin.zero) ∎
+lemma₂ {_} {ℕ.suc n} f g =
+  let
+    p = proj₁ (proj₂ (glue-unglue-once (compare (f (# 0)) (g (# 0)))))
+    h′ , glue≡h′∘h = glue-iter-append (p ∘ f ∘ Fin.suc) (p ∘ g ∘ Fin.suc) p
+    f′ = f ∘ Fin.suc
+    g′ = g ∘ Fin.suc
+    ≡ : proj₂ (glue-iter (p ∘ f′) (p ∘ g′) p) (f Fin.zero)
+      ≡ proj₂ (glue-iter (p ∘ f′) (p ∘ g′) p) (g Fin.zero)
+    ≡ = begin
+        proj₂ (glue-iter (p ∘ f′) (p ∘ g′) p) (f Fin.zero)
+                              ≡⟨ cong-app glue≡h′∘h (f Fin.zero) ⟩
+        h′ (p (f Fin.zero))   ≡⟨ cong h′ (glue-once-correct′ (compare (f (# 0)) (g (# 0)))) ⟩
+        h′ (p (g Fin.zero))   ≡⟨ sym (cong-app glue≡h′∘h (g Fin.zero)) ⟩
+        proj₂ (glue-iter (p ∘ f′) (p ∘ g′) p) (g Fin.zero) ∎
+  in
+    ≡
+  where open ≡-Reasoning