Unresolved meta-variables in equivalence proof

Question

I'm trying to derive a commutative monoid of AVL trees of element type A, given a commutative monoid (A, +, epsilon), where the derived operation is unionWith +. The notion of equivalence for AVL trees is such that two trees are equal iff they have the same toList image.

I'm stuck trying to prove that unionWith + is associative (up to my notion of equivalence). I have commutativity and +-cong as postulates, because I want to use them in the proof of associativity, but haven't yet proved them.

I've isolated the problem to the term bibble in the following code:

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

In bibble, I have a proof that z ≈ z (namely refl), and also a proof that x ∪ tree (Indexed.leaf l<u) ≈ (tree (Indexed.leaf l<u)) ∪ x (by commutativity), and I believe I should then be able to use ∙-cong to derive a proof that the union of the ≈ arguments is also ≈.

However, the compiler seems to be left with some unresolved meta-variables, and unfortunately I don't really understand how to read the messages. Am I just doing something wrong (proof-wise), or do I just need to make some arguments explicit, or what?

Vitus Vitus · Accepted Answer · 2013-12-31T22:38:04

The proof is fine, only the compiler needs few more hints. Implicit arguements are filled in by unification and while it can do some cool stuff, sometimes you have to help it out and push it in the right direction.

Let's take a look at the definition of Preserves₂:

_Preserves₂_⟶_⟶_ :
  ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c} →
  (A → B → C) → Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → Set _
_+_ Preserves₂ P ⟶ Q ⟶ R =
  ∀ {x y u v} → P x y → Q u v → R (x + u) (y + v)

If we specialize it to _+_ = _∪_ and P, Q, R = _≈_, we get:

∀ {x y u v} → x ≈ y → u ≈ v → (x ∪ u) ≈ (y ∪ v)

There are four implicit arguments, let's fill in some of them and watch what happens:

bibble = ∙-cong
  {x = x ∪ tree (Indexed.leaf l<u)}
  (comm x (tree (Indexed.leaf l<u)))
  refl

Nope, it's still yellow. Apparently, knowing only x is not enough. Now y:

bibble = ∙-cong
  {x = x ∪ tree (Indexed.leaf l<u)}
  {y = tree (Indexed.leaf l<u) ∪ x}
  (comm x (tree (Indexed.leaf l<u)))
  refl

And that's it! Giving x and y explicitly was enough for the compiler to figure out u and v.

Also, I wrote something about implicit arguments in this answer, you might want to check that out.

Anyways, the "unsolved meta" error messages are indeed a bit scary (and usually not very helpful), what I usually do is something like this:

    bibble = ∙-cong
      {?} {?} {?} {?}
      (comm x (tree (Indexed.leaf l<u)))
      refl

That is, I just prepare holes for all (or the most relevant) implicit arguments and fill them one by one until the compiler is happy.

Unresolved meta-variables in equivalence proof

1 Answers