agda - 粘性拒绝

Question

这个问题是关于

• 如何帮助 Agda 在解决合一问题时摆脱困境，以及
• 如何说服 Agda 解决“异构约束”(无论那是什么意思)

可以找到我的问题的完整代码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代表成员(member):

  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 和 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 .我不知道使用记录投影而不只是函数是否有助于统一(可能是的，因为如果我们有 proj₁ p == x 和 proj₂ p == y 这样的在你的情况下，然后 p == x , y 并且没有歧义)，但在一般情况下统一必须卡住并且它不是缺陷。参见 this一些解释。