implicit - 等价证明中未解决的元变量

Question

我正在尝试导出元素类型 A 的 AVL 树的可交换幺半群，给定一个可交换幺半群 (A, +, epsilon)，其中派生运算是unionWith +. AVL 树的等价概念是两棵树相等，如果它们具有相同的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