diff options
Diffstat (limited to 'FinMerge')
| -rw-r--r-- | FinMerge/Properties.agda | 72 |
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 |