第III類型與/的rewrite脫糖

的背景是由按鍵有序的有限地圖的數據類型，如本previous question提到：第III類型與/的rewrite脫糖

open import Function 
open import Relation.Binary renaming (IsEquivalence to IsEq) 
open import Relation.Binary.PropositionalEquality as P using (_≡_) 

module Data.Temp 
    {k v ℓ ℓ′} 
    {Key : Set k} 
    (Value : Set v) 
    {_<_ : Rel Key ℓ} 
    (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) 
    where 

    open import Algebra.FunctionProperties 
    open import Data.Product 
    open IsStrictTotalOrder isStrictTotalOrder 
    open import Level 

    KV : Set (k ⊔ v) 
    KV = Key × Value 

    -- Adapted from the sorted lists presented in Why Dependent Types Matter (Altenkirch, Mcbride & McKinna). 
    -- The lower bound is not tight. 
    data FiniteMap (l : Key) : Set (k ⊔ v ⊔ ℓ) where 
     [] : FiniteMap l 
     _∷[_]_ : (kv : KV) → let k = proj₁ kv in l < k → (m : FiniteMap k) → FiniteMap l 

    infixr 3 _∷[_]_ 

    -- Split into two definitions to help the termination checker. 
    unionWith : ∀ {l} → Op₂ Value → Op₂ (FiniteMap l) 
    unionWith′ : ∀ {l} → Op₂ Value → (kv : KV) → let k = proj₁ kv in l < k → FiniteMap k → Op₁ (FiniteMap l) 

    unionWith _ [] [] = [] 
    unionWith _ [] m = m 
    unionWith _ m [] = m 
    unionWith ∙ (k , v ∷[ k<l ] m) (k′ , v′ ∷[ k′<l ] m′) with compare k k′ 
    ... | tri< k<k′ _ _ = k , v ∷[ k<l ] unionWith ∙ m (k′ , v′ ∷[ k<k′ ] m′) 
    ... | tri≈ _ k≡k′ _ rewrite P.sym k≡k′ = k , (v ⟨ ∙ ⟩ v′) ∷[ k<l ] unionWith ∙ m m′ 
    ... | tri> _ _ k′<k = k′ , v′ ∷[ k′<l ] unionWith′ ∙ (k , v) k′<k m m′ 

    unionWith′ _ (k , v) l<k m [] = k , v ∷[ l<k ] m 
    unionWith′ ∙ (k , v) l<k m (k′ , v′ ∷[ k′<l ] m′) with compare k k′ 
    ... | tri< k<k′ _ _ = k , v ∷[ l<k ] unionWith ∙ m (k′ , v′ ∷[ k<k′ ] m′) 
    ... | tri≈ _ k≡k′ _ rewrite P.sym k≡k′ = k , (v ⟨ ∙ ⟩ v′) ∷[ l<k ] unionWith ∙ m m′ 
    ... | tri> _ _ k′<k = k′ , v′ ∷[ k′<l ] unionWith′ ∙ (k , v) k′<k m m′

我現在證明，這種類型的構造保留任何交換感興趣A上的幺半羣結構，其中有限映射的幺半羣運算爲unionWith ∙（其中∙是底層幺半羣的交換操作）。我應該指出，雖然unionWith ∙顯然是可交換的，直至清除地圖中的邊界，但我還不確定它是否「在鼻子上」，即也考慮了邊界。

所以，這告誡不談，我遇到了一個錯誤信息想在我試圖證明說出一個精緻的目標。下面是證明的骨架，有問題的位註釋掉：

comm : ∀ {l} (∙ : Op₂ Value) → Commutative _≡_ ∙ → 
           Commutative _≡_ (unionWith {l} ∙) 
comm ∙ _ [] [] = P.refl 
comm ∙ _ [] (_ ∷[ _ ] _) = P.refl 
comm ∙ _ (_ ∷[ _ ] _) [] = P.refl 
comm {l} ∙ _ (k , v ∷[ k<l ] m) (k′ , v′ ∷[ k′<l ] m′) with compare k k′ 
... | tri< _ _ _ = {!!} 
... | tri≈ _ k≡k′ _ {- rewrite P.sym k≡k′ -} = {!!} 
... | tri> _ _ _ = {!!}

，這裏是成品的目標，我想能夠插入的k≡k′情況：

begin 
    k , (v ⟨ ∙ ⟩ v′) ∷[ l<k ] unionWith ∙ m m′ 
    ≡⟨ ? ⟩ 
    unionWith ∙ (k′ , v′ ∷[ k′<l ] m′) (k , v ∷[ k<l ] m) 
    ∎ where 
    open import Relation.Binary.EqReasoning (P.setoid (FiniteMap l))

但對於這很好的類型，我需要k≡k'。按照unionWith的定義，我想在上面的代碼中插入註釋掉的rewrite P.sym k≡k′。

不幸的是我然後得到一個相當惡劣的錯誤消息：

k′ != w of type Key 
when checking that the type [scary stuff] 
≡ 
(unionWith Value isStrictTotalOrder ∙ (w , v′ ∷[ k′<l ] m′) 
(k₁ , v₁ ∷[ k<l ] m) 
| compare w k₁) 
of the generated with function is well-formed.

with錯誤信息的質量問題進行了討論here。當然，錯誤信息的質量並不是我的直接擔憂，但它並沒有幫助我理解我在這裏做錯了什麼。

我是否正在以大致正確的方式進行操作，即使用with和rewrite來改進我的背景以使我可以開始證明特定情況？（從this question，我認爲答案可能是肯定的。）如果是這樣，導致問題的原因是什麼？

來源

2014-01-20 Roly

我要回答我的問題，因爲它似乎我不理解如何正確使用with條款。在k≡k'的情況下，我需要再次給出兩個有限映射的完整模式，而不是僅僅通過「...」重複使用現有模式。然後，我可以將.k代替k，並將類型k≡k'的值與refl相匹配（以證明.k的正確性）。

然後我精緻目標類型的檢查（該版本已經在合適l，∙和Commutative _≡_ ∙範圍）：

 comm′ : Commutative (unionWith ∙) 
    comm′ [] [] = P.refl 
    comm′ [] (_ ∷[ _ ] _) = P.refl 
    comm′ (_ ∷[ _ ] _) [] = P.refl 
    comm′ (k , _ ∷[ _ ] _) (k′ , _ ∷[ _ ] _) with compare k k′ 
    ... | tri< _ _ _ = {!!} 
    comm′ (k , v ∷[ k<l ] m) (.k , v′ ∷[ k′<l ] m′) | tri≈ _ P.refl _ = 
     begin 
      k , (v ⟨ ∙ ⟩ v′) ∷[ k<l ] unionWith ∙ m m′ 
     ≡⟨ {!!} ⟩ 
      unionWith ∙ (k , v′ ∷[ k′<l ] m′) (k , v ∷[ k<l ] m) 
     ∎ 
    ... | tri> _ _ _ = {!!}

千萬人認爲原來的問題仍然是有用的？否則我可以刪除它。

來源

2014-01-20 17:52:33 Roly

第III類型與/的rewrite脫糖

回答

相關問題