implicit - 等価証明における未解決のメタ変数

Question

可換モノイド (A, +, イプシロン) を指定して、要素型 A の AVL ツリーの可換モノイドを導出しようとしています。ここで、導出された演算はunionWith +です。AVL ツリーの等価性の概念は、2 つのツリーが同じtoListイメージを持っている場合に等しいというものです。

私はそれunionWith +が連想的であることを証明しようとして立ち往生しています（同等の概念まで）。結合性の証明に使用したいので、交換性と +-cong を公準として持っていますが、まだ証明していません。

bibble問題を次のコードの用語に切り分けました。

module Temp
   {A : Set}
   where

open import Algebra.FunctionProperties
open import Algebra.Structures
import Data.AVL
import Data.Nat.Properties as ℕ-Prop
open import Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

-- Specialise AVL trees to keys of type ℕ.
module ℕ-AVL
   = Data.AVL (const A) (StrictTotalOrder.isStrictTotalOrder ℕ-Prop.strictTotalOrder)

open ℕ-AVL

-- Equivalence of AVL tree normal form (ordered list of key-value pairs).
_≈_ : Tree → Tree → Set
_≈_ = _≡_ on toList

infix 4 _≈_

-- Extend a commutative monoid (A, ⊕, ε) to AVL trees of type A, with union and empty.
comm-monoid-AVL-∪ : {⊕ : Op₂ A} → IsCommutativeMonoid _≈_ (unionWith ⊕) empty
comm-monoid-AVL-∪ {⊕} = record {
      isSemigroup = record {
            isEquivalence = record { refl = refl; sym = sym; trans = trans }; assoc = assoc; ∙-cong = {!!}
         };
      identityˡ = λ _ → refl;
      comm = comm
   } where
      _∪_ = unionWith ⊕

      postulate comm : Commutative _≈_ _∪_

      postulate ∙-cong : _∪_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_

      assoc : Associative _≈_ _∪_
      assoc (tree (Indexed.leaf l<u)) y z = refl
      assoc x (tree (Indexed.leaf l<u)) z =
         let bibble : (x ∪ tree (Indexed.leaf l<u)) ∪ z ≈ ((tree (Indexed.leaf l<u)) ∪ x) ∪ z
             bibble = ∙-cong (comm x (tree (Indexed.leaf l<u))) refl in
         begin
            toList ((x ∪ tree (Indexed.leaf l<u)) ∪ z)
         ≡⟨ bibble ⟩
            toList (((tree (Indexed.leaf l<u)) ∪ x) ∪ z)
         ≡⟨ refl ⟩
            toList (x ∪ z)
         ≡⟨ refl ⟩
            toList (x ∪ ((tree (Indexed.leaf l<u)) ∪ z))
         ∎
      assoc x (tree (Indexed.node kv τ₁ τ₂ bal)) z = {!!} -- TODO

ではbibble、z ≈ z(つまりrefl) の証明と(可換性による) の証明があり、これを使用して ≈ 引数の結合も ≈ であるという証明を導き出すx ∪ tree (Indexed.leaf l<u) ≈ (tree (Indexed.leaf l<u)) ∪ xことができると思います。∙-cong

ただし、コンパイラには未解決のメタ変数がいくつか残っているようで、残念ながらメッセージの読み方がよくわかりません。私は何か間違ったことをしているだけですか(証明に関して)、それともいくつかの引数を明示的にする必要があるだけですか?

Answer 1