Неверно набранный с/переписать обессахариванием

Фон — это тип данных конечных карт, упорядоченных по ключам, как упоминалось в этом предыдущем вопросе:

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

Правильно ли я действую, то есть использую with и rewrite для уточнения контекста до такой степени, что я могу начать доказывать конкретные случаи? (Из этот вопрос, я думаю, что ответ, вероятно, да.) Если да, то в чем причина проблемы?


pattern-matching proof agda equations
person Roly    schedule 20.01.2014    source источник

Ответы (1)


arrow_upward
0
arrow_downward

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

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

person Roly    schedule 20.01.2014