[Agda] A sticky refusal

[Andrea Vezzosi]

Hi Martin,

I'd first split on k∈t so you get less cases, but if you need to match
on the tree first for other reasons there's still a workaround.

When unification gets stuck during pattern matching you have to change
the expressions in the indexes to be more unifiable by turning more of
them into variables, especially those that are not patterns
themselves.

In this case you want to change the side of the unification that comes
from the definition of the datatype, the (proj₂ b) is your problem:

  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ʳ}
      {h : _}
      {b : hˡ ∼ hʳ ⊔ h} →

      K ∈ node (K , V) l r b
    left : ∀ {hˡ hʳ K′} {V : Value K′}
      {l : Tree lb [ K′ ] hˡ}
      {r : Tree [ K′ ] ub hʳ}
      {h : _}
      {b : hˡ ∼ hʳ ⊔ h} →
      K < K′ →
      K ∈ l →
      K ∈ node (K′ , V) l r b
    right : ∀ {hˡ hʳ K′} {V : Value K′}
      {l : Tree lb [ K′ ] hˡ}
      {r : Tree [ K′ ] ub hʳ}
      {h : _}
      {b : hˡ ∼ hʳ ⊔ h} →
      K′ < K →
      K ∈ r →
      K ∈ node (K′ , V) l r b

Now you can pattern match. refuse6 still does not go through, but the
following does

  refuse6 : ∀ {kₗ kᵤ h}
            ( t : Tree kₗ kᵤ h )
            ( k : Key )
            ( k∈t : k ∈ t ) →
            Set
  refuse6 (node (k , V) lk ku (∼+ {n = hˡ})) .k (here ._) = { }19

Cheers,
Andrea


On Sat, Aug 15, 2015 at 5:10 AM, Martin Stone Davis
<martin.stone.davis at gmail.com> wrote:
> NB Crossposted to http://stackoverflow.com/q/32021121/1312174.
>
> This question is about
>
> * how to help Agda get unstuck when solving unification problems, and
> * how to convince Agda to solve a "heterogeneous constraint" (whatever that
> means)
>
> The complete code for my question can be found
> [here](http://lpaste.net/138853). I'll lay out my code and eventually get to
> the question. My project concerns proving things in Data.AVL, so I start
> with some boilerplate for that:
>
>     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
>
> I then borrow [an idea from
> Vitus](http://stackoverflow.com/a/21083647/1312174) to represent membership:
>
>       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)
>
> I then declare a function (whose meaning is irrelevant -- this is a
> contrived and simple version of a more meaningful function not shown here):
>
>       refuse1 : ∀ {kₗ kᵤ h}
>                 ( t : Tree kₗ kᵤ h )
>                 ( k : Key )
>                 ( k∈t : k ∈ t ) →
>                 Set
>       refuse1 = {!!}
>
> So far, so good. Now, I case split on the default variables:
>
>       refuse2 : ∀ {kₗ kᵤ h}
>                 ( t : Tree kₗ kᵤ h )
>                 ( k : Key )
>                 ( k∈t : k ∈ t ) →
>                 Set
>       refuse2 t k₁ k∈t = {!!}
>
> And now I split on `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 = {!!}
>
> And now on `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 = {!!}
>
> The first error comes when I try to case split on `k∈t` of the equation
> including `(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 = {!!}
>
> Agda tells me it gets stuck doing the unification, but it's not clear to me
> why or how to help. In [a response to a similar
> question](http://stackoverflow.com/q/30951993/1312174), Ulf suggested first
> case-splitting on another variable. So, now working by hand, I focus on
> case-splitting the `∼+` line from `refuse5` and include many of the implicit
> variables:
>
>       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 _ _ _ = ?
>
> Oops. Now Agda goes from complaining that it's stuck to downright refusing
> to solve. What's going on here? Is it possible to specify the lhs of the
> equations with at least as much detail as in refuse5 **and also** case split
> on `k∈t`? If so, how?
> --
> Martin Stone Davis
>
> Postal/Residential:
> 1223 Ferry St
> Apt 5
> Eugene, OR 97401
> Talk / Text / Voicemail: (310) 699-3578
> Electronic Mail: martin.stone.davis at gmail.com
> Website: martinstonedavis.com
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>