Липкий отказ

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 представлять членство:

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 = {!!} 

Первая ошибка возникает, когда я пытаюсь к разложению на k∈t уравнения, включая (node ... ∼+):

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 = {!!} 

Агда говорит мне, что он застревает, делая унификацию, но мне непонятно, почему и как помочь. В работе a response to a similar question Ульф предложил сначала разбить случай на другую переменную. Таким образом, в настоящее время работает вручную, я сосредотачиваюсь на случай расщепления на ∼+ линии от 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 _ _ _ = ? 

К сожалению. Теперь Агда идет от жалобы, что она застряла, решив отказаться. Что тут происходит? Можно ли указать уравнения уравнений, по крайней мере, так же подробно, как и в случае refuse5 , а также случай, разбитый на k∈t? Если да, то как?

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, потому что иначе Агда выведет, что h - proj₁ b, и это proj₁ сделало бы Агду несчастной.

Наличие «зеленых слизей» - определенные функции в типах возвратов конструкторов - знак опасности.

Есть по крайней мере два других метода, чтобы победить зеленую слизь, но они слишком сложны для этого случая. Вы можете найти обсуждение here. Я не знаю, должно ли использование проекций записи вместо просто функций должно помогать унификации (возможно, да, поскольку, если у нас есть proj₁ p == x и proj₂ p == y, как в вашем случае, то p == x , y и нет никакой двусмысленности), но в общем случае объединение должно зависеть, и это не дефект. См. this для некоторых объяснений.