diff options
Diffstat (limited to 'FinMerge')
| -rw-r--r-- | FinMerge/Properties.agda | 62 |
1 files changed, 58 insertions, 4 deletions
diff --git a/FinMerge/Properties.agda b/FinMerge/Properties.agda index 94b8580..6d6c964 100644 --- a/FinMerge/Properties.agda +++ b/FinMerge/Properties.agda @@ -4,14 +4,15 @@ open import Data.Fin using (Fin; fromℕ<; toℕ; #_; lower₁) open import Data.Fin.Properties using (¬Fin0) open import Data.Nat using (ℕ; _+_; _≤_; _<_; z<s; pred; z≤n; s≤s) open import Data.Nat.Properties using (≤-trans; <⇒≢) -open import Data.Product using (_,_) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; _≢_) +open import Data.Product using (_,_; proj₁; proj₂; Σ-syntax) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong-app; sym; _≢_) open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning) open import Data.Maybe.Base using (Maybe; nothing; just; fromMaybe) +open import Function using (id; _∘_) -open import Util using (_<_<_; _<_≤_; toℕ<) +open import Util using (_<_<_; _<_≤_; toℕ<; less; equal; greater; compare) -open import FinMerge using (merge; pluck) +open import FinMerge using (merge; pluck; glue-iter) private @@ -104,3 +105,56 @@ merge-i-j {_} {i} {j} i<j≤n = ≡ merge i<j≤n i ≡⟨ i-to-i i<j≤n ⟩ lower₁ i (not-n i<j≤n) ≡⟨ sym (j-to-i i<j≤n) ⟩ merge i<j≤n j ∎ + +glue-iter-append + : {y : ℕ} + → (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 = ? + +lemma₂ + : (f g : Fin (ℕ.suc m) → Fin n) + → let p = proj₂ (glue-iter f g id) in p (f (# 0)) ≡ p (g (# 0)) +lemma₂ f g with compare (f (# 0)) (g (# 0)) +lemma₂ f g | 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′ , glue≡h′∘h = ≡ + where + open ≡-Reasoning + p = merge (f0<g0 , g0≤n) + 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′ (merge-i-j (f0<g0 , g0≤n)) ⟩ + 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₂ f g | equal f0≡g0 = cong (proj₂ (glue-iter (f ∘ Fin.suc) (g ∘ Fin.suc) id)) f0≡g0 +lemma₂ f g | 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) ∘ id) +... | h′ , glue≡h′∘h = ≡ + where + open ≡-Reasoning + p = merge (g0<f0 , f0≤n) + 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′ (sym (merge-i-j (g0<f0 , f0≤n))) ⟩ + 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) ∎ |