diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2024-02-22 11:22:01 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2024-02-22 11:22:01 -0600 |
| commit | d65d60fe31f0c25c7e845d66e37c47e4f22924e1 (patch) | |
| tree | 42d06990994e4ca34b42be5dd669b149d21ff67b | |
| parent | 94a6a0f847a2a1c02347bead7901656e4bd33fdb (diff) | |
Fill in omitted proof
| -rw-r--r-- | FinMerge.agda | 8 | ||||
| -rw-r--r-- | FinMerge/Properties.agda | 18 |
2 files changed, 21 insertions, 5 deletions
diff --git a/FinMerge.agda b/FinMerge.agda index 2e0ad03..51e7a67 100644 --- a/FinMerge.agda +++ b/FinMerge.agda @@ -50,10 +50,10 @@ glue-iter → Σ[ 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 +... | 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 +... | 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/FinMerge/Properties.agda b/FinMerge/Properties.agda index 6d6c964..e403d99 100644 --- a/FinMerge/Properties.agda +++ b/FinMerge/Properties.agda @@ -111,7 +111,23 @@ glue-iter-append → (f g : Fin m → Fin y) → (h : Fin n → Fin y) → Σ[ h′ ∈ (Fin y → Fin (proj₁ (glue-iter f g h))) ] (proj₂ (glue-iter f g h) ≡ h′ ∘ h) -glue-iter-append f g h = ? +glue-iter-append {ℕ.zero} f g h = id , refl +glue-iter-append {ℕ.suc m} f g h with compare (f (# 0)) (g (# 0)) +glue-iter-append {ℕ.suc m} f g h | less (f0<g0 , s≤s g0≤n) + with + glue-iter-append + (merge (f0<g0 , g0≤n) ∘ f ∘ Fin.suc) + (merge (f0<g0 , g0≤n) ∘ g ∘ Fin.suc) + (merge (f0<g0 , g0≤n) ∘ h) +... | h′ , glue-p∘h≡h′∘p∘h = h′ ∘ merge (f0<g0 , g0≤n) , glue-p∘h≡h′∘p∘h +glue-iter-append {ℕ.suc m} f g h | equal x = glue-iter-append (f ∘ Fin.suc) (g ∘ Fin.suc) h +glue-iter-append {ℕ.suc m} f g h | greater (g0<f0 , s≤s f0≤n) + with + glue-iter-append + (merge (g0<f0 , f0≤n) ∘ f ∘ Fin.suc) + (merge (g0<f0 , f0≤n) ∘ g ∘ Fin.suc) + (merge (g0<f0 , f0≤n) ∘ h) +... | h′ , glue-p∘h≡h′∘p∘h = h′ ∘ merge (g0<f0 , f0≤n) , glue-p∘h≡h′∘p∘h lemma₂ : (f g : Fin (ℕ.suc m) → Fin n) |