Жестокое набранный/перезапись desugaring

Question

Фоновый тип данных конечных карт упорядоченных по клавишам, как уже упоминалось в этой previous question:

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′ 

сейчас я заинтересован в доказательстве, что этот конструктор типа сохраняет любой коммутативной моноидальной структуры над А, где моноидная операция для конечных отображений равна 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, я думаю, что ответ, вероятно, да.) Если да, то что вызывает проблему?

Answer 1

Я собираюсь ответить на свой вопрос, поскольку, похоже, я не понимал, как правильно использовать 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> _ _ _ = {!!} 

ли люди думают, что первоначальный вопрос все еще полезен? Я мог бы удалить его в противном случае.