From 2207e9b0e3defe2a5b6250ff8a2a1132d8fd10ee Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 21 Feb 2024 18:59:18 -0600
Subject: Add iterative version of glue

---
 FinMerge.agda | 39 +++++++++++++++++++++------------------
 Util.agda     | 17 ++++++++++++++++-
 2 files changed, 37 insertions(+), 19 deletions(-)

diff --git a/FinMerge.agda b/FinMerge.agda
index f237a53..2e0ad03 100644
--- a/FinMerge.agda
+++ b/FinMerge.agda
@@ -3,7 +3,7 @@ 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)
+open import Data.Nat using (ℕ; _+_; _≤_; _<_ ; z<s; s≤s)
 open import Data.Nat.Properties using (≤-trans)
 open import Data.Sum.Base using (_⊎_)
 open import Data.Product using (_×_; _,_; Σ-syntax; map₂)
@@ -12,23 +12,9 @@ open import Relation.Binary.PropositionalEquality.Properties using (module ≡-R
 open import Function using (id ; _∘_ ; _$_)
 open import Data.Maybe.Base using (Maybe; just; nothing; fromMaybe)
 
-open import Util using (_<_<_; _<_≤_; toℕ<)
+open import Util using (_<_<_; _<_≤_; toℕ<; Ordering; less; equal; greater; compare)
 
 
-data Ordering {n : ℕ} : Fin n → Fin n → Set where
-  less : ∀ {i j} → toℕ i < toℕ j < n → Ordering i j
-  equal : ∀ {i j} → toℕ i ≡ toℕ j → Ordering i j
-  greater : ∀ {i j} → toℕ j < toℕ i < n → Ordering i j
-
-compare : ∀ {n : ℕ} (i j : Fin n) → Ordering i j
-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)
-... | equal i≡j = equal (cong ℕ.suc i≡j)
-... | greater (j<i , i<n) = greater (_≤_.s≤s j<i , _≤_.s≤s i<n)
-
 private
   variable
     m n : ℕ
@@ -51,6 +37,23 @@ 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 x , h with compare (h (f (# 0))) (h (g (# 0)))
-...     | less (f0<g0 , _≤_.s≤s g0<n) = x , merge (f0<g0 , g0<n) ∘ h
+...     | less (f0<g0 , s≤s g0<n) = x , merge (f0<g0 , g0<n) ∘ h
 ...     | equal f0≡g0 = ℕ.suc x , h
-...     | greater (g0<f0 , _≤_.s≤s f0<n) = x , merge (g0<f0 , f0<n) ∘ h
+...     | greater (g0<f0 , s≤s f0<n) = x , merge (g0<f0 , f0<n) ∘ h
+
+-- Glue together the image of two finite-set functions, iterative
+glue-iter
+    : {y : ℕ}
+    → (Fin m → Fin y)
+    → (Fin m → Fin y)
+    → (Fin n → Fin y)
+    → Σ[ x ∈ ℕ ] (Fin n → Fin x)
+glue-iter {ℕ.zero} {n} {y} f g h = y , h
+glue-iter {ℕ.suc m} {n} {y} f g h with compare (f (# 0)) (g (# 0))
+... | less (f0<g0 , s≤s g0<n) =
+        let p = merge (f0<g0 , g0<n) in
+        glue-iter (p ∘ f ∘ Fin.suc) (p ∘ g ∘ Fin.suc) (p ∘ h)
+... | equal _ = glue-iter (f ∘ Fin.suc) (g ∘ Fin.suc) h
+... | greater (g0<f0 , s≤s f0<n) =
+        let p = merge (g0<f0 , f0<n) in
+        glue-iter (p ∘ f ∘ Fin.suc) (p ∘ g ∘ Fin.suc) (p ∘ h)
diff --git a/Util.agda b/Util.agda
index 23da7cc..b30aeb5 100644
--- a/Util.agda
+++ b/Util.agda
@@ -2,7 +2,8 @@ module Util where
 
 open import Data.Fin using (Fin; toℕ)
 open import Data.Nat using (ℕ; _≤_; _<_ ; z<s; s≤s)
-open import Data.Product using (_×_)
+open import Data.Product using (_×_; _,_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
 
 
 _<_≤_ : ℕ → ℕ → ℕ → Set
@@ -14,3 +15,17 @@ _<_<_ i j k = (i < j) × (j < k)
 toℕ< : {n : ℕ} → (i : Fin n) → toℕ i < n
 toℕ< Fin.zero = z<s
 toℕ< (Fin.suc i) = s≤s (toℕ< i)
+
+data Ordering {n : ℕ} : Fin n → Fin n → Set where
+  less : ∀ {i j} → toℕ i < toℕ j < n → Ordering i j
+  equal : ∀ {i j} → i ≡ j → Ordering i j
+  greater : ∀ {i j} → toℕ j < toℕ i < n → Ordering i j
+
+compare : ∀ {n : ℕ} (i j : Fin n) → Ordering i j
+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)
+... | equal i≡j = equal (cong Fin.suc i≡j)
+... | greater (j<i , i<n) = greater (_≤_.s≤s j<i , _≤_.s≤s i<n)
-- 
cgit v1.2.3