Remove with-abstractions

1 files changed, 39 insertions, 33 deletions

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