Add helper function for merging finite sets

8 files changed, 55 insertions, 3 deletions

diff --git a/.gitignore b/.gitignore
index d3e342b..171a389 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1 @@
-.stack-work/
-*~
-circuits.cabal
+*.agdai
diff --git a/FinMerge.agda b/FinMerge.agda
new file mode 100644
index 0000000..a327602
--- /dev/null
+++ b/FinMerge.agda
@@ -0,0 +1,51 @@
+module FinMerge where
+
+open import Data.Fin using (Fin; splitAt; join; fromℕ<; cast)
+open import Data.Nat using (ℕ; _+_; _≤_; _<_)
+open import Data.Nat.Properties using (+-comm)
+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 (_$_)
+
+
+_<_≤_ : ℕ → ℕ → ℕ → Set
+_<_≤_ i j k = (i < j) × (j ≤ k)
+
+_<_<_ : ℕ → ℕ → ℕ → Set
+_<_<_ i j k = (i < j) × (j < k)
+
+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)
+
+-- 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′ ∎
diff --git a/tiny/.gitignore b/tiny/.gitignore
new file mode 100644
index 0000000..d3e342b
--- /dev/null
+++ b/tiny/.gitignore
@@ -0,0 +1,3 @@
+.stack-work/
+*~
+circuits.cabal
diff --git a/Setup.hs b/tiny/Setup.hs
index 9a994af..9a994af 100644
--- a/Setup.hs
+++ b/tiny/Setup.hs
diff --git a/package.yaml b/tiny/package.yaml
index 5793777..5793777 100644
--- a/package.yaml
+++ b/tiny/package.yaml
diff --git a/src/Circuit.hs b/tiny/src/Circuit.hs
index d64e8c1..d64e8c1 100644
--- a/src/Circuit.hs
+++ b/tiny/src/Circuit.hs
diff --git a/stack.yaml b/tiny/stack.yaml
index 3dffb2e..3dffb2e 100644
--- a/stack.yaml
+++ b/tiny/stack.yaml
diff --git a/stack.yaml.lock b/tiny/stack.yaml.lock
index dc9b6b0..dc9b6b0 100644
--- a/stack.yaml.lock
+++ b/tiny/stack.yaml.lock