粘性拒绝

Question

这个问题是关于

如何帮助 Agda 在解决统一问题时摆脱困境，以及
如何说服 Agda 解决一个 "heterogeneous constraint"（不管那是什么意思）

可以找到我的问题的完整代码here。我将列出我的代码并最终解决问题。我的项目涉及在 Data.AVL 中证明事情，所以我从一些样板文件开始：

open import Data.Product
open import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

module Data.AVL.Properties-Refuse
  {k v ℓ}
  {Key : Set k} (Value : Key → Set v)
  {_<_ : Rel Key ℓ}
  (isStrictTotalOrder : IsStrictTotalOrder P._≡_ _<_) where

  open import Data.AVL Value isStrictTotalOrder using (KV; module Extended-key; module Height-invariants; module Indexed)
  import Data.AVL Value isStrictTotalOrder as AVL
  open Extended-key                       
  open Height-invariants                  
  open Indexed                            

  open IsStrictTotalOrder isStrictTotalOrder

我再借an idea from Vitus代表会员：

  data _∈_ {lb ub} (K : Key) : ∀ {n} → Tree lb ub n → Set (k ⊔ v ⊔ ℓ) where
    here : ∀ {hˡ hʳ} V
      {l : Tree lb [ K ] hˡ}
      {r : Tree [ K ] ub hʳ}
      {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →
      K ∈ node (K , V) l r (proj₂ b)
    left : ∀ {hˡ hʳ K′} {V : Value K′}
      {l : Tree lb [ K′ ] hˡ}
      {r : Tree [ K′ ] ub hʳ}
      {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →
      K < K′ →
      K ∈ l →
      K ∈ node (K′ , V) l r (proj₂ b)
    right : ∀ {hˡ hʳ K′} {V : Value K′}
      {l : Tree lb [ K′ ] hˡ}
      {r : Tree [ K′ ] ub hʳ}
      {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →
      K′ < K →
      K ∈ r →
      K ∈ node (K′ , V) l r (proj₂ b)

然后我声明一个函数（其含义无关紧要——这是一个更有意义的函数的人为简单版本，此处未显示）：

  refuse1 : ∀ {kₗ kᵤ h}
            ( t : Tree kₗ kᵤ h )
            ( k : Key )
            ( k∈t : k ∈ t ) →
            Set
  refuse1 = {!!}

到目前为止，还不错。现在，我对默认变量进行案例拆分：

  refuse2 : ∀ {kₗ kᵤ h}
            ( t : Tree kₗ kᵤ h )
            ( k : Key )
            ( k∈t : k ∈ t ) →
            Set
  refuse2 t k₁ k∈t = {!!}

现在我分裂 t:

  refuse3 : ∀ {kₗ kᵤ h}
            ( t : Tree kₗ kᵤ h )
            ( k : Key )
            ( k∈t : k ∈ t ) →
            Set
  refuse3 (leaf l<u) k₁ k∈t = {!!}
  refuse3 (node k₁ t t₁ bal) k₂ k∈t = {!!}

现在 bal:

  refuse4 : ∀ {kₗ kᵤ h}
            ( t : Tree kₗ kᵤ h )
            ( k : Key )
            ( k∈t : k ∈ t ) →
            Set
  refuse4 (leaf l<u) k₁ k∈t = {!!}
  refuse4 (node k₁ t t₁ ∼+) k₂ k∈t = {!!}
  refuse4 (node k₁ t t₁ ∼0) k₂ k∈t = {!!}
  refuse4 (node k₁ t t₁ ∼-) k₂ k∈t = {!!}

第一个错误出现在我尝试对包含 (node ... ∼+):

的等式 k∈t 进行大小写拆分时

  refuse5 : ∀ {kₗ kᵤ h}
            ( t : Tree kₗ kᵤ h )
            ( k : Key )
            ( k∈t : k ∈ t ) →
            Set
  refuse5 (leaf l<u) k₁ k∈t = {!!}
  refuse5 (node k₁ t t₁ ∼+) k₂ k∈t = {!k∈t!}
  {- ERROR
    I'm not sure if there should be a case for the constructor here,
    because I get stuck when trying to solve the following unification
    problems (inferred index ≟ expected index):
      {_} ≟ {_}
      node (k₅ , V) l r (proj₂ b) ≟ node k₄
                                    t₂ t₃ ∼+
    when checking that the expression ? has type Set
  -}
  refuse5 (node k₁ t t₁ ∼0) k₂ k∈t = {!!}
  refuse5 (node k₁ t t₁ ∼-) k₂ k∈t = {!!}

Agda 告诉我它在进行统一时卡住了，但我不清楚为什么或如何提供帮助。在 a response to a similar question 中，Ulf 建议首先对另一个变量进行个案拆分。所以，现在手工工作，我专注于从 refuse5 中区分 ∼+ 行并包括许多隐式变量：

  open import Data.Nat.Base as ℕ

  refuse6 : ∀ {kₗ kᵤ h}
            ( t : Tree kₗ kᵤ h )
            ( k : Key )
            ( k∈t : k ∈ t ) →
            Set
  refuse6 {h = ℕ.suc .hˡ}
          (node (k , V) lk ku (∼+ {n = hˡ}))
          .k
          (here {hˡ = .hˡ} {hʳ = ℕ.suc .hˡ} .V {l = .lk} {r = .ku} {b = (ℕ.suc .hˡ , ∼+ {n = .hˡ})}) = {!!}
  {- ERROR
    Refuse to solve heterogeneous constraint proj₂ b :
    n ∼ hʳ ⊔ proj₁ b =?=
    ∼+ : n ∼ ℕ.suc n ⊔ ℕ.suc n
    when checking that the pattern
    here {hˡ = .hˡ} {hʳ = ℕ.suc .hˡ} .V {l = .lk} {r = .ku}
      {b = ℕ.suc .hˡ , ∼+ {n = .hˡ}}
    has type
    k₂ ∈ node (k₁ , V) lk ku ∼+
  -}
  refuse6 _ _ _ = ?

糟糕。现在 Agda 从抱怨它卡住了到彻底拒绝解决。这里发生了什么？是否有可能至少像 refuse5 and also case split on k∈t 一样详细地指定方程的 lhs？如果可以，怎么做？

Answer 1

如评论和 Agda mailing list 中所述，解决方案是将 ∃ 替换为 ∀:

  data _∈_ {lb ub} (K : Key) : ∀ {n} → Tree lb ub n → Set (k ⊔ v ⊔ ℓ) where
    here : ∀ {hˡ hʳ h} V
      {l : Tree lb [ K ] hˡ}
      {r : Tree [ K ] ub hʳ}
      {b : hˡ ∼ hʳ ⊔ h} →
      K ∈ node (K , V) l r b
    ...

不过你也可以这样写

  data _∈_ {lb ub} (K : Key) : ∀ {n} → Tree lb ub n → Set (k ⊔ v ⊔ ℓ) where
    here : ∀ {hˡ hʳ} V
      {l : Tree lb [ K ] hˡ}
      {r : Tree [ K ] ub hʳ}
      {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} {h' b'} →
      h' ≡ proj₁ b →
      b' ≅ proj₂ b →
      K ∈ node {h = h'} (K , V) l r b'
    ...

这是打绿史莱姆的常用技巧，我猜这就是问题的原因。我们需要 b' ≅ proj₂ b 中的异构相等性，否则 Agda 会推断 h 是 proj₁ b，而这个 proj₁ 会让 Agda 不高兴。

The presence of ‘green slime’ — defined functions in the return types of constructors — is a danger sign.

至少还有两种其他方法可以打败绿色粘液，但对于这种情况来说它们太复杂了。您可以找到一些讨论 here. I don't know if using record projections instead of just functions should help unification (probably yes, since if we have proj₁ p == x and proj₂ p == y like in your case, then p == x , y and there is no ambiguity), but in general case unification must stuck and it's not a defect. See 以获得一些解释。

粘性拒绝

A sticky refusal

agda