1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
|
{-# OPTIONS --without-K --safe #-}
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≤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₁; proj₂)
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; map)
open import Util using (_<_<_; _<_≤_; toℕ<; Ordering; less; equal; greater; compare)
private
variable
m n : ℕ
-- 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) = 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)
-- Left-adjoint to merge
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)
-- Merge and unmerge
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)
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 (compare (h (f (# 0))) (h (g (# 0)))))
-- 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} {ℕ.zero} f g h = ⊥-elim (¬Fin0 (f (# 0)))
glue-iter {ℕ.suc m} {n} {ℕ.suc y} f g h =
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)
|
