diff options
| -rw-r--r-- | FinMerge/Properties.agda | 259 |
1 files changed, 148 insertions, 111 deletions
diff --git a/FinMerge/Properties.agda b/FinMerge/Properties.agda index c250abb..5f92905 100644 --- a/FinMerge/Properties.agda +++ b/FinMerge/Properties.agda @@ -2,25 +2,30 @@ module FinMerge.Properties where open import Data.Empty using (⊥-elim) -open import Data.Fin using (Fin; fromℕ<; toℕ; #_; lower₁) +open import Data.Fin using (Fin; fromℕ<; toℕ; #_; lower₁; _↑ˡ_; cast) 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.Nat.Properties using (≤-trans; <⇒≢; <-cmp) 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; map; nothing; just; fromMaybe) open import Function using (id; _∘_) +open import Relation.Binary.Definitions using (tri<; tri≈; tri>) open import Util using (_<_<_; _<_≤_; toℕ<; Ordering; less; equal; greater; compare) -open import FinMerge using (merge; unmerge; pluck; glue-once; glue-unglue-once; glue-iter) +open import FinMerge using (merge; unmerge; pluck; glue-once; glue-unglue-once; glue-iter; unpluck) private variable m n : ℕ +s≡s⁻¹ : {j k : ℕ} → ℕ.suc j ≡ ℕ.suc k → j ≡ k +s≡s⁻¹ {ℕ.zero} {ℕ.zero} _ = refl +s≡s⁻¹ {ℕ.suc j} {ℕ.suc .j} refl = refl + not-n : {x : Fin (ℕ.suc n)} → toℕ x < m ≤ n → n ≢ toℕ x not-n (x<m , m≤n) n≡x = <⇒≢ (≤-trans x<m m≤n) (sym n≡x) @@ -38,7 +43,7 @@ pluck-< {_} {_} {Fin.suc x} (s≤s m≤n) (s≤s x<m) = ≡ ≡ = begin pluck (s≤s m≤n) (Fin.suc x) ≡⟨⟩ Data.Maybe.Base.map Fin.suc (pluck m≤n x) - ≡⟨ cong (Data.Maybe.Base.map Fin.suc) (pluck-< m≤n x<m) ⟩ + ≡⟨ cong (map Fin.suc) (pluck-< m≤n x<m) ⟩ Data.Maybe.Base.map Fin.suc (just (lower₁ x (not-n (x<m , m≤n)))) ≡⟨⟩ just (Fin.suc (lower₁ x (not-n (x<m , m≤n)))) ≡⟨⟩ just (lower₁ (Fin.suc x) (not-n (s≤s x<m , s≤s m≤n))) ∎ @@ -55,9 +60,8 @@ pluck-≡ {_} {_} {Fin.suc x} (s≤s m≤n) refl = ≡ ≡ : pluck (s≤s m≤n) (Fin.suc x) ≡ nothing ≡ = begin pluck (s≤s m≤n) (Fin.suc x) ≡⟨⟩ - Data.Maybe.Base.map Fin.suc (pluck m≤n x) - ≡⟨ cong (Data.Maybe.Base.map Fin.suc) (pluck-≡ m≤n refl) ⟩ - Data.Maybe.Base.map Fin.suc nothing ≡⟨⟩ + map Fin.suc (pluck m≤n x) ≡⟨ cong (map Fin.suc) (pluck-≡ m≤n refl) ⟩ + map Fin.suc nothing ≡⟨⟩ nothing ∎ i-to-i @@ -160,135 +164,168 @@ lemma₂ {_} {ℕ.suc n} f g = ≡ where open ≡-Reasoning -j-to-i′ - : {i : ℕ} - → {j : Fin (ℕ.suc n)} - → ((i<j , j≤n) : i < toℕ j ≤ n) - → merge (i<j , j≤n) j ≡ fromℕ< (≤-trans i<j j≤n) -j-to-i′ (i<j , j≤n) = cong (fromMaybe (fromℕ< (≤-trans i<j j≤n))) (j-to-nothing j≤n) +merge-unmerge-< + : {i j k : Fin (ℕ.suc n)} + → (i<j≤n : toℕ i < toℕ j ≤ n) + → (k<j : toℕ k < toℕ j) + → unmerge i<j≤n (merge i<j≤n k) ≡ k +merge-unmerge-< {_} {_} {_} {k} i<j≤n@(i<j , j≤n) k<j = let open ≡-Reasoning in begin + unmerge i<j≤n (merge i<j≤n k) ≡⟨ cong (unmerge i<j≤n ∘ (fromMaybe (fromℕ< (≤-trans i<j j≤n)))) (k-to-just (k<j , j≤n)) ⟩ + unmerge i<j≤n (fromℕ< (≤-trans k<j j≤n)) ≡⟨⟩ + unpluck j≤n (just (fromℕ< (≤-trans k<j j≤n))) ≡⟨ unpluck-k-< j≤n k<j ⟩ + k ∎ + where + k-to-just + : {j k : Fin (ℕ.suc m)} ((k<j , j≤m) : toℕ k < toℕ j ≤ m) + → pluck j≤m k ≡ just (fromℕ< (≤-trans k<j j≤m)) + k-to-just {ℕ.suc m} {Fin.suc j} {Fin.zero} (s≤s k<j , s≤s j≤m) = refl + k-to-just {ℕ.suc m} {Fin.suc j} {Fin.suc k} (s≤s k<j , s≤s j≤m) = cong (map Fin.suc) (k-to-just (k<j , j≤m)) + unpluck-k-< + : {j k : Fin (ℕ.suc m)} (j≤m : toℕ j ≤ m) (k<j : toℕ k < toℕ j) + → unpluck j≤m (just (fromℕ< (≤-trans k<j j≤m))) ≡ k + unpluck-k-< {ℕ.suc m} {Fin.suc j} {Fin.zero} (s≤s j≤m) (s≤s k<j) = refl + unpluck-k-< {ℕ.suc m} {Fin.suc j} {Fin.suc k} (s≤s j≤m) (s≤s k<j) = cong Fin.suc (unpluck-k-< j≤m k<j) + +merge-unmerge-= + : {i j k : Fin (ℕ.suc n)} + → (i<j≤n : toℕ i < toℕ j ≤ n) + → k ≡ j + → unmerge i<j≤n (merge i<j≤n k) ≡ i +merge-unmerge-= {_} {i} {j} {k} i<j≤n@(i<j , j≤n) k≡j = let open ≡-Reasoning in begin + unmerge i<j≤n (merge i<j≤n k) ≡⟨ cong (unmerge i<j≤n ∘ merge i<j≤n) k≡j ⟩ + unmerge i<j≤n (merge i<j≤n j) ≡⟨ cong (unmerge i<j≤n ∘ fromMaybe (fromℕ< (≤-trans i<j j≤n))) (j-to-nothing j≤n) ⟩ + unmerge i<j≤n (fromℕ< (≤-trans i<j j≤n)) ≡⟨ unmerge-i i<j≤n ⟩ + i ∎ where j-to-nothing : {j : Fin (ℕ.suc n)} → (j≤n : toℕ j ≤ n) → pluck j≤n j ≡ nothing j-to-nothing {ℕ.zero} {Fin.zero} z≤n = refl j-to-nothing {ℕ.suc n} {Fin.zero} z≤n = refl j-to-nothing {ℕ.suc n} {Fin.suc j} (s≤s j≤n) = cong (map Fin.suc) (j-to-nothing j≤n) + unmerge-i + : {i j : Fin (ℕ.suc n)} ((i<j , j≤n) : toℕ i < toℕ j ≤ n) + → unmerge (i<j , j≤n) (fromℕ< (≤-trans i<j j≤n)) ≡ i + unmerge-i {ℕ.suc n} {Fin.zero} {Fin.suc j} (s≤s i<j , s≤s j≤n) = refl + unmerge-i {ℕ.suc n} {Fin.suc i} {Fin.suc j} (s≤s i<j , s≤s j≤n) = cong Fin.suc (unmerge-i (i<j , j≤n)) -unmerge-i - : {i j : Fin (ℕ.suc n)} - → ((i<j , j≤n) : toℕ i < toℕ j ≤ n) - → unmerge (i<j , j≤n) (fromℕ< (≤-trans i<j j≤n)) ≡ i -unmerge-i {ℕ.suc n} {Fin.zero} {Fin.suc j} (s≤s i<j , s≤s j≤n) = refl -unmerge-i {ℕ.suc n} {Fin.suc i} {Fin.suc j} (s≤s i<j , s≤s j≤n) = cong Fin.suc (unmerge-i (i<j , j≤n)) - -unmerge-k-< - : {i j k : Fin (ℕ.suc n)} - → ((i<j , j≤n) : toℕ i < toℕ j ≤ n) - → (k<j : toℕ k < toℕ j) - → unmerge (i<j , j≤n) (fromℕ< (≤-trans k<j j≤n)) ≡ k -unmerge-k-< {ℕ.suc n} {i} {Fin.suc j} {Fin.zero} (_ , s≤s j≤n) (s≤s k<j) = refl -unmerge-k-< {ℕ.suc n} {Fin.zero} {Fin.suc (Fin.suc j)} {Fin.suc k} (s≤s z≤n , s≤s j≤n) (s≤s k<j) = cong Fin.suc (unmerge-k-< (s≤s z≤n , j≤n) k<j) -unmerge-k-< {ℕ.suc n} {Fin.suc i} {Fin.suc j} {Fin.suc k} (s≤s i<j , s≤s j≤n) (s≤s k<j) = cong Fin.suc (unmerge-k-< (i<j , j≤n) k<j) - -k-to-k-< +merge-unmerge-> : {i j k : Fin (ℕ.suc n)} - → ((i<j , j≤n) : toℕ i < toℕ j ≤ n) - → (k<j : toℕ k < toℕ j) - → merge (i<j , j≤n) k ≡ fromℕ< (≤-trans k<j j≤n) -k-to-k-< (i<j , j≤n) k<j = cong (fromMaybe (fromℕ< (≤-trans i<j j≤n))) (k-to-just (k<j , j≤n)) - where - k-to-just - : {j k : Fin (ℕ.suc n)} - → ((k<j , j≤n) : toℕ k < toℕ j ≤ n) - → pluck j≤n k ≡ just (fromℕ< (≤-trans k<j j≤n)) - k-to-just {ℕ.suc n} {Fin.suc j} {Fin.zero} (s≤s k<j , s≤s j≤n) = refl - k-to-just {ℕ.suc n} {Fin.suc j} {Fin.suc k} (s≤s k<j , s≤s j≤n) = cong (map Fin.suc) (k-to-just (k<j , j≤n)) - -sk-to-k-> - : {i j : Fin (ℕ.suc n)} - → {k : Fin n} - → ((i<j , j≤n) : toℕ i < toℕ j ≤ n) - → (j<sk : toℕ j < ℕ.suc (toℕ k)) - → merge (i<j , j≤n) (Fin.suc k) ≡ k -sk-to-k-> (i<j , j≤n) j<sk = cong (fromMaybe (fromℕ< (≤-trans i<j j≤n))) (sk-to-just j≤n j<sk) + → (i<j≤n : toℕ i < toℕ j ≤ n) + → (j<k : toℕ j < toℕ k) + → unmerge i<j≤n (merge i<j≤n k) ≡ k +merge-unmerge-> {n} {i} {j} {Fin.suc k} i<j≤n@(i<j , j≤n) j<k = let open ≡-Reasoning in begin + unmerge i<j≤n (merge i<j≤n (Fin.suc k)) ≡⟨⟩ + unmerge i<j≤n + (fromMaybe + (fromℕ< (≤-trans i<j j≤n)) + (pluck j≤n (Fin.suc k))) ≡⟨ cong (unmerge i<j≤n ∘ fromMaybe (fromℕ< (≤-trans i<j j≤n))) (sk-to-just j≤n j<k) ⟩ + unmerge i<j≤n k ≡⟨⟩ + unpluck j≤n (just k) ≡⟨ unpluck-k-> j≤n j<k ⟩ + Fin.suc k ∎ where sk-to-just - : {n : ℕ} - → {j : Fin (ℕ.suc n)} - → {k : Fin n} - → (j≤n : toℕ j ≤ n) - → (j<sk : toℕ j < ℕ.suc (toℕ k)) + : {n : ℕ} {j : Fin (ℕ.suc n)} {k : Fin n} (j≤n : toℕ j ≤ n) (j<sk : toℕ j < ℕ.suc (toℕ k)) → pluck j≤n (Fin.suc k) ≡ just k sk-to-just {ℕ.suc _} {Fin.zero} {Fin.zero} z≤n (s≤s _) = refl sk-to-just {ℕ.suc _} {Fin.zero} {Fin.suc _} z≤n (s≤s _) = refl sk-to-just {ℕ.suc _} {Fin.suc _} {Fin.suc _} (s≤s j≤n) (s≤s j<sk) = cong (map Fin.suc) (sk-to-just j≤n j<sk) + unpluck-k-> + : {j : Fin (ℕ.suc m)} {k : Fin m} (j≤m : toℕ j ≤ m) (j<sk : toℕ j < ℕ.suc (toℕ k)) + → unpluck j≤m (just k) ≡ Fin.suc k + unpluck-k-> {ℕ.suc m} {Fin.zero} {_} z≤n (s≤s j<sk) = refl + unpluck-k-> {ℕ.suc m} {Fin.suc j} {Fin.suc k} (s≤s j≤m) (s≤s j<sk) = cong Fin.suc (unpluck-k-> j≤m j<sk) -unmerge-k-> - : {i j : Fin (ℕ.suc n)} - → {k : Fin n} - → ((i<j , j≤n) : toℕ i < toℕ j ≤ n) - → (j<sk : toℕ j < ℕ.suc (toℕ k)) - → unmerge (i<j , j≤n) k ≡ Fin.suc k -unmerge-k-> {ℕ.suc n} {Fin.zero} {Fin.suc Fin.zero} {Fin.suc k} (s≤s z≤n , s≤s z≤n) (s≤s j<sk) = refl -unmerge-k-> {ℕ.suc n} {Fin.zero} {Fin.suc (Fin.suc j)} {Fin.suc k} (s≤s z≤n , s≤s j≤n) (s≤s j<sk) = cong Fin.suc (unmerge-k-> (s≤s z≤n , j≤n) j<sk) -unmerge-k-> {ℕ.suc n} {Fin.suc i} {Fin.suc j} {Fin.suc k} (s≤s i<j , s≤s j≤n) (s≤s j<sk) = cong Fin.suc (unmerge-k-> (i<j , j≤n) j<sk) - -unmerge-merge-< +merge-unmerge : {i j k : Fin (ℕ.suc n)} → (i<j≤n : toℕ i < toℕ j ≤ n) + → (f : Fin (ℕ.suc n) → Fin m) + → f i ≡ f j + → f (unmerge i<j≤n (merge i<j≤n k)) ≡ f k +merge-unmerge {n} {m} {i} {j} {k} i<j≤n f fi≡fj with compare k j +... | less (k<j , _) = cong f (merge-unmerge-< i<j≤n k<j) +... | equal k≡j = let open ≡-Reasoning in begin + f (unmerge i<j≤n (merge i<j≤n k)) ≡⟨ cong f (merge-unmerge-= i<j≤n k≡j) ⟩ + f i ≡⟨ fi≡fj ⟩ + f j ≡⟨ cong f (sym k≡j) ⟩ + f k ∎ +... | greater (j<k , _) = cong f (merge-unmerge-> i<j≤n j<k) + +unmerge-merge-< + : {i j : Fin (ℕ.suc n)} + → {k : Fin n} + → (i<j≤n@(i<j , j≤n) : toℕ i < toℕ j ≤ n) → (k<j : toℕ k < toℕ j) - → unmerge i<j≤n (merge i<j≤n k) ≡ k -unmerge-merge-< {n} {i} {j} {k} i<j≤n@(_ , j≤n) k<j = ≡ + → merge i<j≤n (unmerge i<j≤n k) ≡ k +unmerge-merge-< {n} {i} {j} {k} i<j≤n@(i<j , j≤n) k<j = let open ≡-Reasoning in begin + merge i<j≤n (unmerge i<j≤n k) ≡⟨⟩ + merge i<j≤n (unpluck j≤n (just k)) ≡⟨⟩ + fromMaybe + (fromℕ< (≤-trans i<j j≤n)) + (pluck j≤n (unpluck j≤n (just k))) ≡⟨ cong (fromMaybe (fromℕ< (≤-trans i<j j≤n))) (unpluck-pluck-< j≤n k<j) ⟩ + fromMaybe (fromℕ< (≤-trans i<j j≤n)) (just k) ≡⟨⟩ + k ∎ where - open ≡-Reasoning - ≡ : unmerge i<j≤n (merge i<j≤n k) ≡ k - ≡ = begin - unmerge i<j≤n (merge i<j≤n k) ≡⟨ cong (unmerge i<j≤n) (k-to-k-< i<j≤n k<j) ⟩ - unmerge i<j≤n (fromℕ< (≤-trans k<j j≤n)) ≡⟨ unmerge-k-< i<j≤n k<j ⟩ - k ∎ + unpluck-pluck-< + : {j : Fin (ℕ.suc m)} + → {k : Fin m} + → (j≤m : toℕ j ≤ m) + → (k<j : toℕ k < toℕ j) + → pluck j≤m (unpluck j≤m (just k)) ≡ just k + unpluck-pluck-< {ℕ.suc m} {Fin.suc j} {Fin.zero} (s≤s j≤m) (s≤s k<j) = refl + unpluck-pluck-< {ℕ.suc m} {Fin.suc j} {Fin.suc k} (s≤s j≤m) (s≤s k<j) = cong (map Fin.suc) (unpluck-pluck-< j≤m k<j) unmerge-merge-= - : {i j k : Fin (ℕ.suc n)} - → (i<j≤n : toℕ i < toℕ j ≤ n) - → k ≡ j - → unmerge i<j≤n (merge i<j≤n k) ≡ i -unmerge-merge-= {_} {i} {j} {k} i<j≤n@(i<j , j≤n) k≡j = ≡ + : {i j : Fin (ℕ.suc n)} + → {k : Fin n} + → (i<j≤n@(i<j , j≤n) : toℕ i < toℕ j ≤ n) + → toℕ k ≡ toℕ j + → merge i<j≤n (unmerge i<j≤n k) ≡ k +unmerge-merge-= {_} {i} {j} {k} i<j≤n@(i<j , j≤n) k≡j = let open ≡-Reasoning in begin + merge i<j≤n (unmerge i<j≤n k) ≡⟨⟩ + fromMaybe + (fromℕ< (≤-trans i<j j≤n)) + (pluck j≤n (unpluck j≤n (just k))) ≡⟨ cong (fromMaybe (fromℕ< (≤-trans i<j j≤n))) (unpluck-pluck-= j≤n k≡j) ⟩ + fromMaybe (fromℕ< (≤-trans i<j j≤n)) (just k) ≡⟨⟩ + k ∎ where - open ≡-Reasoning - ≡ : unmerge i<j≤n (merge i<j≤n k) ≡ i - ≡ = begin - unmerge i<j≤n (merge i<j≤n k) ≡⟨ cong (unmerge i<j≤n ∘ merge i<j≤n) k≡j ⟩ - unmerge i<j≤n (merge i<j≤n j) ≡⟨ cong (unmerge i<j≤n) (j-to-i′ i<j≤n) ⟩ - unmerge i<j≤n (fromℕ< (≤-trans i<j j≤n)) ≡⟨ unmerge-i i<j≤n ⟩ - i ∎ + unpluck-pluck-= + : {j : Fin (ℕ.suc m)} + → {k : Fin m} + → (j≤m : toℕ j ≤ m) + → toℕ k ≡ toℕ j + → pluck j≤m (unpluck j≤m (just k)) ≡ just k + unpluck-pluck-= {ℕ.suc m} {Fin.zero} {Fin.zero} z≤n k≡j = refl + unpluck-pluck-= {ℕ.suc m} {Fin.suc j} {Fin.suc k} (s≤s j≤m) k≡j = cong (map Fin.suc) (unpluck-pluck-= j≤m (s≡s⁻¹ k≡j)) unmerge-merge-> - : {i j k : Fin (ℕ.suc n)} - → (i<j≤n : toℕ i < toℕ j ≤ n) + : {i j : Fin (ℕ.suc n)} + → {k : Fin n} + → (i<j≤n@(i<j , j≤n) : toℕ i < toℕ j ≤ n) → (j<k : toℕ j < toℕ k) - → unmerge i<j≤n (merge i<j≤n k) ≡ k -unmerge-merge-> {n} {i} {j} {Fin.suc k} i<j≤n j<k = ≡ + → merge i<j≤n (unmerge i<j≤n k) ≡ k +unmerge-merge-> {n} {i} {j} {k} i<j≤n@(i<j , j≤n) j<k = let open ≡-Reasoning in begin + merge i<j≤n (unmerge i<j≤n k) ≡⟨⟩ + merge i<j≤n (unpluck j≤n (just k)) ≡⟨⟩ + fromMaybe + (fromℕ< (≤-trans i<j j≤n)) + (pluck j≤n (unpluck j≤n (just k))) ≡⟨ cong (fromMaybe (fromℕ< (≤-trans i<j j≤n))) (unpluck-pluck-> j≤n j<k) ⟩ + fromMaybe (fromℕ< (≤-trans i<j j≤n)) (just k) ≡⟨⟩ + k ∎ where - open ≡-Reasoning - ≡ : unmerge i<j≤n (merge i<j≤n (Fin.suc k)) ≡ Fin.suc k - ≡ = begin - unmerge i<j≤n (merge i<j≤n (Fin.suc k)) ≡⟨ cong (unmerge i<j≤n) (sk-to-k-> i<j≤n j<k) ⟩ - unmerge i<j≤n k ≡⟨ unmerge-k-> i<j≤n j<k ⟩ - Fin.suc k ∎ + unpluck-pluck-> + : {j : Fin (ℕ.suc m)} + → {k : Fin m} + → (j≤m : toℕ j ≤ m) + → (j<k : toℕ j < toℕ k) + → pluck j≤m (unpluck j≤m (just k)) ≡ just k + unpluck-pluck-> {ℕ.suc m} {Fin.zero} {Fin.suc k} z≤n (s≤s j<k) = refl + unpluck-pluck-> {ℕ.suc m} {Fin.suc j} {Fin.suc k} (s≤s j≤m) (s≤s j<k) = cong (map Fin.suc) (unpluck-pluck-> j≤m j<k) unmerge-merge - : {i j k : Fin (ℕ.suc n)} + : {i j : Fin (ℕ.suc n)} + → {k : Fin n} → (i<j≤n : toℕ i < toℕ j ≤ n) - → (f : Fin (ℕ.suc n) → Fin m) - → f i ≡ f j - → f (unmerge i<j≤n (merge i<j≤n k)) ≡ f k -unmerge-merge {n} {m} {i} {j} {k} i<j≤n f fi≡fj with (compare k j) -... | less (k<j , _) = cong f (unmerge-merge-< i<j≤n k<j) -... | greater (j<k , _) = cong f (unmerge-merge-> i<j≤n j<k) -... | equal k≡j = ≡ - where - open ≡-Reasoning - ≡ : f (unmerge i<j≤n (merge i<j≤n k)) ≡ f k - ≡ = begin - f (unmerge i<j≤n (merge i<j≤n k)) ≡⟨ cong f (unmerge-merge-= i<j≤n k≡j) ⟩ - f i ≡⟨ fi≡fj ⟩ - f j ≡⟨ cong f (sym k≡j) ⟩ - f k ∎ + → merge i<j≤n (unmerge i<j≤n k) ≡ k +unmerge-merge {n} {i} {j} {k} i<j≤n with <-cmp (toℕ k) (toℕ j) +... | tri< k<j _ _ = unmerge-merge-< i<j≤n k<j +... | tri≈ _ k≡j _ = unmerge-merge-= i<j≤n k≡j +... | tri> _ _ j<k = unmerge-merge-> i<j≤n j<k |